From a847f2508da9c567c3e5f97acbf83ffd2deef8da Mon Sep 17 00:00:00 2001 From: Justin Himes <49262679+eqNat@users.noreply.github.com> Date: Thu, 2 Nov 2023 07:36:31 -0500 Subject: [PATCH] 'congR' and 'congL' (#1064) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * '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. --- Cubical/Algebra/CommRing/Properties.agda | 40 ++++++++-------- Cubical/Algebra/Group/Properties.agda | 30 ++++++------ Cubical/Algebra/Module/Properties.agda | 8 ++-- Cubical/Algebra/Monoid/Base.agda | 4 +- Cubical/Algebra/Ring/Properties.agda | 58 ++++++++++-------------- Cubical/Foundations/Prelude.agda | 10 ++++ 6 files changed, 74 insertions(+), 76 deletions(-) diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda index 9cef8285ab..b8d2033797 100644 --- a/Cubical/Algebra/CommRing/Properties.agda +++ b/Cubical/Algebra/CommRing/Properties.agda @@ -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'' ∎ @@ -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 ∎ @@ -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 ∎ @@ -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 _ @@ -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) ⁻¹ᵇ ∎ @@ -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) @@ -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)) ∎ @@ -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) diff --git a/Cubical/Algebra/Group/Properties.agda b/Cubical/Algebra/Group/Properties.agda index b41e2a2420..844106cd31 100644 --- a/Cubical/Algebra/Group/Properties.agda +++ b/Cubical/Algebra/Group/Properties.agda @@ -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 ∎ @@ -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) @@ -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)) diff --git a/Cubical/Algebra/Module/Properties.agda b/Cubical/Algebra/Module/Properties.agda index c7b7b9bd52..ded3e46c7e 100644 --- a/Cubical/Algebra/Module/Properties.agda +++ b/Cubical/Algebra/Module/Properties.agda @@ -21,7 +21,7 @@ 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-+ @@ -29,7 +29,7 @@ module ModuleTheory (R : Ring ℓ') (M : LeftModule R ℓ) where ⋆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) ∎ @@ -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 ∎) diff --git a/Cubical/Algebra/Monoid/Base.agda b/Cubical/Algebra/Monoid/Base.agda index 629386043a..dbf68fb538 100644 --- a/Cubical/Algebra/Monoid/Base.agda +++ b/Cubical/Algebra/Monoid/Base.agda @@ -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 ∎ diff --git a/Cubical/Algebra/Ring/Properties.agda b/Cubical/Algebra/Ring/Properties.agda index adb0294fea..afe940f880 100644 --- a/Cubical/Algebra/Ring/Properties.agda +++ b/Cubical/Algebra/Ring/Properties.agda @@ -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 ∎ @@ -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 ∎ @@ -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) @@ -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 @@ -94,7 +94,7 @@ 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 ∎) @@ -102,7 +102,7 @@ module RingTheory (R' : Ring ℓ) where -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 ∎) @@ -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 = @@ -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 ∎ diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda index fa683d5273..d5796056f3 100644 --- a/Cubical/Foundations/Prelude.agda +++ b/Cubical/Foundations/Prelude.agda @@ -96,6 +96,16 @@ congP₂ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'} congP₂ f p q i = f i (p i) (q i) {-# INLINE congP₂ #-} +congL : {C : Type ℓ} (f : (a : A) → C → B a) (p : x ≡ y) + → {z : C} → PathP (λ i → B (p i)) (f x z) (f y z) +congL f p {z} i = f (p i) z +{-# INLINE congL #-} + +congR : {C : Type ℓ} (f : C → (a : A) → B a) (p : x ≡ y) + → {z : C} → PathP (λ i → B (p i)) (f z x) (f z y) +congR f p {z} i = f z (p i) +{-# INLINE congR #-} + {- The most natural notion of homogenous path composition in a cubical setting is double composition: