[ add ] BooleanRing plus Properties (#2763)

* add: `BooleanRing` plus `Properties`

* Update CHANGELOG.md

Removed spurious entry

* refactor: more general API

* fix: added note to `CHANGELOG`

* refactor: make binomial expansion an explicit step

* rename: `*-isIdempotentMonoid`

* add: `*-idempotentMonoid`

* refactor: use `Cancellative` properties only

* add: stub properties for `CommutativeRing`

* refactor: `BooleanRing` properties in terms of `CommutativeRing` and `BooleanSemiring`

* refactor: put everything together

* add: stub properties for `CommutativeRing`

* refactor: adjust re-exports

* add: `BooleanAlgebra` yields `BooleanRing` etc.

* add: more re-exports

* add: more inherited properties

* add: more properties towards `IsBooleanAlgebra`

* add: yet more properties towards `IsBooleanAlgebra`

* add: grinding towards `IsBooleanAlgebra`

* add: `deMorgan` laws

* add: `Semiring` properties as home for `binomial-expansion`

* more fiddling

* back to square one

* fix: finally!

* fix: remove shadowing of `isBooleanRing` and `booleanRing`

* reset: `CHANGELOG` for v2.4

* fix: whitespace

Author: jamesmckinna

CHANGELOG.md

@@ -47,18 +47,57 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Properties.BooleanRing`.
+
+* `Algebra.Properties.BooleanSemiring`.
+
+* `Algebra.Properties.CommutativeRing`.
+
+* `Algebra.Properties.Semiring`.
+
 * `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Bundles`:
+  ```agda
+  record BooleanSemiring _ _ : Set _
+  record BooleanRing _ _     : Set _
+  ```
+
+* In `Algebra.Consequences.Propositional`:
+  ```agda
+  binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ →
+    ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  ```
+
+* In `Algebra.Consequences.Setoid`:
+  ```agda
+  binomial-expansion : Congruent₂ _∙_  → Associative _∙_ → _◦_ DistributesOver _∙_ →
+    ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  ```
+
+* In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`:
+  ```agda
+  ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤
+  ⊕-∧-booleanRing   : BooleanRing _ _
+  ```
+
 * In `Algebra.Properties.RingWithoutOne`:
   ```agda
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
   ```
 
+* In `Algebra.Structures`:
+  ```agda
+  record IsBooleanSemiring + * 0# 1# : Set _
+  record IsBooleanRing + * - 0# 1# : Set _
+  ```
+  NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`.
+
 * In `Data.Fin.Permutation.Components`:
   ```agda
   transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j

src/Algebra/Bundles.agda

@@ -921,6 +921,41 @@ record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; rawMonoid to *-rawMonoid
     )
 
+record BooleanSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier           : Set c
+    _≈_               : Rel Carrier ℓ
+    _+_               : Op₂ Carrier
+    _*_               : Op₂ Carrier
+    0#                : Carrier
+    1#                : Carrier
+    isBooleanSemiring : IsBooleanSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsBooleanSemiring isBooleanSemiring public
+
+  semiring : Semiring _ _
+  semiring = record { isSemiring = isSemiring }
+
+  open Semiring semiring public
+    using ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma;  *-magma;  *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; rawNearSemiring ; rawSemiring; nearSemiring
+    ; semiringWithoutOne; semiringWithoutAnnihilatingZero
+    )
+
+  *-idempotentMonoid :  IdempotentMonoid c ℓ
+  *-idempotentMonoid = record { isIdempotentMonoid = *-isIdempotentMonoid }
+
+  open IdempotentMonoid *-idempotentMonoid public
+    using () renaming (band to *-band)
+
+
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 1 element
 ------------------------------------------------------------------------
@@ -1106,7 +1141,10 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
   ring : Ring _ _
   ring = record { isRing = isRing }
 
-  open Ring ring public using (_≉_; rawRing; +-invertibleMagma; +-invertibleUnitalMagma; +-group; +-abelianGroup)
+  open Ring ring public
+    using (_≉_; rawRing
+          ; +-invertibleMagma; +-invertibleUnitalMagma
+          ; +-group; +-abelianGroup)
 
   commutativeSemiring : CommutativeSemiring _ _
   commutativeSemiring =
@@ -1124,6 +1162,47 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
     ; commutativeSemiringWithoutOne
     )
 
+
+record BooleanRing c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier       : Set c
+    _≈_           : Rel Carrier ℓ
+    _+_           : Op₂ Carrier
+    _*_           : Op₂ Carrier
+    -_            : Op₁ Carrier
+    0#            : Carrier
+    1#            : Carrier
+    isBooleanRing : IsBooleanRing _≈_ _+_ _*_ -_ 0# 1#
+
+  open IsBooleanRing isBooleanRing public
+    using (isCommutativeRing; *-idem)
+
+  open IsCommutativeRing isCommutativeRing public
+
+  commutativeRing : CommutativeRing _ _
+  commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+  open CommutativeRing commutativeRing public
+    using
+    (_≉_; rawRing
+    ; +-invertibleMagma; +-invertibleUnitalMagma
+    ; +-group; +-abelianGroup
+    ; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid; *-commutativeMonoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero; semiring
+    ; commutativeSemiringWithoutOne; commutativeSemiring
+    ; ring
+    )
+
+
 ------------------------------------------------------------------------
 -- Bundles with 3 binary operations
 ------------------------------------------------------------------------

src/Algebra/Consequences/Propositional.agda

@@ -42,6 +42,7 @@ open Base public
   ; subst∧comm⇒sym
   ; wlog
   ; sel⇒idem
