From d9a11b312ef0df13795d9a1982ca1cd2eba0e124 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 9 Jul 2023 22:27:44 +0200
Subject: Improve int_tac

---
 backends/lean/Base/Arith.lean | 41 ++++++++++++++++++-----------------------
 1 file changed, 18 insertions(+), 23 deletions(-)

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index 8cdf75a3..364447ed 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -183,9 +183,6 @@ elab "display_has_prop_instances" : tactic => do
   hs.forM fun e => do
     trace[Arith] "+ HasProp instance: {e}"
 
-
-set_option trace.Arith true
-
 example (x : U32) : True := by
   let i : HasProp U32 := inferInstance
   have p := @HasProp.prop _ i x
@@ -193,8 +190,6 @@ example (x : U32) : True := by
   display_has_prop_instances
   simp
 
-set_option trace.Arith false
-
 -- Return an instance of `PropHasImp` for `e` if it has some
 def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
   trace[Arith] "lookupPropHasImp"
@@ -223,14 +218,10 @@ elab "display_prop_has_imp_instances" : tactic => do
   hs.forM fun e => do
     trace[Arith] "+ PropHasImp instance: {e}"
 
-set_option trace.Arith true
-
-example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by
+example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by
   display_prop_has_imp_instances
   simp
 
-set_option trace.Arith false
-
 def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
@@ -322,12 +313,15 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
   intro_has_prop_instances
   simp_all [Scalar.max, Scalar.min]
 
--- Tactic to split on a disjunction
+-- Tactic to split on a disjunction.
+-- The expression `h` should be an fvar.
 def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   trace[Arith] "assumption on which to split: {h}"
   -- Retrieve the main goal
   Lean.Elab.Tactic.withMainContext do
   let goalType ← Lean.Elab.Tactic.getMainTarget
+  let hDecl := (← getLCtx).get! h.fvarId!
+  let hName := hDecl.userName
   -- Case disjunction
   let hTy ← inferType h
   hTy.withApp fun f xs => do
@@ -341,14 +335,16 @@ def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM U
   -- - the match branch
   -- - a fresh new mvar id
   let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do
-    -- Introduce a variable for the assumption (`a` or `b`)
-    let asmName ← mkFreshUserName `h
-    withLocalDeclD asmName hTy fun var => do
+    -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse
+    -- the name of the assumption we split.
+    withLocalDeclD hName hTy fun var => do
     -- The new goal
     let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName)
+    -- Clear the assumption that we split
+    let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!]
     -- The branch expression
-    let branch ← mkLambdaFVars #[var] mgoal
-    pure (branch, mgoal.mvarId!)
+    let branch ← mkLambdaFVars #[var] (mkMVar mgoal)
+    pure (branch, mgoal)
   let (inl, mleft) ← mkGoal a "left"
   let (inr, mright) ← mkGoal b "right"
   trace[Arith] "left: {inl}: {mleft}"
@@ -398,8 +394,6 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
   . linarith
   . linarith
 
---syntax "int_tac_preprocess" : tactic
-
 /- Boosting a bit the linarith tac.
 
    We do the following:
@@ -412,7 +406,7 @@ def intTacPreprocess : Tactic.TacticM Unit := do
   -- Lookup the instances of PropHasImp (this is how we detect assumptions
   -- of the proper shape), introduce assumptions in the context and split
   -- on those
-  -- TODO: get rid of the assumption that we split
+  -- TODO: get rid of the assumptions that we split
   let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit :=
     match asms with
     | [] => pure ()
@@ -436,14 +430,16 @@ syntax "int_tac" : tactic
 macro_rules
   | `(tactic| int_tac) =>
     `(tactic|
+      (repeat (apply And.intro)) <;> -- TODO: improve this
       int_tac_preprocess <;>
       linarith)
 
-example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac
+example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
+  int_tac
 
 -- Checking that things append correctly when there are several disjunctions
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
-  int_tac_preprocess <;> apply And.intro <;> linarith
+  int_tac
 
 -- A tactic to solve linear arithmetic goals in the presence of scalars
 syntax "scalar_tac" : tactic
@@ -457,8 +453,7 @@ macro_rules
       have := Scalar.cMax_bound ScalarTy.Isize;
       -- TODO: not too sure about that
       simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *;
-      -- TODO: use int_tac
-      linarith)
+      int_tac)
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   scalar_tac
-- 
cgit v1.2.3