change definition of the Cancellative family to have all its arguments be explicit, as per #1436.

Author: JacquesCarette

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

@@ -124,19 +124,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/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/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/Nat/Binary/Properties.agda

@@ -302,17 +302,17 @@ toℕ-cancel-< : ∀ {x y} → toℕ x ℕ.< toℕ y → x < y
 toℕ-cancel-< {zero}     {2[1+ y ]} x<y = 0<even
 toℕ-cancel-< {zero}     {1+[2 y ]} x<y = 0<odd
 toℕ-cancel-< {2[1+ x ]} {2[1+ y ]} x<y =
-  even<even (toℕ-cancel-< (ℕ.≤-pred (ℕₚ.*-cancelˡ-< 2 x<y)))
+  even<even (toℕ-cancel-< (ℕ.≤-pred (ℕₚ.*-cancelˡ-< 2 _ _ x<y)))
 toℕ-cancel-< {2[1+ x ]} {1+[2 y ]} x<y
   rewrite ℕₚ.*-distribˡ-+ 2 1 (toℕ x) =
-  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (ℕₚ.≤-pred x<y))))
+  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (ℕₚ.≤-pred x<y))))
 toℕ-cancel-< {1+[2 x ]} {2[1+ y ]} x<y with toℕ x ℕₚ.≟ toℕ y
 ... | yes x≡y = odd<even (inj₂ (toℕ-injective x≡y))
 ... | no  x≢y
   rewrite ℕₚ.+-suc (toℕ y) (toℕ y ℕ.+ 0) =
-  odd<even (inj₁ (toℕ-cancel-< (ℕₚ.≤∧≢⇒< (ℕₚ.*-cancelˡ-≤ 2 (ℕₚ.+-cancelˡ-≤ 2 x<y)) x≢y)))
+  odd<even (inj₁ (toℕ-cancel-< (ℕₚ.≤∧≢⇒< (ℕₚ.*-cancelˡ-≤ 2 (ℕₚ.+-cancelˡ-≤ 2 _ _ x<y)) x≢y)))
 toℕ-cancel-< {1+[2 x ]} {1+[2 y ]} x<y =
-  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 (ℕ.≤-pred x<y)))
+  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕ.≤-pred x<y)))
 
 fromℕ-cancel-< : ∀ {x y} → fromℕ x < fromℕ y → x ℕ.< y
 fromℕ-cancel-< = subst₂ ℕ._<_ (toℕ-fromℕ _) (toℕ-fromℕ _) ∘ toℕ-mono-<

src/Data/Nat/DivMod.agda

@@ -222,7 +222,7 @@ m/n≤m m n = *-cancelʳ-≤ (m / n) m n (begin
   m * n       ∎)
 
 m/n<m : ∀ m n .{{_ : NonZero m}} .{{_ : NonZero n}} → n ≥ 2 → m / n < m
-m/n<m m n n≥2 = *-cancelʳ-< (m / n) m (begin-strict
+m/n<m m n n≥2 = *-cancelʳ-< _ (m / n) m (begin-strict
   (m / n) * n ≤⟨ m/n*n≤m m n ⟩
   m           <⟨ m<m*n m n n≥2 ⟩
   m * n       ∎)

src/Data/Nat/DivMod/Core.agda

@@ -244,7 +244,7 @@ a*n[divₕ]n≡a acc (suc a) n = begin-equality
   acc + divₕ 0 (k + j) n j       ≡⟨ cong (acc +_) (divₕ-offsetEq _ n j _ (m≤n+m j k) ≤-refl case) ⟩
   acc + divₕ 0 (k + j) n (k + j) ∎
   where
-  case = inj₂′ (refl , +-cancelˡ-≤ (suc k) leq , m≤n+m j k)
+  case = inj₂′ (refl , +-cancelˡ-≤ (suc k) _ _ leq , m≤n+m j k)
 
 divₕ-mono-≤ : ∀ {acc} k {m n o p} → m ≤ n → p ≤ o → divₕ acc (k + o) m o ≤ divₕ acc (k + p) n p
 divₕ-mono-≤ {acc} k {0} {n} {_} {p} z≤n p≤o = acc≤divₕ[acc] (k + p) n p

src/Data/Nat/Properties.agda

@@ -532,8 +532,8 @@ open ≤-Reasoning
   n + suc m   ∎
 
 +-cancelˡ-≡ : LeftCancellative _≡_ _+_
-+-cancelˡ-≡ zero    eq = eq
-+-cancelˡ-≡ (suc m) eq = +-cancelˡ-≡ m (cong pred eq)
++-cancelˡ-≡ zero    _ _ eq = eq
++-cancelˡ-≡ (suc m) _ _ eq = +-cancelˡ-≡ m _ _ (cong pred eq)
 
 +-cancelʳ-≡ : RightCancellative _≡_ _+_
 +-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
@@ -650,21 +650,21 @@ m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))
 -- Properties of _+_ and _≤_/_<_
 
 +-cancelˡ-≤ : LeftCancellative _≤_ _+_
-+-cancelˡ-≤ zero    le       = le
-+-cancelˡ-≤ (suc m) (s≤s le) = +-cancelˡ-≤ m le
++-cancelˡ-≤ zero    _ _ le       = le
++-cancelˡ-≤ (suc m) _ _ (s≤s le) = +-cancelˡ-≤ m _ _ le
 
 +-cancelʳ-≤ : RightCancellative _≤_ _+_
