From 44163ba92000181091aece157adbde47b6a849c9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 25 Sep 2023 16:21:00 +0100 Subject: [PATCH 01/10] `NonZero` constructor/destructor pairs for the concrete numeric types --- CHANGELOG.md | 23 ++++++++++++++++++- src/Data/Integer/Base.agda | 6 +++++ src/Data/Rational/Base.agda | 7 +++++- src/Data/Rational/Properties.agda | 7 ++++++ src/Data/Rational/Unnormalised/Base.agda | 5 ++++ .../Rational/Unnormalised/Properties.agda | 11 +++++++++ 6 files changed, 57 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b1e8ab2fa6..85a1c8896b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -464,6 +464,9 @@ Non-backwards compatible changes p≄0⇒∣↥p∣≢0 : ∀ p → p ≠ 0ℚᵘ → ℤ.∣ (↥ p) ∣ ≢0 ∣↥p∣≢0⇒p≄0 : ∀ p → ℤ.∣ (↥ p) ∣ ≢0 → p ≠ 0ℚᵘ ``` + Instead, a uniform collection, for each of the various possible equality + relations of the various numeric datatypes, of constructor/destructor pairs + `-nonZero`/`-nonZero⁻¹` for `NonZero` instances are now defined. ### Change in reduction behaviour of rationals @@ -2163,7 +2166,11 @@ Additions to existing modules *-rawMagma : RawMagma 0ℓ 0ℓ *-1-rawMonoid : RawMonoid 0ℓ 0ℓ - ``` + ``` + and new destructor for \`NonZero\` instances: + ```agda + ≢-nonZero⁻¹ : .{{NonZero i}} → i ≢ 0ℤ + ``` * Added new proofs in `Data.Integer.Properties`: ```agda @@ -2475,6 +2482,10 @@ Additions to existing modules floor ceiling truncate round ⌊_⌋ ⌈_⌉ [_] : ℚ → ℤ fracPart : ℚ → ℚ ``` + and new destructor for \`NonZero\` instances: + ```agda + ≢-nonZero⁻¹ : .{{NonZero p}} → p ≢ 0ℚ + ``` * Added new definitions and proofs in `Data.Rational.Properties`: ```agda @@ -2494,6 +2505,8 @@ Additions to existing modules pos⇒nonZero : .{{Positive p}} → NonZero p neg⇒nonZero : .{{Negative p}} → NonZero p nonZero⇒1/nonZero : .{{_ : NonZero p}} → NonZero (1/ p) + + ≄-nonZero⁻¹ : .{{NonZero p}} → ¬ (p ≃ 0ℚ) ``` * Added new rounding functions in `Data.Rational.Unnormalised.Base`: @@ -2501,6 +2514,10 @@ Additions to existing modules floor ceiling truncate round ⌊_⌋ ⌈_⌉ [_] : ℚᵘ → ℤ fracPart : ℚᵘ → ℚᵘ ``` + and new destructor for \`NonZero\` instances: + ```agda + ≢-nonZero⁻¹ : .{{NonZero p}} → p ≢ 0ℚᵘ + ``` * Added new definitions in `Data.Rational.Unnormalised.Properties`: ```agda @@ -2528,6 +2545,10 @@ Additions to existing modules pos⊔pos⇒pos : .{{_ : Positive p}} .{{_ : Positive q}} → Positive (p ⊔ q) 1/nonZero⇒nonZero : .{{_ : NonZero p}} → NonZero (1/ p) ``` + and new destructor for \`NonZero\` instances: + ```agda + ≠-nonZero⁻¹ : .{{NonZero p}} → p ≠ 0ℚᵘ + ``` * Added new functions to `Data.Product.Nary.NonDependent`: ```agda diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda index 338656956b..368cfe460b 100644 --- a/src/Data/Integer/Base.agda +++ b/src/Data/Integer/Base.agda @@ -183,6 +183,12 @@ nonNegative : ∀ {i} → i ≥ 0ℤ → NonNegative i nonNegative {+0} _ = _ nonNegative {+[1+ n ]} _ = _ +-- Destructors -- mostly see `Data.Integer.Properties` + +≢-nonZero⁻¹ : ∀ i → .{{NonZero i}} → i ≢ 0ℤ +≢-nonZero⁻¹ +0 ⦃ () ⦄ +≢-nonZero⁻¹ +[1+ n ] () + ------------------------------------------------------------------------ -- A view of integers as sign + absolute value diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda index 53739b8571..f73f51a9f9 100644 --- a/src/Data/Rational/Base.agda +++ b/src/Data/Rational/Base.agda @@ -125,7 +125,7 @@ normalize m n = mkℚ+ (m ℕ./ gcd m n) (n ℕ./ gcd m n) (coprime-/gcd m n) g≢0 = ℕ.≢-nonZero (gcd[m,n]≢0 m n (inj₂ (ℕ.≢-nonZero⁻¹ n))) n/g≢0 = ℕ.≢-nonZero (n/gcd[m,n]≢0 m n {{gcd≢0 = g≢0}}) --- A constructor for ℚ that (unlike mkℚ) automatically normalises it's +-- A constructor for ℚ that (unlike mkℚ) automatically normalises its -- arguments. See the constants section below for how to use this operator. infixl 7 _/_ @@ -202,6 +202,11 @@ nonPositive {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonPositive {toℚᵘ p} ( nonNegative : ∀ {p} → p ≥ 0ℚ → NonNegative p nonNegative {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonNegative {toℚᵘ p} (ℚᵘ.*≤* p≤q) +-- Destructor -- mostly see `Data.Rational.Properties` + +≢-nonZero⁻¹ : ∀ p → .{{NonZero p}} → p ≢ 0ℚ +≢-nonZero⁻¹ _ ⦃ () ⦄ refl + ------------------------------------------------------------------------ -- Operations on rationals diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 8910cc5998..04ce4521a9 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -165,6 +165,13 @@ mkℚ+-pos (suc n) (suc d) = _ ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq ... | refl = refl + +------------------------------------------------------------------------ +-- Properties of NonZero: destructor + +≄-nonZero⁻¹ : ∀ p → .{{NonZero p}} → ¬ (p ≃ 0ℚ) +≄-nonZero⁻¹ p eq = ≢-nonZero⁻¹ p (≃⇒≡ eq) + ------------------------------------------------------------------------ -- Properties of ↥ ------------------------------------------------------------------------ diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda index ec104895be..cf5c01baf3 100644 --- a/src/Data/Rational/Unnormalised/Base.agda +++ b/src/Data/Rational/Unnormalised/Base.agda @@ -190,6 +190,11 @@ nonNegative : ∀ {p} → p ≥ 0ℚᵘ → NonNegative p nonNegative {mkℚᵘ +0 _} (*≤* _) = _ nonNegative {mkℚᵘ +[1+ n ] _} (*≤* _) = _ +-- Destructors -- mostly see `Data.Rational.Properties` + +≢-nonZero⁻¹ : ∀ p → .{{NonZero p}} → p ≢ 0ℚᵘ +≢-nonZero⁻¹ _ ⦃ () ⦄ refl + ------------------------------------------------------------------------ -- Operations on rationals diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 169c3786ad..d861cead0b 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -570,6 +570,17 @@ module ≤-Reasoning where >0⇒↥>0 {n} {dm} r>0 = ℤ.<-≤-trans (drop-*<* r>0) (ℤ.≤-reflexive $ ℤ.*-identityʳ n) +------------------------------------------------------------------------ +-- Properties of NonZero predicate + +-- Destructor + +≠-nonZero⁻¹ : ∀ p → .{{NonZero p}} → p ≠ 0ℚᵘ +≠-nonZero⁻¹ p (*≡* eq) = contradiction ↥p≡0ℤ (ℤ.≢-nonZero⁻¹ (↥ p)) + where + ↥p≡0ℤ : (↥ p) ≡ 0ℤ + ↥p≡0ℤ = trans (sym (ℤ.*-identityʳ (↥ p))) (trans eq (ℤ.*-zeroˡ (↧ p))) + ------------------------------------------------------------------------ -- Properties of sign predicates From 9c50a21c382e768b70830b152488537e94de7611 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 06:51:41 +0100 Subject: [PATCH 02/10] start on `AlmostCancellative` properties --- src/Data/Integer/Properties.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index ef7528495e..bd3d5fc32a 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -1604,9 +1604,13 @@ abs-* i j = abs-◃ _ _ (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣ik∣≡0)) (sym (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣jk∣≡0))) +*-AlmostRightCancellative : AlmostRightCancellative 0ℤ _*_ +*-AlmostRightCancellative k i j k≢0 i*k≡j*k = *-cancelʳ-≡ i j k ⦃ ≢-nonZero k≢0 ⦄ i*k≡j*k *-cancelˡ-≡ : ∀ i j k .{{_ : NonZero i}} → i * j ≡ i * k → j ≡ k *-cancelˡ-≡ i j k rewrite *-comm i j | *-comm i k = *-cancelʳ-≡ j k i +*-AlmostLeftCancellative : AlmostLeftCancellative 0ℤ _*_ +*-AlmostLeftCancellative k i j k≢0 k*i≡k*j = {!*-cancelˡ-≡ k i j ⦃ ≢-nonZero k≢0 ⦄ k*i≡k*j!} suc-* : ∀ i j → sucℤ i * j ≡ j + i * j suc-* i j = begin sucℤ i * j ≡⟨ *-distribʳ-+ j (+ 1) i ⟩ From 04a9c00a6ecffa08289a40d9b9b7c73116e67eb7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 08:36:36 +0100 Subject: [PATCH 03/10] use of revised `Almost\*Commutative` definitions --- src/Algebra/Consequences/Setoid.agda | 8 ++++---- src/Algebra/Definitions.agda | 4 ++-- .../Properties/CancellativeCommutativeSemiring.agda | 2 +- src/Data/Integer/Properties.agda | 11 ++++++++--- 4 files changed, 15 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 1aa2b8f4c8..6b043e0443 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -157,8 +157,8 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ → AlmostRightCancellative e _•_ - comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx = - cancelˡ-nonZero x y z x≉e $ begin + comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx = + cancelˡ-nonZero y z x≉e $ begin x • y ≈⟨ comm x y ⟩ y • x ≈⟨ yx≈zx ⟩ z • x ≈⟨ comm z x ⟩ @@ -166,8 +166,8 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ → AlmostLeftCancellative e _•_ - comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz = - cancelʳ-nonZero x y z x≉e $ begin + comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz = + cancelʳ-nonZero y z x≉e $ begin y • x ≈⟨ comm y x ⟩ x • y ≈⟨ xy≈xz ⟩ x • z ≈⟨ comm x z ⟩ diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index ae0566a4bf..b964d9d341 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -146,10 +146,10 @@ Cancellative : Op₂ A → Set _ Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_) AlmostLeftCancellative : A → Op₂ A → Set _ -AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z +AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z AlmostRightCancellative : A → Op₂ A → Set _ -AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z +AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z AlmostCancellative : A → Op₂ A → Set _ AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_ diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index e92fa5170e..7d315a86bb 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -31,7 +31,7 @@ xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0# ... | no x≉0 | no y≉0 = contradiction y≈0 y≉0 where xy≈x*0 = trans xy≈0 (sym (zeroʳ x)) - y≈0 = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0 + y≈0 = *-cancelˡ-nonZero y 0# x≉0 xy≈x*0 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0# x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0 diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index bd3d5fc32a..8b5406770a 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -1604,13 +1604,18 @@ abs-* i j = abs-◃ _ _ (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣ik∣≡0)) (sym (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣jk∣≡0))) -*-AlmostRightCancellative : AlmostRightCancellative 0ℤ _*_ -*-AlmostRightCancellative k i j k≢0 i*k≡j*k = *-cancelʳ-≡ i j k ⦃ ≢-nonZero k≢0 ⦄ i*k≡j*k *-cancelˡ-≡ : ∀ i j k .{{_ : NonZero i}} → i * j ≡ i * k → j ≡ k *-cancelˡ-≡ i j k rewrite *-comm i j | *-comm i k = *-cancelʳ-≡ j k i +*-AlmostRightCancellative : AlmostRightCancellative 0ℤ _*_ +*-AlmostRightCancellative i j k≢0 i*k≡j*k = *-cancelʳ-≡ i j _ ⦃ ≢-nonZero k≢0 ⦄ i*k≡j*k + *-AlmostLeftCancellative : AlmostLeftCancellative 0ℤ _*_ -*-AlmostLeftCancellative k i j k≢0 k*i≡k*j = {!*-cancelˡ-≡ k i j ⦃ ≢-nonZero k≢0 ⦄ k*i≡k*j!} +*-AlmostLeftCancellative {i} j k i≢0 i*j≡i*k = *-cancelˡ-≡ i j k ⦃ ≢-nonZero i≢0 ⦄ i*j≡i*k + +*-AlmostCancellative : AlmostCancellative 0ℤ _*_ +*-AlmostCancellative = *-AlmostLeftCancellative , *-AlmostRightCancellative + suc-* : ∀ i j → sucℤ i * j ≡ j + i * j suc-* i j = begin sucℤ i * j ≡⟨ *-distribʳ-+ j (+ 1) i ⟩ From 367dfa7229d5a637807e893a844429e21af334eb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 10:02:53 +0100 Subject: [PATCH 04/10] `CHANGELOG` --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 85a1c8896b..a5ae6ebfb5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1241,6 +1241,10 @@ Deprecated names *-cancelˡ-<-neg ↦ *-cancelˡ-<-nonPos *-cancelʳ-<-neg ↦ *-cancelʳ-<-nonPos + *-AlmostRightCancellative : AlmostRightCancellative 0ℤ _*_ + *-AlmostLeftCancellative : AlmostLeftCancellative 0ℤ _*_ + *-AlmostCancellative : AlmostCancellative 0ℤ _*_ + ^-semigroup-morphism ↦ ^-isMagmaHomomorphism ^-monoid-morphism ↦ ^-isMonoidHomomorphism From 849e706da710a0bcf4e11adfbbcb7fe20ed43b97 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 10:06:12 +0100 Subject: [PATCH 05/10] `CHANGELOG`: removed changes to `Almost*Cancellative` --- CHANGELOG.md | 8 -------- 1 file changed, 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a5ae6ebfb5..8e4763e2ed 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -520,14 +520,6 @@ Non-backwards compatible changes - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z` - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z` - - `AlmostLeftCancellative e _•_` - - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` - - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` - - - `AlmostRightCancellative e _•_` - - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` - - To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` - * Correspondingly some proofs of the above types will need additional arguments passed explicitly. Instances can easily be fixed by adding additional underscores, e.g. - `∙-cancelˡ x` to `∙-cancelˡ x _ _` From 5e8a45dc6e70835a827fd9aff89480c5bc5bb6f1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 26 Sep 2023 12:00:31 +0100 Subject: [PATCH 06/10] =?UTF-8?q?reconciled=20`Left\|RightConguent`=20with?= =?UTF-8?q?=20`Congruent=E2=82=81?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Definitions.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index b964d9d341..32474a60cc 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -37,10 +37,10 @@ Congruent₂ : Op₂ A → Set _ Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ LeftCongruent : Op₂ A → Set _ -LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_ +LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_) RightCongruent : Op₂ A → Set _ -RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_ +RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x) Associative : Op₂ A → Set _ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z)) From b86aaef3a15bac49aa6e003d7d9224ce3d895d96 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 30 Sep 2023 14:26:29 +0100 Subject: [PATCH 07/10] preliminary redesign of `Almost*` algebraic properties --- src/Algebra/Consequences/Setoid.agda | 8 +- src/Algebra/Definitions.agda | 120 +++++++++++++++--- src/Algebra/Properties/Semiring/Binomial.agda | 4 +- 3 files changed, 107 insertions(+), 25 deletions(-) diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 6b043e0443..f8d86102e1 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -157,8 +157,8 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ → AlmostRightCancellative e _•_ - comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx = - cancelˡ-nonZero y z x≉e $ begin + comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} x≉e y z yx≈zx = + cancelˡ-nonZero x≉e y z $ begin x • y ≈⟨ comm x y ⟩ y • x ≈⟨ yx≈zx ⟩ z • x ≈⟨ comm z x ⟩ @@ -166,8 +166,8 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ → AlmostLeftCancellative e _•_ - comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz = - cancelʳ-nonZero y z x≉e $ begin + comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} x≉e y z xy≈xz = + cancelʳ-nonZero x≉e y z $ begin y • x ≈⟨ comm y x ⟩ x • y ≈⟨ xy≈xz ⟩ x • z ≈⟨ comm x z ⟩ diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 32474a60cc..8ab7b304a9 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -16,7 +16,6 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) -open import Relation.Nullary.Negation.Core using (¬_) module Algebra.Definitions {a ℓ} {A : Set a} -- The underlying set @@ -26,10 +25,111 @@ module Algebra.Definitions open import Algebra.Core using (Op₁; Op₂) open import Data.Product.Base using (_×_; ∃-syntax) open import Data.Sum.Base using (_⊎_) +open import Function.Base using (flip; id; _∘_; _on_) +open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Unary using (Pred) + +------------------------------------------------------------------------ +-- Properties of operations + +------------------------------------------------------------------------ +-- A generalisation: because not everything can be defined in terms of +-- a single relation _≈_, AND because the corresponding definitions in +-- `Relation.Binary.Core` use *implicit* quantification... so there is +-- plenty of potential for later/downstream refactoring of this design + +module Monotonicity {ℓ₁ ℓ₂} (_≤₁_ : Rel A ℓ₁) (_≤₂_ : Rel A ℓ₂) where + + Monotone₁ : Op₁ A → Set _ + Monotone₁ f = ∀ x y → x ≤₁ y → (_≤₂_ on f) x y + + Monotone₂ : Op₂ A → Set _ + Monotone₂ _∙_ = ∀ x y u v → x ≤₁ y → u ≤₁ v → (x ∙ u) ≤₂ (y ∙ v) + + MonotoneAt : A → Op₂ A → Set _ + MonotoneAt x f = Monotone₁ (f x) + + LeftMonotone : Op₂ A → Set _ + LeftMonotone _∙_ = ∀ x → MonotoneAt x _∙_ + + RightMonotone : Op₂ A → Set _ + RightMonotone _∙_ = ∀ x → MonotoneAt x (flip _∙_) + + AlmostLeftMonotone : (Pred A ℓ) → Op₂ A → Set _ + AlmostLeftMonotone P _∙_ = ∀ {x} → P x → MonotoneAt x _∙_ + + AlmostRightMonotone : (Pred A ℓ) → Op₂ A → Set _ + AlmostRightMonotone P _∙_ = ∀ {x} → P x → MonotoneAt x (flip _∙_) + +------------------------------------------------------------------------ +-- A second generalisation: this could be expressed, less efficiently, +-- in terms of Monotonicity (I think) + +module Cancellativity {ℓ₁ ℓ₂} (_≤₁_ : Rel A ℓ₁) (_≤₂_ : Rel A ℓ₂) where + + Cancellative₁ : Op₁ A → Set _ + Cancellative₁ f = ∀ x y → (_≤₁_ on f) x y → x ≤₂ y + + Cancellative₂ : Op₂ A → Set _ + Cancellative₂ _∙_ = ∀ x y u v → (x ∙ u) ≤₁ (y ∙ v) → x ≤₂ y × u ≤₂ v + + CancellativeAt : A → Op₂ A → Set _ + CancellativeAt x f = Cancellative₁ (f x) + + LeftCancellative : Op₂ A → Set _ + LeftCancellative _∙_ = ∀ x → CancellativeAt x _∙_ + + RightCancellative : Op₂ A → Set _ + RightCancellative _∙_ = ∀ x → CancellativeAt x (flip _∙_) + + AlmostLeftCancellative : (Pred A ℓ) → Op₂ A → Set _ + AlmostLeftCancellative P _∙_ = ∀ {x} → P x → CancellativeAt x _∙_ + + AlmostRightCancellative : (Pred A ℓ) → Op₂ A → Set _ + AlmostRightCancellative P _∙_ = ∀ {x} → P x → CancellativeAt x (flip _∙_) + ------------------------------------------------------------------------ -- Properties of operations +-- (Anti)Monotonicity + +open Monotonicity _≈_ _≈_ public + hiding (Monotone₂; MonotoneAt) + renaming (Monotone₁ to Monotone) + +open Monotonicity _≈_ (flip _≈_) public + hiding (Monotone₂; MonotoneAt) + renaming (Monotone₁ to AntiMonotone; + LeftMonotone to LeftAntiMonotone; + RightMonotone to RightAntiMonotone; + AlmostLeftMonotone to AlmostLeftAntiMonotone; + AlmostRightMonotone to AlomostRightAntiMonotone) + +-- Cancellativity + +open Cancellativity _≈_ _≈_ public + hiding (Cancellative₁; Cancellative₂; CancellativeAt; + AlmostLeftCancellative; + AlmostRightCancellative) + +Cancellative : Op₂ A → Set _ +Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_) + +AlmostLeftCancellative : A → Op₂ A → Set _ +AlmostLeftCancellative e + = Cancellativity.AlmostLeftCancellative _≈_ _≈_ λ x → ¬ x ≈ e + +AlmostRightCancellative : A → Op₂ A → Set _ +AlmostRightCancellative e + = Cancellativity.AlmostRightCancellative _≈_ _≈_ λ x → ¬ x ≈ e + +AlmostCancellative : A → Op₂ A → Set _ +AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_ + +------------------------------------------------------------------------ +-- The 'usual' algebraic properties + Congruent₁ : Op₁ A → Set _ Congruent₁ f = f Preserves _≈_ ⟶ _≈_ @@ -136,24 +236,6 @@ SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x Involutive : Op₁ A → Set _ Involutive f = ∀ x → f (f x) ≈ x -LeftCancellative : Op₂ A → Set _ -LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z - -RightCancellative : Op₂ A → Set _ -RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z - -Cancellative : Op₂ A → Set _ -Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_) - -AlmostLeftCancellative : A → Op₂ A → Set _ -AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z - -AlmostRightCancellative : A → Op₂ A → Set _ -AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z - -AlmostCancellative : A → Op₂ A → Set _ -AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_ - Interchangable : Op₂ A → Op₂ A → Set _ Interchangable _∘_ _∙_ = ∀ w x y z → ((w ∙ x) ∘ (y ∙ z)) ≈ ((w ∘ y) ∙ (x ∘ z)) diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda index b4d5ef81db..122da9fcb9 100644 --- a/src/Algebra/Properties/Semiring/Binomial.agda +++ b/src/Algebra/Properties/Semiring/Binomial.agda @@ -71,7 +71,7 @@ sum₂ n = ∑[ k ≤ suc n ] term₂ n k ------------------------------------------------------------------------ -- Properties -term₂[n,n+1]≈0# : ∀ n → term₂ n (fromℕ (suc n)) ≈ 0# +term₂[n,n+1]≈0# : ∀ n → term₂ n (fromℕ (suc n)) ≈ 0# term₂[n,n+1]≈0# n rewrite view-fromℕ (suc n) = refl lemma₁ : ∀ n → x * binomialExpansion n ≈ sum₁ n @@ -117,7 +117,7 @@ x*lemma {n} i = begin ------------------------------------------------------------------------ -- Next, a lemma which does require commutativity -y*lemma : x * y ≈ y * x → ∀ {n : ℕ} (j : Fin n) → +y*lemma : x * y ≈ y * x → ∀ {n : ℕ} (j : Fin n) → y * binomialTerm n (suc j) ≈ (n C toℕ (suc j)) × binomial (suc n) (suc (inject₁ j)) y*lemma x*y≈y*x {n} j = begin y * binomialTerm n (suc j) From 7a6392c87eedc68b4ef95c5e6feb4a98736f2306 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 1 Oct 2023 03:31:52 +0100 Subject: [PATCH 08/10] two omitted arg reorderings --- src/Algebra/Properties/CancellativeCommutativeSemiring.agda | 2 +- src/Data/Integer/Properties.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index 7d315a86bb..998e8290e2 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -31,7 +31,7 @@ xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0# ... | no x≉0 | no y≉0 = contradiction y≈0 y≉0 where xy≈x*0 = trans xy≈0 (sym (zeroʳ x)) - y≈0 = *-cancelˡ-nonZero y 0# x≉0 xy≈x*0 + y≈0 = *-cancelˡ-nonZero x≉0 y 0# xy≈x*0 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0# x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0 diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 570b8d5adc..b8d8366e1c 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -1609,10 +1609,10 @@ abs-* i j = abs-◃ _ _ *-cancelˡ-≡ i j k rewrite *-comm i j | *-comm i k = *-cancelʳ-≡ j k i *-AlmostRightCancellative : AlmostRightCancellative 0ℤ _*_ -*-AlmostRightCancellative i j k≢0 i*k≡j*k = *-cancelʳ-≡ i j _ ⦃ ≢-nonZero k≢0 ⦄ i*k≡j*k +*-AlmostRightCancellative k≢0 i j i*k≡j*k = *-cancelʳ-≡ i j _ ⦃ ≢-nonZero k≢0 ⦄ i*k≡j*k *-AlmostLeftCancellative : AlmostLeftCancellative 0ℤ _*_ -*-AlmostLeftCancellative {i} j k i≢0 i*j≡i*k = *-cancelˡ-≡ i j k ⦃ ≢-nonZero i≢0 ⦄ i*j≡i*k +*-AlmostLeftCancellative {i} i≢0 j k i*j≡i*k = *-cancelˡ-≡ i j k ⦃ ≢-nonZero i≢0 ⦄ i*j≡i*k *-AlmostCancellative : AlmostCancellative 0ℤ _*_ *-AlmostCancellative = *-AlmostLeftCancellative , *-AlmostRightCancellative From f89a16345cf54701478c4de119138c6edcadaf9a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 1 Oct 2023 09:01:46 +0100 Subject: [PATCH 09/10] typo --- src/Algebra/Definitions.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 8ab7b304a9..8664dca78f 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -104,7 +104,7 @@ open Monotonicity _≈_ (flip _≈_) public LeftMonotone to LeftAntiMonotone; RightMonotone to RightAntiMonotone; AlmostLeftMonotone to AlmostLeftAntiMonotone; - AlmostRightMonotone to AlomostRightAntiMonotone) + AlmostRightMonotone to AlmostRightAntiMonotone) -- Cancellativity From 23734044648ddb528d149794881d7850897397e4 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sun, 1 Oct 2023 09:13:23 +0100 Subject: [PATCH 10/10] Update Definitions.agda: fixed typo --- src/Algebra/Definitions.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 8ab7b304a9..8664dca78f 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -104,7 +104,7 @@ open Monotonicity _≈_ (flip _≈_) public LeftMonotone to LeftAntiMonotone; RightMonotone to RightAntiMonotone; AlmostLeftMonotone to AlmostLeftAntiMonotone; - AlmostRightMonotone to AlomostRightAntiMonotone) + AlmostRightMonotone to AlmostRightAntiMonotone) -- Cancellativity