add case for 'suc' (#1043)

Cubical/Tactics/NatSolver/Examples.agda

@@ -20,6 +20,9 @@ module ReflectionSolving where
   _ : (x y : ℕ) → (x + y) · (x + y) ≡ x · x + 2 · x · y + y · y
   _ = solve
 
+  _ : (x : ℕ) → 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

Cubical/Tactics/NatSolver/Reflection.agda

@@ -110,18 +110,6 @@ module pr {n : ℕ} where
 module _ where
   open pr
 
-  `0` : List (Arg Term) → Term
-  `0` [] = def (quote 0') []
-  `0` (varg fstcring ∷ xs) = `0` xs
-  `0` (harg _ ∷ xs) = `0` xs
-  `0` _ = unknown
-
-  `1` : List (Arg Term) → Term
-  `1` [] = def (quote 1') []
-  `1` (varg fstcring ∷ xs) = `1` xs
-  `1` (harg _ ∷ xs) = `1` xs
-  `1` _ = unknown
-
   mutual
 
     `_·_` : List (Arg Term) → Term
@@ -138,6 +126,11 @@ module _ where
         (quote _+'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
     `_+_` _ = unknown
 
+    `1+_` : List (Arg Term) → Term
+    `1+_` (varg x ∷ []) =
+      con (quote _+'_) (varg (def (quote 1') []) ∷ varg (buildExpression x) ∷ [])
+    `1+_` _ = unknown
+
     K' : List (Arg Term) → Term
     K' xs = con (quote K) xs
 
@@ -155,8 +148,7 @@ module _ where
         default⇒ (K' xs)
     buildExpression t@(con n xs) =
       switch (n ==_) cases
-        case (quote _·_) ⇒ `_·_` xs   break
-        case (quote _+_) ⇒ `_+_` xs   break
+        case (quote suc) ⇒ `1+_` xs   break
         default⇒ (K' xs)
     buildExpression t = unknown