[ new ] add properties of algebraic semilattices and update dependencies.

Author: sstucki

CHANGELOG.md

@@ -61,6 +61,11 @@ Splitting up `Data.Maybe` into the standard hierarchy.
 * The record `BooleanAlgebra` now exports `∨-isSemigroup`, `∧-isSemigroup`
   directly  so `Algebra.Properties.BooleanAlgebra` no longer does so.
 
+* The proof that every algebraic lattice induces a partial order has been
+  moved from `Algebra.Properties.Lattice` to
+  `Algebra.Properties.Semilattice`.  The corresponding `poset` instance is
+  re-exported in `Algebra.Properties.Lattice`.
+
 #### Relaxation of ring solvers requirements
 
 * In the ring solvers below, the assumption that equality is `Decidable`
@@ -90,6 +95,8 @@ Splitting up `Data.Maybe` into the standard hierarchy.
 Other major changes
 -------------------
 
+* Added new module `Algebra.Properties.Semilattice`
+
 * Added new module `Algebra.FunctionProperties.Consequences.Propositional`
 
 * Added new module `Codata.Cowriter`
@@ -123,6 +130,14 @@ Other minor additions
   wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)
   ```
 
+* Added new proofs to `Algebra.Properties.Lattice`:
+  ```agda
+  ∧-isSemilattice : IsSemilattice _≈_ _∧_
+  ∧-semilattice : Semilattice l₁ l₂
+  ∨-isSemilattice : IsSemilattice _≈_ _∨_
+  ∨-semilattice : Semilattice l₁ l₂
+  ```
+
 * Added new operator to `Algebra.Solver.Ring`.
   ```agda
   _:×_

src/Algebra/Properties/Lattice.agda

@@ -11,6 +11,7 @@ module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where
 open Lattice L
 open import Algebra.Structures
 open import Algebra.FunctionProperties _≈_
+import Algebra.Properties.Semilattice as SL
 open import Relation.Binary
 import Relation.Binary.Lattice as R
 open import Relation.Binary.EqReasoning  setoid
@@ -19,6 +20,9 @@ open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; module Equivalence)
 open import Data.Product using (_,_; swap)
 
+------------------------------------------------------------------------
+-- Every lattice contains two semilattices.
+
 ∧-idempotent : Idempotent _∧_
 ∧-idempotent x = begin
   x ∧ x            ≈⟨ refl ⟨ ∧-cong ⟩ sym (∨-absorbs-∧ _ _) ⟩
@@ -31,6 +35,45 @@ open import Data.Product using (_,_; swap)
   x ∨ x ∧ x  ≈⟨ ∨-absorbs-∧ _ _ ⟩
   x          ∎
 
+∧-isSemilattice : IsSemilattice _≈_ _∧_
+∧-isSemilattice = record
+  { isBand = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = isEquivalence
+        ; ∙-cong        = ∧-cong
+        }
+      ; assoc         = ∧-assoc
+      }
+    ; idem = ∧-idempotent
+    }
+  ; comm   = ∧-comm
+  }
+
+∧-semilattice : Semilattice l₁ l₂
+∧-semilattice = record { isSemilattice = ∧-isSemilattice }
+
+∨-isSemilattice : IsSemilattice _≈_ _∨_
+∨-isSemilattice = record
+  { isBand = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = isEquivalence
+        ; ∙-cong        = ∨-cong
+        }
+      ; assoc         = ∨-assoc
+      }
+    ; idem = ∨-idempotent
+    }
+  ; comm   = ∨-comm
+  }
+
+∨-semilattice : Semilattice l₁ l₂
+∨-semilattice = record { isSemilattice = ∨-isSemilattice }
+
+open SL ∧-semilattice public using (poset)
+open Poset poset using (_≤_; isPartialOrder)
+
 ------------------------------------------------------------------------
 -- The dual construction is also a lattice.
 
@@ -49,88 +92,43 @@ open import Data.Product using (_,_; swap)
 ∧-∨-lattice : Lattice _ _
 ∧-∨-lattice = record { isLattice = ∧-∨-isLattice }
 
