Improve `scalar_tac` and `scalar_decr_tac` (#256)

* Fix an issue in a proof of the hashmap

* Improve scalar_decr_tac

* Improve the error message of scalar_tac and add the missing Termination.lean

2 files changed, 13 insertions, 17 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index b1927cfd..958e31c9 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -106,19 +106,26 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
   Tactic.withMainContext do
   -- Get the local context
   let ctx ← Lean.MonadLCtx.getLCtx
-  -- Just a matter of precaution
-  let ctx ← instantiateLCtxMVars ctx
   -- Initialize the hashset
   let hs := HashSet.empty
   -- Explore the declarations
   let decls ← ctx.getDecls
   let hs ← decls.foldlM (fun hs d => do
     -- Collect instances over all subexpressions in the context.
-    -- Note that we explore the *type* of the local declarations: if we have
+    -- Note that if the local declaration is
+    -- Note that we explore the *type* of propositions: if we have
     -- for instance `h : A ∧ B` in the context, the expression itself is simply
     -- `h`; the information we are interested in is its type.
-    let ty ← Lean.Meta.inferType d.toExpr
-    collectInstances k hs ty
+    -- However, if the decl is not a proposition, we explore it directly.
+    -- For instance: `x : U32`
+    -- TODO: case disjunction on whether the local decl is a Prop or not. If prop,
+    -- we need to explore its type.
+    let d := d.toExpr
+    if d.isProp then
+      collectInstances k hs d
+    else
+      let ty ← Lean.Meta.inferType d
+      collectInstances k hs ty
   ) hs
   -- Also explore the goal
   collectInstances k hs (← Tactic.getMainTarget)
@@ -296,7 +303,7 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess :  Tactic
     try do Tactic.Omega.omegaTactic {}
     catch _ =>
       let g ← Tactic.getMainGoal
-      throwError "{tacName} failed to prove the goal:\n{g}"
+      throwError "{tacName} failed to prove the goal below.\n\nNote that {tacName} is equivalent to:\n  {tacName}_preprocess; omega\n\nGoal: \n{g}"
 
 elab "int_tac" args:(" split_goal"?): tactic =>
   let split := args.raw.getArgs.size > 0
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 31110b95..a36aadf3 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -44,17 +44,6 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
 elab "scalar_tac" : tactic =>
   scalarTac false
 
--- For termination proofs
-syntax "scalar_decr_tac" : tactic
-macro_rules
-  | `(tactic| scalar_decr_tac) =>
-    `(tactic|
-      simp_wf;
-      -- TODO: don't use a macro (namespace problems)
-      (first | apply Arith.to_int_to_nat_lt
-             | apply Arith.to_int_sub_to_nat_lt) <;>
-      simp_all <;> scalar_tac)
-
 instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
   -- prop_ty is inferred
   prop := λ x => And.intro x.hmin x.hmax