Addd middle four exchange law (#1953)

agda · Jun 10, 2023 · cfa2504 · cfa2504
1 parent a35445c
commit cfa2504
Show file tree

Hide file tree

Showing 4 changed files with 85 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1646,8 +1646,30 @@ Other minor changes
  Involutive _≈_ f
  ```
 
+* Added new proofs to `Algebra.Consequences.Propositional`:
+ ```agda
+ comm+assoc⇒middleFour : Commutative _•_ →
+ Associative _•_ →
+ _•_ MiddleFourExchange _•_
+ identity+middleFour⇒assoc : Identity e _•_ →
+ _•_ MiddleFourExchange _•_ →
+ Associative _•_
+ identity+middleFour⇒comm : Identity e _+_ →
+ _•_ MiddleFourExchange _+_ →
+ Commutative _•_
+ ```
+
 * 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
@@ -1711,6 +1733,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 _

diff --git a/src/Algebra/Consequences/Propositional.agda b/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
@@ -90,6 +93,25 @@ module _ {_•_ : Op₂ A} where
  sel⇒idem : Selective _•_ → Idempotent _•_
  sel⇒idem = Base.sel⇒idem _≡_
 
+------------------------------------------------------------------------
+-- Middle-Four Exchange
+
+module _ {_•_ : Op₂ A} where
+
+ 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
 

diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
@@ -29,6 +29,40 @@ open import Relation.Unary using (Pred)
 
 open import Algebra.Consequences.Base public
 
+------------------------------------------------------------------------
+-- 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
 

diff --git a/src/Algebra/Definitions.agda b/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