[Add] Consequences of identity for monoids

CHANGELOG.md

@@ -126,6 +126,10 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* `Algebra.Properties.Monoid` adding consequences for identity for monoids
+
+* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →

src/Algebra/Definitions.agda

@@ -16,7 +16,6 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Nullary.Negation.Core using (¬_)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
@@ -26,6 +25,7 @@ module Algebra.Definitions
 open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 ------------------------------------------------------------------------
 -- Properties of operations

src/Algebra/Properties/Monoid.agda

@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Equational reasoning for monoids
+-- (Utilities for identity and cancellation reasoning, extending semigroup reasoning)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+open import Function using (_∘_)
+
+module Algebra.Properties.Monoid {o ℓ} (M : Monoid o ℓ) where
+
+open Monoid M
+  using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ
+  ; identityʳ ; ∙-cong; refl; assoc; ∙-congˡ; ∙-congʳ; trans)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+open import Algebra.Properties.Semigroup semigroup public
+
+private
+    variable
+        a b c d : Carrier
+
+id-unique : ∀ a → (∀ b → b ∙ a ≈ b) → a ≈ ε
+id-unique a b∙a≈b = trans (sym (identityˡ a)) (b∙a≈b ε)
+
+id-comm : ∀ a → a ∙ ε ≈ ε ∙ a
+id-comm a = trans (identityʳ a) (sym (identityˡ a))
+
+id-comm-sym : ∀ a → ε ∙ a ≈ a ∙ ε
+id-comm-sym = sym ∘ id-comm
+
+module _ (a≈ε : a ≈ ε) where
+    elimʳ : ∀ b → b ∙ a ≈ b
+    elimʳ = trans (∙-congˡ a≈ε) ∘ identityʳ
+
+    elimˡ : ∀ b → a ∙ b ≈ b
+    elimˡ = trans (∙-congʳ a≈ε) ∘ identityˡ
+
+    introʳ : ∀ b → b ≈ b ∙ a
+    introʳ = sym ∘ elimʳ
+
+    introˡ : ∀ b → b ≈ a ∙ b
+    introˡ = sym ∘ elimˡ
+
+    introcenter : ∀ c → b ∙ c ≈ b ∙ (a ∙ c)
+    introcenter c = trans (∙-congˡ (sym (identityˡ c))) (∙-congˡ (∙-congʳ (sym a≈ε)))
+
+module _ (inv : a ∙ c ≈ ε) where
+
+  cancelʳ : ∀ b → (b ∙ a) ∙ c ≈ b
+  cancelʳ b = trans (assoc b a c) (trans (∙-congˡ inv) (identityʳ b))
+
+  cancelˡ : ∀ b → a ∙ (c ∙ b) ≈ b
+  cancelˡ b = trans (sym (assoc a c b)) (trans (∙-congʳ inv) (identityˡ b))
+
+  insertˡ : ∀ b → b ≈ a ∙ (c ∙ b)
+  insertˡ = sym ∘ cancelˡ
+
+  insertʳ : ∀ b → b ≈ (b ∙ a) ∙ c
+  insertʳ = sym ∘ cancelʳ
+
+  cancelInner : ∀ b d → (b ∙ a) ∙ (c ∙ d) ≈ b ∙ d
+  cancelInner b d = trans (uv≈w⇒xu∙vy≈x∙wy inv b d) (∙-congˡ (identityˡ d))
+
+  insertInner : ∀ b d → b ∙ d ≈ (b ∙ a) ∙ (c ∙ d)
+  insertInner = λ b d → sym (cancelInner b d)
+

src/Algebra/Properties/Semigroup.agda

@@ -10,9 +10,15 @@ open import Algebra using (Semigroup)
 
 module Algebra.Properties.Semigroup {a ℓ} (S : Semigroup a ℓ) where
 
+open import Data.Product.Base using (_,_)
+
 open Semigroup S
 open import Algebra.Definitions _≈_
-open import Data.Product.Base using (_,_)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+private
+ variable
+    u v w x y z : Carrier
 
 x∙yz≈xy∙z : ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ y) ∙ z
 x∙yz≈xy∙z x y z = sym (assoc x y z)
@@ -28,3 +34,91 @@ alternative = alternativeˡ , alternativeʳ
 
 flexible : Flexible _∙_
 flexible x y = assoc x y x
