[ refactor ] Revise definitions, consequences, and use, of Algebra.Definitions.(Almost)*Cancellative

CHANGELOG.md

@@ -25,6 +25,12 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
+* The definitions of `LeftCancellative`/`RightCancellative` in `Algebra.Definitions`
+  have been altered to make the quantification for each argument explicit. The
+  definitions of `AlmostLeftCancellative`/`AlmostRightCancellative` have also been
+  changed to rephrase them in 'positive' logical terms. These definitions have been
+  propagated through the numeric types `X` in `Data.X.Properties`.
+
 Minor improvements
 ------------------
 
@@ -57,18 +63,23 @@ Deprecated names
   *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
   ```
 
-* In `Algebra.Modules.Structures.IsLeftModule`:
+* In `Algebra.Module.Structures.IsLeftModule`:
   ```agda
   uniqueˡ‿⁻ᴹ   ↦  Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ
   uniqueʳ‿⁻ᴹ   ↦  Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ
   ```
 
-* In `Algebra.Modules.Structures.IsRightModule`:
+* In `Algebra.Module.Structures.IsRightModule`:
   ```agda
   uniqueˡ‿⁻ᴹ   ↦  Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ
   uniqueʳ‿⁻ᴹ   ↦  Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ
   ```
 
+* In `Algebra.Properties.CancellativeCommutativeSemiring`:
+  ```agda
+  *-almostCancelʳ  ↦  Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣∣-sym       ↦  ∥-sym
@@ -152,6 +163,24 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Base`:
+  ```agda
+  almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ →
+                   Except_LeftCancellative_ _≈_ P _•_
+  almost⇒exceptʳ : _AlmostRightCancellative′_ _≈_ P _•_ →
+                   Except_RightCancellative_ _≈_ P _•_
+  except⇒almostˡ : Decidable P → Except_LeftCancellative_ _≈_ P _•_ →
+                   _AlmostLeftCancellative′_ _≈_ P _•_
+  except⇒almostʳ : Decidable P → Except_RightCancellative_ _≈_ P _•_ →
+                   _AlmostRightCancellative′_ _≈_ P _•_
+  ```
+
+* In `Algebra.Consequences.Setoid`:
+  ```agda
+  comm∧cancelAtˡ⇒cancelAtʳ : LeftCancellativeAt x _∙_ → RightCancellativeAt x _∙_
+  comm∧cancelAtʳ⇒cancelAtˡ : RightCancellativeAt x _∙_ → LeftCancellativeAt x _∙_
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →
@@ -181,6 +210,18 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Definitions`:
+  ```agda
+  LeftCancellativeAt           : A → Op₂ A → Set _
+  RightCancellativeAt          : A → Op₂ A → Set _
+  _AlmostLeftCancellative′_    : (P : Pred A p) → Op₂ A → Set _
+  Provided_LeftCancellative_   : (P : Pred A p) → Op₂ A → Set _
+  Except_LeftCancellative_     : (P : Pred A p) → Op₂ A → Set _
+  _AlmostRightCancellative′_   : (P : Pred A p) → Op₂ A → Set _
+  Provided_RightCancellative_  : (P : Pred A p) → Op₂ A → Set _
+  Except_RightCancellative_    : (P : Pred A p) → Op₂ A → Set _
+  ```
+
 * In `Algebra.Modules.Properties`:
   ```agda
   inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y
@@ -232,6 +273,11 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Data.Nat.Properties`:
+  ```agda
+  *-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_
+  ```
+
 * In `Relation.Binary.Construct.Add.Infimum.Strict`:
   ```agda
   <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋

src/Algebra/Consequences/Base.agda

