adapt also NatSolver

agda · Feb 2, 2024 · eda7ec4 · eda7ec4
1 parent dccd154
commit eda7ec4
Show file tree

Hide file tree

Showing 7 changed files with 152 additions and 212 deletions.
diff --git a/Cubical/Data/Nat/Triangular.agda b/Cubical/Data/Nat/Triangular.agda
@@ -18,7 +18,7 @@ open import Cubical.Algebra.CommSemiring
 open import Cubical.Algebra.CommSemiring.Instances.Nat
 open import Cubical.Algebra.Semiring.BigOps
 
-open import Cubical.Tactics.NatSolver.Reflection
+open import Cubical.Tactics.NatSolver
 
 open Sum (CommSemiring→Semiring ℕasCSR)
 open CommSemiringStr (snd ℕasCSR)
@@ -43,14 +43,11 @@ sumFormula (suc n) =
   2 · (∑ (first (2 + n) ∘ weakenFin) + (suc n))                        ≡⟨ step2 ⟩
   2 · (∑ (first (1 + n)) + (suc n))                                    ≡⟨ step3 ⟩
   2 · ∑ (first (1 + n)) + 2 · (suc n)                                  ≡⟨ step4 ⟩
-  n · (n + 1) + 2 · (suc n)                                            ≡⟨ useSolver n ⟩
+  n · (n + 1) + 2 · (suc n)                                            ≡⟨ solveℕ! ⟩
   (suc n) · (suc (n + 1))                                              ∎
   where
     step0 = cong (λ u → 2 · u) (∑Last (first (2 + n)))
     step1 = cong (λ u → 2 · (∑ (first (2 + n) ∘ weakenFin) + u)) (toFromId _)
     step2 = cong (λ u → 2 · ((∑ u) + (suc n))) (firstDecompose (suc n))
     step3 = ·DistR+ 2 (∑ (first (1 + n))) (suc n)
     step4 = cong (λ u → u + 2 · (suc n)) (sumFormula n)
-
-    useSolver : ∀ (n : ℕ) → n · (n + 1) + 2 · (suc n) ≡ (suc n) · (suc (n + 1))
-    useSolver = solve
diff --git a/Cubical/HITs/James/Inductive/PushoutFormula.agda b/Cubical/HITs/James/Inductive/PushoutFormula.agda
@@ -19,7 +19,7 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.Pointed hiding (pt)
 
 open import Cubical.Data.Nat
-open import Cubical.Tactics.NatSolver.Reflection
+open import Cubical.Tactics.NatSolver
 open import Cubical.Data.Unit
 open import Cubical.Data.Sigma
 
@@ -247,7 +247,7 @@ module _
                   (isEquiv→isConnected _ (𝕁amesPush≃ k .snd) _)))))
 
     nat-path : (n m k : ℕ) → (1 + (k + m)) · n ≡ k · n + (1 + m) · n
-    nat-path = solve
+    nat-path _ _ _ = solveℕ!
 
   -- Connectivity results
 

diff --git a/Cubical/Tactics/CommRingSolver/Reflection.agda b/Cubical/Tactics/CommRingSolver/Reflection.agda
@@ -16,7 +16,6 @@ open import Cubical.Data.Nat.Literals
 open import Cubical.Data.Int.Base hiding (abs)
 open import Cubical.Data.Int using (fromNegℤ; fromNatℤ)
 open import Cubical.Data.Nat using (ℕ; discreteℕ) renaming (_+_ to _+ℕ_)
-open import Cubical.Data.FinData using () renaming (zero to fzero; suc to fsuc)
 open import Cubical.Data.Bool
 open import Cubical.Data.Bool.SwitchStatement
 open import Cubical.Data.Vec using (Vec) renaming ([] to emptyVec; _∷_ to _∷vec_)