+
+module _ (uv≈w : u ∙ v ≈ w) where
+    uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
+    uv≈w⇒xu∙v≈xw x = trans (assoc x u v) (∙-congˡ uv≈w)
+
+    uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x
+    uv≈w⇒u∙vx≈wx x = trans (sym (assoc u v x)) (∙-congʳ uv≈w)
+
+    uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
+    uv≈w⇒u[vx∙y]≈w∙xy x y = trans (∙-congˡ (assoc v x y)) (uv≈w⇒u∙vx≈wx (x ∙ y))
+
+    uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
+    uv≈w⇒x[uv∙y]≈x∙wy x y = ∙-congˡ (uv≈w⇒u∙vx≈wx y)
+
+    uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
+    uv≈w⇒[x∙yu]v≈x∙yw x y = trans (assoc x (y ∙ u) v) (∙-congˡ (uv≈w⇒xu∙v≈xw y))
+
+    uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
+    uv≈w⇒[xu∙v]y≈x∙wy x y = trans (∙-congʳ (uv≈w⇒xu∙v≈xw x)) (assoc x w y)
+
+    uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
+    uv≈w⇒[xy∙u]v≈x∙yw x y = trans (∙-congʳ (assoc x y u)) (uv≈w⇒[x∙yu]v≈x∙yw x  y )
+
+module _ (uv≈w : u ∙ v ≈ w) where
+    uv≈w⇒xw≈xu∙v : ∀ x → x ∙ w ≈ (x ∙ u) ∙ v
+    uv≈w⇒xw≈xu∙v x = sym (uv≈w⇒xu∙v≈xw uv≈w x)
+
+    uv≈w⇒wx≈u∙vx : ∀ x → w ∙ x ≈ u ∙ (v ∙ x)
+    uv≈w⇒wx≈u∙vx x = sym (uv≈w⇒u∙vx≈wx uv≈w x)
+
+    uv≈w⇒w∙xy≈u[vx∙y] : ∀ x y → w ∙ (x ∙ y) ≈ u ∙ ((v ∙ x) ∙ y)
+    uv≈w⇒w∙xy≈u[vx∙y] x y = sym (uv≈w⇒u[vx∙y]≈w∙xy uv≈w x y)
+
+    uv≈w⇒x∙wy≈x[u∙vy] : ∀ x y → x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x[u∙vy] x y = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w x y)
+
+    uv≈w⇒x∙yw≈[x∙yu]v : ∀ x y  → x ∙ (y ∙ w) ≈ (x ∙ (y ∙ u)) ∙ v
+    uv≈w⇒x∙yw≈[x∙yu]v x y  = sym (uv≈w⇒[x∙yu]v≈x∙yw uv≈w x y)
+
+    uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
+    uv≈w⇒xu∙vy≈x∙wy x y = uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx uv≈w y) x
+
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
+    uv≈w⇒xy≈z⇒u[vx∙y]≈wz z xy≈z = trans (∙-congˡ (uv≈w⇒xu∙v≈xw xy≈z v)) (uv≈w⇒u∙vx≈wx uv≈w z)
+
+    uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
+    uv≈w⇒x∙wy≈x∙[u∙vy] = sym (uv≈w⇒x[uv∙y]≈x∙wy uv≈w _ _)
+
+module _ {u v w x : Carrier} where
+    [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
+    [uv∙w]x≈u[vw∙x] = uv≈w⇒[xu∙v]y≈x∙wy refl u x
+
+    [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+    [uv∙w]x≈u[v∙wx] = uv≈w⇒[xy∙u]v≈x∙yw refl u v
+
+    [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
+    [u∙vw]x≈uv∙wx = trans (sym (∙-congʳ (assoc u v w))) (assoc (u ∙ v) w x)
+
+    [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
+    [u∙vw]x≈u[v∙wx] = uv≈w⇒[x∙yu]v≈x∙yw refl u v
+
+    uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
+    uv∙wx≈u[vw∙x] = uv≈w⇒xu∙vy≈x∙wy refl u x
+
+    uv∙wx≈[u∙vw]x : (u ∙ v) ∙ (w ∙ x) ≈ (u ∙ (v ∙ w)) ∙ x
+    uv∙wx≈[u∙vw]x = sym [u∙vw]x≈uv∙wx
+
+    u[vw∙x]≈[uv∙w]x : u ∙ ((v ∙ w) ∙ x) ≈ ((u ∙ v) ∙ w) ∙ x
+    u[vw∙x]≈[uv∙w]x = sym [uv∙w]x≈u[vw∙x]
+
+    u[vw∙x]≈uv∙wx : u ∙ ((v ∙ w) ∙ x) ≈ (u ∙ v) ∙ (w ∙ x)
+    u[vw∙x]≈uv∙wx = sym uv∙wx≈u[vw∙x]
+
+    u[v∙wx]≈[uv∙w]x : u ∙ (v ∙ (w ∙ x)) ≈ ((u ∙ v) ∙ w) ∙ x
+    u[v∙wx]≈[uv∙w]x = sym [uv∙w]x≈u[v∙wx]
+
+    u[v∙wx]≈[u∙vw]x : u ∙ (v ∙ (w ∙ x)) ≈ (u ∙ (v ∙ w)) ∙ x
+    u[v∙wx]≈[u∙vw]x = sym [u∙vw]x≈u[v∙wx]
+
+module _ {u v w x : Carrier} (uv≈wx : u ∙ v ≈ w ∙ x) where
+    uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
+    uv≈wx⇒yu∙v≈yw∙x y = trans (uv≈w⇒xu∙v≈xw uv≈wx y) (sym (assoc y w x))
+
+    uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
+    uv≈wx⇒u∙vy≈w∙xy y = trans (uv≈w⇒u∙vx≈wx uv≈wx y) (assoc w x y)
+
+    uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
+    uv≈wx⇒yu∙vz≈yw∙xz y z = trans (uv≈w⇒xu∙v≈xw (uv≈wx⇒u∙vy≈w∙xy z) y) (sym (assoc y w (x ∙ z)))