Fix a minor issue with the progress tactic

2 files changed, 112 insertions, 82 deletions

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 935af3f5..a64212a5 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -22,8 +22,9 @@ structure PSpecDesc where
   evars : Array Expr
   -- The function applied to its arguments
   fArgsExpr : Expr
-  -- The function
-  fName : Name
+  -- ⊤ if the function is a constant (must be if we are registering a theorem,
+  -- but is not necessarily the case if we are looking at a goal)
+  fIsConst : Bool
   -- The function arguments
   fLevels : List Level
   args : Array Expr
@@ -98,7 +99,12 @@ section Methods
         pure (mExpr, mf, margs)
     let (fArgsExpr, f, args) ← strip_monad mExpr
     trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
-    if ¬ f.isConst then throwError "Not a constant: {f}"
+    let fLevels ← do
+      -- If we are registering a theorem, then the function must be a constant
+      if ¬ f.isConst then
+        if isGoal then pure []
+        else throwError "Not a constant: {f}"
+      else pure f.constLevels!
     -- *Sanity check* (activated if we are analyzing a theorem to register it in a DB)
     -- Check if some existentially quantified variables
     let _ := do
@@ -117,8 +123,8 @@ section Methods
       fvars := fvars
       evars := evars
       fArgsExpr
-      fName := f.constName!
-      fLevels := f.constLevels!
+      fIsConst := f.isConst
+      fLevels
       args := args
       ret := ret
       post := post
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 0fb276aa..dc30c441 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -106,7 +106,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
   withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
   let ngoal ← getMainGoal
   trace[Progress] "current goal: {ngoal}"
-  trace[Progress] "current goal: {← ngoal.isAssigned}"
+  trace[Progress] "current goal is assigned: {← ngoal.isAssigned}"
   -- The assumption should be of the shape:
   -- `∃ x1 ... xn, f args = ... ∧ ...`
   -- We introduce the existentially quantified variables and split the top-most
@@ -131,50 +131,59 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     -- then continue splitting the post-condition
     splitEqAndPost fun hEq hPost ids => do
     trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
