Make Cancellative be more consistent in whole library (#1823)

Author: JacquesCarette

CHANGELOG.md

@@ -366,6 +366,38 @@ Non-backwards compatible changes
   3. Finally, if the above approaches are not viable then you may be forced to explicitly
 	 use `cong` combined with a lemma that proves the old reduction behaviour.
 
+### Change to the definition of `LeftCancellative` and `RightCancellative`
+
+* The definitions of the types for cancellativity in `Algebra.Definitions` previously
+  made some of their arguments implicit. This was under the assumption that the operators were
+  defined by pattern matching on the left argument so that Agda could always infer the 
+  argument on the RHS.
+  
+* Although many of the operators defined in the library follow this convention, this is not
+  always true and cannot be assumed in user's code.
+  
+* Therefore the definitions have been changed as follows to make all their arguments explicit:
+  - `LeftCancellative _•_` 
+	- From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z` 
+	- To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`
+
+  - `RightCancellative _•_`
+    - 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 _ _`
+  - `∙-cancelʳ y z` to `∙-cancelʳ _ y z`
+  
 ### Change in the definition of `Prime`
 
 * The definition of `Prime` in `Data.Nat.Primality` was:

src/Algebra/Consequences/Setoid.agda

@@ -34,14 +34,14 @@ open import Algebra.Consequences.Base public
 module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
 
   comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
-  comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x $ begin
+  comm+cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x 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ʳ y z $ begin
+  comm+cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin
     y • x ≈⟨ comm y x ⟩
     x • y ≈⟨ eq ⟩
     x • z ≈⟨ comm x z ⟩
@@ -90,17 +90,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 y z x≉e $ begin
+  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ˡ : 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 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 ⟩

src/Algebra/Definitions.agda

@@ -7,6 +7,12 @@
 -- The contents of this module should be accessed via `Algebra`, unless
 -- you want to parameterise it via the equality relation.
 
+-- Note that very few of the element arguments are made implicit here,
+-- as we do not assume that the Agda can infer either the right or left
+-- argument of the binary operators. This is despite the fact that the
+-- library defines most of its concrete operators (e.g. in
+-- `Data.Nat.Base`) as being left-biased.
+
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary.Core
@@ -124,19 +130,19 @@ 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
+LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
 
 RightCancellative : Op₂ A → Set _
-RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
+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
+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 _•_

src/Algebra/Morphism/MagmaMonomorphism.agda

@@ -79,14 +79,14 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
     ⟦ y ⟧          ∎))
 
   cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
-  cancelˡ cancelˡ x {y} {z} x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ (begin
+  cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
     ⟦ x ⟧ ◦ ⟦ y ⟧  ≈˘⟨ homo x y ⟩
     ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
     ⟦ x ∙ z ⟧      ≈⟨  homo x z ⟩
     ⟦ x ⟧ ◦ ⟦ z ⟧  ∎))
 
   cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
-  cancelʳ cancelʳ {x} y z y∙x≈z∙x = injective (cancelʳ ⟦ y ⟧ ⟦ z ⟧ (begin
+  cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
     ⟦ y ⟧ ◦ ⟦ x ⟧  ≈˘⟨ homo y x ⟩
     ⟦ y ∙ x ⟧      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
     ⟦ z ∙ x ⟧      ≈⟨  homo z x ⟩

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

src/Algebra/Properties/Group.agda

@@ -39,14 +39,14 @@ private
     x ⁻¹ ∙ (x ∙ y) ∎
 
 ∙-cancelˡ : LeftCancellative _∙_
-∙-cancelˡ x {y} {z} eq = begin
+∙-cancelˡ x y z eq = begin
               y  ≈⟨ right-helper x y ⟩
   x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
   x ⁻¹ ∙ (x ∙ z) ≈˘⟨ right-helper x z ⟩
               z  ∎
 
 ∙-cancelʳ : RightCancellative _∙_
-∙-cancelʳ {x} y z eq = begin
+∙-cancelʳ x y z eq = begin
   y            ≈⟨ left-helper y x ⟩
   y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩
   z ∙ x ∙ x ⁻¹ ≈˘⟨ left-helper z x ⟩
@@ -63,14 +63,14 @@ private
   x                    ∎
 
 ⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y
-⁻¹-injective {x} {y} eq = ∙-cancelʳ x y ( begin
+⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ ( begin
   x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩
   ε        ≈˘⟨ inverseʳ y ⟩
   y ∙ y ⁻¹ ≈˘⟨ ∙-congˡ eq ⟩
   y ∙ x ⁻¹ ∎ )
 
 ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
-⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ ( begin
+⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin
   x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
   ε                     ≈˘⟨ inverseʳ _ ⟩
   x ∙ x ⁻¹              ≈⟨ ∙-congʳ (left-helper x y) ⟩

src/Algebra/Properties/Quasigroup.agda

@@ -16,14 +16,14 @@ open import Relation.Binary.Reasoning.Setoid setoid
 open import Data.Product
 
 cancelˡ : LeftCancellative _∙_
-cancelˡ x {y} {z} eq = begin
+cancelˡ x y z eq = begin
   y             ≈⟨ sym( leftDividesʳ x y) ⟩
   x \\ (x ∙ y)  ≈⟨ \\-congˡ eq ⟩
   x \\ (x ∙ z)  ≈⟨ leftDividesʳ x z ⟩
   z             ∎
 
 cancelʳ : RightCancellative _∙_
-cancelʳ {x} y z eq = begin
+cancelʳ x y z eq = begin
   y             ≈⟨ sym( rightDividesʳ x y) ⟩
   (y ∙ x) // x  ≈⟨ //-congʳ eq ⟩
   (z ∙ x) // x  ≈⟨ rightDividesʳ x z ⟩

src/Data/Fin/Properties.agda

@@ -654,7 +654,7 @@ combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ with <-cmp i k
 combine-injectiveʳ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) →
                      combine i j ≡ combine k l → j ≡ l
 combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ with combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ
-... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) (begin
+... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin
   n ℕ.* toℕ i ℕ.+ toℕ j ≡˘⟨ toℕ-combine i j ⟩
   toℕ (combine i j)     ≡⟨ cong toℕ cᵢⱼ≡cₖₗ ⟩
   toℕ (combine i l)     ≡⟨ toℕ-combine i l ⟩

src/Data/Integer/Properties.agda

@@ -1599,8 +1599,8 @@ abs-*-commute i j = abs-◃ _ _
 *-cancelʳ-≡ : ∀ i j k .{{_ : NonZero k}} → i * k ≡ j * k → i ≡ j
 *-cancelʳ-≡ i j k eq with sign-cong′ eq
 ... | inj₁ s[ik]≡s[jk] = ◃-cong
-  (𝕊ₚ.*-cancelʳ-≡ {sign k} (sign i) (sign j) s[ik]≡s[jk])
-  (ℕ.*-cancelʳ-≡ ∣ i ∣ ∣ j ∣ (abs-cong eq))
+  (𝕊ₚ.*-cancelʳ-≡ (sign k) (sign i) (sign j) s[ik]≡s[jk])
+  (ℕ.*-cancelʳ-≡ ∣ i ∣ ∣ j ∣ _ (abs-cong eq))
 ... | inj₂ (∣ik∣≡0 , ∣jk∣≡0) = trans
   (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣ik∣≡0))
   (sym (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣jk∣≡0)))
@@ -1785,10 +1785,10 @@ neg-distribʳ-* i j = begin
 *-monoʳ-<-pos i {j} {k} rewrite *-comm j i | *-comm k i = *-monoˡ-<-pos i
 
 *-cancelˡ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → k * i < k * j → i < j
-*-cancelˡ-<-nonNeg {+ i}       {+ j}       (+ n) leq = +<+ (ℕ.*-cancelˡ-< n (+◃-cancel-< leq))
+*-cancelˡ-<-nonNeg {+ i}       {+ j}       (+ n) leq = +<+ (ℕ.*-cancelˡ-< n _ _ (+◃-cancel-< leq))
 *-cancelˡ-<-nonNeg {+ i}       { -[1+ j ]} (+ n) leq = contradiction leq +◃≮-◃
 *-cancelˡ-<-nonNeg { -[1+ i ]} {+ j}       (+ n)leq = -<+
-*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (ℕ.≤-pred (ℕ.*-cancelˡ-< n (neg◃-cancel-< leq)))
+*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (ℕ.≤-pred (ℕ.*-cancelˡ-< n _ _ (neg◃-cancel-< leq)))
 
 *-cancelʳ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → i * k < j * k → i < j
 *-cancelʳ-<-nonNeg {i} {j} k rewrite *-comm i k | *-comm j k = *-cancelˡ-<-nonNeg k

src/Data/List/Properties.agda

@@ -183,18 +183,18 @@ module _ {A : Set a} where
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()
 
-  ++-cancelˡ : ∀ xs {ys zs : List A} → xs ++ ys ≡ xs ++ zs → ys ≡ zs
-  ++-cancelˡ []       ys≡zs             = ys≡zs
-  ++-cancelˡ (x ∷ xs) x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)
+  ++-cancelˡ : LeftCancellative _++_
+  ++-cancelˡ []       _ _ ys≡zs             = ys≡zs
+  ++-cancelˡ (x ∷ xs) _ _ x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs _ _ (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)
 
-  ++-cancelʳ : ∀ {xs : List A} ys zs → ys ++ xs ≡ zs ++ xs → ys ≡ zs
-  ++-cancelʳ {_}  []       []       _             = refl
-  ++-cancelʳ {xs} []       (z ∷ zs) eq =
+  ++-cancelʳ : RightCancellative _++_
+  ++-cancelʳ _  []       []       _             = refl
+  ++-cancelʳ xs []       (z ∷ zs) eq =
     contradiction (trans (cong length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
-  ++-cancelʳ {xs} (y ∷ ys) []       eq =
+  ++-cancelʳ xs (y ∷ ys) []       eq =
     contradiction (trans (sym (length-++ (y ∷ ys))) (cong length eq)) (m≢1+n+m (length xs) ∘ sym)
-  ++-cancelʳ {_}  (y ∷ ys) (z ∷ zs) eq =
-    cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ ys zs (∷-injectiveʳ eq))
+  ++-cancelʳ _  (y ∷ ys) (z ∷ zs) eq =
+    cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ _ ys zs (∷-injectiveʳ eq))
 
   ++-cancel : Cancellative _++_
   ++-cancel = ++-cancelˡ , ++-cancelʳ