Pull lattice-like structures out of Algebra, into Algebra.Lattice

CHANGELOG.md

@@ -7,7 +7,7 @@ Highlights
 ----------
 
 * A golden testing library in `Test.Golden`. This allows you to run a set
-  of tests and make sure their output matches an expected `golden' value.
+  of tests and make sure their output matches an expected `golden` value.
   The test runner has many options: filtering tests by name, dumping the
   list of failures to a file, timing the runs, coloured output, etc.
   Cf. the comments in `Test.Golden` and the standard library's own tests
@@ -31,19 +31,11 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
-* In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`,
-  `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to
-  build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and
-  `IsSemiringHomomorphism` respectively, adding a single property at each step.
-  This means that they no longer need to have two separate proofs of
-  `IsRelHomomorphism`. Similarly, `IsLatticeHomomorphism` is now built as
-  `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homorphic.
+#### Removed deprecated names
 
-  Also, `⁻¹-homo` in `IsRingHomomorphism` has been renamed to `-‿homo`.
+* All modules and names that were deprecated prior to v1.0 have been removed.
 
-* move definition of `_>>=_` under `Data.Vec.Base` to its submodule `CartesianBind`
-  in order to keep another new definition of `_>>=_`, located in `DiagonalBind`
-  which is also a submodule of `Data.Vec.Base`.
+### Improvements to pretty printing and regexes
 
 * In `Text.Pretty`, `Doc` is now a record rather than a type alias. This
   helps Agda reconstruct the `width` parameter when the module is opened
@@ -75,9 +67,64 @@ Non-backwards compatible changes
   So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to"
   will return "Main.agdai" when it used to be happy to just return "n.agda".
 
-#### Removed deprecated names
 
-* All modules and names that were deprecated prior to v1.0 have been removed.
+### Refactoring of algebraic lattice hierarchy
+
+* In order to improve modularity and consistency with `Relation.Binary.Lattice`, 
+  the structures & bundles for `Semilattice`, `Lattice`, `DistributiveLattice`
+  & `BooleanAlgebra` have been moved out of the `Algebra` modules and into their
+  own hierarchy in `Algebra.Lattice`.
+
+* All submodules, (e.g. `Algebra.Properties.Semilattice` or `Algebra.Morphism.Lattice`)
+  have been moved to the corresponding place under `Algebra.Lattice` (e.g.
+  `Algebra.Lattice.Properties.Semilattice` or `Algebra.Lattice.Morphism.Lattice`). See
+  the `Deprecated modules` section below for full details.
+
+* Changed definition of `IsDistributiveLattice` and `IsBooleanAlgebra` so that they are 
+  no longer right-biased which hinders compositionality. More concretely, `IsDistributiveLattice`
+  now has fields:
+  ```agda
+  ∨-distrib-∧ : ∨ DistributesOver ∧
+  ∧-distrib-∨ : ∧ DistributesOver ∨
+  ```
+  instead of
+  ```agda
+  ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
+  ```
+  and `IsBooleanAlgebra` now has fields:
+  ```
+  ∨-complement : Inverse ⊤ ¬ ∨
+  ∧-complement : Inverse ⊥ ¬ ∧
+  ```
+  instead of:
+  ```agda
+  ∨-complementʳ : RightInverse ⊤ ¬ ∨
+  ∧-complementʳ : RightInverse ⊥ ¬ ∧
+  ```
+
+* To allow construction of these structures via their old form, smart constructors
+  have been added to a new module `Algebra.Lattice.Structures.Biased`, which are by
+  re-exported automatically by `Algebra.Lattice`. For example, if before you wrote:
+  ```agda
+  ∧-∨-isDistributiveLattice = record
+    { isLattice    = ∧-∨-isLattice
+    ; ∨-distribʳ-∧ = ∨-distribʳ-∧
+    }
+  ```
+  you can use the smart constructor `isDistributiveLatticeʳʲᵐ` to write:
+  ```agda
+  ∧-∨-isDistributiveLattice = isDistributiveLatticeʳʲᵐ (record
+    { isLattice    = ∧-∨-isLattice
+    ; ∨-distribʳ-∧ = ∨-distribʳ-∧
+    })
+  ```
+  without having to prove full distributivity.
+
+* Added new `IsBoundedSemilattice`/`BoundedSemilattice` records.
+
+* Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice`
+  which can be used to indicate meet/join-ness of the original structures.
+
 
 #### Proofs of non-zeroness/positivity/negativity as instance arguments
 
@@ -202,9 +249,23 @@ Non-backwards compatible changes
   domain) so that `_⟶_` can be inferred, which it could not from the
   previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`.
 
