feat: dite propagator for grind

src/Init/Grind/Lemmas.lean

@@ -61,4 +61,9 @@ theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = Tr
   · intro h'; exact Eq.mp h₂ (h' (of_eq_true h₁))
   · intro h'; intros; exact Eq.mpr h₂ h'
 
+/-! dite -/
+
+theorem dite_cond_eq_true' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = True) (h₂ : a (of_eq_true h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]
+theorem dite_cond_eq_false' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = False) (h₂ : b (of_eq_false h₁) = r) : (dite c a b) = r := by simp [h₁, h₂]
+
 end Lean.Grind

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

@@ -7,6 +7,8 @@ prelude
 import Init.Grind
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Internalize
 
 namespace Lean.Meta.Grind
 
@@ -142,4 +144,32 @@ builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
   if (← isEqv a b) then
     pushEqTrue e <| mkApp2 (mkConst ``eq_true) e (← mkHEqProof a b)
 
+/-- Propagates `ite` upwards -/
+builtin_grind_propagator propagateIte ↑ite := fun e => do
+  let_expr f@ite α c h a b := e | return ()
+  if (← isEqTrue c) then
+    pushEq e a <| mkApp6 (mkConst ``ite_cond_eq_true f.constLevels!) α c h a b (← mkEqTrueProof c)
+  else if (← isEqFalse c) then
+    pushEq e b <| mkApp6 (mkConst ``ite_cond_eq_false f.constLevels!) α c h a b (← mkEqFalseProof c)
+
+/-- Propagates `dite` upwards -/
+builtin_grind_propagator propagateDIte ↑dite := fun e => do
+  let_expr f@dite α c h a b := e | return ()
+  if (← isEqTrue c) then
+     let h₁ ← mkEqTrueProof c
+     let ah₁ := mkApp a (mkApp2 (mkConst ``of_eq_true) c h₁)
+     let p ← simp ah₁
+     let r := p.expr
+     let h₂ ← p.getProof
+     internalize r (← getGeneration e)
+     pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_true' f.constLevels!) α c h a b r h₁ h₂
+  else if (← isEqFalse c) then
+     let h₁ ← mkEqFalseProof c
+     let bh₁ := mkApp b (mkApp2 (mkConst ``of_eq_false) c h₁)
+     let p ← simp bh₁
+     let r := p.expr
+     let h₂ ← p.getProof
+     internalize r (← getGeneration e)
+     pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_false' f.constLevels!) α c h a b r h₁ h₂
+
 end Lean.Meta.Grind

tests/lean/run/grind_t1.lean

@@ -83,3 +83,31 @@ info: [grind.debug.proj] { a := b, b := v₁, c := v₂ }.a
 set_option trace.grind.debug.proj true in
 example (a b d e : Nat) (x y z : Boo Nat) (f : Nat → Boo Nat) : (f d).1 ≠ a → f d = ⟨b, v₁, v₂⟩ → x.1 = e → y.1 = e → z.1 = e → f d = x → f d = y → f d = z → b = a → False := by
   grind
+
+example (f : Nat → Nat) (a b c : Nat) : f (if a = b then x else y) = z → a = c → c = b → f x = z := by
+  grind
+
+example (f : Nat → Nat) (a b c : Nat) : f (if a = b then x else y) = z → a = c → b ≠ c → f y = z := by
+  grind
+
+namespace dite_propagator_test
+
+opaque R : Nat → Nat → Prop
+opaque f (a : Nat) (b : Nat) (_ : R a b) : Nat
+opaque g (a : Nat) (b : Nat) (_ : ¬ R a b) : Nat
+open Classical
+
+example (foo : Nat → Nat)
+        (_ : foo (if h : R a c then f a c h else g a c h) = x)
+        (_ : R a b)
+        (_ : c = b) : foo (f a c (by grind)) = x := by
+  grind
+
+example (foo : Nat → Nat)
+        (_ : foo (if h : R a c then f a c h else g a c h) = x)
+        (_ : ¬ R a b)
+        (_ : c = b)
+        : foo (g a c (by grind)) = x := by
+  grind
+
+end dite_propagator_test