@@ -32,14 +31,12 @@ open import Cubical.Tactics.CommRingSolver.Solver renaming (solve to ringSolve)
 
 open import Cubical.Tactics.Reflection
 open import Cubical.Tactics.Reflection.Variables
+open import Cubical.Tactics.Reflection.Utilities
 
 private
   variable
     ℓ : Level
 
-  _==_ = primQNameEquality
-  {-# INLINE _==_ #-}
-
   record RingNames : Type where
     field
       is0 : Name → Bool
@@ -104,13 +101,6 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   open pr
   open RingNames names
 
-  -- error message helper
-  errorOut : List (Arg Term) → TC (Template × Vars)
-  errorOut something = typeError (strErr "CommRingSolver: Don't know what to do with " ∷ map (λ {(arg _ t) → termErr t}) something)
-
-  errorOut' : Term → TC (Template × Vars)
-  errorOut' something = typeError (strErr "CommRingSolver: Don't know what to do with " ∷ termErr something ∷ [])
-
   `0` : List (Arg Term) → TC (Template × Vars)
   `0` [] = returnTC (((λ _ → def (quote 0') (cring v∷ [])) , []))
   `0` (fstcring v∷ xs) = `0` xs
@@ -123,21 +113,20 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   `1` (_ h∷ xs) = `1` xs
   `1` something = errorOut something
 
-  buildExpression' : Term → TC (Template × Vars)
+  buildExpression : Term → TC (Template × Vars)
 
   op2 : Name → Term → Term → TC (Template × Vars)
   op2 op x y = do
-    r1 ← buildExpression' x
-    r2 ← buildExpression' y
+    r1 ← buildExpression x
+    r2 ← buildExpression y
     returnTC ((λ ass → con op (fst r1 ass v∷ fst r2 ass v∷ [])) ,
              appendWithoutRepetition (snd r1) (snd r2))
 
   op1 : Name → Term → TC (Template × Vars)
   op1 op x = do
-    r1 ← buildExpression' x
+    r1 ← buildExpression x
     returnTC ((λ ass → con op (fst r1 ass v∷ [])) , snd r1)
 
-
   `_·_` : List (Arg Term) → TC (Template × Vars)
   `_·_` (_ h∷ xs) = `_·_` xs
   `_·_` (x v∷ y v∷ []) = op2 (quote _·'_) x y
@@ -156,42 +145,37 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   `-_` (_ v∷ x v∷ []) = op1 (quote -'_) x
   `-_` ts = errorOut ts
 
-  finiteNumberAsTerm : Maybe ℕ → Term
-  finiteNumberAsTerm (just ℕ.zero) = con (quote fzero) []
-  finiteNumberAsTerm (just (ℕ.suc n)) = con (quote fsuc) (finiteNumberAsTerm (just n) v∷ [])
-  finiteNumberAsTerm _ = unknown
-
   polynomialVariable : Maybe ℕ → Term
   polynomialVariable n = con (quote ∣) (finiteNumberAsTerm n v∷ [])
 
-  -- buildExpression' : Term → Template × Vars
-  buildExpression' v@(var _ _) =
+  -- buildExpression : Term → Template × Vars
+  buildExpression v@(var _ _) =
     returnTC ((λ ass → polynomialVariable (ass v)) ,
              v ∷ [])
-  buildExpression' t@(def n xs) =
+  buildExpression t@(def n xs) =
     switch (λ f → f n) cases
       case is0 ⇒ `0` xs         break
       case is1 ⇒ `1` xs         break
       case is· ⇒ `_·_` xs       break
       case is+ ⇒ `_+_` xs       break
       case is- ⇒ `-_` xs        break
       default⇒ (returnTC ((λ ass → polynomialVariable (ass t)) , t ∷ []))
-  buildExpression' t@(con n xs) =
+  buildExpression t@(con n xs) =
     switch (λ f → f n) cases
       case is0 ⇒ `0` xs         break
       case is1 ⇒ `1` xs         break
       case is· ⇒ `_·_` xs       break
       case is+ ⇒ `_+_` xs       break
       case is- ⇒ `-_` xs        break
       default⇒ (returnTC ((λ ass → polynomialVariable (ass t)) , t ∷ []))
-  buildExpression' t = errorOut' t
+  buildExpression t = errorOut' t
   -- there should be cases for variables which are functions, those should be detectable by having visible args
   -- there should be cases for definitions (with arguments)
 
   toAlgebraExpression : Term × Term → TC (Term × Term × Vars)
   toAlgebraExpression (lhs , rhs) = do
-      r1 ← buildExpression' lhs
-      r2 ← buildExpression' rhs
+      r1 ← buildExpression lhs
+      r2 ← buildExpression rhs
       vars ← returnTC (appendWithoutRepetition (snd r1) (snd r2))
       returnTC (
         let ass : VarAss
@@ -212,7 +196,7 @@ private
       just (lhs , rhs) ← get-boundary goal
         where
           nothing
-            → typeError(strErr "The CommRingSolver failed to parse the goal"
+            → typeError(strErr "The CommRingSolver failed to parse the goal "
                                ∷ termErr goal ∷ [])
 
       (lhs' , rhs' , vars) ← CommRingReflection.toAlgebraExpression commRing names (lhs , rhs)

diff --git a/Cubical/Tactics/NatSolver.agda b/Cubical/Tactics/NatSolver.agda
@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+{-
+  This is inspired by/copied from:
+  https://github.com/agda/agda-stdlib/blob/master/src/Tactic/MonoidSolver.agda
+  and the 1lab.
+
+  Boilerplate code for calling the ring solver is constructed automatically
+  with agda's reflection features.
+-}
+module Cubical.Tactics.NatSolver where
+
+open import Cubical.Tactics.NatSolver.Reflection public
diff --git a/Cubical/Tactics/NatSolver/Examples.agda b/Cubical/Tactics/NatSolver/Examples.agda
@@ -10,31 +10,19 @@ open import Cubical.Data.Vec.Base
 open import Cubical.Tactics.NatSolver.NatExpression
 open import Cubical.Tactics.NatSolver.HornerForms
 open import Cubical.Tactics.NatSolver.Solver
-open import Cubical.Tactics.NatSolver.Reflection
+open import Cubical.Tactics.NatSolver
 
 private
   variable
     ℓ : Level
 
-module ReflectionSolving where
-  _ : (x y : ℕ) → (x + y) · (x + y) ≡ x · x + 2 · x · y + y · y
-  _ = solve
+module ReflectionSolving (x y : ℕ) where
+  _ : (x + y) · (x + y) ≡ x · x + 2 · x · y + y · y
+  _ = solveℕ!
 
-  _ : (x : ℕ) → suc x ≡ x + 1
-  _ = solve
+  _ : suc x ≡ x + 1
+  _ = solveℕ!
 
-  {-
-    If you want to use the solver in some more complex situation,
-    you have to declare a helper variable (`useSolver` below) that
-    is a term of a dependent function type as above:
-  -}
-  module _ (SomeType : Type ℓ-zero) where
-    complexSolverApplication :
-      (someStuff : SomeType) → (x y : ℕ) → (moreStuff : SomeType)
-      → x + y ≡ y + x
-    complexSolverApplication someStuff x y moreStuff = useSolver x y
-                              where useSolver : (x y : ℕ) → x + y ≡ y + x
-                                    useSolver = solve
 
 module SolvingExplained where
   open EqualityToNormalform renaming (solve to natSolve)
@@ -87,7 +75,6 @@ module SolvingExplained where
   _ : normalize (Z ·' (((K 2) ·' X) ·' Y)) ≡ normalize (Z ·' (Y ·' (X +' X)))
   _ = refl
 
-
   {-
     The solver needs to produce an equality between
     actual ring elements. So we need a proof that