[ add ] BooleanRing plus Properties

CHANGELOG.md

@@ -163,6 +163,8 @@ New modules
 
 * `Algebra.Morphism.Construct.DirectProduct`.
 
+* `Algebra.Properties.BooleanRing`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
@@ -186,6 +188,11 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Bundles`:
+  ```agda
+  record BooleanRing _ _ : Set _
+  ```
+
 * In `Algebra.Consequences.Base`:
   ```agda
   module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)
@@ -254,9 +261,9 @@ Additions to existing modules
   ∣ˡ-preorder   : Preorder a ℓ _
   ```
 
-* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
 
-```
+* In `Algebra.Properties.Semigroup`, consequences for associativity for semigroups:
+  ```
   uv≈w⇒xu∙v≈xw          : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
   uv≈w⇒u∙vx≈wx          : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x
   uv≈w⇒u[vx∙y]≈w∙xy     : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
@@ -275,7 +282,7 @@ Additions to existing modules
   uv≈wx⇒yu∙v≈yw∙x       : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
   uv≈wx⇒u∙vy≈w∙xy       : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
   uv≈wx⇒yu∙vz≈yw∙xz     : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-```
+  ```
 
 * In `Algebra.Properties.Semigroup.Divisibility`:
   ```agda
@@ -291,6 +298,11 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Algebra.Structures`:
+  ```agda
+  record IsBooleanRing + * - 0# 1# : Set _
+  ```
+
 * In `Data.Bool.Properties`:
   ```agda
   if-eta : ∀ b → (if b then x else x) ≡ x

src/Algebra/Bundles.agda

@@ -1124,6 +1124,28 @@ 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
+
+  ring : Ring _ _
+  ring = record { isRing = isRing }
+
+
 ------------------------------------------------------------------------
 -- Bundles with 3 binary operations
 ------------------------------------------------------------------------

src/Algebra/Properties/BooleanRing.agda

@@ -0,0 +1,85 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles
+  using (BooleanRing; CommutativeMonoid; IdempotentCommutativeMonoid; CommutativeRing)
+
+module Algebra.Properties.BooleanRing {r₁ r₂} (R : BooleanRing r₁ r₂) where
+
+open import Function.Base using (_$_)
+
+open BooleanRing R
+open import Algebra.Definitions _≈_
+open import Algebra.Structures _≈_
+  using (IsCommutativeMonoid; IsIdempotentCommutativeMonoid; IsCommutativeRing)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Export properties of rings
+
+open import Algebra.Properties.Ring ring public
+
+------------------------------------------------------------------------
+-- Extra properties of Boolean rings
+
+xy+yx≈0 : ∀ x y → x * y + y * x ≈ 0#
+xy+yx≈0 x y = +-cancelˡ (x * x) _ _ $ +-cancelʳ (y * y) _ _ $ begin
+  x * x + ((x * y) + (y * x)) + y * y ≈⟨ +-congʳ (+-assoc _ _ _) ⟨
+  x * x + x * y + y * x + y * y       ≈⟨ +-assoc _ _ _ ⟩
+  (x * x + x * y) + (y * x + y * y)   ≈⟨ +-cong (distribˡ x x y) (distribˡ y x y) ⟨
+  x * (x + y) + y * (x + y)           ≈⟨ distribʳ (x + y) x y ⟨
+  (x + y) * (x + y)                   ≈⟨ *-idem (x + y) ⟩
+  x + y                               ≈⟨ +-congˡ (*-idem y) ⟨
+  x + y * y                           ≈⟨ +-congʳ (*-idem x) ⟨
+  x * x + y * y                       ≈⟨ +-congʳ (+-identityʳ (x * x)) ⟨
+  x * x + 0# + y * y                  ∎
+
+x+x≈0 : ∀ x → x + x ≈ 0#
+x+x≈0 x = begin
+  x + x         ≈⟨ +-cong (*-idem x) (*-idem x) ⟨
+  x * x + x * x ≈⟨ xy+yx≈0 x x ⟩
+  0#            ∎
+
+-x≈x : ∀ x → - x ≈ x
+-x≈x x = begin
+  - x ≈⟨ +-inverseˡ-unique x x (x+x≈0 x) ⟨
+  x   ∎
+
+*-comm : Commutative _*_
+*-comm x y = begin
+  x * y     ≈⟨ +-inverseˡ-unique  _ _ (xy+yx≈0 x y) ⟩
+  - (y * x) ≈⟨ -x≈x _ ⟩
+  y * x     ∎
+
+------------------------------------------------------------------------
+-- Additional structures
+
+*-isCommutativeMonoid : IsCommutativeMonoid _*_ 1#
+*-isCommutativeMonoid = record { isMonoid = *-isMonoid ; comm = *-comm }
+
+*-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _*_ 1#
+*-isIdempotentCommutativeMonoid = record
+  { isCommutativeMonoid = *-isCommutativeMonoid
+  ; idem = *-idem
+  }
+
+isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
+isCommutativeRing = record { isRing = isRing ; *-comm = *-comm }
+
+------------------------------------------------------------------------
+-- Additional bundles
+
+*-commutativeMonoid : CommutativeMonoid _ _
+*-commutativeMonoid = record { isCommutativeMonoid = *-isCommutativeMonoid }
+
+*-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
+*-idempotentCommutativeMonoid = record
+  { isIdempotentCommutativeMonoid = *-isIdempotentCommutativeMonoid }
+
+commutativeRing : CommutativeRing _ _
+commutativeRing = record { isCommutativeRing = isCommutativeRing }

src/Algebra/Structures.agda

@@ -962,6 +962,18 @@ record IsCommutativeRing
     ; *-isCommutativeMonoid
     )
 
+record IsBooleanRing
+         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isRing : IsRing + * - 0# 1#
+    *-idem : Idempotent *
+
+  open IsRing isRing public
+
+  isIdempotentMonoid :  IsIdempotentMonoid * 1#
+  isIdempotentMonoid = record { isMonoid = *-isMonoid ; idem = *-idem }
+
+
 ------------------------------------------------------------------------
 -- Structures with 3 binary operations
 ------------------------------------------------------------------------