Improve progress to use assumptions and start working on a nice syntax

5 files changed, 140 insertions, 95 deletions

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 20420f36..ab4fd182 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -11,49 +11,9 @@ import Base.Primitives
 import Base.Utils
 import Base.Arith.Base
 
-/-
-Mathlib tactics:
-- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
-- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
-- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
-- should we use linarith or omega?
-- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
-- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
--/
-
-namespace List
-
-  -- TODO: I could not find this function??
-  @[simp] def flatten {a : Type u} : List (List a) → List a
-  | [] => []
-  | x :: ls => x ++ flatten ls
-
-end List
-
-namespace Lean
-
-namespace LocalContext
-
-  open Lean Lean.Elab Command Term Lean.Meta
-
-  -- Small utility: return the list of declarations in the context, from
-  -- the last to the first.
-  def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) :=
-    lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) []
-
-  -- Return the list of declarations in the context, but filter the
-  -- declarations which are considered as implementation details
-  def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do
-    let ls ← lctx.getAllDecls
-    pure (ls.filter (fun d => not d.isImplementationDetail))
-
-end LocalContext
-
-end Lean
-
 namespace Arith
 
-open Primitives
+open Primitives Utils
 
 -- TODO: move?
 theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index d2c91ff8..0a9ea4c4 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -6,28 +6,6 @@ import Mathlib.Tactic.Linarith
 
 import Base.Primitives
 
-/-
-TODO:
-- we want an easier to use cases:
-  - keeps in the goal an equation of the shape: `t = case`
-  - if called on Prop terms, uses Classical.em
-  Actually, the cases from mathlib seems already quite powerful
-  (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases)
-  For instance: cases h : e
-  Also: **casesm**
-- better split tactic
-- we need conversions to operate on the head of applications.
-  Actually, something like this works:
-  ```
-  conv at Hl =>
-    apply congr_fun
-    simp [fix_fuel_P]
-  ```
-  Maybe we need a rpt ... ; focus?
-- simplifier/rewriter have a strange behavior sometimes
--/
-
-
 /- TODO: this is very useful, but is there more? -/
 set_option profiler true
 set_option profiler.threshold 100
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 613f38f8..a288d889 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -60,7 +60,7 @@ section Methods
     trace[Progress] "Theorem: {th}"
     -- Dive into the quantified variables and the assumptions
     forallTelescope th fun fvars th => do
-    trace[Progress] "All argumens: {fvars}"
+    trace[Progress] "All arguments: {fvars}"
   /-  -- Filter the argumens which are not propositions
     let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
       if i ≥ fargs.size then pure i
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a4df5c96..b0db465d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -21,24 +21,11 @@ namespace Test
   #eval pspecAttr.find? ``Primitives.Vec.index
 end Test
 
-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}"
+inductive TheoremOrLocal where
+| Theorem (thName : Name)
+| Local (asm : LocalDecl)
+
+def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
   /- 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
@@ -48,10 +35,14 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
      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
+  let thTy ← do
+    match th with
+    | .Theorem thName =>
+      let thDecl := env.constants.find! thName
+      pure thDecl.type
+    | .Local asmDecl => pure asmDecl.type
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
   -- withNewMCtxDepth do
   let (mvars, binders, thExBody) ← forallMetaTelescope thTy
@@ -63,18 +54,19 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
     -- 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}"
+  trace[Progress] "Maching `{thBody}` with `{fnExpr}`"
+  let ok ← isDefEq thBody fnExpr
+  if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fnExpr}"
+  let mgoal ← Tactic.getMainGoal
   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 th ← do
+    match th with
+    | .Theorem thName => mkAppOptM thName (mvars.map some)
+    |  .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
   let asmName ← mkFreshUserName `h
   let thTy ← inferType th
   let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
@@ -112,18 +104,71 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   -- 
   pure ()
 
-elab "progress" : tactic => do
-  progressLookupTheorem (firstTac [assumptionTac, Arith.scalarTac])
+-- The array of ids are identifiers to use when introducing fresh variables
+def progressAsmsOrLookupTheorem (ids : Array Name) (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: this should be in the pspec desc
+  let fnExpr := mkAppN (.const fName fLevels) args
+  trace[Progress] "Function: {fName}"
+  -- Try all the assumptions one by one and if it fails try to lookup a theorem
+  let ctx ← Lean.MonadLCtx.getLCtx
+  let decls ← ctx.getDecls
+  for decl in decls.reverse do
+    trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
+    try
+      progressWith fnExpr (.Local decl) ids asmTac
+      return ()
+    catch _ => continue
+  -- It failed: try to lookup a theorem
+  -- TODO: use a list of theorems, and try them one by one?
+  trace[Progress] "No assumption succeeded: trying to lookup a theorem"
+  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
+  progressWith fnExpr (.Theorem thName) ids asmTac
+
+#check Syntax
+syntax progressArgs := ("as" " ⟨ " (ident)+ " ⟩")?
+
+def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
+  let args := args.raw
+  -- Process the arguments to retrieve the identifiers to use
+  trace[Progress] "Progressing arguments: {args}"
+  let args := args.getArgs
+  let ids :=
+    if args.size > 0 then
+      let args := (args.get! 0).getArgs
+      let args := (args.get! 2).getArgs
+      args.map Syntax.getId
+    else #[]
+  trace[Progress] "Ids: {ids}"
+  --if args[0] ≠ some "as" then throwError "Invalid syntax: should be: `progress as ⟨ ... ⟩`"
+  progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
+
+elab "progress" args:progressArgs : tactic =>
+  evalProgress args
 
 namespace Test
   open Primitives
 
   set_option trace.Progress true
+  set_option pp.rawOnError 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
+      progress as ⟨ x y z ⟩
       simp
 
   set_option trace.Progress false
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 14feb567..505412b9 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -2,6 +2,68 @@ import Lean
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.LeftRight
 
+/-
+Mathlib tactics:
+- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
+- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
+- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
+- should we use linarith or omega?
+- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
+- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
+-/
+
+/-
+TODO:
+- we want an easier to use cases:
+  - keeps in the goal an equation of the shape: `t = case`
+  - if called on Prop terms, uses Classical.em
+  Actually, the cases from mathlib seems already quite powerful
+  (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases)
+  For instance: cases h : e
+  Also: **casesm**
+- better split tactic
+- we need conversions to operate on the head of applications.
+  Actually, something like this works:
+  ```
+  conv at Hl =>
+    apply congr_fun
+    simp [fix_fuel_P]
+  ```
+  Maybe we need a rpt ... ; focus?
+- simplifier/rewriter have a strange behavior sometimes
+-/
+
+
+namespace List
+
+  -- TODO: I could not find this function??
+  @[simp] def flatten {a : Type u} : List (List a) → List a
+  | [] => []
+  | x :: ls => x ++ flatten ls
+
+end List
+
+namespace Lean
+
+namespace LocalContext
+
+  open Lean Lean.Elab Command Term Lean.Meta
+
+  -- Small utility: return the list of declarations in the context, from
+  -- the last to the first.
+  def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) :=
+    lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) []
+
+  -- Return the list of declarations in the context, but filter the
+  -- declarations which are considered as implementation details
+  def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do
+    let ls ← lctx.getAllDecls
+    pure (ls.filter (fun d => not d.isImplementationDetail))
+
+end LocalContext
+
+end Lean
+
 namespace Utils
 
 open Lean Elab Term Meta Tactic