Refactor Data.Integer.Divisibility.Signed (#2307)

* removed extra space

* refactor to introduce new `Data.Integer.Properties`

* refactor proofs to use new properties; streamline reasoning

* remove final blank line

* first review comment: missing annotation

* removed two new lemmas: `i*j≢0⇒i≢0` and `i*j≢0⇒j≢0`

Author: jamesmckinna

CHANGELOG.md

@@ -229,11 +229,18 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
-* In `Data.Integer.Divisisbility`: introduce `divides` as an explicit pattern synonym
+* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
   ```agda
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
   ```
 
+* In `Data.Integer.Properties`:
+  ```agda
+  ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
+  sign-*    : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
+  i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)

src/Data/Integer/Divisibility.agda

@@ -27,7 +27,7 @@ infix 4 _∣_
 _∣_ : Rel ℤ 0ℓ
 _∣_ = ℕ._∣_ on ∣_∣
 
-pattern divides k eq  = ℕ.divides k eq
+pattern divides k eq = ℕ.divides k eq
 
 ------------------------------------------------------------------------
 -- Properties of divisibility

src/Data/Integer/Divisibility/Signed.agda

@@ -29,6 +29,7 @@ import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 open import Relation.Nullary.Decidable as Dec using (yes; no)
 open import Relation.Binary.Reasoning.Syntax
 
+
 ------------------------------------------------------------------------
 -- Type
 
@@ -44,43 +45,35 @@ open _∣_ using (quotient) public
 -- Conversion between signed and unsigned divisibility
 
 ∣ᵤ⇒∣ : ∀ {k i} → k Unsigned.∣ i → k ∣ i
-∣ᵤ⇒∣ {k} {i} (Unsigned.divides 0           eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
+∣ᵤ⇒∣ {k} {i} (Unsigned.divides 0           eq) = divides +0 (∣i∣≡0⇒i≡0 eq)
 ∣ᵤ⇒∣ {k} {i} (Unsigned.divides q@(ℕ.suc _) eq) with k ≟ +0
 ... | yes refl = divides +0 (∣i∣≡0⇒i≡0 (trans eq (ℕ.*-zeroʳ q)))
-... | no  neq  = divides (sign i Sign.* sign k ◃ q) (◃-cong sign-eq abs-eq)
+... | no  neq  = divides s[i*k]◃q (◃-cong sign-eq abs-eq)
   where
-  ikq = sign i Sign.* sign k ◃ q
-
-  *-nonZero : ∀ m n .{{_ : ℕ.NonZero m}} .{{_ : ℕ.NonZero n}} → ℕ.NonZero (m ℕ.* n)
-  *-nonZero (ℕ.suc _) (ℕ.suc _) = _
-
-  ◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
-  ◃-nonZero Sign.- (ℕ.suc _) = _
-  ◃-nonZero Sign.+ (ℕ.suc _) = _
-
-  ikq≢0 : NonZero ikq
-  ikq≢0 = ◃-nonZero (sign i Sign.* sign k) q
+  s[i*k] = sign i Sign.* sign k
+  s[i*k]◃q = s[i*k] ◃ q
 
   instance
-    ikq*∣k∣≢0 : ℕ.NonZero (∣ ikq ∣ ℕ.* ∣ k ∣)
-    ikq*∣k∣≢0 = *-nonZero ∣ ikq ∣ ∣ k ∣ {{ikq≢0}} {{≢-nonZero neq}}
+    _ = ≢-nonZero neq
+    _ = ◃-nonZero s[i*k] q
+    _ = i*j≢0 s[i*k]◃q k
 
-  sign-eq : sign i ≡ sign (ikq * k)
+  sign-eq : sign i ≡ sign (s[i*k]◃q * k)
   sign-eq = sym $ begin
-    sign (ikq * k)                        ≡⟨ sign-◃ (sign ikq Sign.* sign k) (∣ ikq ∣ ℕ.* ∣ k ∣) ⟩
-    sign ikq Sign.* sign k                ≡⟨ cong (Sign._* sign k) (sign-◃ (sign i Sign.* sign k) q) ⟩
-    (sign i Sign.* sign k) Sign.* sign k  ≡⟨ Sign.*-assoc (sign i) (sign k) (sign k) ⟩
+    sign (s[i*k]◃q * k)                   ≡⟨ sign-* s[i*k]◃q k ⟩
+    sign s[i*k]◃q Sign.* sign k           ≡⟨ cong (Sign._* _) (sign-◃ s[i*k] q) ⟩
+    s[i*k] Sign.* sign k                  ≡⟨ Sign.*-assoc (sign i) (sign k) (sign k) ⟩
     sign i Sign.* (sign k Sign.* sign k)  ≡⟨ cong (sign i Sign.*_) (Sign.s*s≡+ (sign k)) ⟩
     sign i Sign.* Sign.+                  ≡⟨ Sign.*-identityʳ (sign i) ⟩
-    sign i                          ∎
+    sign i                                ∎
     where open ≡-Reasoning
 
-  abs-eq : ∣ i ∣ ≡ ∣ ikq * k ∣
+  abs-eq : ∣ i ∣ ≡ ∣ s[i*k]◃q * k ∣
   abs-eq = sym $ begin
-    ∣ ikq * k ∣        ≡⟨ ∣i*j∣≡∣i∣*∣j∣ ikq k ⟩
-    ∣ ikq ∣ ℕ.* ∣ k ∣  ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ (sign i Sign.* sign k) q) ⟩
-    q ℕ.* ∣ k ∣        ≡⟨ sym eq ⟩
-    ∣ i ∣              ∎
+    ∣ s[i*k]◃q * k ∣        ≡⟨ abs-* s[i*k]◃q k ⟩
+    ∣ s[i*k]◃q ∣ ℕ.* ∣ k ∣  ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ s[i*k] q) ⟩
+    q ℕ.* ∣ k ∣             ≡⟨ eq ⟨
+    ∣ i ∣                   ∎
     where open ≡-Reasoning
 
 ∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k Unsigned.∣ i
@@ -148,7 +141,7 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 ∣m⇒∣-m : ∀ {i m} → i ∣ m → i ∣ - m
 ∣m⇒∣-m {i} {m} i∣m = ∣ᵤ⇒∣ $′ begin
   ∣ i ∣   ∣⟨ ∣⇒∣ᵤ i∣m ⟩
-  ∣ m ∣   ≡⟨ sym (∣-i∣≡∣i∣ m) ⟩
+  ∣ m ∣   ≡⟨ ∣-i∣≡∣i∣ m ⟨
   ∣ - m ∣ ∎
   where open ℕ.∣-Reasoning
 
@@ -159,7 +152,7 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 ∣m+n∣m⇒∣n {i} {m} {n} i∣m+n i∣m = begin
   i             ∣⟨ ∣m∣n⇒∣m-n i∣m+n i∣m ⟩
   m + n - m     ≡⟨ +-comm (m + n) (- m) ⟩
-  - m + (m + n) ≡⟨ sym (+-assoc (- m) m n) ⟩
+  - m + (m + n) ≡⟨ +-assoc (- m) m n ⟨
   - m + m + n   ≡⟨ cong (_+ n) (+-inverseˡ m) ⟩
   + 0 + n       ≡⟨ +-identityˡ n ⟩
   n             ∎
@@ -171,7 +164,7 @@ m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl
 ∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
 ∣n⇒∣m*n {i} m {n} (divides q eq) = divides (m * q) $′ begin
   m * n       ≡⟨ cong (m *_) eq ⟩
-  m * (q * i) ≡⟨ sym (*-assoc m q i) ⟩
+  m * (q * i) ≡⟨ *-assoc m q i ⟨
   m * q * i   ∎
   where open ≡-Reasoning
 

src/Data/Integer/Properties.agda

@@ -23,7 +23,7 @@ import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
 open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_)
+open import Data.Sign as Sign using (Sign)
 import Data.Sign.Properties as Sign
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
@@ -508,6 +508,10 @@ neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
 ------------------------------------------------------------------------
 -- Properties of sign and _◃_
 
+◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
+◃-nonZero Sign.- (ℕ.suc _) = _
+◃-nonZero Sign.+ (ℕ.suc _) = _
+
 ◃-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
 ◃-inverse -[1+ n ] = refl
 ◃-inverse +0       = refl
@@ -1348,7 +1352,7 @@ private
 *-assoc i j +0 rewrite
     ℕ.*-zeroʳ ∣ j ∣
   | ℕ.*-zeroʳ ∣ i ∣
-  | ℕ.*-zeroʳ ∣ sign i 𝕊* sign j ◃ ∣ i ∣ ℕ.* ∣ j ∣ ∣
+  | ℕ.*-zeroʳ ∣ sign i Sign.* sign j ◃ ∣ i ∣ ℕ.* ∣ j ∣ ∣
   = refl
 *-assoc -[1+ m ] -[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
 *-assoc -[1+ m ] +[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
@@ -1390,11 +1394,11 @@ private
         = refl
 *-distribʳ-+ x +0 z
   rewrite +-identityˡ z
-        | +-identityˡ (sign z 𝕊* sign x ◃ ∣ z ∣ ℕ.* ∣ x ∣)
+        | +-identityˡ (sign z Sign.* sign x ◃ ∣ z ∣ ℕ.* ∣ x ∣)
         = refl
 *-distribʳ-+ x y +0
   rewrite +-identityʳ y
-        | +-identityʳ (sign y 𝕊* sign x ◃ ∣ y ∣ ℕ.* ∣ x ∣)
+        | +-identityʳ (sign y Sign.* sign x ◃ ∣ y ∣ ℕ.* ∣ x ∣)
         = refl
 *-distribʳ-+ -[1+ m ] -[1+ n ] -[1+ o ] = cong (+_) $
   solve 3 (λ m n o → (con 2 :+ n :+ o) :* (con 1 :+ m)
@@ -1594,6 +1598,9 @@ private
 abs-* : ℤtoℕ.Homomorphic₂ ∣_∣ _*_ ℕ._*_
 abs-* i j = abs-◃ _ _
 
+sign-* : ∀ i j → .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
+sign-* i j rewrite abs-* i j = sign-◃ (sign i Sign.* sign j) (∣ i ∣ ℕ.* ∣ j ∣)
+
 *-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
@@ -1631,6 +1638,9 @@ i*j≡0⇒i≡0∨j≡0 i p with ℕ.m*n≡0⇒m≡0∨n≡0 ∣ i ∣ (abs-cong
 ... | inj₁ ∣i∣≡0 = inj₁ (∣i∣≡0⇒i≡0 ∣i∣≡0)
 ... | inj₂ ∣j∣≡0 = inj₂ (∣i∣≡0⇒i≡0 ∣j∣≡0)
 
+i*j≢0 : ∀ i j .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
+i*j≢0 i j rewrite abs-* i j = ℕ.m*n≢0 ∣ i ∣ ∣ j ∣
+
 ------------------------------------------------------------------------
 -- Properties of _^_
 ------------------------------------------------------------------------
@@ -1704,7 +1714,7 @@ neg-distribʳ-* i j = begin
 ------------------------------------------------------------------------
 -- Properties of _*_ and _◃_
 
-◃-distrib-* :  ∀ s t m n → (s 𝕊* t) ◃ (m ℕ.* n) ≡ (s ◃ m) * (t ◃ n)
+◃-distrib-* :  ∀ s t m n → (s Sign.* t) ◃ (m ℕ.* n) ≡ (s ◃ m) * (t ◃ n)
 ◃-distrib-* s t zero    zero    = refl
 ◃-distrib-* s t zero    (suc n) = refl
 ◃-distrib-* s t (suc m) zero    =
@@ -1713,7 +1723,7 @@ neg-distribʳ-* i j = begin
     (*-comm (t ◃ zero) (s ◃ suc m))
 ◃-distrib-* s t (suc m) (suc n) =
   sym (cong₂ _◃_
-    (cong₂ _𝕊*_ (sign-◃ s (suc m)) (sign-◃ t (suc n)))
+    (cong₂ Sign._*_ (sign-◃ s (suc m)) (sign-◃ t (suc n)))
     (∣s◃m∣*∣t◃n∣≡m*n s t (suc m) (suc n)))
 
 ------------------------------------------------------------------------
@@ -1828,7 +1838,7 @@ neg-distribʳ-* i j = begin
 -- Properties of _*_ and ∣_∣
 
 ∣i*j∣≡∣i∣*∣j∣ : ∀ i j → ∣ i * j ∣ ≡ ∣ i ∣ ℕ.* ∣ j ∣
-∣i*j∣≡∣i∣*∣j∣ i j = abs-◃ (sign i 𝕊* sign j) (∣ i ∣ ℕ.* ∣ j ∣)
+∣i*j∣≡∣i∣*∣j∣ = abs-*
 
 ------------------------------------------------------------------------
 -- Properties of _⊓_ and _⊔_