fix: bug ite/dite propagator used in grind (#11295)

This PR fixes a bug in the propagation rules for `ite` and `dite` used
in `grind`. The bug prevented equalities from being propagated to the
satellite solvers. Here is an example affected by this issue.

```lean
example
    [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
    [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
    (a b c : α) :
  (if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
  ((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
    if b - d ≤ -(b - d) then -(b - d) else b - d := by
  grind
```

Author: leodemoura

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

@@ -300,8 +300,13 @@ Helper function for propagating over-applied `ite` and `dite`-applications.
 `prefixSize <= args.size`
 -/
 private def applyCongrFun (e rhs : Expr) (h : Expr) (prefixSize : Nat) (args : Array Expr) : GoalM Unit := do
+  /-
+  **Note**: We did not use to set `e` as the parent for `rhs`. This was incorrect because some
+  solvers will inspect the parent to decide whether the term should be internalized or not in the
+  solver.
+  -/
   if prefixSize == args.size then
-    internalize rhs (← getGeneration e)
+    internalize rhs (← getGeneration e) e
     pushEq e rhs h
   else
     go rhs h prefixSize
@@ -314,7 +319,7 @@ where
       go rhs' h' (i+1)
     else
       let rhs ← preprocessLight rhs
-      internalize rhs (← getGeneration e)
+      internalize rhs (← getGeneration e) e
       pushEq e rhs h
 
 /-- Propagates `ite` upwards -/

tests/lean/run/grind_ite_parent.lean

@@ -0,0 +1,75 @@
+/-
+The `ite` and `dite` propagators in `grind` were not internalizing
+their children using the correct parent information. Several examples
+in this file were failing because of this bug.
+-/
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.IntModule α] [DecidableLE α] [Lean.Grind.OrderedAdd α]
+    (a b c d : α)
+    (h : ¬(-(a - b)) ≤ ((-(a - c)) + -(c - d)) + -(b - d))
+    (h_1 : b - d ≤ -(b - d)) : False := by
+  grind
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.IntModule α] [DecidableLE α] [Lean.Grind.OrderedAdd α]
+    (a b c d : α)
+    (h : ¬(-(a - b)) ≤ ((-(a - c)) + -(c - d)) + if b - d ≤ -(b - d) then -(b - d) else b - d)
+    (h_1 : b - d ≤ -(b - d)) : False := by
+  grind
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
+    (a b c : α)
+    (h : a ≤ a + if b ≤ c then (-1 : α) else (-2))
+    (h_1 : b ≤ c)
+    : False := by
+  grind
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
+    (a b c : α)
+    (h : a ≤ a + if b ≤ c then (-1 : α) else (-2))
+    : False := by
+  grind
+
+example [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α] (a b c : α) :
+  (if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
+  ((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
+    if b - d ≤ -(b - d) then -(b - d) else b - d := by
+  grind
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.IntModule α] [DecidableLE α] [Lean.Grind.OrderedAdd α]
+    (a b c d : α)
+    (h : ¬(-(a - b)) ≤ ((-(a - c)) + -(c - d)) + -(b - d))
+    (h_1 : b - d ≤ -(b - d)) : False := by
+  grind -order
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.IntModule α] [DecidableLE α] [Lean.Grind.OrderedAdd α]
+    (a b c d : α)
+    (h : ¬(-(a - b)) ≤ ((-(a - c)) + -(c - d)) + if b - d ≤ -(b - d) then -(b - d) else b - d)
+    (h_1 : b - d ≤ -(b - d)) : False := by
+  grind -order
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
+    (a b c : α)
+    (h : a ≤ a + if b ≤ c then (-1 : α) else (-2))
+    (h_1 : b ≤ c)
+    : False := by
+  grind -order
+
+example {α : Type _} [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
+    [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
+    (a b c : α)
+    (h : a ≤ a + if b ≤ c then (-1 : α) else (-2))
+    : False := by
+  grind -order
+
+example [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α] (a b c : α) :
+  (if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
+  ((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
+    if b - d ≤ -(b - d) then -(b - d) else b - d := by
+  grind -order