-  ### Creation of `Relation.Binary.Lattice` hierarchy
-  * In order to improve modularity Relation.Binary.Lattice is split out into Relation.Binary.Lattice.(Definitions/Structures/Bundles).
-  ###
+* In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`,
+  `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to
+  build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and
+  `IsSemiringHomomorphism` respectively, adding a single property at each step.
+  This means that they no longer need to have two separate proofs of
+  `IsRelHomomorphism`. Similarly, `IsLatticeHomomorphism` is now built as
+  `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homorphic.
+
+  Also, `⁻¹-homo` in `IsRingHomomorphism` has been renamed to `-‿homo`.
+
+* Moved definition of `_>>=_` under `Data.Vec.Base` to its submodule `CartesianBind`
+  in order to keep another new definition of `_>>=_`, located in `DiagonalBind`
+  which is also a submodule of `Data.Vec.Base`.
+
+* The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer 
+  exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)`
+  directly to use them.
 
 Deprecated modules
 ------------------
@@ -227,6 +288,17 @@ Deprecated modules
   Equivalence-kind    ↦ EquivalenceKind
   ```
 
+### Moving `Algebra.Lattice` files
+
+* As discussed above the following files have been moved:
+  ```agda
+  Algebra.Properties.Semilattice               ↦ Algebra.Lattice.Properties.Semilattice
+  Algebra.Properties.Lattice                   ↦ Algebra.Lattice.Properties.Lattice
+  Algebra.Properties.DistributiveLattice       ↦ Algebra.Lattice.Properties.DistributiveLattice
+  Algebra.Properties.BooleanAlgebra            ↦ Algebra.Lattice.Properties.BooleanAlgebra
+  Algebra.Properties.BooleanAlgebra.Expression ↦ Algebra.Lattice.Properties.BooleanAlgebra.Expression
+  Algebra.Morphism.LatticeMonomorphism         ↦ Algebra.Lattice.Morphism.LatticeMonomorphism
+  ```
 
 Deprecated names
 ----------------
@@ -406,6 +478,15 @@ New modules
   Function.Properties.Surjection
   ```
 
+* In order to improve modularity, the contents of `Relation.Binary.Lattice` has been 
+  split out into the standard:
+  ```
+  Relation.Binary.Lattice.Definitions
+  Relation.Binary.Lattice.Structures
+  Relation.Binary.Lattice.Bundles
+  ```
+  All contents is re-exported by `Relation.Binary.Lattice` as before.
+
 * Both versions of equality on predications are equivalences
   ```
   Relation.Unary.Relation.Binary.Equality
@@ -460,12 +541,15 @@ Other minor changes
 
 * Added new proofs to `Algebra.Consequences.Setoid`:
   ```agda
