fix: bugs at grind => finish? (#10936)

This PR fixes issues in `grind => finish?` that were preventing
generated `grind` tactic scripts from being successfully replayed.

Author: leodemoura

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -379,7 +379,7 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
     -- **Note**: We use `withCheapCasesOnly` to ensure multiple goals are not created.
     -- We will add support for this case in the future.
     let (goal, _) ← withCheapCasesOnly <| SearchM.run goal do
-      intros 0
+      intros 0; discard <| assertAll
       getGoal
     let goals := if goal.inconsistent then [] else [goal]
     let ctx ← readThe Meta.Grind.Context

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -281,7 +281,7 @@ def logAnchor (e : Expr) : TermElabM Unit := do
   goal.withContext <| withRef anchor <| logAnchor e
   let goals ← goals.filterMapM fun goal => do
     let (goal, _) ← liftGrindM <| SearchM.run goal do
-      intros genNew
+      intros genNew; discard <| assertAll
       getGoal
     if goal.inconsistent then
       return none

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

@@ -108,7 +108,7 @@ def mkInstantiateTactic (goal : Goal) (usedThms : Array EMatchTheorem) (approx :
   | false, true  => `(grind| instantiate only approx [$params,*])
 
 def mkNewSeq (goal : Goal) (thms : Array EMatchTheorem) (seq : List TGrind) (approx : Bool) : GrindM (List TGrind) := do
-  if thms.isEmpty then
+  if thms.isEmpty && !approx then
     return seq
   else
     return ((← mkInstantiateTactic goal thms approx) :: seq)

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

@@ -444,7 +444,7 @@ def splitNext (stopAtFirstFailure := true) (compress := true) : Action := fun go
     | kna goal
   let cExpr := c.getExpr
   let gen := goal.getGeneration cExpr
-  let x : Action := splitCore c numCases isRec stopAtFirstFailure compress >> intros gen
+  let x : Action := splitCore c numCases isRec stopAtFirstFailure compress >> intros gen >> assertAll
   x goal kna kp
 
 end Action

tests/lean/run/grind_ite_trace.lean

@@ -0,0 +1,113 @@
+module
+public import Std.Data.HashMap
+public import Std.Data.TreeMap
+
+inductive IfExpr
+  | lit : Bool → IfExpr
+  | var : Nat → IfExpr
+  | ite : IfExpr → IfExpr → IfExpr → IfExpr
+deriving DecidableEq
+
+namespace IfExpr
+
+def hasNestedIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite (ite _ _ _) _ _ => true
+  | ite _ t e => t.hasNestedIf || e.hasNestedIf
+
+def hasConstantIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite (lit _) _ _ => true
+  | ite i t e => i.hasConstantIf || t.hasConstantIf || e.hasConstantIf
+
+def hasRedundantIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite i t e => t == e || i.hasRedundantIf || t.hasRedundantIf || e.hasRedundantIf
+
+def vars : IfExpr → List Nat
+  | lit _ => []
+  | var i => [i]
+  | ite i t e => i.vars ++ t.vars ++ e.vars
+
+def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool
+  | [], _ => true
+  | x::xs, ys => x ∉ ys && xs.disjoint ys
+
+def disjoint : IfExpr → Bool
+  | lit _ => true
+  | var _ => true
+  | ite i t e =>
+      i.vars.disjoint t.vars && i.vars.disjoint e.vars && i.disjoint && t.disjoint && e.disjoint
+
+def normalized (e : IfExpr) : Bool :=
+  !e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint
+
+def eval (f : Nat → Bool) : IfExpr → Bool
+  | lit b => b
+  | var i => f i
+  | ite i t e => bif i.eval f then t.eval f else e.eval f
+
+end IfExpr
+
+def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }
+
+namespace IfExpr
+
+@[simp] def normSize : IfExpr → Nat
+  | lit _ => 0
+  | var _ => 1
+  | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
+
+def normalize (assign : Std.HashMap Nat Bool) : IfExpr → IfExpr
+  | lit b => lit b
+  | var v =>
+    match assign[v]? with
+    | none => var v
+    | some b => lit b
+  | ite (lit true)  t _ => normalize assign t
+  | ite (lit false) _ e => normalize assign e
+  | ite (ite a b c) t e => normalize assign (ite a (ite b t e) (ite c t e))
+  | ite (var v)     t e =>
+    match assign[v]? with
+    | none =>
+      let t' := normalize (assign.insert v true) t
+      let e' := normalize (assign.insert v false) e
+      if t' = e' then t' else ite (var v) t' e'
+    | some b => normalize assign (ite (lit b) t e)
+  termination_by e => e.normSize
+
+-- We tell `grind` to unfold our definitions above.
+attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval List.disjoint
+
+theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) :
+    (normalize assign e).normalized
+    ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
+    ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → ¬ v ∈ assign := by
+  fun_induction normalize
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish -- TODO: ensure `finish?` works here
+  next => grind => finish -- TODO: ensure `finish?` works here
+  next => grind => finish?
+
+example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
+    (normalize assign e).normalized
+    ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
+    ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign.contains v = false := by
+  fun_induction normalize
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish?
+  next => grind => finish -- TODO: ensure `finish?` works here
+  next => grind => finish -- TODO: ensure `finish?` works here
+  next => grind => finish?