-+-cancelʳ-≤ {m} n o le =
-  +-cancelˡ-≤ m (subst₂ _≤_ (+-comm n m) (+-comm o m) le)
++-cancelʳ-≤ m n o le =
+  +-cancelˡ-≤ m _ _ (subst₂ _≤_ (+-comm n m) (+-comm o m) le)
 
 +-cancel-≤ : Cancellative _≤_ _+_
 +-cancel-≤ = +-cancelˡ-≤ , +-cancelʳ-≤
 
 +-cancelˡ-< : LeftCancellative _<_ _+_
-+-cancelˡ-< m {n} {o} = +-cancelˡ-≤ m ∘ subst (_≤ m + o) (sym (+-suc m n))
++-cancelˡ-< m n o = +-cancelˡ-≤ m (suc n) o ∘ subst (_≤ m + o) (sym (+-suc m n))
 
 +-cancelʳ-< : RightCancellative _<_ _+_
-+-cancelʳ-< n o n+m<o+m = +-cancelʳ-≤ (suc n) o n+m<o+m
++-cancelʳ-< m n o n+m<o+m = +-cancelʳ-≤ m (suc n) o n+m<o+m
 
 +-cancel-< : Cancellative _<_ _+_
 +-cancel-< = +-cancelˡ-< , +-cancelʳ-<
@@ -915,7 +915,7 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 *-cancelʳ-≡ : ∀ m n {o} .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
 *-cancelʳ-≡ zero    zero    {suc o} eq = refl
 *-cancelʳ-≡ (suc m) (suc n) {suc o} eq =
-  cong suc (*-cancelʳ-≡ m n (+-cancelˡ-≡ (suc o) eq))
+  cong suc (*-cancelʳ-≡ m n (+-cancelˡ-≡ (suc o) (m * suc o) (n * suc o) eq))
 
 *-cancelˡ-≡ : ∀ {m n} o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
 *-cancelˡ-≡ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n
@@ -953,7 +953,7 @@ m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)
 *-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
 *-cancelʳ-≤ zero    _       (suc o) _  = z≤n
 *-cancelʳ-≤ (suc m) (suc n) (suc o) le =
-  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ (suc o) le))
+  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ _ _ _ le))
 
 *-cancelˡ-≤ : ∀ {m n} o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
 *-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
@@ -1011,13 +1011,13 @@ m<n⇒m<o*n {m} {n} o m<n = begin-strict
   o * n ∎
 
 *-cancelʳ-< : RightCancellative _<_ _*_
-*-cancelʳ-< {zero}  zero    (suc o) _     = 0<1+n
-*-cancelʳ-< {suc m} zero    (suc o) _     = 0<1+n
-*-cancelʳ-< {m}     (suc n) (suc o) nm<om =
-  s≤s (*-cancelʳ-< n o (+-cancelˡ-< m nm<om))
+*-cancelʳ-< zero    zero    (suc o) _     = 0<1+n
+*-cancelʳ-< (suc m) zero    (suc o) _     = 0<1+n
+*-cancelʳ-< m       (suc n) (suc o) nm<om =
+  s≤s (*-cancelʳ-< m n o (+-cancelˡ-< m _ _ nm<om))
 
 *-cancelˡ-< : LeftCancellative _<_ _*_
-*-cancelˡ-< x {y} {z} rewrite *-comm x y | *-comm x z = *-cancelʳ-< y z
+*-cancelˡ-< x y z rewrite *-comm x y | *-comm x z = *-cancelʳ-< x y z
 
 *-cancel-< : Cancellative _<_ _*_
 *-cancel-< = *-cancelˡ-< , *-cancelʳ-<
@@ -2071,7 +2071,7 @@ _>″?_ = flip _<″?_
 ≤″-irrelevant : Irrelevant _≤″_
 ≤″-irrelevant {m} (less-than-or-equal eq₁)
                   (less-than-or-equal eq₂)
-  with +-cancelˡ-≡ m (trans eq₁ (sym eq₂))
+  with +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
 ... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
 
 <″-irrelevant : Irrelevant _<″_

src/Data/Sign/Properties.agda

@@ -82,14 +82,14 @@ s*s≡+ - = refl
 *-assoc - - - = refl
 
 *-cancelʳ-≡ : RightCancellative _*_
-*-cancelʳ-≡ - - _  = refl
-*-cancelʳ-≡ - + eq = ⊥-elim (s≢opposite[s] _ $ sym eq)
-*-cancelʳ-≡ + - eq = ⊥-elim (s≢opposite[s] _ eq)
-*-cancelʳ-≡ + + _  = refl
+*-cancelʳ-≡ _ - - _  = refl
+*-cancelʳ-≡ _ - + eq = ⊥-elim (s≢opposite[s] _ $ sym eq)
+*-cancelʳ-≡ _ + - eq = ⊥-elim (s≢opposite[s] _ eq)
+*-cancelʳ-≡ _ + + _  = refl
 
 *-cancelˡ-≡ : LeftCancellative _*_
-*-cancelˡ-≡ - eq = opposite-injective eq
-*-cancelˡ-≡ + eq = eq
+*-cancelˡ-≡ - _ _ eq = opposite-injective eq
+*-cancelˡ-≡ + _ _ eq = eq
 
 *-cancel-≡ : Cancellative _*_
 *-cancel-≡ = *-cancelˡ-≡ , *-cancelʳ-≡