-    tryTac (
-      simpAt true []
-             [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
-             [hEq.fvarId!] (.targets #[] true))
-    -- TODO: remove this (some types get unfolded too much: we "fold" them back)
-    tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
-    -- 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 post following the user's instructions
-    match hPost with
-    | none =>
-      -- Sanity check
-      if ¬ ids.isEmpty then
-        return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
-      else return .Ok
-    | some hPost => do
-      let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids0 : List (Option Name)) : TacticM ProgressError := do
-        match ids0 with
-        | [] =>
-          /- We used all the user provided ids.
-             Split the remaining conjunctions by using fresh ids if the user
-             instructed to fully split the post-condition, otherwise stop -/
-          if splitPost then
-            splitFullConjTac true hPost (λ _ => pure .Ok)
-          else pure .Ok
-        | nid :: ids => do
-          trace[Progress] "Splitting post: {← inferType hPost}"
-          -- Split
-          let nid ← do
-            match nid with
-            | none => mkFreshAnonPropUserName
-            | some nid => pure nid
-          trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
-          if ← isConj (← inferType hPost) then
-            splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
-          else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
-      let curPostId := (← hPost.fvarId!.getDecl).userName
-      splitPostWithIds curPostId hPost ids
+    trace[Progress] "current goal: {← getMainGoal}"
+    Tactic.focus do
+    let _ ←
+      tryTac
+        (simpAt true []
+               [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+               [hEq.fvarId!] (.targets #[] true))
+    -- It may happen that at this point the goal is already solved (though this is rare)
+    -- TODO: not sure this is the best way of checking it
+    if (← getUnsolvedGoals) == [] then pure .Ok
+    else
+       trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
+       -- TODO: remove this (some types get unfolded too much: we "fold" them back)
+       let _ ← tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
+       trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
+       -- 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 post following the user's instructions
+       match hPost with
+       | none =>
+         -- Sanity check
+         if ¬ ids.isEmpty then
+           return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
+         else return .Ok
+       | some hPost => do
+         let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids0 : List (Option Name)) : TacticM ProgressError := do
+           match ids0 with
+           | [] =>
+             /- We used all the user provided ids.
+                Split the remaining conjunctions by using fresh ids if the user
+                instructed to fully split the post-condition, otherwise stop -/
+             if splitPost then
+               splitFullConjTac true hPost (λ _ => pure .Ok)
+             else pure .Ok
+           | nid :: ids => do
+             trace[Progress] "Splitting post: {← inferType hPost}"
+             -- Split
+             let nid ← do
+               match nid with
+               | none => mkFreshAnonPropUserName
+               | some nid => pure nid
+             trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
+             if ← isConj (← inferType hPost) then
+               splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
+             else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
+         let curPostId := (← hPost.fvarId!.getDecl).userName
+         splitPostWithIds curPostId hPost ids
   match res with
   | .Error _ => return res -- Can we get there? We're using "return"
   | .Ok =>
@@ -223,9 +232,9 @@ def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost :
           pure (some res)
         catch _ => none
   match res with
-  | some .Ok => return true
+  | some .Ok => pure true
   | some (.Error msg) => throwError msg
-  | none => return false
+  | none => pure false
 
 -- The array of ids are identifiers to use when introducing fresh variables
 def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal)
@@ -266,36 +275,42 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
-    -- It failed: lookup the pspec theorems which match the expression
-    trace[Progress] "No assumption succeeded: trying to lookup a pspec theorem"
-    let pspecs : Array TheoremOrLocal ← do
-      let thNames ← pspecAttr.find? fExpr
-      -- TODO: because of reduction, there may be several valid theorems (for
-      -- instance for the scalars). We need to sort them from most specific to
-      -- least specific. For now, we assume the most specific theorems are at
-      -- the end.
-      let thNames := thNames.reverse
-      trace[Progress] "Looked up pspec theorems: {thNames}"
-      pure (thNames.map fun th => TheoremOrLocal.Theorem th)
-    -- Try the theorems one by one
-    for pspec in pspecs do
-      if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return ()
-      else pure ()
-    -- It failed: try to use the recursive assumptions
-    trace[Progress] "Failed using a pspec theorem: trying to use a recursive assumption"
-    -- We try to apply the assumptions of kind "auxDecl"
-    let ctx ← Lean.MonadLCtx.getLCtx
-    let decls ← ctx.getAllDecls
-    let decls := decls.filter (λ decl => match decl.kind with
-      | .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 fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
-      match res with
-      | .Ok => return ()
-      | .Error msg => throwError msg
-    -- Nothing worked: failed
-    throwError "Progress failed"
+    -- It failed: lookup the pspec theorems which match the expression *only
+    -- if the function is a constant*
+    let fIsConst ← do
+      fExpr.consumeMData.withApp fun mf _ => do
+      pure mf.isConst
+    if ¬ fIsConst then throwError "Progress failed"
+    else do
+      trace[Progress] "No assumption succeeded: trying to lookup a pspec theorem"
+      let pspecs : Array TheoremOrLocal ← do
+        let thNames ← pspecAttr.find? fExpr
+        -- TODO: because of reduction, there may be several valid theorems (for
+        -- instance for the scalars). We need to sort them from most specific to
+        -- least specific. For now, we assume the most specific theorems are at
+        -- the end.
+        let thNames := thNames.reverse
+        trace[Progress] "Looked up pspec theorems: {thNames}"
+        pure (thNames.map fun th => TheoremOrLocal.Theorem th)
+      -- Try the theorems one by one
+      for pspec in pspecs do
+        if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return ()
+        else pure ()
+      -- It failed: try to use the recursive assumptions
+      trace[Progress] "Failed using a pspec theorem: trying to use a recursive assumption"
+      -- We try to apply the assumptions of kind "auxDecl"
+      let ctx ← Lean.MonadLCtx.getLCtx
+      let decls ← ctx.getAllDecls
+      let decls := decls.filter (λ decl => match decl.kind with
+        | .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 fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
+        match res with
+        | .Ok => return ()
+        | .Error msg => throwError msg
+      -- Nothing worked: failed
+      throwError "Progress failed"
 
 syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?
 
@@ -434,6 +449,15 @@ namespace Test
     progress
     simp [*]
 
+  /- Checking the case where simplifying the goal after instantiating the
+     pspec theorem the goal actually solves it, and where the function is
+     not a constant. We also test the case where the function under scrutinee
+     is not a constant. -/
+  example {x : U32}
+    (f : U32 → Result Unit) (h : ∀ x, f x = .ret ()) :
+    f x = ret () := by
+    progress
+
 end Test
 
 end Progress