-------------------------------------------------------------------------
--- Every lattice can be turned into a poset.
-
-poset : Poset _ _ _
-poset = record
-  { Carrier        = Carrier
-  ; _≈_            = _≈_
-  ; _≤_            = λ x y → x ≈ x ∧ y
-  ; isPartialOrder = record
-    { isPreorder = record
-      { isEquivalence = isEquivalence
-      ; reflexive     = λ {i} {j} i≈j → begin
-                          i      ≈⟨ sym $ ∧-idempotent _ ⟩
-                          i ∧ i  ≈⟨ ∧-cong refl i≈j ⟩
-                          i ∧ j  ∎
-      ; trans         = λ {i} {j} {k} i≈i∧j j≈j∧k → begin
-                          i            ≈⟨ i≈i∧j ⟩
-                          i ∧ j        ≈⟨ ∧-cong refl j≈j∧k ⟩
-                          i ∧ (j ∧ k)  ≈⟨ sym (∧-assoc _ _ _) ⟩
-                          (i ∧ j) ∧ k  ≈⟨ ∧-cong (sym i≈i∧j) refl ⟩
-                          i ∧ k        ∎
-      }
-    ; antisym = λ {x} {y} x≈x∧y y≈y∧x → begin
-                  x      ≈⟨ x≈x∧y ⟩
-                  x ∧ y  ≈⟨ ∧-comm _ _ ⟩
-                  y ∧ x  ≈⟨ sym y≈y∧x ⟩
-                  y      ∎
-    }
-  }
-
-open Poset poset using (_≤_; isPartialOrder)
-
 ------------------------------------------------------------------------
 -- Every algebraic lattice can be turned into an order-theoretic one.
 
 isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_
 isOrderTheoreticLattice = record
   { isPartialOrder = isPartialOrder
-  ; supremum       = λ x y →
-                       sym (∧-absorbs-∨ x y) ,
-                       (begin
-                         y            ≈⟨ sym (∧-absorbs-∨ y x) ⟩
-                         y ∧ (y ∨ x)  ≈⟨ ∧-cong refl (∨-comm y x) ⟩
-                         y ∧ (x ∨ y)  ∎) ,
-                       (λ z x≤z y≤z → sound (begin
-                         (x ∨ y) ∨ z  ≈⟨ ∨-assoc x y z ⟩
-                         x ∨ (y ∨ z)  ≈⟨ ∨-cong refl (complete y≤z) ⟩
-                         x ∨ z        ≈⟨ complete x≤z  ⟩
-                         z            ∎))
-  ; infimum        = λ x y →
-                       (begin
-                         x ∧ y        ≈⟨ ∧-cong (sym (∧-idempotent x)) refl ⟩
-                         (x ∧ x) ∧ y  ≈⟨ ∧-assoc x x y  ⟩
-                         x ∧ (x ∧ y)  ≈⟨ ∧-comm x (x ∧ y) ⟩
-                         (x ∧ y) ∧ x  ∎) ,
-                       (begin
-                         x ∧ y        ≈⟨ ∧-cong refl (sym (∧-idempotent y)) ⟩
-                         x ∧ (y ∧ y)  ≈⟨ sym (∧-assoc x y y) ⟩
-                         (x ∧ y) ∧ y  ∎) ,
-                       (λ z z≈z∧x z≈z∧y → begin
-                         z            ≈⟨ z≈z∧y ⟩
-                         z ∧ y        ≈⟨ ∧-cong z≈z∧x refl ⟩
-                         (z ∧ x) ∧ y  ≈⟨ ∧-assoc z x y ⟩
-                         z ∧ (x ∧ y)  ∎)
+  ; supremum       = supremum
+  ; infimum        = infimum
   }
   where
+  ∧-meetSemilattice = SL.orderTheoreticMeetSemilattice ∧-semilattice
+  ∨-joinSemilattice = SL.orderTheoreticJoinSemilattice ∨-semilattice
+  open R.MeetSemilattice ∧-meetSemilattice using (infimum)
+  open R.JoinSemilattice ∨-joinSemilattice using ()
+    renaming (supremum to supremum′; _≤_ to _≤′_)
 
   -- An alternative but equivalent interpretation of the order _≤_.
 
