Improve progress further and move some lemmas

3 files changed, 109 insertions, 105 deletions

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index ddb10236..1773e593 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -175,6 +175,73 @@ theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
     apply hi
     linarith
 
+@[simp]
+theorem index_ne
+  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
+   0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i →
+    (l.update i x).index j = l.index j
+  :=
+  λ _ _ _ _ _ => match l with
+  | [] => by simp at *
+  | hd :: tl =>
+    if h: i = 0 then
+      have : j ≠ 0 := by scalar_tac
+      by simp [*]
+    else if h : j = 0 then
+      have : i ≠ 0 := by scalar_tac
+      by simp [*]
+    else
+      by
+        simp [*]
+        simp at *
+        apply index_ne <;> scalar_tac
+
+@[simp]
+theorem index_eq
+  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) :
+   0 ≤ i → i < l.len →
+    (l.update i x).index i = x
+  :=
+  fun _ _ => match l with
+  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
+  | hd :: tl =>
+    if h: i = 0 then
+      by
+        simp [*]
+    else
+      by
+        simp [*]
+        simp at *
+        apply index_eq <;> scalar_tac
+
+def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
+  foldr (fun a r => p a ∧ r) True l
+
+@[simp]
+theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p :=
+  by simp [allP, foldr]
+
+@[simp]
+theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) :
+  allP (hd :: tl) p ↔ p hd ∧ allP tl p
+  := by simp [allP, foldr]
+
+def pairwise_rel
+  {α : Type u} (rel : α → α → Prop) (l: List α) : Prop
+  := match l with
+  | [] => True
+  | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
+
+@[simp]
+theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) :
+  pairwise_rel rel []
+  := by simp [pairwise_rel]
+
+@[simp]
+theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) :
+  pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl
+  := by simp [pairwise_rel]
+
 end Lemmas
 
 end List
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 974a6364..1f734415 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -39,7 +39,7 @@ inductive ProgressError
 | Error (msg : MessageData)
 deriving Inhabited
 
-def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
+def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name)
   (asmTac : TacticM Unit) : TacticM ProgressError := do
   /- Apply the theorem
      We try to match the theorem with the goal
@@ -88,7 +88,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
     match th with
     | .Theorem thName => mkAppOptM thName (mvars.map some)
     | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
-  let asmName ← mkFreshUserName `h
+  let asmName ← do match keep with | none => mkFreshUserName `h | some n => do pure n
   let thTy ← inferType th
   let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
   withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
@@ -109,7 +109,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
       if ← isConj (← inferType h) then do
         let hName := (← h.fvarId!.getDecl).userName
         let (optId, ids) := listTryPopHead ids
-        let optIds := match optId with | none => none | some id => some (hName, id)
+        let optIds ← match optId with
+          | none => do pure (some (hName, ← mkFreshUserName `h))
+          | some id => do pure (some (hName, id))
         splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids)
       else k h none ids
     -- Simplify the target by using the equality and some monad simplifications,
@@ -118,9 +120,12 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
     trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
     simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
            [hEq.fvarId!] (.targets #[] true)
-    -- Clear the equality
-    let mgoal ← getMainGoal
-    let mgoal ← mgoal.tryClearMany #[hEq.fvarId!]
+    -- Clear the equality, unless the user requests not to do so
+    let mgoal ← do
+      if keep.isSome then getMainGoal
+      else do
+        let mgoal ← getMainGoal
+        mgoal.tryClearMany #[hEq.fvarId!]
     setGoals (mgoal :: (← getUnsolvedGoals))
     trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}"
     -- Continue splitting following the ids provided by the user
@@ -170,7 +175,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do
 
 /- Helper: try to lookup a theorem and apply it, or continue with another tactic
    if it fails -/
-def tryLookupApply (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
+def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
   (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
   let res ← do
     match th with
@@ -182,7 +187,7 @@ def tryLookupApply (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
       -- Apply the theorem
       let res ← do
         try
-          let res ← progressWith fnExpr th ids asmTac
+          let res ← progressWith fnExpr th keep ids asmTac
           pure (some res)
         catch _ => none
   match res with
@@ -191,7 +196,7 @@ def tryLookupApply (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
   | none => x
 
 -- The array of ids are identifiers to use when introducing fresh variables
-def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
+def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
@@ -209,7 +214,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
   -- Otherwise, lookup one.
   match withTh with
   | some th => do
-    match ← progressWith fnExpr th ids asmTac with
+    match ← progressWith fnExpr th keep ids asmTac with
     | .Ok => return ()
     | .Error msg => throwError msg
   | none =>
@@ -218,7 +223,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
     let decls ← ctx.getDecls
     for decl in decls.reverse do
       trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
-      let res ← do try progressWith fnExpr (.Local decl) ids asmTac catch _ => continue
+      let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
@@ -228,7 +233,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
     let pspec ← do
       let thName ← pspecAttr.find? fName
       pure (thName.map fun th => .Theorem th)
-    tryLookupApply ids asmTac fnExpr "pspec theorem" pspec do
+    tryLookupApply keep ids asmTac fnExpr "pspec theorem" pspec do
     -- It failed: try to lookup a *class* expr spec theorem (those are more
     -- specific than class spec theorems)
     let pspecClassExpr ← do
@@ -237,7 +242,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
       | some arg => do
         let thName ← pspecClassExprAttr.find? fName arg
         pure (thName.map fun th => .Theorem th)
-    tryLookupApply ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do
+    tryLookupApply keep ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do
     -- It failed: try to lookup a *class* spec theorem
     let pspecClass ← do
       match ← getFirstArgAppName args with
@@ -245,7 +250,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
       | some argName => do
         let thName ← pspecClassAttr.find? fName argName
         pure (thName.map fun th => .Theorem th)
-    tryLookupApply ids asmTac fnExpr "pspec class theorem" pspecClass do
+    tryLookupApply keep ids asmTac fnExpr "pspec class theorem" pspecClass do
     -- Try a recursive call - we try the assumptions of kind "auxDecl"
     let ctx ← Lean.MonadLCtx.getLCtx
     let decls ← ctx.getAllDecls
@@ -253,21 +258,29 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
       | .default | .implDetail => false | .auxDecl => true)
     for decl in decls.reverse do
       trace[Progress] "Trying recursive assumption: {decl.userName} : {decl.type}"
-      let res ← do try progressWith fnExpr (.Local decl) ids asmTac catch _ => continue
+      let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
     -- Nothing worked: failed
     throwError "Progress failed"
 
-syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
+syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("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] "Progress arguments: {args}"
   let args := args.getArgs
-  let withArg := (args.get! 0).getArgs
+  let keep : Option Name ← do
+    let args := (args.get! 0).getArgs
+    if args.size > 0 then do
+      let args := (args.get! 1).getArgs
+      if args.size > 0 then pure (some (args.get! 1).getId)
+      else do pure (some (← mkFreshUserName `h))
+    else pure none
+  trace[Progress] "Keep: {keep}"
+  let withArg := (args.get! 1).getArgs
   let withArg ← do
     if withArg.size > 0 then
       let id := withArg.get! 1
