Skip to content

Commit 505cc14

Browse files
MatthewDaggittMatthewDaggitt
committed
Reversed left and right congruency definitions
1 parent 20cef93 commit 505cc14

13 files changed

+97
-99
lines changed

‎CHANGELOG.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -636,8 +636,8 @@ Other minor additions
636636
RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
637637
Conical e ∙ = LeftConical e ∙ × RightConical e ∙
638638
639-
LeftCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
640-
RightCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
639+
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
640+
RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
641641
```
642642

643643
* Added new proof to `Algebra.FunctionProperties.Consequences`:

‎src/Algebra/FunctionProperties.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ Congruent₂ : Op₂ A → Set _
115115
Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
116116

117117
LeftCongruent : Op₂ A → Set _
118-
LeftCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
118+
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
119119

120120
RightCongruent : Op₂ A → Set _
121-
RightCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
121+
RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_

‎src/Algebra/Properties/AbelianGroup.agda

+5-7
Original file line numberDiff line numberDiff line change
@@ -27,26 +27,24 @@ private
2727

2828
lemma₁ : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
2929
lemma₁ x y = begin
30-
x ∙ y ∙ x ⁻¹ ≈⟨ ∙-congˡ $ comm _ _ ⟩
30+
x ∙ y ∙ x ⁻¹ ≈⟨ ∙-congʳ $ comm _ _ ⟩
3131
y ∙ x ∙ x ⁻¹ ≈⟨ assoc _ _ _ ⟩
32-
y ∙ (x ∙ x ⁻¹) ≈⟨ ∙-congʳ $ inverseʳ _ ⟩
32+
y ∙ (x ∙ x ⁻¹) ≈⟨ ∙-congˡ $ inverseʳ _ ⟩
3333
y ∙ ε ≈⟨ identityʳ _ ⟩
3434
y ∎
3535

3636
lemma₂ : ∀ x y → x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ≈ y ⁻¹
3737
lemma₂ x y = begin
3838
x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ≈˘⟨ assoc _ _ _ ⟩
39-
x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹ ≈˘⟨ ∙-congˡ $ assoc _ _ _ ⟩
40-
x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-congˡ $ inverseʳ _ ⟩
39+
x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹ ≈˘⟨ ∙-congʳ $ assoc _ _ _ ⟩
40+
x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹ ≈⟨ ∙-congʳ $ inverseʳ _ ⟩
4141
ε ∙ y ⁻¹ ≈⟨ identityˡ _ ⟩
4242
y ⁻¹ ∎
4343

4444
⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
4545
⁻¹-∙-comm x y = begin
4646
x ⁻¹ ∙ y ⁻¹ ≈⟨ comm _ _ ⟩
47-
y ⁻¹ ∙ x ⁻¹ ≈˘⟨ ∙-congˡ $ lemma₂ x y ⟩
47+
y ⁻¹ ∙ x ⁻¹ ≈˘⟨ ∙-congʳ $ lemma₂ x y ⟩
4848
x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹ ≈⟨ lemma₁ _ _ ⟩
4949
y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹ ≈⟨ lemma₁ _ _ ⟩
5050
(x ∙ y) ⁻¹ ∎
51-
where
52-

‎src/Algebra/Properties/BooleanAlgebra.agda

+40-40
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ open import Data.Product using (_,_)
6868

6969
∧-identityʳ : RightIdentity ⊤ _∧_
7070
∧-identityʳ x = begin
71-
x ∧ ⊤ ≈⟨ ∧-congʳ (sym (∨-complementʳ _)) ⟩
71+
x ∧ ⊤ ≈⟨ ∧-congˡ (sym (∨-complementʳ _)) ⟩
7272
x ∧ (x ∨ ¬ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩
7373
x ∎
7474

@@ -80,7 +80,7 @@ open import Data.Product using (_,_)
8080

8181
∨-identityʳ : RightIdentity ⊥ _∨_
8282
∨-identityʳ x = begin
83-
x ∨ ⊥ ≈⟨ ∨-congʳ $ sym (∧-complementʳ _) ⟩
83+
x ∨ ⊥ ≈⟨ ∨-congˡ $ sym (∧-complementʳ _) ⟩
8484
x ∨ x ∧ ¬ x ≈⟨ ∨-absorbs-∧ _ _ ⟩
8585
x ∎
8686

@@ -92,9 +92,9 @@ open import Data.Product using (_,_)
9292

9393
∧-zeroʳ : RightZero ⊥ _∧_
9494
∧-zeroʳ x = begin
95-
x ∧ ⊥ ≈⟨ ∧-congʳ $ sym (∧-complementʳ _) ⟩
95+
x ∧ ⊥ ≈⟨ ∧-congˡ $ sym (∧-complementʳ _) ⟩
9696
x ∧ x ∧ ¬ x ≈˘⟨ ∧-assoc _ _ _ ⟩
97-
(x ∧ x) ∧ ¬ x ≈⟨ ∧-congˡ $ ∧-idempotent _ ⟩
97+
(x ∧ x) ∧ ¬ x ≈⟨ ∧-congʳ $ ∧-idempotent _ ⟩
9898
x ∧ ¬ x ≈⟨ ∧-complementʳ _ ⟩
9999
⊥ ∎
100100

@@ -106,9 +106,9 @@ open import Data.Product using (_,_)
106106

107107
∨-zeroʳ : ∀ x → x ∨ ⊤ ≈ ⊤
108108
∨-zeroʳ x = begin
109-
x ∨ ⊤ ≈⟨ ∨-congʳ $ sym (∨-complementʳ _) ⟩
109+
x ∨ ⊤ ≈⟨ ∨-congˡ $ sym (∨-complementʳ _) ⟩
110110
x ∨ x ∨ ¬ x ≈˘⟨ ∨-assoc _ _ _ ⟩
111-
(x ∨ x) ∨ ¬ x ≈⟨ ∨-congˡ $ ∨-idempotent _ ⟩
111+
(x ∨ x) ∨ ¬ x ≈⟨ ∨-congʳ $ ∨-idempotent _ ⟩
112112
x ∨ ¬ x ≈⟨ ∨-complementʳ _ ⟩
113113
⊤ ∎
114114

@@ -213,12 +213,12 @@ private
213213
lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y
214214
lemma x y x∧y=⊥ x∨y=⊤ = begin
215215
¬ x ≈˘⟨ ∧-identityʳ _ ⟩
216-
¬ x ∧ ⊤ ≈˘⟨ ∧-congʳ x∨y=⊤ ⟩
216+
¬ x ∧ ⊤ ≈˘⟨ ∧-congˡ x∨y=⊤ ⟩
217217
¬ x ∧ (x ∨ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
218-
¬ x ∧ x ∨ ¬ x ∧ y ≈⟨ ∨-congˡ $ ∧-complementˡ _ ⟩
219-
⊥ ∨ ¬ x ∧ y ≈˘⟨ ∨-congˡ x∧y=⊥ ⟩
218+
¬ x ∧ x ∨ ¬ x ∧ y ≈⟨ ∨-congʳ $ ∧-complementˡ _ ⟩
219+
⊥ ∨ ¬ x ∧ y ≈˘⟨ ∨-congʳ x∧y=⊥ ⟩
220220
x ∧ y ∨ ¬ x ∧ y ≈˘⟨ ∧-∨-distribʳ _ _ _ ⟩
221-
(x ∨ ¬ x) ∧ y ≈⟨ ∧-congˡ $ ∨-complementʳ _ ⟩
221+
(x ∨ ¬ x) ∧ y ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩
222222
⊤ ∧ y ≈⟨ ∧-identityˡ _ ⟩
223223
y ∎
224224

@@ -236,26 +236,26 @@ deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
236236
where
237237
lem₁ = begin
238238
(x ∧ y) ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
239-
(x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∨-congˡ $ ∧-congˡ $ ∧-comm _ _ ⟩
239+
(x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∨-congʳ $ ∧-congʳ $ ∧-comm _ _ ⟩
240240
(y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩
241-
y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y) ≈⟨ (∧-congʳ $ ∧-complementʳ _) ⟨ ∨-cong ⟩
242-
(∧-congʳ $ ∧-complementʳ _) ⟩
241+
y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y) ≈⟨ (∧-congˡ $ ∧-complementʳ _) ⟨ ∨-cong ⟩
242+
(∧-congˡ $ ∧-complementʳ _) ⟩
243243
(y ∧ ⊥) ∨ (x ∧ ⊥) ≈⟨ ∧-zeroʳ _ ⟨ ∨-cong ⟩ ∧-zeroʳ _ ⟩
244244
⊥ ∨ ⊥ ≈⟨ ∨-identityʳ _ ⟩
245245
⊥ ∎
246246

247247
lem₃ = begin
248248
(x ∧ y) ∨ ¬ x ≈⟨ ∨-∧-distribʳ _ _ _ ⟩
249-
(x ∨ ¬ x) ∧ (y ∨ ¬ x) ≈⟨ ∧-congˡ $ ∨-complementʳ _ ⟩
249+
(x ∨ ¬ x) ∧ (y ∨ ¬ x) ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩
250250
⊤ ∧ (y ∨ ¬ x) ≈⟨ ∧-identityˡ _ ⟩
251251
y ∨ ¬ x ≈⟨ ∨-comm _ _ ⟩
252252
¬ x ∨ y ∎
253253

254254
lem₂ = begin
255255
(x ∧ y) ∨ (¬ x ∨ ¬ y) ≈˘⟨ ∨-assoc _ _ _ ⟩
256-
((x ∧ y) ∨ ¬ x) ∨ ¬ y ≈⟨ ∨-congˡ lem₃ ⟩
256+
((x ∧ y) ∨ ¬ x) ∨ ¬ y ≈⟨ ∨-congʳ lem₃ ⟩
257257
(¬ x ∨ y) ∨ ¬ y ≈⟨ ∨-assoc _ _ _ ⟩
258-
¬ x ∨ (y ∨ ¬ y) ≈⟨ ∨-congʳ $ ∨-complementʳ _ ⟩
258+
¬ x ∨ (y ∨ ¬ y) ≈⟨ ∨-congˡ $ ∨-complementʳ _ ⟩
259259
¬ x ∨ ⊤ ≈⟨ ∨-zeroʳ _ ⟩
260260
⊤ ∎
261261

@@ -325,19 +325,19 @@ module XorRing
325325
⊕-¬-distribˡ x y = begin
326326
¬ (x ⊕ y) ≈⟨ ¬-cong $ ⊕-def _ _ ⟩
327327
¬ ((x ∨ y) ∧ (¬ (x ∧ y))) ≈⟨ ¬-cong (∧-∨-distribʳ _ _ _) ⟩
328-
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y))) ≈⟨ ¬-cong $ ∨-congʳ $ ∧-congʳ $ ¬-cong (∧-comm _ _) ⟩
328+
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y))) ≈⟨ ¬-cong $ ∨-congˡ $ ∧-congˡ $ ¬-cong (∧-comm _ _) ⟩
329329
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x))) ≈⟨ ¬-cong $ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩
330330
¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x)) ≈⟨ deMorgan₂ _ _ ⟩
331-
¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩
332-
(¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x) ≈⟨ helper (∨-congʳ $ ¬-involutive _) (∧-comm _ _) ⟩
331+
¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x) ≈⟨ ∧-congʳ $ deMorgan₁ _ _ ⟩
332+
(¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x) ≈⟨ helper (∨-congˡ $ ¬-involutive _) (∧-comm _ _) ⟩
333333
(¬ x ∨ y) ∧ ¬ (¬ x ∧ y) ≈˘⟨ ⊕-def _ _ ⟩
334334
¬ x ⊕ y ∎
335335
where
336336
lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
337337
lem x y = begin
338-
x ∧ ¬ (x ∧ y) ≈⟨ ∧-congʳ $ deMorgan₁ _ _ ⟩
338+
x ∧ ¬ (x ∧ y) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩
339339
x ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
340-
(x ∧ ¬ x) ∨ (x ∧ ¬ y) ≈⟨ ∨-congˡ $ ∧-complementʳ _ ⟩
340+
(x ∧ ¬ x) ∨ (x ∧ ¬ y) ≈⟨ ∨-congʳ $ ∧-complementʳ _ ⟩
341341
⊥ ∨ (x ∧ ¬ y) ≈⟨ ∨-identityˡ _ ⟩
342342
x ∧ ¬ y ∎
343343

@@ -359,7 +359,7 @@ module XorRing
359359
⊕-identityˡ x = begin
360360
⊥ ⊕ x ≈⟨ ⊕-def _ _ ⟩
361361
(⊥ ∨ x) ∧ ¬ (⊥ ∧ x) ≈⟨ helper (∨-identityˡ _) (∧-zeroˡ _) ⟩
362-
x ∧ ¬ ⊥ ≈⟨ ∧-congʳ ¬⊥=⊤ ⟩
362+
x ∧ ¬ ⊥ ≈⟨ ∧-congˡ ¬⊥=⊤ ⟩
363363
x ∧ ⊤ ≈⟨ ∧-identityʳ _ ⟩
364364
x ∎
365365

@@ -384,45 +384,45 @@ module XorRing
384384

385385
∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_
386386
∧-distribˡ-⊕ x y z = begin
387-
x ∧ (y ⊕ z) ≈⟨ ∧-congʳ $ ⊕-def _ _ ⟩
387+
x ∧ (y ⊕ z) ≈⟨ ∧-congˡ $ ⊕-def _ _ ⟩
388388
x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩
389-
(x ∧ (y ∨ z)) ∧ ¬ (y ∧ z) ≈⟨ ∧-congʳ $ deMorgan₁ _ _ ⟩
389+
(x ∧ (y ∨ z)) ∧ ¬ (y ∧ z) ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩
390390
(x ∧ (y ∨ z)) ∧
391391
(¬ y ∨ ¬ z) ≈˘⟨ ∨-identityˡ _ ⟩
392392
⊥ ∨
393393
((x ∧ (y ∨ z)) ∧
394-
(¬ y ∨ ¬ z)) ≈⟨ ∨-congˡ lem₃ ⟩
394+
(¬ y ∨ ¬ z)) ≈⟨ ∨-congʳ lem₃ ⟩
395395
((x ∧ (y ∨ z)) ∧ ¬ x) ∨
396396
((x ∧ (y ∨ z)) ∧
397397
(¬ y ∨ ¬ z)) ≈˘⟨ ∧-∨-distribˡ _ _ _ ⟩
398398
(x ∧ (y ∨ z)) ∧
399-
(¬ x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∧-congʳ $ ∨-congʳ (deMorgan₁ _ _) ⟩
399+
(¬ x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∧-congˡ $ ∨-congˡ (deMorgan₁ _ _) ⟩
400400
(x ∧ (y ∨ z)) ∧
401-
(¬ x ∨ ¬ (y ∧ z)) ≈˘⟨ ∧-congʳ (deMorgan₁ _ _) ⟩
401+
(¬ x ∨ ¬ (y ∧ z)) ≈˘⟨ ∧-congˡ (deMorgan₁ _ _) ⟩
402402
(x ∧ (y ∨ z)) ∧
403403
¬ (x ∧ (y ∧ z)) ≈⟨ helper refl lem₁ ⟩
404404
(x ∧ (y ∨ z)) ∧
405-
¬ ((x ∧ y) ∧ (x ∧ z)) ≈⟨ ∧-congˡ $ ∧-∨-distribˡ _ _ _ ⟩
405+
¬ ((x ∧ y) ∧ (x ∧ z)) ≈⟨ ∧-congʳ $ ∧-∨-distribˡ _ _ _ ⟩
406406
((x ∧ y) ∨ (x ∧ z)) ∧
407407
¬ ((x ∧ y) ∧ (x ∧ z)) ≈˘⟨ ⊕-def _ _ ⟩
408408
(x ∧ y) ⊕ (x ∧ z) ∎
409409
where
410410
lem₂ = begin
411411
x ∧ (y ∧ z) ≈˘⟨ ∧-assoc _ _ _ ⟩
412-
(x ∧ y) ∧ z ≈⟨ ∧-congˡ $ ∧-comm _ _ ⟩
412+
(x ∧ y) ∧ z ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩
413413
(y ∧ x) ∧ z ≈⟨ ∧-assoc _ _ _ ⟩
414414
y ∧ (x ∧ z) ∎
415415

416416
lem₁ = begin
417-
x ∧ (y ∧ z) ≈˘⟨ ∧-congˡ (∧-idempotent _) ⟩
417+
x ∧ (y ∧ z) ≈˘⟨ ∧-congʳ (∧-idempotent _) ⟩
418418
(x ∧ x) ∧ (y ∧ z) ≈⟨ ∧-assoc _ _ _ ⟩
419-
x ∧ (x ∧ (y ∧ z)) ≈⟨ ∧-congʳ lem₂ ⟩
419+
x ∧ (x ∧ (y ∧ z)) ≈⟨ ∧-congˡ lem₂ ⟩
420420
x ∧ (y ∧ (x ∧ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩
421421
(x ∧ y) ∧ (x ∧ z) ∎
422422

423423
lem₃ = begin
424424
⊥ ≈˘⟨ ∧-zeroʳ _ ⟩
425-
(y ∨ z) ∧ ⊥ ≈˘⟨ ∧-congʳ (∧-complementʳ _) ⟩
425+
(y ∨ z) ∧ ⊥ ≈˘⟨ ∧-congˡ (∧-complementʳ _) ⟩
426426
(y ∨ z) ∧ (x ∧ ¬ x) ≈˘⟨ ∧-assoc _ _ _ ⟩
427427
((y ∨ z) ∧ x) ∧ ¬ x ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩
428428
(x ∧ (y ∨ z)) ∧ ¬ x ∎
@@ -457,7 +457,7 @@ module XorRing
457457
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ ∧-assoc _ _ _ ⟩
458458
((x ∨ y) ∨ z) ∧
459459
(((x ∨ ¬ y) ∨ ¬ z) ∧
460-
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈⟨ ∧-congʳ lem₅ ⟩
460+
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈⟨ ∧-congˡ lem₅ ⟩
461461
((x ∨ y) ∨ z) ∧
462462
(((¬ x ∨ ¬ y) ∨ z) ∧
463463
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈˘⟨ ∧-assoc _ _ _ ⟩
@@ -470,14 +470,14 @@ module XorRing
470470
where
471471
lem₁ = begin
472472
((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z) ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩
473-
((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z ≈˘⟨ ∨-congˡ $ ∧-congʳ (deMorgan₁ _ _) ⟩
473+
((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z ≈˘⟨ ∨-congʳ $ ∧-congˡ (deMorgan₁ _ _) ⟩
474474
((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z ∎
475475

476476
lem₂' = begin
477477
(x ∨ ¬ y) ∧ (¬ x ∨ y) ≈˘⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
478478
(⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤) ≈˘⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
479479
⟨ ∧-cong ⟩
480-
(∧-congʳ $ ∨-complementˡ _) ⟩
480+
(∧-congˡ $ ∨-complementˡ _) ⟩
481481
((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧
482482
((¬ x ∨ y) ∧ (¬ y ∨ y)) ≈˘⟨ lemma₂ _ _ _ _ ⟩
483483
(¬ x ∧ ¬ y) ∨ (x ∧ y) ≈˘⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
@@ -486,12 +486,12 @@ module XorRing
486486

487487
lem₂ = begin
488488
((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z) ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩
489-
((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z ≈⟨ ∨-congˡ lem₂' ⟩
489+
((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z ≈⟨ ∨-congʳ lem₂' ⟩
490490
¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z ≈˘⟨ deMorgan₁ _ _ ⟩
491491
¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ∎
492492

493493
lem₃ = begin
494-
x ∨ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congʳ $ ∧-congʳ $ deMorgan₁ _ _ ⟩
494+
x ∨ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congˡ $ ∧-congˡ $ deMorgan₁ _ _ ⟩
495495
x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z)) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
496496
(x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z)) ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
497497
((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z) ∎
@@ -503,14 +503,14 @@ module XorRing
503503
((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧
504504
((¬ y ∨ z) ∧ (¬ z ∨ z)) ≈⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
505505
⟨ ∧-cong ⟩
506-
(∧-congʳ $ ∨-complementˡ _) ⟩
506+
(∧-congˡ $ ∨-complementˡ _) ⟩
507507
(⊤ ∧ (y ∨ ¬ z)) ∧
508508
((¬ y ∨ z) ∧ ⊤) ≈⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
509509
(y ∨ ¬ z) ∧ (¬ y ∨ z) ∎
510510

511511
lem₄ = begin
512512
¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ deMorgan₁ _ _ ⟩
513-
¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congʳ lem₄' ⟩
513+
¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∨-congˡ lem₄' ⟩
514514
¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z)) ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
515515
(¬ x ∨ (y ∨ ¬ z)) ∧
516516
(¬ x ∨ (¬ y ∨ z)) ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
@@ -523,7 +523,7 @@ module XorRing
523523
((x ∨ ¬ y) ∨ ¬ z) ∧
524524
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈˘⟨ ∧-assoc _ _ _ ⟩
525525
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
526-
((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-congˡ $ ∧-comm _ _ ⟩
526+
((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩
527527
(((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
528528
((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-assoc _ _ _ ⟩
529529
((¬ x ∨ ¬ y) ∨ z) ∧

0 commit comments

Comments
 (0)