From 6166c410a4b3353377e640acbae9f56e877a9118 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jul 2023 15:23:49 +0200
Subject: Work on the progress tactic

---
 backends/lean/Base/Progress/Progress.lean | 112 ++++++++++++++++++++++++++++++
 1 file changed, 112 insertions(+)
 create mode 100644 backends/lean/Base/Progress/Progress.lean

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
new file mode 100644
index 00000000..1b9ee55c
--- /dev/null
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -0,0 +1,112 @@
+import Lean
+import Base.Arith
+import Base.Progress.Base
+
+namespace Progress
+
+open Lean Elab Term Meta Tactic
+open Utils
+
+namespace Test
+  open Primitives
+
+  set_option trace.Progress true
+
+  @[pspec]
+  theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
+    ∃ x, v.index α i = .ret x := by
+      apply
+      sorry
+
+  #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
+  let mgoal ← Tactic.getMainGoal
+  let goalTy ← mgoal.getType
+  -- Dive into the goal to lookup the theorem
+  let (fName, fLevels, args) ← do
+    withPSpec goalTy fun desc =>
+    -- TODO: check that no universally quantified variables in the arguments
+    pure (desc.fName, desc.fLevels, desc.args)
+  -- TODO: also try the assumptions
+  trace[Progress] "Function: {fName}"
+  -- TODO: use a list of theorems, and try them one by one?
+  let thName ← do
+    match ← pspecAttr.find? fName with
+    | none => throwError "Could not find a pspec theorem for {fName}"
+    | some thName => pure thName
+  trace[Progress] "Lookuped up: {thName}"
+  /- Apply the theorem
+     We try to match the theorem with the goal
+     In order to do so, we introduce meta-variables for all the parameters
+     (i.e., quantified variables and assumpions), and unify those with the goal.
+     Remark: we do not introduce meta-variables for the quantified variables
+     which don't appear in the function arguments (we want to let them
+     quantified).
+     We also make sure that all the meta variables which appear in the
+     function arguments have been instantiated
+   -/  
+  let env ← getEnv
+  let thDecl := env.constants.find! thName
+  let thTy := thDecl.type
+  -- TODO: the tactic fails if we uncomment withNewMCtxDepth
+  -- withNewMCtxDepth do
+  let (mvars, binders, thExBody) ← forallMetaTelescope thTy
+  -- Introduce the existentially quantified variables and the post-condition
+  -- in the context
+  let thBody ←
+    existsTelescope thExBody fun _evars thBody => do
+    let (thBody, _) ← destEq thBody
+    -- There shouldn't be any existential variables in thBody
+    pure thBody
+  -- Match the body with the target
+  let target := mkAppN (.const fName fLevels) args
+  trace[Progress] "mvars:\n{mvars.map Expr.mvarId!}"
+  trace[Progress] "thBody: {thBody}"
+  trace[Progress] "target: {target}"
+  let ok ← isDefEq thBody target
+  if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {target}"
+  postprocessAppMVars `progress mgoal mvars binders true true
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let thBody ← instantiateMVars thBody
+  trace[Progress] "thBody (after instantiation): {thBody}"
+  -- Add the instantiated theorem to the assumptions (we apply it on the metavariables).
+  let th ← mkAppOptM thName (mvars.map some)
+  let asmName ← mkFreshUserName `h
+  let thTy ← inferType th
+  let thAsm ← Utils.addDecl asmName th thTy (asLet := false)
+  -- Update the set of goals
+  let curGoals ← getUnsolvedGoals
+  let newGoals := mvars.map Expr.mvarId!
+  let newGoals ← newGoals.filterM fun mvar => not <$> mvar.isAssigned
+  trace[Progress] "new goals: {newGoals}"
+  setGoals newGoals.toList
+  allGoals asmTac
+  let newGoals ← getUnsolvedGoals
+  setGoals (newGoals ++ curGoals)
+  -- 
+  pure ()
+
+elab "progress" : tactic => do
+  progressLookupTheorem (firstTac [assumptionTac, Arith.intTac])
+
+namespace Test
+  open Primitives
+
+  set_option trace.Progress true
+
+  @[pspec]
+  theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
+    ∃ x, v.index α i = .ret x := by
+      progress
+      tauto
+      
+end Test
+
+end Progress
-- 
cgit v1.2.3