3 files changed, 21 insertions, 5 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