@@ -12,23 +12,60 @@ module Algebra.Consequences.Base
 
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions
-  using (Selective; Idempotent; SelfInverse; Involutive)
-open import Data.Sum.Base using (_⊎_; reduce)
+  using (Selective; Idempotent; SelfInverse; Involutive
+        ; _AlmostLeftCancellative′_; Except_LeftCancellative_
+        ; _AlmostRightCancellative′_; Except_RightCancellative_)
+open import Data.Sum.Base using (inj₁; inj₂; reduce; [_,_]′)
+open import Function.Base using (id; const; flip)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Recomputable using (¬-recompute)
+open import Relation.Unary using (Pred; Decidable)
+
 
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
   sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
   sel⇒idem sel x = reduce (sel x x)
 
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
+         {P : Pred A p} where
+
+  almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ →
+                   Except_LeftCancellative_ _≈_ P _•_
+  almost⇒exceptˡ cancel x y z {{¬px}} =
+    [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x)
+
+  almost⇒exceptʳ : _AlmostRightCancellative′_ _≈_ P _•_ →
+                   Except_RightCancellative_ _≈_ P _•_
+  almost⇒exceptʳ cancel x y z {{¬px}} =
+    [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x)
+
+module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ)
+         {P : Pred A p} (dec : Decidable P) where
+
+  except⇒almostˡ : Except_LeftCancellative_ _≈_ P _•_ →
+                   _AlmostLeftCancellative′_ _≈_ P _•_
+  except⇒almostˡ cancel x with dec x
+  ... | yes px = inj₁ px
+  ... | no ¬px = inj₂ (λ y z → cancel x y z {{¬px}})
+
+  except⇒almostʳ : Except_RightCancellative_ _≈_ P _•_ →
+                   _AlmostRightCancellative′_ _≈_ P _•_
+  except⇒almostʳ cancel x with dec x
+  ... | yes px = inj₁ px
+  ... | no ¬px = inj₂ λ y z → cancel x y z {{¬px}}
+
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
   reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
                                      SelfInverse _≈_ f →
                                      Involutive _≈_ f
   reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Algebra/Consequences/Setoid.agda

@@ -16,7 +16,7 @@ module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 open Setoid S renaming (Carrier to A)
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-open import Data.Sum.Base using (inj₁; inj₂)
+open import Data.Sum.Base using (map₂)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
@@ -100,20 +100,28 @@ module _ {f : Op₁ A} (self : SelfInverse f) where
 
 module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
 
-  comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
-  comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
+  comm∧cancelAtˡ⇒cancelAtʳ : ∀ {x} → LeftCancellativeAt x _∙_ →
+                             RightCancellativeAt x _∙_
+  comm∧cancelAtˡ⇒cancelAtʳ {x = x} cancel y z eq = cancel y z $ begin
     x ∙ y ≈⟨ comm x y ⟩
     y ∙ x ≈⟨ eq ⟩
     z ∙ x ≈⟨ comm z x ⟩
     x ∙ z ∎
 
-  comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_
-  comm∧cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin
+  comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
+  comm∧cancelˡ⇒cancelʳ cancel = comm∧cancelAtˡ⇒cancelAtʳ ∘ cancel
+
+  comm∧cancelAtʳ⇒cancelAtˡ : ∀ {x} → RightCancellativeAt x _∙_ →
+                             LeftCancellativeAt x _∙_
+  comm∧cancelAtʳ⇒cancelAtˡ {x = x} cancel y z eq = cancel y z $ begin
     y ∙ x ≈⟨ comm y x ⟩
     x ∙ y ≈⟨ eq ⟩
     x ∙ z ≈⟨ comm x z ⟩
     z ∙ x ∎
 
+  comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_
+  comm∧cancelʳ⇒cancelˡ cancel = comm∧cancelAtʳ⇒cancelAtˡ ∘ cancel
+
 ------------------------------------------------------------------------
 -- Monoid-like structures
 
@@ -157,21 +165,13 @@ 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
-      x ∙ y ≈⟨ comm x y ⟩
-      y ∙ x ≈⟨ yx≈zx ⟩
-      z ∙ x ≈⟨ comm z x ⟩
-      x ∙ z ∎
+  comm∧almostCancelˡ⇒almostCancelʳ cancel =
+    map₂ (comm∧cancelAtˡ⇒cancelAtʳ comm) ∘ cancel
 
   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
-      y ∙ x ≈⟨ comm y x ⟩
-      x ∙ y ≈⟨ xy≈xz ⟩
-      x ∙ z ≈⟨ comm x z ⟩
-      z ∙ x ∎
+  comm∧almostCancelʳ⇒almostCancelˡ cancel  =
+    map₂ (comm∧cancelAtʳ⇒cancelAtˡ comm) ∘ cancel
 
 ------------------------------------------------------------------------
 -- Group-like structures

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,6 +25,7 @@ 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 Relation.Unary using (Pred; ∁)
 
 ------------------------------------------------------------------------
 -- Properties of operations
