{-# OPTIONS --without-K --safe #-}
open import Algebra.Lattice.Bundles
import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties
open import Relation.Binary
import Relation.Binary.Lattice as R
open import Function.Base
open import Data.Product using (_,_; swap)
module Algebra.Lattice.Properties.Lattice
{l₁ l₂} (L : Lattice l₁ l₂) where
open Lattice L
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
open import Algebra.Lattice.Structures _≈_
open import Relation.Binary.Reasoning.Setoid setoid
∧-idem : Idempotent _∧_
∧-idem x = begin
x ∧ x ≈˘⟨ ∧-congˡ (∨-absorbs-∧ _ _) ⟩
x ∧ (x ∨ x ∧ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩
x ∎
∧-isMagma : IsMagma _∧_
∧-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = ∧-cong
}
∧-isSemigroup : IsSemigroup _∧_
∧-isSemigroup = record
{ isMagma = ∧-isMagma
; assoc = ∧-assoc
}
∧-isBand : IsBand _∧_
∧-isBand = record
{ isSemigroup = ∧-isSemigroup
; idem = ∧-idem
}
∧-isSemilattice : IsSemilattice _∧_
∧-isSemilattice = record
{ isBand = ∧-isBand
; comm = ∧-comm
}
∧-semilattice : Semilattice l₁ l₂
∧-semilattice = record
{ isSemilattice = ∧-isSemilattice
}
open SemilatticeProperties ∧-semilattice public
using
( ∧-isOrderTheoreticMeetSemilattice
; ∧-isOrderTheoreticJoinSemilattice
; ∧-orderTheoreticMeetSemilattice
; ∧-orderTheoreticJoinSemilattice
)
∨-idem : Idempotent _∨_
∨-idem x = begin
x ∨ x ≈˘⟨ ∨-congˡ (∧-idem _) ⟩
x ∨ x ∧ x ≈⟨ ∨-absorbs-∧ _ _ ⟩
x ∎
∨-isMagma : IsMagma _∨_
∨-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = ∨-cong
}
∨-isSemigroup : IsSemigroup _∨_
∨-isSemigroup = record
{ isMagma = ∨-isMagma
; assoc = ∨-assoc
}
∨-isBand : IsBand _∨_
∨-isBand = record
{ isSemigroup = ∨-isSemigroup
; idem = ∨-idem
}
∨-isSemilattice : IsSemilattice _∨_
∨-isSemilattice = record
{ isBand = ∨-isBand
; comm = ∨-comm
}
∨-semilattice : Semilattice l₁ l₂
∨-semilattice = record
{ isSemilattice = ∨-isSemilattice
}
open SemilatticeProperties ∨-semilattice public
using ()
renaming
( ∧-isOrderTheoreticMeetSemilattice to ∨-isOrderTheoreticMeetSemilattice
; ∧-isOrderTheoreticJoinSemilattice to ∨-isOrderTheoreticJoinSemilattice
; ∧-orderTheoreticMeetSemilattice to ∨-orderTheoreticMeetSemilattice
; ∧-orderTheoreticJoinSemilattice to ∨-orderTheoreticJoinSemilattice
)
∧-∨-isLattice : IsLattice _∧_ _∨_
∧-∨-isLattice = record
{ isEquivalence = isEquivalence
; ∨-comm = ∧-comm
; ∨-assoc = ∧-assoc
; ∨-cong = ∧-cong
; ∧-comm = ∨-comm
; ∧-assoc = ∨-assoc
; ∧-cong = ∨-cong
; absorptive = swap absorptive
}
∧-∨-lattice : Lattice _ _
∧-∨-lattice = record
{ isLattice = ∧-∨-isLattice
}
open SemilatticeProperties ∧-semilattice public using (poset)
open Poset poset using (_≤_; isPartialOrder)
∨-∧-isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_
∨-∧-isOrderTheoreticLattice = record
{ isPartialOrder = isPartialOrder
; supremum = supremum
; infimum = infimum
}
where
open R.MeetSemilattice ∧-orderTheoreticMeetSemilattice using (infimum)
open R.JoinSemilattice ∨-orderTheoreticJoinSemilattice using (x≤x∨y; y≤x∨y; ∨-least)
renaming (_≤_ to _≤′_)
sound : ∀ {x y} → x ≤′ y → x ≤ y
sound {x} {y} y≈y∨x = sym $ begin
x ∧ y ≈⟨ ∧-congˡ y≈y∨x ⟩
x ∧ (y ∨ x) ≈⟨ ∧-congˡ (∨-comm y x) ⟩
x ∧ (x ∨ y) ≈⟨ ∧-absorbs-∨ x y ⟩
x ∎
complete : ∀ {x y} → x ≤ y → x ≤′ y
complete {x} {y} x≈x∧y = sym $ begin
y ∨ x ≈⟨ ∨-congˡ x≈x∧y ⟩
y ∨ (x ∧ y) ≈⟨ ∨-congˡ (∧-comm x y) ⟩
y ∨ (y ∧ x) ≈⟨ ∨-absorbs-∧ y x ⟩
y ∎
supremum : R.Supremum _≤_ _∨_
supremum x y =
sound (x≤x∨y x y) ,
sound (y≤x∨y x y) ,
λ z x≤z y≤z → sound (∨-least (complete x≤z) (complete y≤z))
∨-∧-orderTheoreticLattice : R.Lattice _ _ _
∨-∧-orderTheoreticLattice = record
{ isLattice = ∨-∧-isOrderTheoreticLattice
}