From 6af14e7036c1d9d3e1a2fe12f892b856b8697b14 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 12 May 2023 22:37:56 -0300 Subject: [PATCH 1/8] added theorems of fields --- CHANGELOG.md | 13 ++ .../Properties/HeytingCommutativeRing.agda | 125 +++++++++++++++++- 2 files changed, 131 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e9cd648ab..b343769ebf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3042,3 +3042,16 @@ This is a full list of proofs that have changed form to use irrelevant instance ```agda ↭-reverse : (xs : List A) → reverse xs ↭ xs ``` + +* Added new functions to `Algebra.Apartness.Bundles` + ```agda + leftInv→rightInv : LeftInvertible _≈_ 1# _*_ (x - y) → RightInvertible _≈_ 1# _*_ (x - y) + rightInv→leftInv : RightInvertible _≈_ 1# _*_ (x - y) → LeftInvertible _≈_ 1# _*_ (x - y) + leftInv→Inv : LeftInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) + rightInv→Inv : RightInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) + leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y + rightInvertible⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y + x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# + #-congʳ : x ≈ y → x # z → y # z + #-sym : Symmetric _#_ + ``` diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index 7ac5b3e58a..bb5bfc590c 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -11,23 +11,134 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing) module Algebra.Apartness.Properties.HeytingCommutativeRing {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where -open import Data.Product using (_,_; proj₂) -open import Algebra using (CommutativeRing; RightIdentity) +open import Function using (_∘_) +open import Data.Product using (_,_; proj₁; proj₂) +open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible) open HeytingCommutativeRing HCR open CommutativeRing commutativeRing using (ring) -open import Algebra.Properties.Ring ring using (-0#≈0#) +open import Algebra.Properties.Ring ring + using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive) +open import Relation.Binary.Definitions using (Symmetric) +import Relation.Binary.Reasoning.Setoid as ReasonSetoid +private variable + x y z : Carrier + +leftInv→rightInv : LeftInvertible _≈_ 1# _*_ (x - y) → RightInvertible _≈_ 1# _*_ (x - y) +leftInv→rightInv {x} {y} (x-y⁻¹ , x-y⁻¹*x-y≈1) = x-y⁻¹ , trans (*-comm (x + - y) x-y⁻¹) x-y⁻¹*x-y≈1 + +rightInv→leftInv : RightInvertible _≈_ 1# _*_ (x - y) → LeftInvertible _≈_ 1# _*_ (x - y) +rightInv→leftInv {x} {y} (x-y⁻¹ , x-y*x-y⁻¹≈1) = x-y⁻¹ , trans (*-comm x-y⁻¹ (x + - y)) x-y*x-y⁻¹≈1 + +leftInv→Inv : LeftInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) +leftInv→Inv left@(x-y⁻¹ , x-y⁻¹*x-y≈1) = x-y⁻¹ , x-y⁻¹*x-y≈1 , leftInv→rightInv left .proj₂ + +rightInv→Inv : RightInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) +rightInv→Inv right@(x-y⁻¹ , x-y*x-y⁻¹≈1) = x-y⁻¹ , rightInv→leftInv right .proj₂ , x-y*x-y⁻¹≈1 + +leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y +leftInvertible⇒# = invertible⇒# ∘ leftInv→Inv + +rightInvertible⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y +rightInvertible⇒# = invertible⇒# ∘ rightInv→Inv x-0≈x : RightIdentity _≈_ 0# _-_ x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x) 1#0 : 1# # 0# -1#0 = invertible⇒# (1# , 1*[x-0]≈x , [x-0]*1≈x) +1#0 = leftInvertible⇒# (1# , 1*[x-0]≈x) where - 1*[x-0]≈x : ∀ {x} → 1# * (x - 0#) ≈ x + 1*[x-0]≈x : 1# * (x - 0#) ≈ x 1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x) - [x-0]*1≈x : ∀ {x} → (x - 0#) * 1# ≈ x - [x-0]*1≈x {x} = trans (*-comm (x - 0#) 1#) 1*[x-0]≈x +x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# +x#0y#0→xy#0 {x} {y} x#0 y#0 = leftInvertible⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1) + where + open ReasonSetoid setoid + + InvX : Invertible _≈_ 1# _*_ (x - 0#) + InvX = #⇒invertible x#0 + + x⁻¹ = InvX .proj₁ + + x⁻¹*x≈1 : x⁻¹ * (x - 0#) ≈ 1# + x⁻¹*x≈1 = InvX .proj₂ .proj₁ + + x*x⁻¹≈1 : (x - 0#) * x⁻¹ ≈ 1# + x*x⁻¹≈1 = InvX .proj₂ .proj₂ + + InvY : Invertible _≈_ 1# _*_ (y - 0#) + InvY = #⇒invertible y#0 + + y⁻¹ = InvY .proj₁ + + y⁻¹*y≈1 : y⁻¹ * (y - 0#) ≈ 1# + y⁻¹*y≈1 = InvY .proj₂ .proj₁ + + y*y⁻¹≈1 : (y - 0#) * y⁻¹ ≈ 1# + y*y⁻¹≈1 = InvY .proj₂ .proj₂ + + y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1# + y⁻¹*x⁻¹*x*y≈1 = begin + y⁻¹ * x⁻¹ * (x * y - 0#) ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩ + y⁻¹ * x⁻¹ * (x * y) ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩ + y⁻¹ * (x⁻¹ * (x * y)) ≈˘⟨ *-congˡ (*-assoc x⁻¹ x y) ⟩ + y⁻¹ * ((x⁻¹ * x) * y) ≈˘⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟩ + y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩ + y⁻¹ * (1# * y) ≈⟨ *-congˡ (*-identityˡ y) ⟩ + y⁻¹ * y ≈˘⟨ *-congˡ (x-0≈x y) ⟩ + y⁻¹ * (y - 0#) ≈⟨ y⁻¹*y≈1 ⟩ + 1# ∎ + + +#-sym : Symmetric _#_ +#-sym {x} {y} x#y = leftInvertible⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1) + where + open ReasonSetoid setoid + InvX-Y : Invertible _≈_ 1# _*_ (x - y) + InvX-Y = #⇒invertible x#y + + x-y⁻¹ = InvX-Y .proj₁ + + y-x≈-[x-y] : y - x ≈ - (x - y) + y-x≈-[x-y] = begin + y - x ≈˘⟨ +-congʳ (-‿involutive y) ⟩ + - - y - x ≈˘⟨ -‿anti-homo-+ x (- y) ⟩ + - (x - y) ∎ + + x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1# + x-y⁻¹*y-x≈1 = begin + (- x-y⁻¹) * (y - x) ≈˘⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟩ + - (x-y⁻¹ * (y - x)) ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩ + - (x-y⁻¹ * - (x - y)) ≈˘⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟩ + - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩ + x-y⁻¹ * (x - y) ≈⟨ InvX-Y .proj₂ .proj₁ ⟩ + 1# ∎ + + +#-congʳ : x ≈ y → x # z → y # z +#-congʳ {x} {y} {z} x≈y x#z = leftInvertible⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1) + where + open ReasonSetoid setoid + + InvXZ : Invertible _≈_ 1# _*_ (x - z) + InvXZ = #⇒invertible x#z + + x-z⁻¹ = InvXZ .proj₁ + + x-z⁻¹*x-z≈1# : x-z⁻¹ * (x - z) ≈ 1# + x-z⁻¹*x-z≈1# = InvXZ .proj₂ .proj₁ + + x-z*x-z⁻¹≈1# : (x - z) * x-z⁻¹ ≈ 1# + x-z*x-z⁻¹≈1# = InvXZ .proj₂ .proj₂ + + x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1# + x-z⁻¹*y-z≈1 = begin + x-z⁻¹ * (y - z) ≈˘⟨ *-congˡ (+-congʳ x≈y) ⟩ + x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩ + 1# ∎ + +#-congˡ : y ≈ z → x # y → x # z +#-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y)) From fcae7eb23556d5b97ba14c4ba9ef7f0d436e37c5 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 12 May 2023 22:40:09 -0300 Subject: [PATCH 2/8] updated changelog --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b343769ebf..2c47bfe201 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3052,6 +3052,7 @@ This is a full list of proofs that have changed form to use irrelevant instance leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y rightInvertible⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# - #-congʳ : x ≈ y → x # z → y # z #-sym : Symmetric _#_ + #-congʳ : x ≈ y → x # z → y # z + #-congˡ : y ≈ z → x # y → x # z ``` From f6ff124ae62a14aa525445ce3931a8961a5e49f0 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 15 May 2023 17:18:30 -0300 Subject: [PATCH 3/8] changed x - y to x --- .../Apartness/Properties/HeytingCommutativeRing.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index bb5bfc590c..2b25aa3847 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -26,17 +26,17 @@ import Relation.Binary.Reasoning.Setoid as ReasonSetoid private variable x y z : Carrier -leftInv→rightInv : LeftInvertible _≈_ 1# _*_ (x - y) → RightInvertible _≈_ 1# _*_ (x - y) -leftInv→rightInv {x} {y} (x-y⁻¹ , x-y⁻¹*x-y≈1) = x-y⁻¹ , trans (*-comm (x + - y) x-y⁻¹) x-y⁻¹*x-y≈1 +leftInv→rightInv : LeftInvertible _≈_ 1# _*_ x → RightInvertible _≈_ 1# _*_ x +leftInv→rightInv {x} (x⁻¹ , x⁻¹*x≈1) = x⁻¹ , trans (*-comm x x⁻¹) x⁻¹*x≈1 -rightInv→leftInv : RightInvertible _≈_ 1# _*_ (x - y) → LeftInvertible _≈_ 1# _*_ (x - y) -rightInv→leftInv {x} {y} (x-y⁻¹ , x-y*x-y⁻¹≈1) = x-y⁻¹ , trans (*-comm x-y⁻¹ (x + - y)) x-y*x-y⁻¹≈1 +rightInv→leftInv : RightInvertible _≈_ 1# _*_ x → LeftInvertible _≈_ 1# _*_ x +rightInv→leftInv {x} (x⁻¹ , x*x⁻¹≈1) = x⁻¹ , trans (*-comm x⁻¹ x) x*x⁻¹≈1 leftInv→Inv : LeftInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) -leftInv→Inv left@(x-y⁻¹ , x-y⁻¹*x-y≈1) = x-y⁻¹ , x-y⁻¹*x-y≈1 , leftInv→rightInv left .proj₂ +leftInv→Inv left@(x⁻¹ , x⁻¹*x≈1) = x⁻¹ , x⁻¹*x≈1 , leftInv→rightInv left .proj₂ rightInv→Inv : RightInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) -rightInv→Inv right@(x-y⁻¹ , x-y*x-y⁻¹≈1) = x-y⁻¹ , rightInv→leftInv right .proj₂ , x-y*x-y⁻¹≈1 +rightInv→Inv right@(x⁻¹ , x*x⁻¹≈1) = x⁻¹ , rightInv→leftInv right .proj₂ , x*x⁻¹≈1 leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y leftInvertible⇒# = invertible⇒# ∘ leftInv→Inv From 8c07dedfffee64be5b97fbc8215ccbb1f301d88d Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 15 May 2023 17:37:31 -0300 Subject: [PATCH 4/8] moved Inverted definitions --- .../Properties/HeytingCommutativeRing.agda | 15 ++------------- src/Algebra/Properties/CommutativeMonoid.agda | 17 +++++++++++++++++ 2 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index 2b25aa3847..a07c91028f 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -16,28 +16,17 @@ open import Data.Product using (_,_; proj₁; proj₂) open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible) open HeytingCommutativeRing HCR -open CommutativeRing commutativeRing using (ring) +open CommutativeRing commutativeRing using (ring; *-commutativeMonoid) open import Algebra.Properties.Ring ring using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive) open import Relation.Binary.Definitions using (Symmetric) import Relation.Binary.Reasoning.Setoid as ReasonSetoid +open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid private variable x y z : Carrier -leftInv→rightInv : LeftInvertible _≈_ 1# _*_ x → RightInvertible _≈_ 1# _*_ x -leftInv→rightInv {x} (x⁻¹ , x⁻¹*x≈1) = x⁻¹ , trans (*-comm x x⁻¹) x⁻¹*x≈1 - -rightInv→leftInv : RightInvertible _≈_ 1# _*_ x → LeftInvertible _≈_ 1# _*_ x -rightInv→leftInv {x} (x⁻¹ , x*x⁻¹≈1) = x⁻¹ , trans (*-comm x⁻¹ x) x*x⁻¹≈1 - -leftInv→Inv : LeftInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) -leftInv→Inv left@(x⁻¹ , x⁻¹*x≈1) = x⁻¹ , x⁻¹*x≈1 , leftInv→rightInv left .proj₂ - -rightInv→Inv : RightInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) -rightInv→Inv right@(x⁻¹ , x*x⁻¹≈1) = x⁻¹ , rightInv→leftInv right .proj₂ , x*x⁻¹≈1 - leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y leftInvertible⇒# = invertible⇒# ∘ leftInv→Inv diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda index 091e88ec61..04bfb3d874 100644 --- a/src/Algebra/Properties/CommutativeMonoid.agda +++ b/src/Algebra/Properties/CommutativeMonoid.agda @@ -7,6 +7,8 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles +open import Algebra.Definitions +open import Data.Product using (_,_; proj₂) module Algebra.Properties.CommutativeMonoid {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where @@ -23,3 +25,18 @@ open CommutativeMonoid M ; assoc to +-assoc ; comm to +-comm ) + +private variable + x : Carrier + +leftInv→rightInv : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x +leftInv→rightInv {x} (-x , -x+x≈1) = -x , trans (+-comm x -x) -x+x≈1 + +rightInv→leftInv : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x +rightInv→leftInv {x} (-x , x+-x≈1) = -x , trans (+-comm -x x) x+-x≈1 + +leftInv→Inv : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x +leftInv→Inv left@(-x , -x+x≈1) = -x , -x+x≈1 , leftInv→rightInv left .proj₂ + +rightInv→Inv : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x +rightInv→Inv right@(-x , x+-x≈1) = -x , rightInv→leftInv right .proj₂ , x+-x≈1 From 7c2df77e628e2af4d4881d91543b7aca575bd9ea Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 15 May 2023 18:15:10 -0300 Subject: [PATCH 5/8] updated CHANGELOG --- CHANGELOG.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c47bfe201..f42c497e80 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3043,12 +3043,16 @@ This is a full list of proofs that have changed form to use irrelevant instance ↭-reverse : (xs : List A) → reverse xs ↭ xs ``` -* Added new functions to `Algebra.Apartness.Bundles` +* Added new functions to `Algebra.Properties.CommutativeMonoid` ```agda leftInv→rightInv : LeftInvertible _≈_ 1# _*_ (x - y) → RightInvertible _≈_ 1# _*_ (x - y) rightInv→leftInv : RightInvertible _≈_ 1# _*_ (x - y) → LeftInvertible _≈_ 1# _*_ (x - y) leftInv→Inv : LeftInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) rightInv→Inv : RightInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) + ``` + +* Added new functions to `Algebra.Apartness.Bundles` + ```agda leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y rightInvertible⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# From 00844e718aa8fd815650b9841f26f4d287d9a61b Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 11 Jun 2023 00:55:47 -0300 Subject: [PATCH 6/8] renamed functions, added pattern match... --- CHANGELOG.md | 20 ++-- .../Properties/HeytingCommutativeRing.agda | 106 +++++++----------- src/Algebra/Properties/CommutativeMonoid.agda | 16 +-- 3 files changed, 60 insertions(+), 82 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f42c497e80..2e7c7a810a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3045,18 +3045,18 @@ This is a full list of proofs that have changed form to use irrelevant instance * Added new functions to `Algebra.Properties.CommutativeMonoid` ```agda - leftInv→rightInv : LeftInvertible _≈_ 1# _*_ (x - y) → RightInvertible _≈_ 1# _*_ (x - y) - rightInv→leftInv : RightInvertible _≈_ 1# _*_ (x - y) → LeftInvertible _≈_ 1# _*_ (x - y) - leftInv→Inv : LeftInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) - rightInv→Inv : RightInvertible _≈_ 1# _*_ (x - y) → Invertible _≈_ 1# _*_ (x - y) + invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x + invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x + invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x + invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x ``` * Added new functions to `Algebra.Apartness.Bundles` ```agda - leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y - rightInvertible⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y - x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# - #-sym : Symmetric _#_ - #-congʳ : x ≈ y → x # z → y # z - #-congˡ : y ≈ z → x # y → x # z + invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y + invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y + x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# + #-sym : Symmetric _#_ + #-congʳ : x ≈ y → x # z → y # z + #-congˡ : y ≈ z → x # y → x # z ``` diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index a07c91028f..86d0e3b3ff 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -27,63 +27,48 @@ open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid private variable x y z : Carrier -leftInvertible⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y -leftInvertible⇒# = invertible⇒# ∘ leftInv→Inv +invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y +invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible -rightInvertible⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y -rightInvertible⇒# = invertible⇒# ∘ rightInv→Inv +invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y +invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible x-0≈x : RightIdentity _≈_ 0# _-_ x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x) 1#0 : 1# # 0# -1#0 = leftInvertible⇒# (1# , 1*[x-0]≈x) +1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x) where 1*[x-0]≈x : 1# * (x - 0#) ≈ x 1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x) -x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# -x#0y#0→xy#0 {x} {y} x#0 y#0 = leftInvertible⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1) - where - open ReasonSetoid setoid - - InvX : Invertible _≈_ 1# _*_ (x - 0#) - InvX = #⇒invertible x#0 - - x⁻¹ = InvX .proj₁ - - x⁻¹*x≈1 : x⁻¹ * (x - 0#) ≈ 1# - x⁻¹*x≈1 = InvX .proj₂ .proj₁ - - x*x⁻¹≈1 : (x - 0#) * x⁻¹ ≈ 1# - x*x⁻¹≈1 = InvX .proj₂ .proj₂ - - InvY : Invertible _≈_ 1# _*_ (y - 0#) - InvY = #⇒invertible y#0 - - y⁻¹ = InvY .proj₁ - - y⁻¹*y≈1 : y⁻¹ * (y - 0#) ≈ 1# - y⁻¹*y≈1 = InvY .proj₂ .proj₁ - - y*y⁻¹≈1 : (y - 0#) * y⁻¹ ≈ 1# - y*y⁻¹≈1 = InvY .proj₂ .proj₂ - - y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1# - y⁻¹*x⁻¹*x*y≈1 = begin - y⁻¹ * x⁻¹ * (x * y - 0#) ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩ - y⁻¹ * x⁻¹ * (x * y) ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩ - y⁻¹ * (x⁻¹ * (x * y)) ≈˘⟨ *-congˡ (*-assoc x⁻¹ x y) ⟩ - y⁻¹ * ((x⁻¹ * x) * y) ≈˘⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟩ - y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩ - y⁻¹ * (1# * y) ≈⟨ *-congˡ (*-identityˡ y) ⟩ - y⁻¹ * y ≈˘⟨ *-congˡ (x-0≈x y) ⟩ - y⁻¹ * (y - 0#) ≈⟨ y⁻¹*y≈1 ⟩ - 1# ∎ +private + x#0y#0→xy#0-helper : x # 0# → y # 0# + → Invertible _≈_ 1# _*_ (x - 0#) + → Invertible _≈_ 1# _*_ (y - 0#) + → x * y # 0# + x#0y#0→xy#0-helper {x} {y} x#0 y#0 (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1) + = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1) + where + open ReasonSetoid setoid + + y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1# + y⁻¹*x⁻¹*x*y≈1 = begin + y⁻¹ * x⁻¹ * (x * y - 0#) ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩ + y⁻¹ * x⁻¹ * (x * y) ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩ + y⁻¹ * (x⁻¹ * (x * y)) ≈˘⟨ *-congˡ (*-assoc x⁻¹ x y) ⟩ + y⁻¹ * ((x⁻¹ * x) * y) ≈˘⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟩ + y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩ + y⁻¹ * (1# * y) ≈⟨ *-congˡ (*-identityˡ y) ⟩ + y⁻¹ * y ≈˘⟨ *-congˡ (x-0≈x y) ⟩ + y⁻¹ * (y - 0#) ≈⟨ y⁻¹*y≈1 ⟩ + 1# ∎ +x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# +x#0y#0→xy#0 {x} {y} x#0 y#0 = x#0y#0→xy#0-helper x#0 y#0 (#⇒invertible x#0) (#⇒invertible y#0) #-sym : Symmetric _#_ -#-sym {x} {y} x#y = leftInvertible⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1) +#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1) where open ReasonSetoid setoid InvX-Y : Invertible _≈_ 1# _*_ (x - y) @@ -106,28 +91,21 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = leftInvertible⇒# (y⁻¹ * x⁻¹ , y⁻¹*x x-y⁻¹ * (x - y) ≈⟨ InvX-Y .proj₂ .proj₁ ⟩ 1# ∎ +private + #-congʳ-helper : x ≈ y → x # z → Invertible _≈_ 1# _*_ (x - z) → y # z + #-congʳ-helper {x} {y} {z} x≈y x#z (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#) + = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1) + where + open ReasonSetoid setoid -#-congʳ : x ≈ y → x # z → y # z -#-congʳ {x} {y} {z} x≈y x#z = leftInvertible⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1) - where - open ReasonSetoid setoid - - InvXZ : Invertible _≈_ 1# _*_ (x - z) - InvXZ = #⇒invertible x#z + x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1# + x-z⁻¹*y-z≈1 = begin + x-z⁻¹ * (y - z) ≈˘⟨ *-congˡ (+-congʳ x≈y) ⟩ + x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩ + 1# ∎ - x-z⁻¹ = InvXZ .proj₁ - - x-z⁻¹*x-z≈1# : x-z⁻¹ * (x - z) ≈ 1# - x-z⁻¹*x-z≈1# = InvXZ .proj₂ .proj₁ - - x-z*x-z⁻¹≈1# : (x - z) * x-z⁻¹ ≈ 1# - x-z*x-z⁻¹≈1# = InvXZ .proj₂ .proj₂ - - x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1# - x-z⁻¹*y-z≈1 = begin - x-z⁻¹ * (y - z) ≈˘⟨ *-congˡ (+-congʳ x≈y) ⟩ - x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩ - 1# ∎ +#-congʳ : x ≈ y → x # z → y # z +#-congʳ {x} {y} {z} x≈y x#z = #-congʳ-helper x≈y x#z (#⇒invertible x#z) #-congˡ : y ≈ z → x # y → x # z #-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y)) diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda index 04bfb3d874..e83be61ac7 100644 --- a/src/Algebra/Properties/CommutativeMonoid.agda +++ b/src/Algebra/Properties/CommutativeMonoid.agda @@ -29,14 +29,14 @@ open CommutativeMonoid M private variable x : Carrier -leftInv→rightInv : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x -leftInv→rightInv {x} (-x , -x+x≈1) = -x , trans (+-comm x -x) -x+x≈1 +invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x +invertibleˡ⇒invertibleʳ {x} (-x , -x+x≈1) = -x , trans (+-comm x -x) -x+x≈1 -rightInv→leftInv : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x -rightInv→leftInv {x} (-x , x+-x≈1) = -x , trans (+-comm -x x) x+-x≈1 +invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x +invertibleʳ⇒invertibleˡ {x} (-x , x+-x≈1) = -x , trans (+-comm -x x) x+-x≈1 -leftInv→Inv : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x -leftInv→Inv left@(-x , -x+x≈1) = -x , -x+x≈1 , leftInv→rightInv left .proj₂ +invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x +invertibleˡ⇒invertible left@(-x , -x+x≈1) = -x , -x+x≈1 , invertibleˡ⇒invertibleʳ left .proj₂ -rightInv→Inv : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x -rightInv→Inv right@(-x , x+-x≈1) = -x , rightInv→leftInv right .proj₂ , x+-x≈1 +invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x +invertibleʳ⇒invertible right@(-x , x+-x≈1) = -x , invertibleʳ⇒invertibleˡ right .proj₂ , x+-x≈1 From 8704dfcd940f01115a3e89f075eb1df54508a4b1 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Sun, 11 Jun 2023 10:50:42 -0300 Subject: [PATCH 7/8] changed private function to helper --- .../Properties/HeytingCommutativeRing.agda | 27 +++++++++---------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index 86d0e3b3ff..4e6c9f6fdc 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -42,12 +42,12 @@ x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x) 1*[x-0]≈x : 1# * (x - 0#) ≈ x 1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x) -private - x#0y#0→xy#0-helper : x # 0# → y # 0# - → Invertible _≈_ 1# _*_ (x - 0#) - → Invertible _≈_ 1# _*_ (y - 0#) - → x * y # 0# - x#0y#0→xy#0-helper {x} {y} x#0 y#0 (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1) +x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# +x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0) + where + + helper : Invertible _≈_ 1# _*_ (x - 0#) → Invertible _≈_ 1# _*_ (y - 0#) → x * y # 0# + helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1) = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1) where open ReasonSetoid setoid @@ -64,9 +64,6 @@ private y⁻¹ * (y - 0#) ≈⟨ y⁻¹*y≈1 ⟩ 1# ∎ -x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# -x#0y#0→xy#0 {x} {y} x#0 y#0 = x#0y#0→xy#0-helper x#0 y#0 (#⇒invertible x#0) (#⇒invertible y#0) - #-sym : Symmetric _#_ #-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1) where @@ -91,9 +88,12 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = x#0y#0→xy#0-helper x#0 y#0 (#⇒invertible x#0 x-y⁻¹ * (x - y) ≈⟨ InvX-Y .proj₂ .proj₁ ⟩ 1# ∎ -private - #-congʳ-helper : x ≈ y → x # z → Invertible _≈_ 1# _*_ (x - z) → y # z - #-congʳ-helper {x} {y} {z} x≈y x#z (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#) +#-congʳ : x ≈ y → x # z → y # z +#-congʳ {x} {y} {z} x≈y x#z = helper (#⇒invertible x#z) + where + + helper : Invertible _≈_ 1# _*_ (x - z) → y # z + helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#) = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1) where open ReasonSetoid setoid @@ -104,8 +104,5 @@ private x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩ 1# ∎ -#-congʳ : x ≈ y → x # z → y # z -#-congʳ {x} {y} {z} x≈y x#z = #-congʳ-helper x≈y x#z (#⇒invertible x#z) - #-congˡ : y ≈ z → x # y → x # z #-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y)) From 058fc24ab3d42cdd2f267a35796d432a63a01a8c Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Fri, 11 Aug 2023 11:23:40 +0900 Subject: [PATCH 8/8] Fix bad merge --- src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index 788624d7f4..7f4f164f42 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -12,7 +12,7 @@ module Algebra.Apartness.Properties.HeytingCommutativeRing {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where open import Function.Base using (_∘_) -open import Data.Product.Base using (_,_; proj₂; proj₂) +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible) open HeytingCommutativeRing HCR