[ refactor ] straightening out the Algebra hierarchy (agda#535)

Author: MatthewDaggitt

CHANGELOG.md

@@ -45,9 +45,29 @@ Splitting up `Data.Maybe` into the standard hierarchy.
 
 #### Changes to the algebra hierarchy
 
+* Over time the algebra inheritance hierarchy has become a little
+  wonky due to poorly structured additions. This attempts to straighten
+  the hierarchy out and new policies have been put in place so that
+  the need for additional such changes will be minimised in the future.
+
 * Added `Magma` and `IsMagma` to the algebra hierarchy.
 
-* The name `RawSemigroup` in `Algebra` has been deprecated in favour of `RawMagma`.
+* The name `RawSemigroup` in `Algebra` has been deprecated in favour
+  of `RawMagma`.
+
+* The fields `isEquivalence` and `∙-cong` in `IsSemigroup` have been
+  replaced with `isMagma`.
+
+* The fields `isEquivalence`, `∨-cong`, `∨-assoc`, `∨-comm`, `∧-cong`,
+  `∧-assoc`  and `∧-comm` in `IsLattice` have been replaced with
+  `∨-isSemilattice` and `∧-isSemilattice`.
+
+* The record `Lattice` now exports proofs of `∨-idem` and `∧-idem` directly.
+  Therefore `∨-idempotence` and `∧-idempotence` in `Algebra.Properties.Lattice`
+  have been deprecated.
+
+* The record `BooleanAlgebra` now exports `∨-isSemigroup`, `∧-isSemigroup`
+  directly  so `Algebra.Properties.BooleanAlgebra` no longer does so.
 
 #### Relaxation of ring solvers requirements
 
@@ -143,6 +163,23 @@ Other minor additions
   lookup-iterate-identity : lookup n (iterate f a) ≡ fold a f n
   ```
 
+* Added new proofs to `Data.Bool.Properties`:
+  ```agda
+  ∧-isMagma       : IsMagma _∧_
+  ∨-isMagma       : IsMagma _∨_
+  ∨-isBand        : IsBand _∨_
+  ∨-isSemilattice : IsSemilattice _∨_
+  ∧-isBand        : IsBand _∧_
+  ∧-isSemilattice : IsSemilattice _∧_
+
+  ∧-magma         : Magma 0ℓ 0ℓ
+  ∨-magma         : Magma 0ℓ 0ℓ
+  ∨-band          : Band 0ℓ 0ℓ
+  ∧-band          : Band 0ℓ 0ℓ
+  ∨-semilattice   : Semilattice 0ℓ 0ℓ
+  ∧-semilattice   : Semilattice 0ℓ 0ℓ
+  ```
+
 * Added new function to `Data.Fin.Base`:
   ```agda
   cast : m ≡ n → Fin m → Fin n
@@ -153,6 +190,36 @@ Other minor additions
   toℕ-cast    : toℕ (cast eq k) ≡ toℕ k
   ```
 
+* Added new proofs to `Data.Fin.Subset.Properties`:
+  ```agda
+  ∩-isMagma       : IsMagma _∩_
+  ∪-isMagma       : IsMagma _∪_
+  ∩-isBand        : IsBand _∩_
+  ∪-isBand        : IsBand _∪_
+  ∩-isSemilattice : IsSemilattice _∩_
+  ∪-isSemilattice : IsSemilattice _∪_
+
+  ∩-magma         : Magma _ _
+  ∪-magma         : Magma _ _
+  ∩-band          : Band _ _
+  ∪-band          : Band _ _
+  ∩-semilattice   : Semilattice _ _
+  ∪-semilattice   : Semilattice _ _
+  ```
+
+* Added new proofs to `Data.Integer.Properties`:
+  ```agda
+  +-isMagma   : IsMagma _+_
+  *-isMagma   : IsMagma _*_
+
+  +-magma     : Magma 0ℓ 0ℓ
+  *-magma     : Magma 0ℓ 0ℓ
+  +-semigroup : Semigroup 0ℓ 0ℓ
+  *-semigroup : Semigroup 0ℓ 0ℓ
+  +-0-monoid  : Monoid 0ℓ 0ℓ
+  *-1-monoid  : Monoid 0ℓ 0ℓ
+  ```
+
 * Added new operations to `Data.List.All`:
   ```agda
   zipWith   : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
@@ -203,11 +270,19 @@ Other minor additions
 
 * Added new proofs to `Data.List.Properties`:
   ```agda
-  length-%= : length (xs [ k ]%= f) ≡ length xs
-  length-∷= : length (xs [ k ]∷= v) ≡ length xs
-  map-∷=    : map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
-  length-─  : length (xs ─ k) ≡ pred (length xs)
-  map-─     : map f (xs ─ k) ≡ map f xs ─ cast eq k
+  ++-isMagma : IsMagma _++_
+
+  length-%=  : length (xs [ k ]%= f) ≡ length xs
+  length-∷=  : length (xs [ k ]∷= v) ≡ length xs
+  map-∷=     : map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
+  length-─   : length (xs ─ k) ≡ pred (length xs)
+  map-─      : map f (xs ─ k) ≡ map f xs ─ cast eq k
+  ```
+
+* Added new proofs to `Data.List.Relation.Permutation.Inductive.Properties`:
+  ```agda
+  ++-isMagma : IsMagma _↭_ _++_
+  ++-magma   : Magma _ _
   ```
 
 * Added new proofs to `Data.Maybe.All`:
@@ -259,6 +334,33 @@ Other minor additions
   _<∣>_     : Maybe A → Maybe A → Maybe A
   ```
 
+* Added new proofs to `Data.Nat.Properties`:
+  ```agda
+  +-isMagma       : IsMagma _+_
+  *-isMagma       : IsMagma _*_
+  ⊔-isMagma       : IsMagma _⊔_
+  ⊓-isMagma       : IsMagma _⊓_
+  ⊔-isBand        : IsBand _⊔_
+  ⊓-isBand        : IsBand _⊓_
+  ⊔-isSemilattice : IsSemilattice _⊔_
+  ⊓-isSemilattice : IsSemilattice _⊓_
+
+  +-magma       : Magma 0ℓ 0ℓ
+  *-magma       : Magma 0ℓ 0ℓ
+  ⊔-magma       : Magma 0ℓ 0ℓ
+  ⊓-magma       : Magma 0ℓ 0ℓ
+  ⊔-band        : Band 0ℓ 0ℓ
+  ⊓-band        : Band 0ℓ 0ℓ
+  ⊔-semilattice : Semilattice 0ℓ 0ℓ
+  ⊓-semilattice : Semilattice 0ℓ 0ℓ
+  ```
+
+* Added new proofs to `Data.Sign.Properties`:
+  ```agda
+  *-isMagma : IsMagma _*_
+  *-magma   : Magma 0ℓ 0ℓ
+  ```
+
 * Added new functions to `Data.Sum.Base`:
   ```agda
   fromDec : Dec P → P ⊎ ¬ P
@@ -280,6 +382,15 @@ Other minor additions
   toAny   : x ∈ xs → P x → Any P xs
   ```
 
+* Added new proofs to `Function.Related.TypeIsomorphisms`:
+  ```agda
+  ×-isMagma : ∀ k ℓ → IsMagma (Related ⌊ k ⌋) _×_
+  ⊎-isMagma : ∀ k ℓ → IsMagma (Related ⌊ k ⌋) _⊎_
+
+  ⊎-magma : Symmetric-kind → (ℓ : Level) → Semigroup _ _
+  ×-magma : Symmetric-kind → (ℓ : Level) → Magma _ _
+  ```
+
 * Added new proofs to `Relation.Binary.Consequences`:
   ```agda
   wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b

src/Algebra.agda

@@ -73,6 +73,23 @@ record Band c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semigroup semigroup public using (magma; rawMagma)
 
+
+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)
+
 ------------------------------------------------------------------------
 -- Monoids
 
