feat: lazy ite branch internalization in grind (#6737)

This PR ensures that the branches of an `if-then-else` term are
internalized only after establishing the truth value of the condition.
This change makes its behavior consistent with the `match`-expression
and dependent `if-then-else` behavior in `grind`.
This feature is particularly important for recursive functions defined
by well-founded recursion and `if-then-else`. Without lazy
`if-then-else` branch internalization, the equation theorem for the
recursive function would unfold until reaching the generation depth
threshold, and before performing any case analysis. See new tests for an
example.

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

@@ -211,6 +211,10 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
         let c := args[0]!
         internalize c generation e
         registerParent e c
+      else if f.isConstOf ``ite && args.size == 5 then
+        let c := args[1]!
+        internalize c generation e
+        registerParent e c
       else
         if let .const fName _ := f then
           activateTheoremPatterns fName generation

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

@@ -171,8 +171,10 @@ builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
 builtin_grind_propagator propagateIte ↑ite := fun e => do
   let_expr f@ite α c h a b := e | return ()
   if (← isEqTrue c) then
+    internalize a (← getGeneration e)
     pushEq e a <| mkApp6 (mkConst ``ite_cond_eq_true f.constLevels!) α c h a b (← mkEqTrueProof c)
   else if (← isEqFalse c) then
+    internalize b (← getGeneration e)
     pushEq e b <| mkApp6 (mkConst ``ite_cond_eq_false f.constLevels!) α c h a b (← mkEqFalseProof c)
 
 /-- Propagates `dite` upwards -/

tests/lean/run/grind_lazy_ite.lean

@@ -0,0 +1,24 @@
+def f (n : Nat) (m : Nat) :=
+  if n < m then
+    f (n+1) m + n
+  else
+    n
+
+/--
+info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example : f 5 m > 0 := by
+  fail_if_success grind (splits := 0) [f.eq_def]
+  sorry
+
+/--
+info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5
+[grind.ematch.instance] f.eq_def: f 6 m = if 6 < m then f (6 + 1) m + 6 else 6
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example : f 5 m > 0 := by
+  fail_if_success grind (splits := 1) [f.eq_def]
+  sorry