Skip to content

Commit d0e9374

Browse files
jamesmckinnaMatthewDaggitt
authored andcommitted
Addd middle four exchange law (#1953)
1 parent 1933346 commit d0e9374

File tree

4 files changed

+85
-1
lines changed

4 files changed

+85
-1
lines changed

CHANGELOG.md

+24
Original file line numberDiff line numberDiff line change
@@ -1646,8 +1646,30 @@ Other minor changes
16461646
Involutive _≈_ f
16471647
```
16481648

1649+
* Added new proofs to `Algebra.Consequences.Propositional`:
1650+
```agda
1651+
comm+assoc⇒middleFour : Commutative _•_ →
1652+
Associative _•_ →
1653+
_•_ MiddleFourExchange _•_
1654+
identity+middleFour⇒assoc : Identity e _•_ →
1655+
_•_ MiddleFourExchange _•_ →
1656+
Associative _•_
1657+
identity+middleFour⇒comm : Identity e _+_ →
1658+
_•_ MiddleFourExchange _+_ →
1659+
Commutative _•_
1660+
```
1661+
16491662
* Added new proofs to `Algebra.Consequences.Setoid`:
16501663
```agda
1664+
comm+assoc⇒middleFour : Congruent₂ _•_ → Commutative _•_ → Associative _•_ →
1665+
_•_ MiddleFourExchange _•_
1666+
identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ →
1667+
_•_ MiddleFourExchange _•_ →
1668+
Associative _•_
1669+
identity+middleFour⇒comm : Congruent₂ _•_ → Identity e _+_ →
1670+
_•_ MiddleFourExchange _+_ →
1671+
Commutative _•_
1672+
16511673
involutive⇒surjective : Involutive f → Surjective f
16521674
selfInverse⇒involutive : SelfInverse f → Involutive f
16531675
selfInverse⇒congruent : SelfInverse f → Congruent f
@@ -1711,6 +1733,8 @@ Other minor changes
17111733

17121734
* Added new definition to `Algebra.Definitions`:
17131735
```agda
1736+
_MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
1737+
17141738
SelfInverse : Op₁ A → Set _
17151739
17161740
LeftDividesˡ : Op₂ A → Op₂ A → Set _

src/Algebra/Consequences/Propositional.agda

+23-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,10 @@ import Algebra.Consequences.Setoid (setoid A) as Base
2424

2525
open Base public
2626
hiding
27-
( assoc+distribʳ+idʳ+invʳ⇒zeˡ
27+
( comm+assoc⇒middleFour
28+
; identity+middleFour⇒assoc
29+
; identity+middleFour⇒comm
30+
; assoc+distribʳ+idʳ+invʳ⇒zeˡ
2831
; assoc+distribˡ+idʳ+invʳ⇒zeʳ
2932
; assoc+id+invʳ⇒invˡ-unique
3033
; assoc+id+invˡ⇒invʳ-unique
@@ -90,6 +93,25 @@ module _ {_•_ : Op₂ A} where
9093
sel⇒idem : Selective _•_ Idempotent _•_
9194
sel⇒idem = Base.sel⇒idem _≡_
9295

96+
------------------------------------------------------------------------
97+
-- Middle-Four Exchange
98+
99+
module _ {_•_ : Op₂ A} where
100+
101+
comm+assoc⇒middleFour : Commutative _•_ Associative _•_
102+
_•_ MiddleFourExchange _•_
103+
comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _•_)
104+
105+
identity+middleFour⇒assoc : {e : A} Identity e _•_
106+
_•_ MiddleFourExchange _•_
107+
Associative _•_
108+
identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _•_)
109+
110+
identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} Identity e _+_
111+
_•_ MiddleFourExchange _+_
112+
Commutative _•_
113+
identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _•_)
114+
93115
------------------------------------------------------------------------
94116
-- Without Loss of Generality
95117

src/Algebra/Consequences/Setoid.agda

+34
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,40 @@ open import Relation.Unary using (Pred)
2929

3030
open import Algebra.Consequences.Base public
3131

32+
------------------------------------------------------------------------
33+
-- MiddleFourExchange
34+
35+
module _ {_•_ : Op₂ A} (cong : Congruent₂ _•_) where
36+
37+
comm+assoc⇒middleFour : Commutative _•_ Associative _•_
38+
_•_ MiddleFourExchange _•_
39+
comm+assoc⇒middleFour comm assoc w x y z = begin
40+
(w • x) • (y • z) ≈⟨ assoc w x (y • z) ⟩
41+
w • (x • (y • z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
42+
w • ((x • y) • z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
43+
w • ((y • x) • z) ≈⟨ cong refl (assoc y x z) ⟩
44+
w • (y • (x • z)) ≈⟨ sym (assoc w y (x • z)) ⟩
45+
(w • y) • (x • z) ∎
46+
47+
identity+middleFour⇒assoc : {e : A} Identity e _•_
48+
_•_ MiddleFourExchange _•_
49+
Associative _•_
50+
identity+middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
51+
(x • y) • z ≈⟨ cong refl (sym (identityˡ z)) ⟩
52+
(x • y) • (e • z) ≈⟨ middleFour x y e z ⟩
53+
(x • e) • (y • z) ≈⟨ cong (identityʳ x) refl ⟩
54+
x • (y • z) ∎
55+
56+
identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} Identity e _+_
57+
_•_ MiddleFourExchange _+_
58+
Commutative _•_
59+
identity+middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
60+
= begin
61+
x • y ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
62+
(e + x) • (y + e) ≈⟨ middleFour e x y e ⟩
63+
(e + y) • (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
64+
y • x ∎
65+
3266
------------------------------------------------------------------------
3367
-- Involutive/SelfInverse functions
3468

src/Algebra/Definitions.agda

+4
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,10 @@ _*_ DistributesOverʳ _+_ =
108108
_DistributesOver_ : Op₂ A Op₂ A Set _
109109
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
110110

111+
_MiddleFourExchange_ : Op₂ A Op₂ A Set _
112+
_*_ MiddleFourExchange _+_ =
113+
w x y z ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
114+
111115
_IdempotentOn_ : Op₂ A A Set _
112116
_∙_ IdempotentOn x = (x ∙ x) ≈ x
113117

0 commit comments

Comments
 (0)