middle four exchange law in a Setoid: definition and consequences

CHANGELOG.md

@@ -1603,6 +1603,15 @@ Other minor changes
 
 * Added new proofs to `Algebra.Consequences.Setoid`:
   ```agda
+  comm+assoc⇒middleFour : Congruent₂ _•_ → Commutative _•_ → Associative _•_ →
+                           _•_ MiddleFourExchange _•_
+  identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ →
+                               _•_ MiddleFourExchange _•_ →
+                               Associative _•_
+  identity+middleFour⇒comm : Congruent₂ _•_ → Identity e _+_ →
+                              _•_ MiddleFourExchange _+_ →
+                              Commutative _•_
+
   involutive⇒surjective  : Involutive f  → Surjective f
   selfInverse⇒involutive : SelfInverse f → Involutive f
   selfInverse⇒congruent  : SelfInverse f → Congruent f
@@ -1666,6 +1675,8 @@ Other minor changes
 
 * Added new definition to `Algebra.Definitions`:
   ```agda
+  _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
+
   SelfInverse : Op₁ A → Set _
 
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _

src/Algebra/Consequences/Propositional.agda

@@ -24,7 +24,10 @@ import Algebra.Consequences.Setoid (setoid A) as Base
 
 open Base public
   hiding
-  ( assoc+distribʳ+idʳ+invʳ⇒zeˡ
+  ( comm+assoc⇒middleFour
+  ; identity+middleFour⇒assoc
+  ; identity+middleFour⇒comm
+  ; assoc+distribʳ+idʳ+invʳ⇒zeˡ
   ; assoc+distribˡ+idʳ+invʳ⇒zeʳ
   ; assoc+id+invʳ⇒invˡ-unique
   ; assoc+id+invˡ⇒invʳ-unique
@@ -83,13 +86,27 @@ module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where
   comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm
 
 ------------------------------------------------------------------------
--- Selectivity
+-- Selectivity and Middle-Four Exchange
 
 module _ {_•_ : Op₂ A} where
 
   sel⇒idem : Selective _•_ → Idempotent _•_
   sel⇒idem = Base.sel⇒idem _≡_
 
+  comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
+                           _•_ MiddleFourExchange _•_
+  comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _•_)
+
+  identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
+                               _•_ MiddleFourExchange _•_ →
+                               Associative _•_
+  identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _•_)
+
+  identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
+                              _•_ MiddleFourExchange _+_ →
+                              Commutative _•_
+  identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _•_)
+
 ------------------------------------------------------------------------
 -- Without Loss of Generality
 

src/Algebra/Consequences/Setoid.agda

@@ -29,6 +29,40 @@ open import Relation.Unary using (Pred)
 
 open import Algebra.Consequences.Base public
 
+------------------------------------------------------------------------
+-- Congruence and MiddleFourExchange
+
+module _ {_•_ : Op₂ A} (cong : Congruent₂ _•_) where
+
+  comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
+                                _•_ MiddleFourExchange _•_
+  comm+assoc⇒middleFour comm assoc w x y z = begin
+    (w • x) • (y • z) ≈⟨ assoc w x (y • z) ⟩
+    w • (x • (y • z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
+    w • ((x • y) • z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
+    w • ((y • x) • z) ≈⟨ cong refl (assoc y x z) ⟩
+    w • (y • (x • z)) ≈⟨ sym (assoc w y (x • z)) ⟩
+    (w • y) • (x • z) ∎
+
+  identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
+                                    _•_ MiddleFourExchange _•_ →
+                                    Associative _•_
+  identity+middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
+    (x • y) • z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
+    (x • y) • (e • z) ≈⟨ middleFour x y e z ⟩
+    (x • e) • (y • z) ≈⟨ cong (identityʳ x) refl ⟩
+    x • (y • z) ∎
+
+  identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
+                                   _•_ MiddleFourExchange _+_ →
+                                   Commutative _•_
+  identity+middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
+    = begin
+    x • y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+    (e + x) • (y + e) ≈⟨ middleFour e x y e ⟩
+    (e + y) • (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
+    y • x             ∎
+
 ------------------------------------------------------------------------
 -- Involutive/SelfInverse functions
 

src/Algebra/Definitions.agda

@@ -108,6 +108,10 @@ _*_ DistributesOverʳ _+_ =
 _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
+_MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
+_*_ MiddleFourExchange _+_ = 
+  ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
+
 _IdempotentOn_ : Op₂ A → A → Set _
 _∙_ IdempotentOn x = (x ∙ x) ≈ x