Skip to content

Commit

Permalink
'congR' and 'congL' (#1064)
Browse files Browse the repository at this point in the history 
* 'congL' and 'congR'

'congR' can replace 'cong' applied to a curried function.
'congL' can replace 'cong' applied to a function whose second argument
    is fixed.

Useful for shortening lines expressing equality chains (_≡⟨_⟩≡_).

* Replaced 'cong' with 'congL' or 'congR' to make lines shorter

There are plenty more places 'congL' and 'congR' can be used to shorten
lines.
  • Loading branch information
@jhimes2
jhimes2 authored Nov 2, 2023
1 parent 2e45d12 commit a847f25
Show file tree
Hide file tree
Showing 6 changed files with 74 additions and 76 deletions.
40 changes: 20 additions & 20 deletions Cubical/Algebra/CommRing/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,10 +43,10 @@ module Units (R' : CommRing ℓ) where
where
path : r' ≡ r''
path = r' ≡⟨ sym (·IdR _) ⟩
r' · 1r ≡⟨ cong (r' ·_) (sym rr''≡1) ⟩
r' · 1r ≡⟨ congR _·_ (sym rr''≡1) ⟩
r' · (r · r'') ≡⟨ ·Assoc _ _ _ ⟩
(r' · r) · r'' ≡⟨ cong (_· r'') (·Comm _ _) ⟩
(r · r') · r'' ≡⟨ cong (_· r'') rr'≡1 ⟩
(r' · r) · r'' ≡⟨ congL _·_ (·Comm _ _) ⟩
(r · r') · r'' ≡⟨ congL _·_ rr'≡1 ⟩
1r · r'' ≡⟨ ·IdL _ ⟩
r'' ∎

Expand All @@ -73,11 +73,11 @@ module Units (R' : CommRing ℓ) where
RˣMultClosed r r' = (r ⁻¹ · r' ⁻¹) , path
where
path : r · r' · (r ⁻¹ · r' ⁻¹) ≡ 1r
path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ cong (_· (r ⁻¹ · r' ⁻¹)) (·Comm _ _) ⟩
path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ congL _·_ (·Comm _ _) ⟩
r' · r · (r ⁻¹ · r' ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
r' · r · r ⁻¹ · r' ⁻¹ ≡⟨ cong (_· r' ⁻¹) (sym (·Assoc _ _ _)) ⟩
r' · r · r ⁻¹ · r' ⁻¹ ≡⟨ congL _·_ (sym (·Assoc _ _ _)) ⟩
r' · (r · r ⁻¹) · r' ⁻¹ ≡⟨ cong (λ x → r' · x · r' ⁻¹) (·-rinv _) ⟩
r' · 1r · r' ⁻¹ ≡⟨ cong (_· r' ⁻¹) (·IdR _) ⟩
r' · 1r · r' ⁻¹ ≡⟨ congL _·_ (·IdR _) ⟩
r' · r' ⁻¹ ≡⟨ ·-rinv _ ⟩
1r ∎

Expand All @@ -99,9 +99,9 @@ module Units (R' : CommRing ℓ) where
UnitsAreNotZeroDivisors : (r : R) ⦃ _ : r ∈ Rˣ ⦄
→ ∀ r' → r' · r ≡ 0r → r' ≡ 0r
UnitsAreNotZeroDivisors r r' p = r' ≡⟨ sym (·IdR _) ⟩
r' · 1r ≡⟨ cong (r' ·_) (sym (·-rinv _)) ⟩
r' · 1r ≡⟨ congR _·_ (sym (·-rinv _)) ⟩
r' · (r · r ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
r' · r · r ⁻¹ ≡⟨ cong (_· r ⁻¹) p ⟩
r' · r · r ⁻¹ ≡⟨ congL _·_ p ⟩
0r · r ⁻¹ ≡⟨ 0LeftAnnihilates _ ⟩
0r ∎

Expand Down Expand Up @@ -139,9 +139,9 @@ module Units (R' : CommRing ℓ) where
PathPΣ (inverseUniqueness r' (r ⁻¹ , subst (λ x → x · r ⁻¹ ≡ 1r) p (r∈Rˣ .snd)) r'∈Rˣ) .fst

⁻¹-eq-elim : {r r' r'' : R} ⦃ r∈Rˣ : r ∈ Rˣ ⦄ → r' ≡ r'' · r → r' · r ⁻¹ ≡ r''
⁻¹-eq-elim {r = r} {r'' = r''} p = cong (_· r ⁻¹) p
⁻¹-eq-elim {r = r} {r'' = r''} p = congL _·_ p
∙ sym (·Assoc _ _ _)
∙ cong (r'' ·_) (·-rinv _)
∙ congR _·_ (·-rinv _)
∙ ·IdR _


Expand Down Expand Up @@ -220,11 +220,11 @@ module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
→ f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
f (r ⁻¹ᵃ) ≡⟨ sym (·B-rid _) ⟩
f (r ⁻¹ᵃ) ·B 1b ≡⟨ cong (f (r ⁻¹ᵃ) ·B_) (sym (·B-rinv _)) ⟩
f (r ⁻¹ᵃ) ·B 1b ≡⟨ congR _·B_ (sym (·B-rinv _)) ⟩
f (r ⁻¹ᵃ) ·B ((f r) ·B (f r) ⁻¹ᵇ) ≡⟨ ·B-assoc _ _ _ ⟩
f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ ≡⟨ cong (_·B (f r) ⁻¹ᵇ) (sym (pres· _ _)) ⟩
f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ ≡⟨ congL _·B_ (sym (pres· _ _)) ⟩
f (r ⁻¹ᵃ ·A r) ·B (f r) ⁻¹ᵇ ≡⟨ cong (λ x → f x ·B (f r) ⁻¹ᵇ) (·A-linv _) ⟩
f 1a ·B (f r) ⁻¹ᵇ ≡⟨ cong (_·B (f r) ⁻¹ᵇ) (pres1) ⟩
f 1a ·B (f r) ⁻¹ᵇ ≡⟨ congL _·B_ pres1 ⟩
1b ·B (f r) ⁻¹ᵇ ≡⟨ ·B-lid _ ⟩
(f r) ⁻¹ᵇ ∎

Expand All @@ -247,7 +247,7 @@ module Exponentiation (R' : CommRing ℓ) where

·-of-^-is-^-of-+ : (f : R) (m n : ℕ) → (f ^ m) · (f ^ n) ≡ f ^ (m +ℕ n)
·-of-^-is-^-of-+ f zero n = ·IdL _
·-of-^-is-^-of-+ f (suc m) n = sym (·Assoc _ _ _) ∙ cong (f ·_) (·-of-^-is-^-of-+ f m n)
·-of-^-is-^-of-+ f (suc m) n = sym (·Assoc _ _ _) ∙ congR _·_ (·-of-^-is-^-of-+ f m n)

^-ldist-· : (f g : R) (n : ℕ) → (f · g) ^ n ≡ (f ^ n) · (g ^ n)
^-ldist-· f g zero = sym (·IdL 1r)
Expand All @@ -256,9 +256,9 @@ module Exponentiation (R' : CommRing ℓ) where
path : f · g · ((f · g) ^ n) ≡ f · (f ^ n) · (g · (g ^ n))
path = f · g · ((f · g) ^ n) ≡⟨ cong (f · g ·_) (^-ldist-· f g n) ⟩
f · g · ((f ^ n) · (g ^ n)) ≡⟨ ·Assoc _ _ _ ⟩
f · g · (f ^ n) · (g ^ n) ≡⟨ cong (_· (g ^ n)) (sym (·Assoc _ _ _)) ⟩
f · g · (f ^ n) · (g ^ n) ≡⟨ congL _·_ (sym (·Assoc _ _ _)) ⟩
f · (g · (f ^ n)) · (g ^ n) ≡⟨ cong (λ r → (f · r) · (g ^ n)) (·Comm _ _) ⟩
f · ((f ^ n) · g) · (g ^ n) ≡⟨ cong (_· (g ^ n)) (·Assoc _ _ _) ⟩
f · ((f ^ n) · g) · (g ^ n) ≡⟨ congL _·_ (·Assoc _ _ _) ⟩
f · (f ^ n) · g · (g ^ n) ≡⟨ sym (·Assoc _ _ _) ⟩
f · (f ^ n) · (g · (g ^ n)) ∎

Expand All @@ -282,17 +282,17 @@ module CommRingTheory (R' : CommRing ℓ) where
private R = fst R'

·CommAssocl : (x y z : R) → x · (y · z) ≡ y · (x · z)
·CommAssocl x y z = ·Assoc x y z ∙∙ cong (_· z) (·Comm x y) ∙∙ sym (·Assoc y x z)
·CommAssocl x y z = ·Assoc x y z ∙∙ congL _·_ (·Comm x y) ∙∙ sym (·Assoc y x z)

·CommAssocr : (x y z : R) → x · y · z ≡ x · z · y
·CommAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·Comm y z) ∙∙ ·Assoc x z y
·CommAssocr x y z = sym (·Assoc x y z) ∙∙ congR _·_ (·Comm y z) ∙∙ ·Assoc x z y

·CommAssocr2 : (x y z : R) → x · y · z ≡ z · y · x
·CommAssocr2 x y z = ·CommAssocr _ _ _ ∙∙ cong (_· y) (·Comm _ _) ∙∙ ·CommAssocr _ _ _
·CommAssocr2 x y z = ·CommAssocr _ _ _ ∙∙ congL _·_ (·Comm _ _) ∙∙ ·CommAssocr _ _ _

·CommAssocSwap : (x y z w : R) → (x · y) · (z · w) ≡ (x · z) · (y · w)
·CommAssocSwap x y z w =
·Assoc (x · y) z w ∙∙ cong (_· w) (·CommAssocr x y z) ∙∙ sym (·Assoc (x · z) y w)
·Assoc (x · y) z w ∙∙ congL _·_ (·CommAssocr x y z) ∙∙ sym (·Assoc (x · z) y w)



Expand Down
30 changes: 13 additions & 17 deletions Cubical/Algebra/Group/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,15 +32,15 @@ module GroupTheory (G : Group ℓ) where
abstract
·CancelL : (a : ⟨ G ⟩) {b c : ⟨ G ⟩} → a · b ≡ a · c → b ≡ c
·CancelL a {b} {c} p =
b ≡⟨ sym (·IdL b) ∙ cong (_· b) (sym (·InvL a)) ∙ sym (·Assoc _ _ _) ⟩
inv a · (a · b) ≡⟨ cong (inv a ·_) p ⟩
inv a · (a · c) ≡⟨ ·Assoc _ _ _ ∙ cong (_· c) (·InvL a) ∙ ·IdL c ⟩
b ≡⟨ sym (·IdL b) ∙ congL _·_ (sym (·InvL a)) ∙ sym (·Assoc _ _ _) ⟩
inv a · (a · b) ≡⟨ congR _·_ p ⟩
inv a · (a · c) ≡⟨ ·Assoc _ _ _ ∙ congL _·_ (·InvL a) ∙ ·IdL c ⟩
c ∎

·CancelR : {a b : ⟨ G ⟩} (c : ⟨ G ⟩) → a · c ≡ b · c → a ≡ b
·CancelR {a} {b} c p =
a ≡⟨ sym (·IdR a) ∙ cong (a ·_) (sym (·InvR c)) ∙ ·Assoc _ _ _ ⟩
(a · c) · inv c ≡⟨ cong (_· inv c) p ⟩
a ≡⟨ sym (·IdR a) ∙ congR _·_ (sym (·InvR c)) ∙ ·Assoc _ _ _ ⟩
(a · c) · inv c ≡⟨ congL _·_ p ⟩
(b · c) · inv c ≡⟨ sym (·Assoc _ _ _) ∙ cong (b ·_) (·InvR c) ∙ ·IdR b ⟩
b ∎

Expand All @@ -65,22 +65,18 @@ module GroupTheory (G : Group ℓ) where
idFromIdempotency : (x : ⟨ G ⟩) → x ≡ x · x → x ≡ 1g
idFromIdempotency x p =
x ≡⟨ sym (·IdR x) ⟩
x · 1g ≡⟨ cong (λ u → x · u) (sym (·InvR _)) ⟩
x · 1g ≡⟨ congR _·_ (sym (·InvR _)) ⟩
x · (x · inv x) ≡⟨ ·Assoc _ _ _ ⟩
(x · x) · (inv x) ≡⟨ cong (λ u → u · (inv x)) (sym p) ⟩
(x · x) · (inv x) ≡⟨ congL _·_ (sym p) ⟩
x · (inv x) ≡⟨ ·InvR _ ⟩
1g ∎


invDistr : (a b : ⟨ G ⟩) → inv (a · b) ≡ inv b · inv a
invDistr a b = sym (invUniqueR γ) where
γ : (a · b) · (inv b · inv a) ≡ 1g
γ = (a · b) · (inv b · inv a)
≡⟨ sym (·Assoc _ _ _) ⟩
a · b · (inv b) · (inv a)
≡⟨ cong (a ·_) (·Assoc _ _ _ ∙ cong (_· (inv a)) (·InvR b)) ⟩
a · (1g · inv a)
≡⟨ cong (a ·_) (·IdL (inv a)) ∙ ·InvR a ⟩
γ = (a · b) · (inv b · inv a) ≡⟨ sym (·Assoc _ _ _) ⟩
a · b · (inv b) · (inv a) ≡⟨ congR _·_ (·Assoc _ _ _ ∙ congL _·_ (·InvR b)) ⟩
a · (1g · inv a) ≡⟨ congR _·_ (·IdL (inv a)) ∙ ·InvR a ⟩
1g ∎

congIdLeft≡congIdRight : (_·G_ : G → G → G) (-G_ : G → G)
Expand All @@ -89,10 +85,10 @@ congIdLeft≡congIdRight : (_·G_ : G → G → G) (-G_ : G → G)
(lUnitG : (x : G) → 0G ·G x ≡ x)
→ (r≡l : rUnitG 0G ≡ lUnitG 0G)
→ (p : 0G ≡ 0G) →
cong (0G ·G_) p ≡ cong (_·G 0G) p
congR _·G_ p ≡ congL _·G_ p
congIdLeft≡congIdRight _·G_ -G_ 0G rUnitG lUnitG r≡l p =
rUnit (cong (0G ·G_) p)
rUnit (congR _·G_ p)
∙∙ ((λ i → (λ j → lUnitG 0G (i ∧ j)) ∙∙ cong (λ x → lUnitG x i) p ∙∙ λ j → lUnitG 0G (i ∧ ~ j))
∙∙ cong₂ (λ x y → x ∙∙ p ∙∙ y) (sym r≡l) (cong sym (sym r≡l))
∙∙ λ i → (λ j → rUnitG 0G (~ i ∧ j)) ∙∙ cong (λ x → rUnitG x (~ i)) p ∙∙ λ j → rUnitG 0G (~ i ∧ ~ j))
∙∙ sym (rUnit (cong (_·G 0G) p))
∙∙ sym (rUnit (congL _·G_ p))
8 changes: 4 additions & 4 deletions Cubical/Algebra/Module/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,15 @@ module ModuleTheory (R : Ring ℓ') (M : LeftModule R ℓ) where

⋆AnnihilL : (x : ⟨ M ⟩) → R.0r ⋆ x ≡ 0m
⋆AnnihilL x =
let idempotent-+ = R.0r ⋆ x ≡⟨ cong (λ u → u ⋆ x) (sym (RingTheory.0Idempotent R)) ⟩
let idempotent-+ = R.0r ⋆ x ≡⟨ congL _⋆_ (sym (RingTheory.0Idempotent R)) ⟩
(R.0r R.+ R.0r) ⋆ x ≡⟨ ⋆DistL+ R.0r R.0r x ⟩
(R.0r ⋆ x) + (R.0r ⋆ x) ∎
in GroupTheory.idFromIdempotency (LeftModule→Group M) (R.0r ⋆ x) idempotent-+

⋆AnnihilR : (r : ⟨ R ⟩) → r ⋆ 0m ≡ 0m
⋆AnnihilR r = GroupTheory.idFromIdempotency (LeftModule→Group M) (r ⋆ 0m) helper
where helper =
r ⋆ 0m ≡⟨ cong (λ u → r ⋆ u) (sym (+IdL (0m))) ⟩
r ⋆ 0m ≡⟨ congR _⋆_ (sym (+IdL (0m))) ⟩
r ⋆ (0m + 0m) ≡⟨ ⋆DistR+ r 0m 0m ⟩
(r ⋆ 0m) + (r ⋆ 0m) ∎

Expand All @@ -38,8 +38,8 @@ module ModuleTheory (R : Ring ℓ') (M : LeftModule R ℓ) where
minusByMult x =
let open AbGroupTheory (LeftModule→AbGroup M)
in implicitInverse
( x + (R.- R.1r) ⋆ x ≡⟨ cong (_+ (R.- R.1r) ⋆ x) (sym (⋆IdL x)) ⟩
( x + (R.- R.1r) ⋆ x ≡⟨ congL _+_ (sym (⋆IdL x)) ⟩
R.1r ⋆ x + (R.- R.1r) ⋆ x ≡⟨ sym (⋆DistL+ R.1r (R.- R.1r) x) ⟩
(R.1r R.+ (R.- R.1r)) ⋆ x ≡⟨ cong (_⋆ x) (R.+InvR R.1r) ⟩
(R.1r R.+ (R.- R.1r)) ⋆ x ≡⟨ congL _⋆_ (R.+InvR R.1r) ⟩
R.0r ⋆ x ≡⟨ ⋆AnnihilL x ⟩
0m ∎)
4 changes: 2 additions & 2 deletions Cubical/Algebra/Monoid/Base.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,8 +135,8 @@ module MonoidTheory {ℓ} (M : Monoid ℓ) where
inv-lemma : (x y z : ⟨ M ⟩) → y · x ≡ ε → x · z ≡ ε → y ≡ z
inv-lemma x y z left-inverse right-inverse =
y ≡⟨ sym (·IdR y) ⟩
y · ε ≡⟨ cong (λ - → y · -) (sym right-inverse) ⟩
y · ε ≡⟨ congR _·_ (sym right-inverse) ⟩
y · (x · z) ≡⟨ ·Assoc y x z ⟩
(y · x) · z ≡⟨ cong (λ - → - · z) left-inverse ⟩
(y · x) · z ≡⟨ congL _·_ left-inverse ⟩
ε · z ≡⟨ ·IdL z ⟩
z ∎
58 changes: 25 additions & 33 deletions Cubical/Algebra/Ring/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,9 +41,9 @@ module RingTheory (R' : Ring ℓ) where
→ y ≡ - x
implicitInverse x y p =
y ≡⟨ sym (+IdL y) ⟩
0r + y ≡⟨ cong (λ u → u + y) (sym (+InvL x)) ⟩
0r + y ≡⟨ congL _+_ (sym (+InvL x)) ⟩
(- x + x) + y ≡⟨ sym (+Assoc _ _ _) ⟩
(- x) + (x + y) ≡⟨ cong (λ u → (- x) + u) p ⟩
(- x) + (x + y) ≡⟨ congR _+_ p ⟩
(- x) + 0r ≡⟨ +IdR _ ⟩
- x ∎

Expand All @@ -52,9 +52,9 @@ module RingTheory (R' : Ring ℓ) where
→ x ≡ y
equalByDifference x y p =
x ≡⟨ sym (+IdR _) ⟩
x + 0r ≡⟨ cong (λ u → x + u) (sym (+InvL y)) ⟩
x + 0r ≡⟨ congR _+_ (sym (+InvL y)) ⟩
x + ((- y) + y) ≡⟨ +Assoc _ _ _ ⟩
(x - y) + y ≡⟨ cong (λ u → u + y) p ⟩
(x - y) + y ≡⟨ congL _+_ p ⟩
0r + y ≡⟨ +IdL _ ⟩
y ∎

Expand All @@ -76,7 +76,7 @@ module RingTheory (R' : Ring ℓ) where
0RightAnnihilates x =
let x·0-is-idempotent : x · 0r ≡ x · 0r + x · 0r
x·0-is-idempotent =
x · 0r ≡⟨ cong (λ u → x · u) (sym 0Idempotent) ⟩
x · 0r ≡⟨ congR _·_ (sym 0Idempotent) ⟩
x · (0r + 0r) ≡⟨ ·DistR+ _ _ _ ⟩
(x · 0r) + (x · 0r) ∎
in (+Idempotency→0 _ x·0-is-idempotent)
Expand All @@ -85,7 +85,7 @@ module RingTheory (R' : Ring ℓ) where
0LeftAnnihilates x =
let 0·x-is-idempotent : 0r · x ≡ 0r · x + 0r · x
0·x-is-idempotent =
0r · x ≡⟨ cong (λ u → u · x) (sym 0Idempotent) ⟩
0r · x ≡⟨ congL _·_ (sym 0Idempotent) ⟩
(0r + 0r) · x ≡⟨ ·DistL+ _ _ _ ⟩
(0r · x) + (0r · x) ∎
in +Idempotency→0 _ 0·x-is-idempotent
Expand All @@ -94,15 +94,15 @@ module RingTheory (R' : Ring ℓ) where
-DistR· x y = implicitInverse (x · y) (x · (- y))

(x · y + x · (- y) ≡⟨ sym (·DistR+ _ _ _) ⟩
x · (y + (- y)) ≡⟨ cong (λ u → x · u) (+InvR y) ⟩
x · (y + (- y)) ≡⟨ congR _·_ (+InvR y) ⟩
x · 0r ≡⟨ 0RightAnnihilates x ⟩
0r ∎)

-DistL· : (x y : R) → (- x) · y ≡ - (x · y)
-DistL· x y = implicitInverse (x · y) ((- x) · y)

(x · y + (- x) · y ≡⟨ sym (·DistL+ _ _ _) ⟩
(x - x) · y ≡⟨ cong (λ u → u · y) (+InvR x) ⟩
(x - x) · y ≡⟨ congL _·_ (+InvR x) ⟩
0r · y ≡⟨ 0LeftAnnihilates y ⟩
0r ∎)

Expand All @@ -116,49 +116,41 @@ module RingTheory (R' : Ring ℓ) where
-Dist x y =
implicitInverse _ _
((x + y) + ((- x) + (- y)) ≡⟨ sym (+Assoc _ _ _) ⟩
x + (y + ((- x) + (- y))) ≡⟨ cong
(λ u → x + (y + u))
(+Comm _ _) ⟩
x + (y + ((- y) + (- x))) ≡⟨ cong (λ u → x + u) (+Assoc _ _ _) ⟩
x + ((y + (- y)) + (- x)) ≡⟨ cong (λ u → x + (u + (- x)))
(+InvR _) ⟩
x + (0r + (- x)) ≡⟨ cong (λ u → x + u) (+IdL _) ⟩
x + (y + ((- x) + (- y))) ≡⟨ congR _+_ (congR _+_ (+Comm _ _)) ⟩
x + (y + ((- y) + (- x))) ≡⟨ congR _+_ (+Assoc _ _ _) ⟩
x + ((y + (- y)) + (- x)) ≡⟨ congR _+_ (congL _+_ (+InvR _)) ⟩
x + (0r + (- x)) ≡⟨ congR _+_ (+IdL _) ⟩
x + (- x) ≡⟨ +InvR _ ⟩
0r ∎)

translatedDifference : (x a b : R) → a - b ≡ (x + a) - (x + b)
translatedDifference x a b =
a - b ≡⟨ cong (λ u → a + u)
(sym (+IdL _)) ⟩
(a + (0r + (- b))) ≡⟨ cong (λ u → a + (u + (- b)))
(sym (+InvR _)) ⟩
(a + ((x + (- x)) + (- b))) ≡⟨ cong (λ u → a + u)
(sym (+Assoc _ _ _)) ⟩
a - b ≡⟨ congR _+_ (sym (+IdL _)) ⟩
(a + (0r + (- b))) ≡⟨ congR _+_ (congL _+_ (sym (+InvR _))) ⟩
(a + ((x + (- x)) + (- b))) ≡⟨ congR _+_ (sym (+Assoc _ _ _)) ⟩
(a + (x + ((- x) + (- b)))) ≡⟨ (+Assoc _ _ _) ⟩
((a + x) + ((- x) + (- b))) ≡⟨ cong (λ u → u + ((- x) + (- b)))
(+Comm _ _) ⟩
((x + a) + ((- x) + (- b))) ≡⟨ cong (λ u → (x + a) + u)
(-Dist _ _) ⟩
((a + x) + ((- x) + (- b))) ≡⟨ congL _+_ (+Comm _ _) ⟩
((x + a) + ((- x) + (- b))) ≡⟨ congR _+_ (-Dist _ _) ⟩
((x + a) - (x + b)) ∎

+Assoc-comm1 : (x y z : R) → x + (y + z) ≡ y + (x + z)
+Assoc-comm1 x y z = +Assoc x y z ∙∙ cong (λ x → x + z) (+Comm x y) ∙∙ sym (+Assoc y x z)
+Assoc-comm1 x y z = +Assoc x y z ∙∙ congL _+_ (+Comm x y) ∙∙ sym (+Assoc y x z)

+Assoc-comm2 : (x y z : R) → x + (y + z) ≡ z + (y + x)
+Assoc-comm2 x y z = +Assoc-comm1 x y z ∙∙ cong (λ x → y + x) (+Comm x z) ∙∙ +Assoc-comm1 y z x
+Assoc-comm2 x y z = +Assoc-comm1 x y z ∙∙ congR _+_ (+Comm x z) ∙∙ +Assoc-comm1 y z x

+ShufflePairs : (a b c d : R)
→ (a + b) + (c + d) ≡ (a + c) + (b + d)
+ShufflePairs a b c d =
(a + b) + (c + d) ≡⟨ +Assoc _ _ _ ⟩
((a + b) + c) + d ≡⟨ cong (λ u → u + d) (sym (+Assoc _ _ _)) ⟩
(a + (b + c)) + d ≡⟨ cong (λ u → (a + u) + d) (+Comm _ _) ⟩
(a + (c + b)) + d ≡⟨ cong (λ u → u + d) (+Assoc _ _ _) ⟩
((a + b) + c) + d ≡⟨ congL _+_ (sym (+Assoc _ _ _)) ⟩
(a + (b + c)) + d ≡⟨ congL _+_ (congR _+_ (+Comm _ _)) ⟩
(a + (c + b)) + d ≡⟨ congL _+_ (+Assoc _ _ _) ⟩
((a + c) + b) + d ≡⟨ sym (+Assoc _ _ _) ⟩
(a + c) + (b + d) ∎

·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w
·-assoc2 x y z w = ·Assoc (x · y) z w ∙ cong (_· w) (sym (·Assoc x y z))
·-assoc2 x y z w = ·Assoc (x · y) z w ∙ congL _·_ (sym (·Assoc x y z))

Ring→Semiring : Ring ℓ → Semiring ℓ
Ring→Semiring R =
Expand Down Expand Up @@ -265,8 +257,8 @@ module RingHomTheory {R : Ring ℓ} {S : Ring ℓ'} (φ : RingHom R S) where
where
path : f (x - y) ≡ 0r
path = f (x - y) ≡⟨ pres+ _ _ ⟩
f x + f (- y) ≡⟨ cong (f x +_) (pres- _) ⟩
f x - f y ≡⟨ cong (_- f y) p ⟩
f x + f (- y) ≡⟨ congR _+_ (pres- _) ⟩
f x - f y ≡⟨ congL _-_ p ⟩
f y - f y ≡⟨ +InvR _ ⟩
0r ∎

Expand Down
Loading

0 comments on commit a847f25

Please sign in to comment.