-  complete : ∀ {x y} → x ≤ y → x ∨ y ≈ y
-  complete {x} {y} x≈x∧y = begin
-    x ∨ y        ≈⟨ ∨-cong x≈x∧y refl ⟩
-    (x ∧ y) ∨ y  ≈⟨ ∨-cong (∧-comm x y) refl ⟩
-    (y ∧ x) ∨ y  ≈⟨ ∨-comm (y ∧ x) y ⟩
+  sound : ∀ {x y} → x ≤′ y → x ≤ y
+  sound {x} {y} y≈y∨x = sym $ begin
+    x ∧ y        ≈⟨ ∧-cong refl y≈y∨x ⟩
+    x ∧ (y ∨ x)  ≈⟨ ∧-cong refl (∨-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 refl x≈x∧y ⟩
+    y ∨ (x ∧ y)  ≈⟨ ∨-cong refl (∧-comm x y) ⟩
     y ∨ (y ∧ x)  ≈⟨ ∨-absorbs-∧ y x ⟩
     y            ∎
 
-  sound : ∀ {x y} → x ∨ y ≈ y → x ≤ y
-  sound {x} {y} x∨y≈y = begin
-    x            ≈⟨ sym (∧-absorbs-∨ x y) ⟩
-    x ∧ (x ∨ y)  ≈⟨ ∧-cong refl x∨y≈y ⟩
-    x ∧ y        ∎
+  supremum : R.Supremum _≤_ _∨_
+  supremum x y =
+    let x∨y≥x , x∨y≥y , greatest = supremum′ x y
+    in sound x∨y≥x , sound x∨y≥y ,
+       λ z x≤z y≤z → sound (greatest z (complete x≤z) (complete y≤z))
 
 orderTheoreticLattice : R.Lattice _ _ _
 orderTheoreticLattice = record { isLattice = isOrderTheoreticLattice }

src/Algebra/Properties/Semilattice.agda

@@ -0,0 +1,86 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some derivable properties
+------------------------------------------------------------------------
+
+open import Algebra
+
+module Algebra.Properties.Semilattice {l₁ l₂} (L : Semilattice l₁ l₂) where
+
+open Semilattice L
+open import Algebra.Structures
+open import Relation.Binary
+import Relation.Binary.Lattice as R
+import Relation.Binary.Properties.Poset as R
+import Relation.Binary.EqReasoning as EqR; open EqR setoid
+open import Function
+open import Data.Product
+
+-- Every semilattice can be turned into a poset.
+
+poset : Poset _ _ _
+poset = record
+  { Carrier        = Carrier
+  ; _≈_            = _≈_
+  ; _≤_            = λ x y → x ≈ x ∧ y
+  ; isPartialOrder = record
+    { isPreorder = record
+      { isEquivalence = isEquivalence
+      ; reflexive     = λ {i} {j} i≈j → begin
+                          i      ≈⟨ sym $ idem _ ⟩
+                          i ∧ i  ≈⟨ ∧-cong refl i≈j ⟩
+                          i ∧ j  ∎
+      ; trans         = λ {i} {j} {k} i≈i∧j j≈j∧k → begin
+                          i            ≈⟨ i≈i∧j ⟩
+                          i ∧ j        ≈⟨ ∧-cong refl j≈j∧k ⟩
+                          i ∧ (j ∧ k)  ≈⟨ sym (assoc _ _ _) ⟩
+                          (i ∧ j) ∧ k  ≈⟨ ∧-cong (sym i≈i∧j) refl ⟩
+                          i ∧ k        ∎
+      }
+    ; antisym = λ {x} {y} x≈x∧y y≈y∧x → begin
+                  x      ≈⟨ x≈x∧y ⟩
+                  x ∧ y  ≈⟨ comm _ _ ⟩
+                  y ∧ x  ≈⟨ sym y≈y∧x ⟩
+                  y      ∎
+    }
+  }
+
+open Poset poset using (_≤_; isPartialOrder)
+
+-- Every algebraic semilattice can be turned into an order-theoretic one.
+
+isOrderTheoreticMeetSemilattice : R.IsMeetSemilattice _≈_ _≤_ _∧_
+isOrderTheoreticMeetSemilattice = record
+  { isPartialOrder = isPartialOrder
+  ; infimum        = λ x y →
+                       (begin
+                         x ∧ y        ≈⟨ ∧-cong (sym (idem x)) refl ⟩
+                         (x ∧ x) ∧ y  ≈⟨ assoc x x y  ⟩
+                         x ∧ (x ∧ y)  ≈⟨ comm x (x ∧ y) ⟩
+                         (x ∧ y) ∧ x  ∎) ,
+                       (begin
+                         x ∧ y        ≈⟨ ∧-cong refl (sym (idem y)) ⟩
+                         x ∧ (y ∧ y)  ≈⟨ sym (assoc x y y) ⟩
+                         (x ∧ y) ∧ y  ∎) ,
+                       λ z z≈z∧x z≈z∧y → begin
+                         z            ≈⟨ z≈z∧y ⟩
+                         z ∧ y        ≈⟨ ∧-cong z≈z∧x refl ⟩
+                         (z ∧ x) ∧ y  ≈⟨ assoc z x y ⟩
+                         z ∧ (x ∧ y)  ∎
+  }
+
+orderTheoreticMeetSemilattice : R.MeetSemilattice _ _ _
+orderTheoreticMeetSemilattice = record
+  { isMeetSemilattice = isOrderTheoreticMeetSemilattice }
+
+isOrderTheoreticJoinSemilattice : R.IsJoinSemilattice _≈_ (flip _≤_) _∧_
+isOrderTheoreticJoinSemilattice = record
+  { isPartialOrder = R.invIsPartialOrder poset
+  ; supremum       = R.IsMeetSemilattice.infimum
+                       isOrderTheoreticMeetSemilattice
+  }
+
+orderTheoreticJoinSemilattice : R.JoinSemilattice _ _ _
+orderTheoreticJoinSemilattice = record
+  { isJoinSemilattice = isOrderTheoreticJoinSemilattice }

src/Algebra/Structures.agda

@@ -439,7 +439,8 @@ record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
   -- because the idempotence laws of ∨ and ∧ can be derived from the
   -- absorption laws, which makes the corresponding "idem" fields
   -- redundant.  The derived idempotence laws are stated and proved in
-  -- Algebra.Properties.Lattice.
+  -- Algebra.Properties.Lattice along with the fact that every lattice
+  -- consists of two semilattices.
 
   ∨-absorbs-∧ : ∨ Absorbs ∧
   ∨-absorbs-∧ = proj₁ absorptive

src/Relation/Binary/Properties/JoinSemilattice.agda

@@ -11,6 +11,8 @@ module Relation.Binary.Properties.JoinSemilattice
 
 open JoinSemilattice J
 
+import Algebra as Alg
+import Algebra.Structures as Alg
 import Algebra.FunctionProperties as P; open P _≈_
 open import Data.Product
 open import Function using (_∘_; flip)
@@ -64,6 +66,26 @@ x≤y⇒x∨y≈y {x} {y} x≤y = antisym
   (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 _≤_) _∨_

src/Relation/Binary/Properties/MeetSemilattice.agda

@@ -32,11 +32,13 @@ dualJoinSemilattice = record
   ; isJoinSemilattice = dualIsJoinSemilattice
   }
 
-open J dualJoinSemilattice public using () renaming
-  ( ∨-monotonic  to ∧-monotonic
-  ; ∨-cong       to ∧-cong
-  ; ∨-comm       to ∧-comm
-  ; ∨-assoc      to ∧-assoc
-  ; ∨-idempotent to ∧-idempotent
-  ; x≤y⇒x∨y≈y    to y≤x⇒x∧y≈y
-  )
+open J dualJoinSemilattice public
+  using (isAlgSemilattice; algSemilattice)
+  renaming
+    ( ∨-monotonic  to ∧-monotonic
+    ; ∨-cong       to ∧-cong
+    ; ∨-comm       to ∧-comm
+    ; ∨-assoc      to ∧-assoc
+    ; ∨-idempotent to ∧-idempotent
+    ; x≤y⇒x∨y≈y    to y≤x⇒x∧y≈y
+    )