@@ -287,11 +300,11 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
         | id :: _ =>
           pure (some (.Theorem id))
     else pure none
-  let args := (args.get! 1).getArgs
+  let args := (args.get! 2).getArgs
   let args := (args.get! 2).getArgs
   let ids := args.map Syntax.getId
   trace[Progress] "User-provided ids: {ids}"
-  progressAsmsOrLookupTheorem withArg ids (firstTac [assumptionTac, Arith.scalarTac])
+  progressAsmsOrLookupTheorem keep withArg ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
@@ -306,11 +319,11 @@ namespace Test
   #eval showStoredPSpec
   #eval showStoredPSpecClass
 
-  theorem Scalar.add_spec {ty} {x y : Scalar ty}
+  theorem Scalar.add_spec1 {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
     ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
-    progress
+    progress keep as h with Scalar.add_spec as ⟨ z ⟩
     simp [*]
 
 /-
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 3b9b960f..baa8f5c8 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -3,75 +3,6 @@ import Hashmap.Funs
 open Primitives
 open Result
 
-namespace List
-
-theorem index_ne
-  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
-   0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i →
-    (l.update i x).index j = l.index j
-  :=
-  λ _ _ _ _ _ => match l with
-  | [] => by simp at *
-  | hd :: tl =>
-    if h: i = 0 then
-      have : j ≠ 0 := by scalar_tac
-      by simp [*]
-    else if h : j = 0 then
-      have : i ≠ 0 := by scalar_tac
-      by simp [*]
-    else
-      by
-        simp [*]
-        simp at *
-        apply index_ne <;> scalar_tac
-
-theorem index_eq
-  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) :
-   0 ≤ i → i < l.len →
-    (l.update i x).index i = x
-  :=
-  fun _ _ => match l with
-  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
-  | hd :: tl =>
-    if h: i = 0 then
-      by
-        simp [*]
-    else
-      by
-        simp [*]
-        simp at *
-        apply index_eq <;> scalar_tac
-
-def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
-  foldr (fun a r => p a ∧ r) True l
-
-@[simp]
-theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p :=
-  by simp [allP, foldr]
-
-@[simp]
-theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) :
-  allP (hd :: tl) p ↔ p hd ∧ allP tl p
-  := by simp [allP, foldr]
-
-def pairwise_rel 
-  {α : Type u} (rel : α → α → Prop) (l: List α) : Prop
-  := match l with
-  | [] => True
-  | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
-
-@[simp]
-theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) :
-  pairwise_rel rel []
-  := by simp [pairwise_rel]
-
-@[simp]
-theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) :
-  pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl
-  := by simp [pairwise_rel]
-
-end List
-
 namespace hashmap
 
 namespace List
@@ -104,18 +35,16 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
         rw [insert_in_list_loop]
         simp [h]
     else
+      have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
       by
-        -- TODO: use progress: detect that this is a recursive call, or give
-        -- the possibility of specifying an identifier
-        have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
         exists b
         simp [insert_in_list, List.lookup]
-        rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion
+        rw [insert_in_list_loop] -- TODO: Using simp leads to infinite recursion
         simp [h]
         simp [insert_in_list] at hi
         exact hi
 
-set_option trace.Progress true
+-- Variation: use progress
 @[pspec]
 theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
@@ -134,18 +63,13 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α)
         simp only [insert_in_list]
         rw [insert_in_list_loop]
         conv => rhs; ext; simp [*]
-        progress as ⟨ b hi ⟩
-
-        -- TODO: use progress: detect that this is a recursive call, or give
-        -- the possibility of specifying an identifier
-        have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
+        progress keep as heq as ⟨ b hi ⟩
+        simp only [insert_in_list] at heq
         exists b
-        simp [insert_in_list, List.lookup]
-        rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion
-        simp [h]
-        simp [insert_in_list] at hi
-        exact hi
+        simp only [heq, hi]
+        simp [*, List.lookup]
 
+-- Variation: use tactics from the beginning
 @[pspec]
 theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,