From 44163ba92000181091aece157adbde47b6a849c9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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 <j.mckinna@hw.ac.uk>
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