Improve progress

4 files changed, 32 insertions, 18 deletions

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 00b0a478..7eace667 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -58,10 +58,10 @@ section Methods
   def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a)
     (sanityChecks : Bool := false) :
     m a := do
-    trace[Progress] "Theorem: {th}"
+    trace[Progress] "Proposition: {th}"
     -- Dive into the quantified variables and the assumptions
     forallTelescope th fun fvars th => do
-    trace[Progress] "All arguments: {fvars}"
+    trace[Progress] "Universally quantified arguments and assumptions: {fvars}"
   /-  -- Filter the argumens which are not propositions
     let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
       if i ≥ fargs.size then pure i
@@ -83,12 +83,16 @@ section Methods
     -- Dive into the existentials
     existsTelescope th fun evars th => do
     trace[Progress] "Existentials: {evars}"
+    trace[Progress] "Proposition after stripping the quantifiers: {th}"
     -- Take the first conjunct
     let (th, post) ← optSplitConj th
+    trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}"
     -- Destruct the equality
     let (th, ret) ← destEq th
+    trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}"
     -- Destruct the application to get the name
-    th.withApp fun f args => do
+    th.consumeMData.withApp fun f args => do
+    trace[Progress] "After stripping the arguments:\n- f: {f}\n- args: {args}"
     if ¬ f.isConst then throwError "Not a constant: {f}"
     -- Compute the set of universally quantified variables which appear in the function arguments
     let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
@@ -114,6 +118,7 @@ section Methods
       post := post
     }
     k thDesc
+
 end Methods
 
 
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 001967e5..ace92f4f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -55,14 +55,20 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
       let thDecl := env.constants.find! thName
       pure thDecl.type
     | .Local asmDecl => pure asmDecl.type
+  trace[Progress] "theorem/assumption type: {thTy}"
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
   -- withNewMCtxDepth do
   let (mvars, binders, thExBody) ← forallMetaTelescope thTy
+  trace[Progress] "After stripping foralls: {thExBody}"
   -- Introduce the existentially quantified variables and the post-condition
   -- in the context
   let thBody ←
     existsTelescope thExBody fun _evars thBody => do
+    trace[Progress] "After stripping existentials: {thBody}"
+    let (thBody, _) ← optSplitConj thBody
+    trace[Progress] "After splitting the conjunction: {thBody}"
     let (thBody, _) ← destEq thBody
+    trace[Progress] "After splitting equality: {thBody}"
     -- There shouldn't be any existential variables in thBody
     pure thBody
   -- Match the body with the target
@@ -152,6 +158,7 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
   let goalTy ← mgoal.getType
+  trace[Progress] "goal: {goalTy}"
   -- Dive into the goal to lookup the theorem
   let (fName, fLevels, args) ← do
     withPSpec goalTy fun desc =>
@@ -188,7 +195,7 @@ 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}"
+  trace[Progress] "Progress arguments: {args}"
   let args := args.getArgs
   let ids :=
     if args.size > 0 then
@@ -196,7 +203,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
       let args := (args.get! 2).getArgs
       args.map Syntax.getId
     else #[]
-  trace[Progress] "Ids: {ids}"
+  trace[Progress] "User-provided ids: {ids}"
   progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 599c3a9f..9cd0db23 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -43,6 +43,10 @@ namespace List
 
 end List
 
+-- TODO: move?
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
 namespace Lean
 
 namespace LocalContext
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 1db39422..ee22bebd 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -105,6 +105,8 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
         simp [h]
     else
       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]
@@ -112,13 +114,12 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
         simp [h]
         simp [insert_in_list] at hi
         exact hi
-   
-/--
+
 @[pspec]
 theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
     insert_in_list α key value ls = ret b ∧
-    (b = (List.lookup ls.v key = none))
+    (b ↔ (List.lookup ls.v key = none))
   := by
   induction ls
   case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup]
@@ -130,11 +131,12 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α)
      simp [h]
     else
      conv =>
-       rhs; ext; arg 1; simp [h] -- TODO: Simplify
-     simp [insert_in_list] at ih;
-     progress -- TODO: Does not work
---/
-    
+       rhs; ext; left; simp [h] -- TODO: Simplify
+     simp only [insert_in_list] at ih;
+     -- TODO: give the possibility of using underscores
+     progress as ⟨ b h ⟩
+     simp [*]
+
 @[pspec]
 theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) :
   ∃ l1,
@@ -150,8 +152,7 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List
          rw [insert_in_list_loop_back]
          simp [h, List.lookup]
          intro k1 h1
-         have h2 : ¬(key = k1) := by tauto -- TODO: Why is the order of args in eq swapped
-         simp [h2]
+         simp [*]
      else
        by
          simp [insert_in_list_back, List.lookup]
@@ -159,12 +160,9 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List
          simp [h, List.lookup]
          have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress
          simp [insert_in_list_back] at *
-         simp [*]
-         have : ¬ (key = k) := by tauto
          simp [List.lookup, *]
          simp (config := {contextual := true}) [*]
         
 end HashMap
--- def distinct_keys {α : Type u}
 
 end hashmap