From a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 14:34:55 +0200
Subject: Finish a first version of the progress tactic

---
 backends/lean/Base/Progress/Base.lean     | 24 +--------------------
 backends/lean/Base/Progress/Progress.lean | 36 ++++++++++++++++++++++++-------
 2 files changed, 29 insertions(+), 31 deletions(-)

(limited to 'backends/lean/Base/Progress')

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 3f44f46c..613f38f8 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -10,26 +10,6 @@ open Utils
 -- We can't define and use trace classes in the same file
 initialize registerTraceClass `Progress
 
--- Return the first conjunct if the expression is a conjunction, or the
--- expression itself otherwise. Also return the second conjunct if it is a
--- conjunction.
-def getFirstConj (e : Expr) : MetaM (Expr × Option Expr) := do
-  e.withApp fun f args =>
-  if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
-  else pure (e, none)
-
--- Destruct an equaliy and return the two sides
-def destEq (e : Expr) : MetaM (Expr × Expr) := do
-  e.withApp fun f args =>
-  if f.isConstOf ``Eq ∧ args.size = 3 then pure (args.get! 1, args.get! 2)
-  else throwError "Not an equality: {e}"
-
--- Return the set of FVarIds in the expression
-partial def getFVarIds (e : Expr) (hs : HashSet FVarId := HashSet.empty) : MetaM (HashSet FVarId) := do
-  e.withApp fun body args => do
-  let hs := if body.isFVar then hs.insert body.fvarId! else hs
-  args.foldlM (fun hs arg => getFVarIds arg hs) hs
-
 /- # Progress tactic -/
 
 structure PSpecDesc where
@@ -103,7 +83,7 @@ section Methods
     existsTelescope th fun evars th => do
     trace[Progress] "Existentials: {evars}"
     -- Take the first conjunct
-    let (th, post) ← getFirstConj th
+    let (th, post) ← optSplitConj th
     -- Destruct the equality
     let (th, ret) ← destEq th
     -- Destruct the application to get the name
@@ -169,7 +149,5 @@ initialize pspecAttr : PSpecAttr ← do
 
 def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
   return (s.ext.getState (← getEnv)).find? name
-  --return s.ext.find? (← getEnv) name
-
 
 end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 1b9ee55c..4c68b3bd 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -21,9 +21,6 @@ namespace Test
   #eval pspecAttr.find? ``Primitives.Vec.index
 end Test
 
-#check isDefEq
-#check allGoals
-
 def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
@@ -80,7 +77,28 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   let th ← mkAppOptM thName (mvars.map some)
   let asmName ← mkFreshUserName `h
   let thTy ← inferType th
-  let thAsm ← Utils.addDecl asmName th thTy (asLet := false)
+  let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
+  withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
+  let ngoal ← getMainGoal
+  trace[Progress] "current goal: {ngoal}"
+  trace[Progress] "current goal: {← ngoal.isAssigned}"
+  -- The assumption should be of the shape:
+  -- `∃ x1 ... xn, f args = ... ∧ ...`
+  -- We introduce the existentially quantified variables and split the top-most
+  -- conjunction if there is one
+  splitAllExistsTac thAsm fun h => do
+    -- Split the conjunction
+    let splitConj (k : Expr → TacticM Unit) : TacticM Unit := do
+      if ← isConj (← inferType h) then
+        splitConjTac h (fun h _ => k h)
+      else k h
+    -- Simplify the target by using the equality
+    splitConj fun h => do
+    simpAt [] [] [h.fvarId!] (.targets #[] true)
+    -- Clear the equality
+    let mgoal ← getMainGoal
+    let mgoal ← mgoal.tryClearMany #[h.fvarId!]
+    setGoals (mgoal :: (← getUnsolvedGoals))
   -- Update the set of goals
   let curGoals ← getUnsolvedGoals
   let newGoals := mvars.map Expr.mvarId!
@@ -94,7 +112,7 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   pure ()
 
 elab "progress" : tactic => do
-  progressLookupTheorem (firstTac [assumptionTac, Arith.intTac])
+  progressLookupTheorem (firstTac [assumptionTac, Arith.scalarTac])
 
 namespace Test
   open Primitives
@@ -103,10 +121,12 @@ namespace Test
 
   @[pspec]
   theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
-    ∃ x, v.index α i = .ret x := by
+    ∃ (x: α), v.index α i = .ret x := by
       progress
-      tauto
-      
+      simp
+
+  set_option trace.Progress false
+
 end Test
 
 end Progress
-- 
cgit v1.2.3