+  ; binomial-expansion
 -- plus all the deprecated versions of the above
   ; comm+assoc⇒middleFour
   ; identity+middleFour⇒assoc
@@ -101,6 +102,15 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
   comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
   comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
 
+module _ {_∙_ _◦_ : Op₂ A}
+         (∙-assoc : Associative _∙_)
+         (distrib : _◦_ DistributesOver _∙_)
+         where
+
+  binomial-expansion : ∀ w x y z →
+             ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib
+
 ------------------------------------------------------------------------
 -- Selectivity
 

src/Algebra/Consequences/Setoid.agda

@@ -292,6 +292,21 @@ module _ {_∙_ _◦_ : Op₂ A}
     (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z))  ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
     (x ∙ y) ◦ (x ∙ z)              ∎
 
+module _ {_∙_ _◦_ : Op₂ A}
+         (∙-cong  : Congruent₂ _∙_)
+         (∙-assoc : Associative _∙_)
+         (distrib@(distribˡ , distribʳ) : _◦_ DistributesOver _∙_)
+         where
+
+  binomial-expansion : ∀ w x y z →
+             ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  binomial-expansion w x y z = begin
+    (w ∙ x) ◦ (y ∙ z)                         ≈⟨ distribʳ _ _ _ ⟩
+    (w ◦ (y ∙ z)) ∙ (x ◦ (y ∙ z))             ≈⟨ ∙-cong (distribˡ _ _ _) (distribˡ _ _ _) ⟩
+    ((w ◦ y) ∙ (w ◦ z)) ∙ ((x ◦ y) ∙ (x ◦ z)) ≈⟨ ∙-assoc _ _ _ ⟨
+    (((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z) ∎
+
+
 ------------------------------------------------------------------------
 -- Ring-like structures
 

src/Algebra/Lattice/Properties/BooleanAlgebra.agda

@@ -6,30 +6,31 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice.Bundles
+open import Algebra.Lattice.Bundles using (BooleanAlgebra)
 
 module Algebra.Lattice.Properties.BooleanAlgebra
-  {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
+  {c ℓ} (booleanAlgebra : BooleanAlgebra c ℓ)
   where
 
-open BooleanAlgebra B
+open import Algebra.Bundles
+  using (CommutativeSemiring; CommutativeRing; BooleanRing)
+open import Algebra.Core using (Op₂)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id; _$_; _⟨_⟩_)
+open import Function.Bundles using (_⇔_; module Equivalence)
 
-import Algebra.Lattice.Properties.DistributiveLattice as DistribLatticeProperties
-open import Algebra.Core using (Op₁; Op₂)
+open BooleanAlgebra booleanAlgebra
 open import Algebra.Structures _≈_
 open import Algebra.Definitions _≈_
 open import Algebra.Consequences.Setoid setoid
-open import Algebra.Bundles using (CommutativeSemiring; CommutativeRing)
 open import Algebra.Lattice.Structures _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Function.Base using (id; _$_; _⟨_⟩_)
-open import Function.Bundles using (_⇔_; module Equivalence)
-open import Data.Product.Base using (_,_)
+
 
 ------------------------------------------------------------------------
 -- Export properties from distributive lattices
 
-open DistribLatticeProperties distributiveLattice public
+open import Algebra.Lattice.Properties.DistributiveLattice distributiveLattice public
 
 ------------------------------------------------------------------------
 -- The dual construction is also a boolean algebra
@@ -529,6 +530,12 @@ module XorRing
     { isCommutativeRing = ⊕-∧-isCommutativeRing
     }
 
+  ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤
+  ⊕-∧-isBooleanRing = record
+    { isCommutativeRing = ⊕-∧-isCommutativeRing ; *-idem = ∧-idem }
+
+  ⊕-∧-booleanRing : BooleanRing _ _
+  ⊕-∧-booleanRing = record { isBooleanRing = ⊕-∧-isBooleanRing }
 
 infixl 6 _⊕_
 

src/Algebra/Properties/BooleanRing.agda

@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Boolean Rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles
+  using (CommutativeRing; BooleanSemiring; BooleanRing)
+
+module Algebra.Properties.BooleanRing
+  {c ℓ} (booleanRing : BooleanRing c ℓ) where
+
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_)
+
+open BooleanRing booleanRing
+open import Algebra.Structures _≈_
+  using (IsBooleanSemiring)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Re-export properties of Commutative Rings
+
+open import Algebra.Properties.CommutativeRing commutativeRing public
+
+------------------------------------------------------------------------
+-- Structures
+
+isBooleanSemiring : IsBooleanSemiring _+_ _*_ 0# 1#
+isBooleanSemiring = record
+  { isSemiring = isSemiring
+  ; +-cancel = +-cancel
+  ; *-idem = *-idem
+  }
+
+open IsBooleanSemiring isBooleanSemiring public
+  using (*-isIdempotentMonoid)
+
+------------------------------------------------------------------------
+-- Bundles
+
+booleanSemiring : BooleanSemiring _ _
+booleanSemiring = record { isBooleanSemiring = isBooleanSemiring }
+
+open BooleanSemiring booleanSemiring public
+  using (*-idempotentMonoid)
+
+------------------------------------------------------------------------
+-- Export properties of Boolean semirings
+
+open import Algebra.Properties.BooleanSemiring booleanSemiring public
+  hiding (isBooleanRing; booleanRing)
+
+------------------------------------------------------------------------
+-- Further consequences
+
+-x≈x : ∀ x → - x ≈ x
+-x≈x = x+y≈0⇒y≈x ∘ -‿inverseʳ
+