Remove uses of Data.Nat.Solver from a number of places (#2337)

* tighten imports in some files, and make imports explicit in others. Driven by staring at a partial dependency graph.

* more tightening of imports

* and even more tightening of imports

* some explicit  for precision

* new Nat Lemmas to use instead of Solve in Data.Integer.Properties

* use direct proofs instead of solver for all Nat proofs in these files

* two more uses of Data.Nat.Solver for rather simple proofs, now made direct.

* fix whitespace violations

* remove some unneeded parens

* minor fixups based on review

Author: JacquesCarette

src/Data/Digit.agda

@@ -9,20 +9,24 @@
 module Data.Digit where
 
 open import Data.Nat.Base
-open import Data.Nat.Properties using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n)
-open import Data.Nat.Solver using (module +-*-Solver)
+  using (ℕ; zero; suc; _<_; _/_; _%_; sz<ss; _+_; _*_; 2+; _≤′_)
+open import Data.Nat.Properties
+  using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n; +-comm; +-assoc;
+    *-distribˡ-+; *-identityʳ)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base using (Char)
-open import Data.List.Base
+open import Data.List.Base using (List; replicate; [_]; _∷_; [])
 open import Data.Product.Base using (∃; _,_)
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
-open import Data.Nat.DivMod
+open import Data.Nat.DivMod using (m/n<m; _divMod_; result)
 open import Data.Nat.Induction
+  using (Acc; acc; <-wellFounded-fast; <′-Rec; <′-rec)
+open import Function.Base using (_$_)
 open import Relation.Nullary.Decidable using (True; does; toWitness)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong)
-open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
 
 ------------------------------------------------------------------------
 -- Digits
@@ -87,20 +91,32 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
   cons : ∀ {m} (r : Digit base) → Pred m → Pred (toℕ r + m * base)
   cons r (ds , eq) = (r ∷ ds , cong (λ i → toℕ r + i * base) eq)
 
-  open ≤-Reasoning
-  open +-*-Solver
+  lem′ : ∀ x k → x + x + (k + x * k) ≡ k + x * 2+ k
+  lem′ x k = begin
+    x + x + (k + x * k)   ≡⟨ +-assoc (x + x) k _ ⟨
+    x + x + k + x * k     ≡⟨ cong (_+ x * k) (+-comm _ k) ⟩
+    k + (x + x) + x * k   ≡⟨ +-assoc k (x + x) _ ⟩
+    k + ((x + x) + x * k) ≡⟨ cong (k +_) (begin
+      (x + x) + x * k       ≡⟨ +-assoc x x _ ⟩
+      x + (x + x * k)       ≡⟨ cong (x +_) (cong (_+ x * k) (*-identityʳ x)) ⟨
+      x + (x * 1 + x * k)   ≡⟨ cong₂ _+_ (*-identityʳ x) (*-distribˡ-+ x 1 k ) ⟨
+      x * 1 + (x * suc k)   ≡⟨ *-distribˡ-+ x 1 (1 + k) ⟨
+      x * 2+ k              ∎) ⟩
+    k + x * 2+ k          ∎
+    where open ≡-Reasoning
 
   lem : ∀ x k r → 2 + x ≤′ r + (1 + x) * (2 + k)
   lem x k r = ≤⇒≤′ $ begin
-    2 + x
-      ≤⟨ m≤m+n _ _ ⟩
-    2 + x + (x + (1 + x) * k + r)
-      ≡⟨ solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r)
-                              :=
-                            r :+ (con 1 :+ x) :* (con 2 :+ k))
-                 refl x r k ⟩
-    r + (1 + x) * (2 + k)
-      ∎
+    2 + x                             ≤⟨ m≤m+n _ _ ⟩
+    2 + x + (x + (1 + x) * k + r)     ≡⟨ cong ((2 + x) +_) (+-comm _ r) ⟩
+    2 + x + (r + (x + (1 + x) * k))   ≡⟨ +-assoc (2 + x) r _ ⟨
+    2 + x + r + (x + (1 + x) * k)     ≡⟨ cong (_+ (x + (1 + x) * k)) (+-comm (2 + x) r) ⟩
+    r + (2 + x) + (x + (1 + x) * k)   ≡⟨ +-assoc r (2 + x) _ ⟩
+    r + ((2 + x) + (x + (1 + x) * k)) ≡⟨ cong (r +_) (cong 2+ (+-assoc x x _)) ⟨
+    r + (2 + (x + x + (1 + x) * k))   ≡⟨ cong (λ z → r + (2+ z)) (lem′ x k) ⟩
+    r + (2 + (k + x * (2 + k)))       ≡⟨⟩
+    r + (1 + x) * (2 + k)             ∎
+    where open ≤-Reasoning
 
   helper : ∀ n → <′-Rec Pred n → Pred n
   helper n                       rec with n divMod base

