123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126-------------------------------------------------------------------------- The Agda standard library---- Properties satisfied by join semilattices------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Lattice module Relation.Binary.Lattice.Properties.JoinSemilattice {c ℓ₁ ℓ₂} (J : JoinSemilattice c ℓ₁ ℓ₂) where open JoinSemilattice J import Algebra.Lattice as Algimport Algebra.Structures as Algopen import Algebra.Definitions _≈_open import Data.Product.Base using (_,_)open import Function.Base using (_∘_; flip)open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_)open import Relation.Binary.Structures using (IsDecPartialOrder)open import Relation.Binary.Definitions using (Decidable)open import Relation.Binary.Properties.Poset posetopen import Relation.Nullary using (¬_; yes; no)open import Relation.Nullary.Negation using (contraposition) import Relation.Binary.Reasoning.PartialOrder as PoR -------------------------------------------------------------------------- Algebraic properties -- The join operation is monotonic. ∨-monotonic : _∨_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_∨-monotonic {x} {y} {u} {v} x≤y u≤v = let _ , _ , least = supremum x u y≤y∨v , v≤y∨v , _ = supremum y v in least (y ∨ v) (trans x≤y y≤y∨v) (trans u≤v v≤y∨v) ∨-cong : _∨_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_∨-cong x≈y u≈v = antisym (∨-monotonic (reflexive x≈y) (reflexive u≈v)) (∨-monotonic (reflexive (Eq.sym x≈y)) (reflexive (Eq.sym u≈v))) -- The join operation is commutative, associative and idempotent. ∨-comm : Commutative _∨_∨-comm x y = let x≤x∨y , y≤x∨y , least = supremum x y y≤y∨x , x≤y∨x , least′ = supremum y x in antisym (least (y ∨ x) x≤y∨x y≤y∨x) (least′ (x ∨ y) y≤x∨y x≤x∨y) ∨-assoc : Associative _∨_∨-assoc x y z = let x∨y≤[x∨y]∨z , z≤[x∨y]∨z , least = supremum (x ∨ y) z x≤x∨[y∨z] , y∨z≤x∨[y∨z] , least′ = supremum x (y ∨ z) y≤y∨z , z≤y∨z , _ = supremum y z x≤x∨y , y≤x∨y , _ = supremum x y in antisym (least (x ∨ (y ∨ z)) (∨-monotonic refl y≤y∨z) (trans z≤y∨z y∨z≤x∨[y∨z])) (least′ ((x ∨ y) ∨ z) (trans x≤x∨y x∨y≤[x∨y]∨z) (∨-monotonic y≤x∨y refl)) ∨-idempotent : Idempotent _∨_∨-idempotent x = let x≤x∨x , _ , least = supremum x x in antisym (least x refl refl) x≤x∨x x≤y⇒x∨y≈y : ∀ {x y} → x ≤ y → x ∨ y ≈ yx≤y⇒x∨y≈y {x} {y} x≤y = antisym (begin x ∨ y ≤⟨ ∨-monotonic x≤y refl ⟩ y ∨ y ≈⟨ ∨-idempotent _ ⟩ y ∎) (y≤x∨y _ _) where open PoR poset -- Every order-theoretic semilattice can be turned into an algebraic one. isAlgSemilattice : Alg.IsSemilattice _≈_ _∨_isAlgSemilattice = record { isBand = record { isSemigroup = record { isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∨-cong } ; assoc = ∨-assoc } ; idem = ∨-idempotent } ; comm = ∨-comm } algSemilattice : Alg.Semilattice c ℓ₁algSemilattice = record { isSemilattice = isAlgSemilattice } -------------------------------------------------------------------------- The dual construction is a meet semilattice. dualIsMeetSemilattice : IsMeetSemilattice _≈_ (flip _≤_) _∨_dualIsMeetSemilattice = record { isPartialOrder = ≥-isPartialOrder ; infimum = supremum } dualMeetSemilattice : MeetSemilattice c ℓ₁ ℓ₂dualMeetSemilattice = record { _∧_ = _∨_ ; isMeetSemilattice = dualIsMeetSemilattice } -------------------------------------------------------------------------- If ≈ is decidable then so is ≤ ≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_≈-dec⇒≤-dec _≟_ x y with (x ∨ y) ≟ y... | yes x∨y≈y = yes (trans (x≤x∨y x y) (reflexive x∨y≈y))... | no x∨y≉y = no (contraposition x≤y⇒x∨y≈y x∨y≉y) ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_≈-dec⇒isDecPartialOrder _≟_ = record { isPartialOrder = isPartialOrder ; _≟_ = _≟_ ; _≤?_ = ≈-dec⇒≤-dec _≟_ }