From b1c2070e62f634ed5f17ae1e126e4a236e09ee28 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Sun, 30 Oct 2022 16:08:46 -0400 Subject: [PATCH 1/8] Update Ring.agda --- src/Algebra/Properties/Ring.agda | 46 +++++++++++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 824850d112..7dec9ab960 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -6,7 +6,7 @@ {-# OPTIONS --without-K --safe #-} -open import Algebra +open import Algebra using (Ring) module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where @@ -15,6 +15,8 @@ open Ring R import Algebra.Properties.AbelianGroup as AbelianGroupProperties open import Function.Base using (_$_) open import Relation.Binary.Reasoning.Setoid setoid +open import Algebra.Definitions _≈_ +open import Data.Product ------------------------------------------------------------------------ -- Export properties of abelian groups @@ -67,3 +69,45 @@ open AbelianGroupProperties +-abelianGroup public - (1# * x) ≈⟨ -‿cong ( *-identityˡ x ) ⟩ - x ∎ +zeroʳ-unique : ∀ x z → x + z ≈ x → z ≈ 0# +zeroʳ-unique x z eq = begin + z ≈⟨ sym (+-identityˡ z) ⟩ + 0# + z ≈⟨ +-congʳ (sym (-‿inverseʳ x)) ⟩ + x - x + z ≈⟨ +-congʳ (+-comm x (- x)) ⟩ + - x + x + z ≈⟨ +-assoc (- x) x z ⟩ + - x + (x + z) ≈⟨ +-congˡ eq ⟩ + - x + x ≈⟨ -‿inverseˡ x ⟩ + 0# ∎ + +zeroˡ-unique : ∀ x z → z + x ≈ x → z ≈ 0# +zeroˡ-unique x z eq = begin + z ≈⟨ sym (+-identityʳ z) ⟩ + z + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ + z + (x - x) ≈⟨ sym(+-assoc z x (- x)) ⟩ + z + x - x ≈⟨ +-congʳ eq ⟩ + x - x ≈⟨ -‿inverseʳ x ⟩ + 0# ∎ + +zero-unique : ∀ z → Zero z _+_ → z ≈ 0# +zero-unique z x = zeroˡ-unique z z (proj₂ x z) + +x≈0 : ∀ x → x + x ≈ x → x ≈ 0# +x≈0 x eq = begin + x ≈⟨ sym(+-identityʳ x) ⟩ + x + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ + x + (x - x) ≈⟨ sym (+-assoc x x (- x)) ⟩ + x + x - x ≈⟨ +-congʳ(eq) ⟩ + x - x ≈⟨ -‿inverseʳ x ⟩ + 0# ∎ + +xy-z≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z +xy-z≈xy-xz x y z = begin + x * (y - z) ≈⟨ distribˡ x y (- z) ⟩ + x * y + x * - z ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩ + x * y - x * z ∎ + +y-zx≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) +y-zx≈yx-zx x y z = begin + (y - z) * x ≈⟨ distribʳ x y (- z) ⟩ + y * x + - z * x ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩ + y * x - z * x ∎ From 191661cb0791b0bd61896cec7ef13e1f75045759 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Sun, 30 Oct 2022 16:10:02 -0400 Subject: [PATCH 2/8] Update CHANGELOG.md --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4448791d5a..84f296acc7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1570,6 +1570,12 @@ Other minor changes * Added new proofs to `Algebra.Properties.Ring`: ```agda -1*x≈-x : ∀ x → - 1# * x ≈ - x + zeroʳ-unique : ∀ x z → x + z ≈ x → z ≈ 0# + zeroˡ-unique : ∀ x z → z + x ≈ x → z ≈ 0# + zero-unique : ∀ z → Zero z _+_ → z ≈ 0# + x≈0 : ∀ x → x + x ≈ x → x ≈ 0# + xy-z≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z + y-zx≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) ``` * Added new definitions to `Algebra.Structures`: From 3333f5a57b0157ec20da7f9dd102960b05343f76 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Sun, 30 Oct 2022 16:14:42 -0400 Subject: [PATCH 3/8] align --- src/Algebra/Properties/Ring.agda | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 7dec9ab960..8e99d8239f 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -93,21 +93,21 @@ zero-unique z x = zeroˡ-unique z z (proj₂ x z) x≈0 : ∀ x → x + x ≈ x → x ≈ 0# x≈0 x eq = begin - x ≈⟨ sym(+-identityʳ x) ⟩ - x + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ - x + (x - x) ≈⟨ sym (+-assoc x x (- x)) ⟩ - x + x - x ≈⟨ +-congʳ(eq) ⟩ - x - x ≈⟨ -‿inverseʳ x ⟩ - 0# ∎ + x ≈⟨ sym(+-identityʳ x) ⟩ + x + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ + x + (x - x) ≈⟨ sym (+-assoc x x (- x)) ⟩ + x + x - x ≈⟨ +-congʳ(eq) ⟩ + x - x ≈⟨ -‿inverseʳ x ⟩ + 0# ∎ xy-z≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z xy-z≈xy-xz x y z = begin - x * (y - z) ≈⟨ distribˡ x y (- z) ⟩ - x * y + x * - z ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩ - x * y - x * z ∎ + x * (y - z) ≈⟨ distribˡ x y (- z) ⟩ + x * y + x * - z ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩ + x * y - x * z ∎ y-zx≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) y-zx≈yx-zx x y z = begin - (y - z) * x ≈⟨ distribʳ x y (- z) ⟩ - y * x + - z * x ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩ - y * x - z * x ∎ + (y - z) * x ≈⟨ distribʳ x y (- z) ⟩ + y * x + - z * x ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩ + y * x - z * x ∎ From 76795d0b23384409344d00ac1f10ee26548124e0 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Tue, 1 Nov 2022 12:42:42 -0400 Subject: [PATCH 4/8] Remove duplicate proof --- src/Algebra/Properties/Ring.agda | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 8e99d8239f..1852c5dee2 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -69,28 +69,6 @@ open AbelianGroupProperties +-abelianGroup public - (1# * x) ≈⟨ -‿cong ( *-identityˡ x ) ⟩ - x ∎ -zeroʳ-unique : ∀ x z → x + z ≈ x → z ≈ 0# -zeroʳ-unique x z eq = begin - z ≈⟨ sym (+-identityˡ z) ⟩ - 0# + z ≈⟨ +-congʳ (sym (-‿inverseʳ x)) ⟩ - x - x + z ≈⟨ +-congʳ (+-comm x (- x)) ⟩ - - x + x + z ≈⟨ +-assoc (- x) x z ⟩ - - x + (x + z) ≈⟨ +-congˡ eq ⟩ - - x + x ≈⟨ -‿inverseˡ x ⟩ - 0# ∎ - -zeroˡ-unique : ∀ x z → z + x ≈ x → z ≈ 0# -zeroˡ-unique x z eq = begin - z ≈⟨ sym (+-identityʳ z) ⟩ - z + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ - z + (x - x) ≈⟨ sym(+-assoc z x (- x)) ⟩ - z + x - x ≈⟨ +-congʳ eq ⟩ - x - x ≈⟨ -‿inverseʳ x ⟩ - 0# ∎ - -zero-unique : ∀ z → Zero z _+_ → z ≈ 0# -zero-unique z x = zeroˡ-unique z z (proj₂ x z) - x≈0 : ∀ x → x + x ≈ x → x ≈ 0# x≈0 x eq = begin x ≈⟨ sym(+-identityʳ x) ⟩ From cecd01a9482b3dc9307d58345fce1b5bf22a7e73 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Tue, 1 Nov 2022 12:43:22 -0400 Subject: [PATCH 5/8] update changelog --- CHANGELOG.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 84f296acc7..6d105d048e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1570,9 +1570,6 @@ Other minor changes * Added new proofs to `Algebra.Properties.Ring`: ```agda -1*x≈-x : ∀ x → - 1# * x ≈ - x - zeroʳ-unique : ∀ x z → x + z ≈ x → z ≈ 0# - zeroˡ-unique : ∀ x z → z + x ≈ x → z ≈ 0# - zero-unique : ∀ z → Zero z _+_ → z ≈ 0# x≈0 : ∀ x → x + x ≈ x → x ≈ 0# xy-z≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z y-zx≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) From 287009df013295d0f7afb43c4b9f14f2faad6620 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Sat, 5 Nov 2022 13:36:00 -0400 Subject: [PATCH 6/8] semimedial in commutative semigroup --- CHANGELOG.md | 1 + src/Algebra/Properties/CommutativeSemigroup.agda | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6d105d048e..5d3c7fe1cf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1557,6 +1557,7 @@ Other minor changes leftSemimedial : LeftSemimedial _∙_ rightSemimedial : RightSemimedial _∙_ middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x) + semimedial : Semimedial _∙_ ``` * Added new proofs to `Algebra.Properties.Semigroup`: diff --git a/src/Algebra/Properties/CommutativeSemigroup.agda b/src/Algebra/Properties/CommutativeSemigroup.agda index 209a6b19af..1fa5250e17 100644 --- a/src/Algebra/Properties/CommutativeSemigroup.agda +++ b/src/Algebra/Properties/CommutativeSemigroup.agda @@ -16,6 +16,7 @@ open CommutativeSemigroup CS open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid +open import Data.Product ------------------------------------------------------------------------------ -- Re-export the contents of semigroup @@ -168,3 +169,6 @@ middleSemimedial x y z = begin x ∙ ((z ∙ y) ∙ x) ≈⟨ ∙-congˡ ( assoc z y x) ⟩ x ∙ (z ∙ (y ∙ x)) ≈⟨ sym (assoc x z ((y ∙ x))) ⟩ (x ∙ z) ∙ (y ∙ x) ∎ + +semimedial : Semimedial _∙_ +semimedial = semimedialˡ , semimedialʳ From cc2c8f4fcdd2762ff2a2b21bdbe2349a70127058 Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Tue, 8 Nov 2022 15:28:37 -0500 Subject: [PATCH 7/8] fix comments --- CHANGELOG.md | 6 +++--- src/Algebra/Properties/Ring.agda | 12 ++++++------ 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5d3c7fe1cf..e0b7bc60bd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1571,9 +1571,9 @@ Other minor changes * Added new proofs to `Algebra.Properties.Ring`: ```agda -1*x≈-x : ∀ x → - 1# * x ≈ - x - x≈0 : ∀ x → x + x ≈ x → x ≈ 0# - xy-z≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z - y-zx≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) + x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0# + x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z + [y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) ``` * Added new definitions to `Algebra.Structures`: diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 1852c5dee2..cd3ef96233 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -69,8 +69,8 @@ open AbelianGroupProperties +-abelianGroup public - (1# * x) ≈⟨ -‿cong ( *-identityˡ x ) ⟩ - x ∎ -x≈0 : ∀ x → x + x ≈ x → x ≈ 0# -x≈0 x eq = begin +x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0# +x+x≈x⇒x≈0 x eq = begin x ≈⟨ sym(+-identityʳ x) ⟩ x + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ x + (x - x) ≈⟨ sym (+-assoc x x (- x)) ⟩ @@ -78,14 +78,14 @@ x≈0 x eq = begin x - x ≈⟨ -‿inverseʳ x ⟩ 0# ∎ -xy-z≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z -xy-z≈xy-xz x y z = begin +x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z +x[y-z]≈xy-xz x y z = begin x * (y - z) ≈⟨ distribˡ x y (- z) ⟩ x * y + x * - z ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩ x * y - x * z ∎ -y-zx≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) -y-zx≈yx-zx x y z = begin +[y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) +[y-z]x≈yx-zx x y z = begin (y - z) * x ≈⟨ distribʳ x y (- z) ⟩ y * x + - z * x ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩ y * x - z * x ∎ From 7a0720a6873526a61ad69bbaacb3af3ae9468ecb Mon Sep 17 00:00:00 2001 From: "Akshobhya.Madhusudana" Date: Thu, 15 Dec 2022 10:55:06 -0500 Subject: [PATCH 8/8] fix proof --- src/Algebra/Properties/Ring.agda | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index cd3ef96233..63759f34cd 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -70,13 +70,7 @@ open AbelianGroupProperties +-abelianGroup public - x ∎ x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0# -x+x≈x⇒x≈0 x eq = begin - x ≈⟨ sym(+-identityʳ x) ⟩ - x + 0# ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩ - x + (x - x) ≈⟨ sym (+-assoc x x (- x)) ⟩ - x + x - x ≈⟨ +-congʳ(eq) ⟩ - x - x ≈⟨ -‿inverseʳ x ⟩ - 0# ∎ +x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z x[y-z]≈xy-xz x y z = begin