@@ -13,55 +13,66 @@ open import Relation.Binary.Definitions
1313
1414module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
1515
16- open Setoid S renaming (Carrier to A)
16+ import Algebra.Consequences.Base as Base
1717open import Algebra.Core
18- open import Algebra.Definitions _≈_
1918open import Data.Sum.Base using (inj₁; inj₂)
2019open import Data.Product.Base using (_,_)
2120open import Function.Base using (_$_; id; _∘_)
2221open import Function.Definitions
2322import Relation.Binary.Consequences as Bin
2423open import Relation.Binary.Core using (Rel)
25- open import Relation.Binary.Reasoning.Setoid S
2624open import Relation.Unary using (Pred)
2725
26+ open Setoid S renaming (Carrier to A)
27+ open import Algebra.Definitions _≈_
28+ open import Relation.Binary.Reasoning.Setoid S
29+
2830------------------------------------------------------------------------
2931-- Re-exports
3032
3133-- Export base lemmas that don't require the setoid
3234
33- open import Algebra.Consequences.Base public
35+ open Base public
36+ hiding (module Congruence )
37+
38+ -- Export congruence lemmas using reflexivity
39+
40+ module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
41+
42+ open Base.Congruence _≈_ cong refl public
3443
3544------------------------------------------------------------------------
3645-- MiddleFourExchange
3746
3847module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
3948
49+ open Congruence cong
50+
4051 comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
4152 _∙_ MiddleFourExchange _∙_
4253 comm∧assoc⇒middleFour comm assoc w x y z = begin
4354 (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
44- w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym ( assoc x y z)) ⟩
45- w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl ) ⟩
46- w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
47- w ∙ (y ∙ (x ∙ z)) ≈⟨ sym ( assoc w y (x ∙ z)) ⟩
55+ w ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ ( assoc x y z) ⟨
56+ w ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
57+ w ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
58+ w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
4859 (w ∙ y) ∙ (x ∙ z) ∎
4960
5061 identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
5162 _∙_ MiddleFourExchange _∙_ →
5263 Associative _∙_
5364 identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
54- (x ∙ y) ∙ z ≈⟨ cong refl (sym ( identityˡ z)) ⟩
65+ (x ∙ y) ∙ z ≈⟨ ∙-congˡ ( identityˡ z) ⟨
5566 (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
56- (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
67+ (x ∙ e) ∙ (y ∙ z) ≈⟨ ∙-congʳ (identityʳ x) ⟩
5768 x ∙ (y ∙ z) ∎
5869
5970 identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
6071 _∙_ MiddleFourExchange _+_ →
6172 Commutative _∙_
6273 identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
6374 = begin
64- x ∙ y ≈⟨ sym ( cong (identityˡ x) (identityʳ y)) ⟩
75+ x ∙ y ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
6576 (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
6677 (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
6778 y ∙ x ∎
@@ -198,25 +209,27 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
198209
199210module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
200211
212+ open Congruence cong
213+
201214 assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ →
202215 Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
203216 ∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
204217 assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
205- x ≈⟨ sym ( idʳ x) ⟩
206- x ∙ e ≈⟨ cong refl (sym ( invʳ y)) ⟩
207- x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym ( assoc x y (y ⁻¹)) ⟩
208- (x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩
218+ x ≈⟨ idʳ x ⟨
219+ x ∙ e ≈⟨ ∙-congˡ ( invʳ y) ⟨
220+ x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
221+ (x ∙ y) ∙ (y ⁻¹) ≈⟨ ∙-congʳ eq ⟩
209222 e ∙ (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩
210223 y ⁻¹ ∎
211224
212225 assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ →
213226 Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
214227 ∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
215228 assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
216- y ≈⟨ sym ( idˡ y) ⟩
217- e ∙ y ≈⟨ cong (sym ( invˡ x)) refl ⟩
229+ y ≈⟨ idˡ y ⟨
230+ e ∙ y ≈⟨ ∙-congʳ ( invˡ x) ⟨
218231 ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
219- (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
232+ (x ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
220233 (x ⁻¹) ∙ e ≈⟨ idʳ (x ⁻¹) ⟩
221234 x ⁻¹ ∎
222235
@@ -228,6 +241,8 @@ module _ {_∙_ _◦_ : Op₂ A}
228241 (∙-comm : Commutative _∙_)
229242 where
230243
244+ open Congruence ◦-cong renaming (∙-congˡ to ◦-congˡ)
245+
231246 comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
232247 comm∧distrˡ⇒distrʳ distrˡ x y z = begin
233248 (y ◦ z) ∙ x ≈⟨ ∙-comm (y ◦ z) x ⟩
@@ -250,7 +265,7 @@ module _ {_∙_ _◦_ : Op₂ A}
250265
251266 comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z)))
252267 comm⇒sym[distribˡ] x {y} {z} prf = begin
253- x ◦ (z ∙ y) ≈⟨ ◦-cong refl (∙-comm z y) ⟩
268+ x ◦ (z ∙ y) ≈⟨ ◦-congˡ (∙-comm z y) ⟩
254269 x ◦ (y ∙ z) ≈⟨ prf ⟩
255270 (x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩
256271 (x ◦ z) ∙ (x ◦ y) ∎
@@ -262,16 +277,18 @@ module _ {_∙_ _◦_ : Op₂ A}
262277 (◦-comm : Commutative _◦_)
263278 where
264279
280+ open Congruence ∙-cong
281+
265282 distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ →
266283 _◦_ Absorbs _∙_ →
267284 _◦_ DistributesOver _∙_ →
268285 _∙_ DistributesOverˡ _◦_
269286 distrib∧absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin
270- x ∙ (y ◦ z) ≈⟨ ∙-cong (∙-absorbs-◦ _ _) refl ⟨
271- (x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-cong (∙-cong refl (◦-comm _ _)) refl ⟩
287+ x ∙ (y ◦ z) ≈⟨ ∙-congʳ (∙-absorbs-◦ _ _) ⟨
288+ (x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-congʳ (∙-congˡ (◦-comm _ _)) ⟩
272289 (x ∙ (y ◦ x)) ∙ (y ◦ z) ≈⟨ ∙-assoc _ _ _ ⟩
273- x ∙ ((y ◦ x) ∙ (y ◦ z)) ≈⟨ ∙-cong refl (◦-distribˡ-∙ _ _ _) ⟨
274- x ∙ (y ◦ (x ∙ z)) ≈⟨ ∙-cong (◦-absorbs-∙ _ _) refl ⟨
290+ x ∙ ((y ◦ x) ∙ (y ◦ z)) ≈⟨ ∙-congˡ (◦-distribˡ-∙ _ _ _) ⟨
291+ x ∙ (y ◦ (x ∙ z)) ≈⟨ ∙-congʳ (◦-absorbs-∙ _ _) ⟨
275292 (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z)) ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
276293 (x ∙ y) ◦ (x ∙ z) ∎
277294
@@ -284,27 +301,31 @@ module _ {_+_ _*_ : Op₂ A}
284301 (*-cong : Congruent₂ _*_)
285302 where
286303
304+ open Congruence +-cong renaming (∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ)
305+
306+ open Congruence *-cong renaming (∙-congˡ to *-congˡ; ∙-congʳ to *-congʳ)
307+
287308 assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
288309 RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
289310 LeftZero 0# _*_
290311 assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin
291- 0# * x ≈⟨ sym ( idʳ _) ⟩
292- (0# * x) + 0# ≈⟨ +-cong refl (sym ( invʳ _)) ⟩
293- (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym ( +-assoc _ _ _) ⟩
294- ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym ( distribʳ _ _ _)) refl ⟩
295- ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
312+ 0# * x ≈⟨ idʳ _ ⟨
313+ (0# * x) + 0# ≈⟨ +-congˡ ( invʳ _) ⟨
314+ (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨
315+ ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-congʳ ( distribʳ _ _ _) ⟨
316+ ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-congʳ (*-congʳ (idʳ _)) ⟩
296317 (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩
297318 0# ∎
298319
299320 assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
300321 RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
301322 RightZero 0# _*_
302323 assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin
303- x * 0# ≈⟨ sym ( idʳ _) ⟩
304- (x * 0#) + 0# ≈⟨ +-cong refl (sym ( invʳ _)) ⟩
305- (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym ( +-assoc _ _ _) ⟩
306- ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym ( distribˡ _ _ _)) refl ⟩
307- (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
324+ x * 0# ≈⟨ idʳ _ ⟨
325+ (x * 0#) + 0# ≈⟨ +-congˡ ( invʳ _) ⟨
326+ (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨
327+ ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-congʳ ( distribˡ _ _ _) ⟨
328+ (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-congʳ (*-congˡ (idʳ _)) ⟩
308329 ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩
309330 0# ∎
310331
0 commit comments