@@ -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))
@@ -140,20 +140,45 @@ SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x
 Involutive : Op₁ A → Set _
 Involutive f = ∀ x → f (f x) ≈ x
 
+LeftCancellativeAt : A → Op₂ A → Set _
+LeftCancellativeAt x _•_ = ∀ y z → (x • y) ≈ (x • z) → y ≈ z
+
 LeftCancellative : Op₂ A → Set _
-LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
+LeftCancellative _•_ = ∀ x → LeftCancellativeAt x _•_
+
+RightCancellativeAt : A → Op₂ A → Set _
+RightCancellativeAt x _•_ = ∀ y z → (y • x) ≈ (z • x) → y ≈ z
 
 RightCancellative : Op₂ A → Set _
-RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
+RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_
 
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
+_AlmostLeftCancellative′_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+
+P AlmostLeftCancellative′ _•_   = ∀ x → P x ⊎ LeftCancellativeAt x _•_
+
+Provided_LeftCancellative_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Provided P LeftCancellative _•_ = ∀ x y z → .{{P x}} → (x • y) ≈ (x • z) → y ≈ z
+
+Except_LeftCancellative_    : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Except P LeftCancellative _•_   = Provided (∁ P) LeftCancellative _•_
+
 AlmostLeftCancellative : A → Op₂ A → Set _
-AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+AlmostLeftCancellative e = (_≈ e) AlmostLeftCancellative′_
+
+_AlmostRightCancellative′_  : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+P AlmostRightCancellative′ _•_    = ∀ x → P x ⊎ RightCancellativeAt x _•_
+
+Provided_RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Provided P RightCancellative _•_ = ∀ x y z → .{{P x}} → (y • x) ≈ (z • x) → y ≈ z
+
+Except_RightCancellative_   : ∀ {p} (P : Pred A p) → Op₂ A → Set _
+Except_RightCancellative_ P      = Provided (∁ P) RightCancellative_
 
 AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+AlmostRightCancellative e = (_≈ e) AlmostRightCancellative′_
 
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -12,29 +12,36 @@ module Algebra.Properties.CancellativeCommutativeSemiring
   {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
   where
 
-open import Algebra.Definitions using (AlmostRightCancellative)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; [_,_]′; map₂)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
 
-open CancellativeCommutativeSemiring R
-open import Algebra.Consequences.Setoid setoid
-open import Relation.Binary.Reasoning.Setoid setoid
+open CancellativeCommutativeSemiring R renaming (Carrier to A)
 
-*-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_
-*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
+private
+  variable
+    x y : A
 
-xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
-xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#
-... | yes x≈0 | _       = inj₁ x≈0
-... | no  _   | yes y≈0 = inj₂ 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
 
-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
-... | inj₁ x≈0 = x≉0 x≈0
-... | inj₂ y≈0 = y≉0 y≈0
+module _ (_≟_ : Decidable _≈_) where
+
+  xy≈0⇒x≈0∨y≈0 : x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+  xy≈0⇒x≈0∨y≈0 {x} {y} xy≈0 =
+    map₂ (λ cancel → cancel _ _ (trans xy≈0 (sym (zeroʳ x)))) (*-cancelˡ-nonZero x)
+
+  x≉0∧y≉0⇒xy≉0 : x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+  x≉0∧y≉0⇒xy≉0 x≉0 y≉0 xy≈0 = [ x≉0 , y≉0 ]′ (xy≈0⇒x≈0∨y≈0 xy≈0)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+*-almostCancelʳ = *-cancelʳ-nonZero
+{-# WARNING_ON_USAGE *-almostCancelʳ
+"Warning: *-almostCancelʳ was deprecated in v2.3.
+Please use Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero instead."
+#-}

src/Data/Integer/Properties.agda

@@ -44,7 +44,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 import Relation.Nullary.Decidable as Dec
 
 open import Algebra.Definitions {A = ℤ} _≡_
-open import Algebra.Consequences.Propositional
+open import Algebra.Consequences.Propositional {A = ℤ}
   using (comm∧idˡ⇒idʳ; comm∧invˡ⇒invʳ; comm∧zeˡ⇒zeʳ; comm∧distrʳ⇒distrˡ)
 open import Algebra.Structures {A = ℤ} _≡_
 module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_