@@ -536,22 +553,6 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 ------------------------------------------------------------------------
 -- Lattices and boolean algebras
 
-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)
-
 record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
   infixr 6 _∨_
@@ -565,8 +566,27 @@ record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsLattice isLattice public
 
-  setoid : Setoid _ _
-  setoid = record { isEquivalence = isEquivalence }
+  ∨-semilattice : Semilattice c ℓ
+  ∨-semilattice = record { isSemilattice = ∨-isSemilattice }
+
+  open Semilattice ∨-semilattice public
+    using () renaming
+    ( rawMagma  to ∨-rawMagma
+    ; magma     to ∨-magma
+    ; semigroup to ∨-semigroup
+    ; band      to ∨-band
+    )
+
+  ∧-semilattice : Semilattice c ℓ
+  ∧-semilattice = record { isSemilattice = ∧-isSemilattice }
+
+  open Semilattice ∧-semilattice public
+    using () renaming
+    ( rawMagma  to ∧-rawMagma
+    ; magma     to ∧-magma
+    ; semigroup to ∧-semigroup
+    ; band      to ∧-band
+    )
 
 record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -584,7 +604,11 @@ record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   lattice : Lattice _ _
   lattice = record { isLattice = isLattice }
 
-  open Lattice lattice public using (setoid)
+  open Lattice lattice public
+    using
+    ( ∧-rawMagma; ∧-magma; ∧-semigroup; ∧-band; ∧-semilattice
+    ; ∨-rawMagma; ∨-magma; ∨-semigroup; ∨-band; ∨-semilattice
+    )
 
 record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 ¬_
@@ -604,12 +628,14 @@ record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
   open IsBooleanAlgebra isBooleanAlgebra public
 
   distributiveLattice : DistributiveLattice _ _
-  distributiveLattice =
-    record { isDistributiveLattice = isDistributiveLattice }
+  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
 
   open DistributiveLattice distributiveLattice public
