fix: finish? checks whether solver propagation steps are needed (#10949)

This PR ensures that solver propagation steps are necessary in the
generated tactic script to close the goal.

It produces more compact proof scripts, but this is not just an
optimization, if we include an unnecessary step, we may fail to replay
the generated script when `cases` steps are pruned using
non-chronological backtracking (NCB). For example, when executing
`finish?`, we may have performed a `cases #<anchor>` step that enabled
`ring` to propagate a new fact. If this fact is not used in the final
proof, and the corresponding `cases #<anchor>` step is pruned by NCB,
the `ring` step will fail during replay.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Action.lean

@@ -257,22 +257,6 @@ def terminalAction (check : GoalM Bool) (mkTac : GrindM (TSyntax `grind)) : Acti
   else
     kna goal'
 
-/--
-Helper action for satellite solvers that use `CheckResult`.
--/
-def solverAction (check : GoalM CheckResult) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
-  let (result, goal') ← GoalM.run goal check
-  match result with
-  | .none       => kna goal'
-  | .progress   => kp goal'
-  | .propagated =>
-    let goal' ← GoalM.run' goal' processNewFacts
-    if goal'.inconsistent then
-      closeWith mkTac
-    else
-      concatTactic (← kp goal') mkTac
-  | .closed     => closeWith mkTac
-
 def saveStateIfTracing : GrindM (Option SavedState) := do
   if (← getConfig).trace then
     return some (← saveState)
@@ -309,6 +293,40 @@ def checkTactic : Action := fun goal _ kp => do
     return r
   | _ => return r
 
+/--
+Helper action for satellite solvers that use `CheckResult`.
+-/
+def solverAction (check : GoalM CheckResult) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
+  let saved? ← saveStateIfTracing
+  let (result, goal') ← GoalM.run goal check
+  match result with
+  | .none       => kna goal'
+  | .progress   => kp goal'
+  | .propagated =>
+    let goal' ← GoalM.run' goal' processNewFacts
+    if goal'.inconsistent then
+      closeWith mkTac
+    else if (← getConfig).trace then
+      match (← kp goal') with
+      | .closed seq =>
+        /-
+        **Note**: Check whether the progress made by this solver was actually used to close the goal.
+        This is not just an optimization, if we include an unnecessary step, we may fail to replay
+        the generated script when `cases` steps are pruned using non-chronological backtracking (NCB).
+        For example, when executing `finish?`, we may have performed a `cases #<anchor>` step
+        that enabled `ring` to propagate a new fact. If this fact is not used in the final proof,
+        and the corresponding `cases #<anchor>` step is pruned by NCB, the `ring` step will fail during replay.
+        -/
+        if (← checkSeqAt saved? goal seq) then
+          return .closed seq
+        else
+          let tac ← mkTac
+          return .closed (tac :: seq)
+      | r => return r
+    else
+      kp goal'
+  | .closed     => closeWith mkTac
+
 section
 /-!
 Some sanity check properties.

tests/lean/run/grind_finish_trace.lean

@@ -2,7 +2,7 @@ open Lean Grind
 
 /--
 info: Try this:
-  [apply] cases #c4b6 <;> ring <;> cases #4c68 <;> ring
+  [apply] cases #c4b6 <;> cases #4c68 <;> ring
 -/
 #guard_msgs in
 example {α : Type} [CommRing α] (a b c d e : α) :
@@ -30,9 +30,7 @@ example (p : Nat → Prop) (x y z w : Int) :
 
 /--
 info: Try this:
-  [apply] ⏎
-    ac
-    cases #5c4b <;> cases #896f <;> ac
+  [apply] cases #5c4b <;> cases #896f <;> ac
 -/
 #guard_msgs in
 example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d e : α) :
@@ -68,12 +66,10 @@ info: Try this:
   [apply] ⏎
     cases #c4b6
     next =>
-      ring
       cases #8c9f
       next => ring
       next => sorry
     next =>
-      ring
       cases #8c9f
       next => ring
       next => sorry
@@ -91,11 +87,28 @@ info: Try this:
     instantiate only [= Nat.min_def]
     cases #7640
     next => sorry
-    next =>
-      ring
-      lia
+    next => lia
 -/
 #guard_msgs in
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
     (_ : ¬as.size = 0) : min lo (as.size - 1) < i := by
   grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    instantiate only [= getMsbD_setWidth']
+    cases #aa9d
+-/
+#guard_msgs in
+open BitVec in
+example (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsbD (setWidth' ge x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
+  grind => finish?
+
+open BitVec in
+example (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsbD (setWidth' ge x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
+  grind =>
+    instantiate only [= getMsbD_setWidth']
+    cases #aa9d