Numeric non-zero equivalents/Redesign of Almost* properties in Algebra.Definitions

CHANGELOG.md

@@ -470,6 +470,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
 
@@ -523,14 +526,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 _ _`
@@ -1283,6 +1278,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
 
@@ -2245,7 +2244,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
@@ -2557,6 +2560,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
@@ -2576,13 +2583,19 @@ 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`:
   ```agda
   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
@@ -2610,6 +2623,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

src/Algebra/Consequences/Setoid.agda

@@ -157,17 +157,17 @@ 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} 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 ⟩
       x • z ∎
 
   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} 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 ⟩

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,21 +25,122 @@ 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 AlmostRightAntiMonotone)
+
+-- 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 _≈_ ⟶ _≈_
 
 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))
@@ -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))
 

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

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)

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
 

src/Data/Integer/Properties.agda

@@ -1608,6 +1608,15 @@ abs-* i j = abs-◃ _ _
 *-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 k≢0 i j i*k≡j*k = *-cancelʳ-≡ i j _ ⦃ ≢-nonZero k≢0 ⦄ i*k≡j*k
+
+*-AlmostLeftCancellative : AlmostLeftCancellative 0ℤ _*_
+*-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
+
 suc-* : ∀ i j → sucℤ i * j ≡ j + i * j
 suc-* i j = begin
   sucℤ i * j      ≡⟨ *-distribʳ-+ j (+ 1) i ⟩

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
 

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 ↥
 ------------------------------------------------------------------------

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
 

src/Data/Rational/Unnormalised/Properties.agda

@@ -572,6 +572,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