-         using (setoid; lattice)
-
+    using
+    ( ∧-rawMagma; ∧-magma; ∧-semigroup; ∧-band; ∧-semilattice
+    ; ∨-rawMagma; ∨-magma; ∨-semigroup; ∨-band; ∨-semilattice
+    ; lattice
+    )
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Algebra/Properties/BooleanAlgebra.agda

@@ -7,8 +7,8 @@
 open import Algebra
 
 module Algebra.Properties.BooleanAlgebra
-         {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
-         where
+  {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
+  where
 
 open BooleanAlgebra B
 import Algebra.Properties.DistributiveLattice
@@ -18,8 +18,7 @@ private
     hiding (replace-equality)
 open import Algebra.Structures _≈_
 open import Algebra.FunctionProperties _≈_
-open import Algebra.FunctionProperties.Consequences
-  record {isEquivalence = isEquivalence}
+open import Algebra.FunctionProperties.Consequences setoid
 open import Relation.Binary.EqReasoning setoid
 open import Relation.Binary
 open import Function
@@ -68,7 +67,7 @@ open import Data.Product
 ∧-identityʳ : RightIdentity ⊤ _∧_
 ∧-identityʳ x = begin
   x ∧ ⊤          ≈⟨ refl ⟨ ∧-cong ⟩ sym (∨-complementʳ _) ⟩
-  x ∧ (x ∨ ¬ x)  ≈⟨ proj₂ absorptive _ _ ⟩
+  x ∧ (x ∨ ¬ x)  ≈⟨ ∧-absorbs-∨ _ _ ⟩
   x              ∎
 
 ∧-identityˡ : LeftIdentity ⊤ _∧_
@@ -80,7 +79,7 @@ open import Data.Product
 ∨-identityʳ : RightIdentity ⊥ _∨_
 ∨-identityʳ x = begin
   x ∨ ⊥          ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-complementʳ _) ⟩
-  x ∨ x ∧ ¬ x    ≈⟨ proj₁ absorptive _ _ ⟩
+  x ∨ x ∧ ¬ x    ≈⟨ ∨-absorbs-∧ _ _ ⟩
   x              ∎
 
 ∨-identityˡ : LeftIdentity ⊥ _∨_
@@ -117,20 +116,6 @@ open import Data.Product
 ∨-zero : Zero ⊤ _∨_
 ∨-zero = ∨-zeroˡ , ∨-zeroʳ
 
-∨-isSemigroup : IsSemigroup _∨_
-∨-isSemigroup = record
-  { isEquivalence = isEquivalence
-  ; assoc         = ∨-assoc
-  ; ∙-cong        = ∨-cong
-  }
-
-∧-isSemigroup : IsSemigroup _∧_
-∧-isSemigroup = record
-  { isEquivalence = isEquivalence
-  ; assoc         = ∧-assoc
-  ; ∙-cong        = ∧-cong
-  }
-
 ∨-⊥-isMonoid : IsMonoid _∨_ ⊥
 ∨-⊥-isMonoid = record
   { isSemigroup = ∨-isSemigroup
@@ -146,23 +131,23 @@ open import Data.Product
 ∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _∨_ ⊥
 ∨-⊥-isCommutativeMonoid = record
   { isSemigroup = ∨-isSemigroup
-  ; identityˡ = ∨-identityˡ
-  ; comm      = ∨-comm
+  ; identityˡ   = ∨-identityˡ
+  ; comm        = ∨-comm
   }
 
 ∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _∧_ ⊤
 ∧-⊤-isCommutativeMonoid = record
   { isSemigroup = ∧-isSemigroup
-  ; identityˡ = ∧-identityˡ
-  ; comm      = ∧-comm
+  ; identityˡ   = ∧-identityˡ
+  ; comm        = ∧-comm
   }
 
 ∨-∧-isCommutativeSemiring : IsCommutativeSemiring _∨_ _∧_ ⊥ ⊤
 ∨-∧-isCommutativeSemiring = record
   { +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid
   ; *-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid
-  ; distribʳ = proj₂ ∧-∨-distrib
-  ; zeroˡ    = ∧-zeroˡ
+  ; distribʳ              = proj₂ ∧-∨-distrib
+  ; zeroˡ                 = ∧-zeroˡ
   }
 
 ∨-∧-commutativeSemiring : CommutativeSemiring _ _
@@ -530,13 +515,18 @@ module XorRing
       ((¬ x ∨ ¬ y) ∨ z) ∧
       (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ∎
 
-  ⊕-isSemigroup : IsSemigroup _⊕_
-  ⊕-isSemigroup = record
+  ⊕-isMagma : IsMagma _⊕_
+  ⊕-isMagma = record
     { isEquivalence = isEquivalence
-    ; assoc         = ⊕-assoc
     ; ∙-cong        = ⊕-cong
     }
 
+  ⊕-isSemigroup : IsSemigroup _⊕_
+  ⊕-isSemigroup = record
+    { isMagma = ⊕-isMagma
+    ; assoc   = ⊕-assoc
+    }
+
   ⊕-⊥-isMonoid : IsMonoid _⊕_ ⊥
   ⊕-⊥-isMonoid = record
     { isSemigroup = ⊕-isSemigroup