src/Data/Fin/Properties.agda

@@ -6,7 +6,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)
 
 module Data.Fin.Properties where
 
@@ -21,7 +21,6 @@ open import Data.Fin.Patterns
 open import Data.Nat.Base as ℕ
   using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕ
-open import Data.Nat.Solver
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base as Product
   using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
@@ -669,12 +668,14 @@ toℕ-combine {suc m} {n} i@0F j = begin
   n ℕ.* toℕ i ℕ.+ toℕ j      ∎
   where open ≡-Reasoning
 toℕ-combine {suc m} {n} (suc i) j = begin
-  toℕ (combine (suc i) j)        ≡⟨⟩
-  toℕ (n ↑ʳ combine i j)         ≡⟨ toℕ-↑ʳ n (combine i j) ⟩
-  n ℕ.+ toℕ (combine i j)        ≡⟨ cong (n ℕ.+_) (toℕ-combine i j) ⟩
-  n ℕ.+ (n ℕ.* toℕ i ℕ.+ toℕ j)  ≡⟨ solve 3 (λ n i j → n :+ (n :* i :+ j) := n :* (con 1 :+ i) :+ j) refl n (toℕ i) (toℕ j) ⟩
-  n ℕ.* toℕ (suc i) ℕ.+ toℕ j    ∎
-  where open ≡-Reasoning; open +-*-Solver
+  toℕ (combine (suc i) j)            ≡⟨⟩
+  toℕ (n ↑ʳ combine i j)             ≡⟨ toℕ-↑ʳ n (combine i j) ⟩
+  n ℕ.+ toℕ (combine i j)            ≡⟨ cong (n ℕ.+_) (toℕ-combine i j) ⟩
+  n ℕ.+ (n ℕ.* toℕ i ℕ.+ toℕ j)     ≡⟨ ℕ.+-assoc n _ (toℕ j) ⟨
+  n ℕ.+ n ℕ.* toℕ i ℕ.+ toℕ j       ≡⟨ cong (λ z → z ℕ.+ n ℕ.* toℕ i ℕ.+ toℕ j) (ℕ.*-identityʳ n) ⟨
+  n ℕ.* 1 ℕ.+ n ℕ.* toℕ i ℕ.+ toℕ j ≡⟨ cong (ℕ._+ toℕ j) (ℕ.*-distribˡ-+ n 1 (toℕ i) ) ⟨
+  n ℕ.* toℕ (suc i) ℕ.+ toℕ j       ∎
+  where open ≡-Reasoning
 
 combine-monoˡ-< : ∀ {i j : Fin m} (k l : Fin n) →
                   i < j → combine i k < combine j l
@@ -688,7 +689,7 @@ combine-monoˡ-< {m} {n} {i} {j} k l i<j = begin-strict
   n ℕ.* toℕ j            ≤⟨ ℕ.m≤m+n (n ℕ.* toℕ j) (toℕ l) ⟩
   n ℕ.* toℕ j ℕ.+ toℕ l  ≡⟨ toℕ-combine j l ⟨
   toℕ (combine j l)      ∎
-  where open ℕ.≤-Reasoning; open +-*-Solver
+  where open ℕ.≤-Reasoning
 
 combine-injectiveˡ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) →
                      combine i j ≡ combine k l → i ≡ k

src/Data/Integer/Properties.agda

@@ -16,11 +16,11 @@ import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.AbelianGroup
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base renaming (suc to sucℤ)
+open import Data.Integer.Properties.NatLemmas
 open import Data.Nat.Base as ℕ
   using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s; s≤s⁻¹; s<s⁻¹)
   hiding (module ℕ)
 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.Base as Sign using (Sign)
@@ -45,7 +45,6 @@ open import Algebra.Consequences.Propositional
 open import Algebra.Structures {A = ℤ} _≡_
 module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_
 module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_
-open +-*-Solver
 
 private
   variable
@@ -1337,15 +1336,6 @@ pred-mono (+≤+ m≤n)         = ⊖-monoˡ-≤ 1 m≤n
 *-zero : Zero 0ℤ _*_
 *-zero = *-zeroˡ , *-zeroʳ
 