-  comm+idˡ⇒id       : Commutative _•_ → LeftIdentity  e _•_ → Identity e _•_
-  comm+idʳ⇒id       : Commutative _•_ → RightIdentity e _•_ → Identity e _•_
-  comm+zeˡ⇒ze       : Commutative _•_ → LeftZero      e _•_ → Zero     e _•_
-  comm+zeʳ⇒ze       : Commutative _•_ → RightZero     e _•_ → Zero     e _•_
-  comm+distrˡ⇒distr : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_
-  comm+distrʳ⇒distr : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_
+  comm+idˡ⇒id              : Commutative _•_ → LeftIdentity  e _•_ → Identity e _•_
+  comm+idʳ⇒id              : Commutative _•_ → RightIdentity e _•_ → Identity e _•_
+  comm+zeˡ⇒ze              : Commutative _•_ → LeftZero      e _•_ → Zero     e _•_
+  comm+zeʳ⇒ze              : Commutative _•_ → RightZero     e _•_ → Zero     e _•_
+  comm+invˡ⇒inv            : Commutative _•_ → LeftInverse  e _⁻¹ _•_ → Inverse e _⁻¹ _•_
+  comm+invʳ⇒inv            : Commutative _•_ → RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
+  comm+distrˡ⇒distr        : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_
+  comm+distrʳ⇒distr        : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_
+  distrib+absorbs⇒distribˡ : Associative _•_ → Commutative _◦_ → _•_ Absorbs _◦_ → _◦_ Absorbs _•_ → _◦_ DistributesOver _•_ → _•_ DistributesOverˡ _◦_
   ```
 
 * Added new functions to `Algebra.Construct.DirectProduct`:

src/Algebra/Bundles.agda

@@ -143,25 +143,6 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   commutativeMagma : CommutativeMagma c ℓ
   commutativeMagma = record { isCommutativeMagma = isCommutativeMagma }
 
-
-record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixr 7 _∧_
-  infix  4 _≈_
-  field
-    Carrier       : Set c
-    _≈_           : Rel Carrier ℓ
-    _∧_           : Op₂ Carrier
-    isSemilattice : IsSemilattice _≈_ _∧_
-
-  open IsSemilattice isSemilattice public
-
-  band : Band c ℓ
-  band = record { isBand = isBand }
-
-  open Band band public
-    using (_≉_; rawMagma; magma; semigroup)
-
-
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation & 1 element
 ------------------------------------------------------------------------
@@ -417,81 +398,6 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   open CommutativeMonoid commutativeMonoid public
     using (commutativeMagma; commutativeSemigroup)
 
-
-------------------------------------------------------------------------
--- Bundles with 2 binary operations
-------------------------------------------------------------------------
-
-record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixr 7 _∧_
-  infixr 6 _∨_
-  infix  4 _≈_
-  field
-    Carrier : Set c
-    _≈_     : Rel Carrier ℓ
-    _∧_     : Op₂ Carrier
-    _∨_     : Op₂ Carrier
-
-  ∨-rawMagma : RawMagma c ℓ
-  ∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ }
-
-  ∧-rawMagma : RawMagma c ℓ
-  ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
-
-  open RawMagma ∨-rawMagma public
-    using (_≉_)
-
-
-record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixr 7 _∧_
-  infixr 6 _∨_
-  infix  4 _≈_
-  field
-    Carrier   : Set c
-    _≈_       : Rel Carrier ℓ
-    _∨_       : Op₂ Carrier
-    _∧_       : Op₂ Carrier
-    isLattice : IsLattice _≈_ _∨_ _∧_
-
-  open IsLattice isLattice public
-
-  rawLattice : RawLattice c ℓ
-  rawLattice = record
-    { _≈_  = _≈_
-    ; _∧_  = _∧_
-    ; _∨_  = _∨_
-    }
-
-  open RawLattice rawLattice public
-    using (∨-rawMagma; ∧-rawMagma)
-
-  setoid : Setoid _ _
-  setoid = record { isEquivalence = isEquivalence }
-
-  open Setoid setoid public
-    using (_≉_)
-
-
-record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixr 7 _∧_
-  infixr 6 _∨_
-  infix  4 _≈_
-  field
-    Carrier               : Set c
-    _≈_                   : Rel Carrier ℓ
-    _∨_                   : Op₂ Carrier
-    _∧_                   : Op₂ Carrier
-    isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
-
-  open IsDistributiveLattice isDistributiveLattice public
-
-  lattice : Lattice _ _
-  lattice = record { isLattice = isLattice }
-
-  open Lattice lattice public
-    using (_≉_; rawLattice; setoid)
-
-
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations & 1 element
 ------------------------------------------------------------------------
@@ -976,31 +882,6 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
     ; commutativeSemiringWithoutOne
     )
 
-
-record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
-  infix  8 ¬_
-  infixr 7 _∧_
-  infixr 6 _∨_
-  infix  4 _≈_
-  field
-    Carrier          : Set c
-    _≈_              : Rel Carrier ℓ
-    _∨_              : Op₂ Carrier
-    _∧_              : Op₂ Carrier
-    ¬_               : Op₁ Carrier
-    ⊤                : Carrier
-    ⊥                : Carrier
-    isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
-
-  open IsBooleanAlgebra isBooleanAlgebra public
-
-  distributiveLattice : DistributiveLattice _ _
-  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
-
-  open DistributiveLattice distributiveLattice public
-    using (_≉_; setoid; lattice)
-
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Algebra/Consequences/Setoid.agda

@@ -117,12 +117,18 @@ module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) whe
     (x ⁻¹) • x ≈⟨ invˡ x ⟩
     e          ∎
 
+  comm+invˡ⇒inv : LeftInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
+  comm+invˡ⇒inv invˡ = invˡ , comm+invˡ⇒invʳ invˡ
+
   comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_
   comm+invʳ⇒invˡ invʳ x = begin
     (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩
     x • (x ⁻¹) ≈⟨ invʳ x ⟩
     e          ∎
 
+  comm+invʳ⇒inv : RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
+  comm+invʳ⇒inv invʳ = comm+invʳ⇒invˡ invʳ , invʳ
+
 module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where
 
   assoc+id+invʳ⇒invˡ-unique : Associative _•_ →
@@ -182,6 +188,26 @@ module _ {_•_ _◦_ : Op₂ A}
     (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩
     (x ◦ z) • (x ◦ y) ∎
 
+
+module _ {_•_ _◦_ : Op₂ A}
+         (•-cong  : Congruent₂ _•_)
+         (•-assoc : Associative _•_)
+         (◦-comm  : Commutative _◦_)
+         where
+
+  distrib+absorbs⇒distribˡ : _•_ Absorbs _◦_ →
+                             _◦_ Absorbs _•_ →
+                             _◦_ DistributesOver _•_ →
+                             _•_ DistributesOverˡ _◦_
+  distrib+absorbs⇒distribˡ •-absorbs-◦ ◦-absorbs-• (◦-distribˡ-• , ◦-distribʳ-•) x y z = begin
+    x • (y ◦ z)                    ≈˘⟨ •-cong (•-absorbs-◦ _ _) refl ⟩
+    (x • (x ◦ y)) • (y ◦ z)        ≈⟨  •-cong (•-cong refl (◦-comm _ _)) refl ⟩
+    (x • (y ◦ x)) • (y ◦ z)        ≈⟨  •-assoc _ _ _ ⟩
+    x • ((y ◦ x) • (y ◦ z))        ≈˘⟨ •-cong refl (◦-distribˡ-• _ _ _) ⟩
+    x • (y ◦ (x • z))              ≈˘⟨ •-cong (◦-absorbs-• _ _) refl ⟩
+    (x ◦ (x • z)) • (y ◦ (x • z))  ≈˘⟨ ◦-distribʳ-• _ _ _ ⟩
+    (x • y) ◦ (x • z)              ∎
+
 ----------------------------------------------------------------------
 -- Ring-like structures
 

src/Algebra/Construct/DirectProduct.agda

@@ -111,15 +111,6 @@ commutativeSemigroup G H = record
     }
   } where module G = CommutativeSemigroup G; module H = CommutativeSemigroup H
 
-semilattice : Semilattice a ℓ₁ → Semilattice b ℓ₂ →
-              Semilattice (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-semilattice L M = record
-  { isSemilattice = record
-    { isBand = Band.isBand (band L.band M.band)
-    ; comm = λ x y → (L.comm , M.comm) <*> x <*> y
-    }
-  } where module L = Semilattice L; module M = Semilattice M
-
 monoid : Monoid a ℓ₁ → Monoid b ℓ₂ → Monoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 monoid M N = record
   { ε = M.ε , N.ε