-private
-  lemma : ∀ m n o → o ℕ.+ (n ℕ.+ m ℕ.* suc n) ℕ.* suc o
-                  ≡ o ℕ.+ n ℕ.* suc o ℕ.+ m ℕ.* suc (o ℕ.+ n ℕ.* suc o)
-  lemma =
-    solve 3 (λ m n o → o :+ (n :+ m :* (con 1 :+ n)) :* (con 1 :+ o)
-                    := o :+ n :* (con 1 :+ o) :+
-                       m :* (con 1 :+ (o :+ n :* (con 1 :+ o))))
-            refl
-
 *-assoc : Associative _*_
 *-assoc +0 _ _ = refl
 *-assoc i +0 _ rewrite ℕ.*-zeroʳ ∣ i ∣ = refl
@@ -1354,14 +1344,14 @@ private
   | ℕ.*-zeroʳ ∣ i ∣
   | ℕ.*-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)
-*-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)
-*-assoc -[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] (lemma m n o)
-*-assoc -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] (lemma m n o)
-*-assoc +[1+ m ] -[1+ n ] +[1+ o ] = cong -[1+_] (lemma m n o)
-*-assoc +[1+ m ] +[1+ n ] -[1+ o ] = cong -[1+_] (lemma m n o)
+*-assoc -[1+ m ] -[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc -[1+ m ] +[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc +[1+ m ] +[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc +[1+ m ] -[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc -[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] (inner-assoc m n o)
+*-assoc -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] (inner-assoc m n o)
+*-assoc +[1+ m ] -[1+ n ] +[1+ o ] = cong -[1+_] (inner-assoc m n o)
+*-assoc +[1+ m ] +[1+ n ] -[1+ o ] = cong -[1+_] (inner-assoc m n o)
 
 private
 
@@ -1400,26 +1390,10 @@ private
   rewrite +-identityʳ y
         | +-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)
-                  := (con 1 :+ n) :* (con 1 :+ m) :+
-                     (con 1 :+ o) :* (con 1 :+ m))
-          refl m n o
-*-distribʳ-+ +[1+ m ] +[1+ n ] +[1+ o ] = cong (+_) $
-  solve 3 (λ m n o → (con 1 :+ n :+ (con 1 :+ o)) :* (con 1 :+ m)
-                  := (con 1 :+ n) :* (con 1 :+ m) :+
-                     (con 1 :+ o) :* (con 1 :+ m))
-        refl m n o
-*-distribʳ-+ -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] $
-  solve 3 (λ m n o → m :+ (n :+ (con 1 :+ o)) :* (con 1 :+ m)
-                   := (con 1 :+ n) :* (con 1 :+ m) :+
-                      (m :+ o :* (con 1 :+ m)))
-         refl m n o
-*-distribʳ-+ +[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] $
-  solve 3 (λ m n o → m :+ (con 1 :+ m :+ (n :+ o) :* (con 1 :+ m))
-                  := (con 1 :+ n) :* (con 1 :+ m) :+
-                     (m :+ o :* (con 1 :+ m)))
-         refl m n o
+*-distribʳ-+ -[1+ m ] -[1+ n ] -[1+ o ] = cong (+_) $ assoc₁ m n o
+*-distribʳ-+ +[1+ m ] +[1+ n ] +[1+ o ] = cong +[1+_] $ ℕ.suc-injective (assoc₂ m n o)
+*-distribʳ-+ -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] $ assoc₃ m n o
+*-distribʳ-+ +[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] $ assoc₄ m n o
 *-distribʳ-+ -[1+ m ] -[1+ n ] +[1+ o ] = begin
   (suc o ⊖ suc n) * -[1+ m ]                ≡⟨ cong (_* -[1+ m ]) ([1+m]⊖[1+n]≡m⊖n o n) ⟩
   (o ⊖ n) * -[1+ m ]                        ≡⟨ distrib-lemma m n o ⟩

src/Data/Integer/Properties/NatLemmas.agda

@@ -0,0 +1,69 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some extra lemmas about natural numbers only needed for
+-- Data.Integer.Properties (for distributivity)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Integer.Properties.NatLemmas where
+
+open import Data.Nat.Base using (ℕ; _+_; _*_; suc)
+open import Data.Nat.Properties
+  using (*-distribʳ-+; *-assoc; +-assoc; +-comm; +-suc)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; cong; cong₂; sym; module ≡-Reasoning)
+
+open ≡-Reasoning
+
+inner-assoc : ∀ m n o → o + (n + m * suc n) * suc o
+                ≡ o + n * suc o + m * suc (o + n * suc o)
+inner-assoc m n o = begin
+  o + (n + m * suc n) * suc o                ≡⟨ cong (o +_) (begin
+    (n + m * suc n) * suc o             ≡⟨ *-distribʳ-+ (suc o) n (m * suc n) ⟩
+    n * suc o + m * suc n * suc o       ≡⟨ cong (n * suc o +_) (*-assoc m (suc n) (suc o)) ⟩
+    n * suc o + m * suc (o + n * suc o) ∎) ⟩
+  o + (n * suc o + m * suc (o + n * suc o))  ≡⟨ +-assoc o _ _ ⟨
+  o + n * suc o + m * suc (o + n * suc o)    ∎
+
+private
+  assoc-comm : ∀ a b c d → a + b + c + d ≡ (a + c) + (b + d)
+  assoc-comm a b c d = begin
+    a + b + c + d     ≡⟨ cong (_+ d) (+-assoc a b c) ⟩
+    a + (b + c) + d   ≡⟨ cong (λ z → a + z + d) (+-comm b c) ⟩
+    a + (c + b) + d   ≡⟨ cong (_+ d) (+-assoc a c b) ⟨
+    (a + c) + b + d   ≡⟨ +-assoc (a + c) b d ⟩
+    (a + c) + (b + d) ∎
+
+  assoc-comm′ : ∀ a b c d → a + (b + (c + d)) ≡ a + c + (b + d)
+  assoc-comm′ a b c d = begin
+    a + (b + (c + d)) ≡⟨ cong (a +_) (+-assoc b c d) ⟨
+    a + (b + c + d)   ≡⟨ cong (λ z → a + (z + d)) (+-comm b c) ⟩
+    a + (c + b + d)   ≡⟨ cong (a +_) (+-assoc c b d) ⟩
+    a + (c + (b + d)) ≡⟨ +-assoc a c _ ⟨
+    a + c + (b + d)   ∎
+
+assoc₁ : ∀ m n o → (2 + n + o) * (1 + m) ≡ (1 + n) * (1 + m) + (1 + o) * (1 + m)
+assoc₁ m n o = begin
+  (2 + n + o) * (1 + m)                  ≡⟨ cong (_* (1 + m)) (assoc-comm 1 1 n o) ⟩
+  ((1 + n) + (1 + o)) * (1 + m)          ≡⟨ *-distribʳ-+ (1 + m) (1 + n) (1 + o) ⟩
+  (1 + n) * (1 + m) + (1 + o) * (1 + m)   ∎
+
+assoc₂ : ∀ m n o → (1 + n + (1 + o)) * (1 + m) ≡ (1 + n) * (1 + m) + (1 + o) * (1 + m)
+assoc₂ m n o = *-distribʳ-+ (1 + m) (1 + n) (1 + o)
+
+assoc₃ : ∀ m n o → m + (n + (1 + o)) * (1 + m) ≡ (1 + n) * (1 + m) + (m + o * (1 + m))
+assoc₃ m n o = begin
+  m + (n + (1 + o)) * (1 + m)           ≡⟨ cong (m +_) (*-distribʳ-+ (1 + m) n (1 + o)) ⟩
+  m + (n * (1 + m) + (1 + o) * (1 + m)) ≡⟨ +-assoc m _ _ ⟨
+  (m + n * (1 + m)) + (1 + o) * (1 + m) ≡⟨ +-suc _ _ ⟩
+  (1 + n) * (1 + m) + (m + o * (1 + m)) ∎
+
+assoc₄ : ∀ m n o → m + (1 + m + (n + o) * (1 + m)) ≡ (1 + n) * (1 + m) + (m + o * (1 + m))
+assoc₄ m n o = begin
+  m + (1 + m + (n + o) * (1 + m))           ≡⟨ +-suc _ _ ⟩
+  1 + m + (m + (n + o) * (1 + m))           ≡⟨ cong (λ z → suc (m + (m + z))) (*-distribʳ-+ (suc m) n o) ⟩
+  1 + m + (m + (n * (1 + m) + o * (1 + m))) ≡⟨ cong suc (assoc-comm′ m m _ _) ⟩
+  (1 + n) * (1 + m) + (m + o * (1 + m))     ∎