feat: dependent forall propagator in grind (#6498)

This PR adds support in the `grind` tactic for propagating dependent
forall terms `forall (h : p), q[h]` where `p` is a proposition.

src/Init/Grind/Lemmas.lean

@@ -8,6 +8,7 @@ import Init.Core
 import Init.SimpLemmas
 import Init.Classical
 import Init.ByCases
+import Init.Grind.Util
 
 namespace Lean.Grind
 
@@ -50,4 +51,11 @@ theorem false_of_not_eq_self {a : Prop} (h : (Not a) = a) : False := by
 theorem eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b := by simp [h]
 theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by simp [h]
 
+/-! Forall -/
+
+theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q (of_eq_true h₁) = q') : (∀ hp : p, q hp) = q' := by
+  apply propext; apply Iff.intro
+  · intro h'; exact Eq.mp h₂ (h' (of_eq_true h₁))
+  · intro h'; intros; exact Eq.mpr h₂ h'
+
 end Lean.Grind

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

@@ -88,7 +88,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
     -- `lhs` and `rhs` are already in the same equivalence class.
     trace[grind.debug] "{← ppENodeRef lhs} and {← ppENodeRef rhs} are already in the same equivalence class"
     return ()
-  trace[grind.eqc] "{lhs} {if isHEq then "≡" else "="} {rhs}"
+  trace[grind.eqc] "{← if isHEq then mkHEq lhs rhs else mkEq lhs rhs}"
   let lhsRoot ← getENode lhsNode.root
   let rhsRoot ← getENode rhsNode.root
   let mut valueInconsistency := false

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

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Lemmas
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Internalize
+import Lean.Meta.Tactic.Grind.Simp
+
+namespace Lean.Meta.Grind
+/--
+If `parent` is a projection-application `proj_i c`,
+check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`.
+If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`.
+-/
+def propagateForallProp (parent : Expr) : GoalM Unit := do
+  let .forallE n p q bi := parent | return ()
+  unless (← isEqTrue p) do return ()
+  let h₁ ← mkEqTrueProof p
+  let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
+  let r ← pre qh₁
+  let q := mkLambda n bi p q
+  let q' := r.expr
+  internalize q' (← getGeneration parent)
+  let h₂ ← r.getProof
+  let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂
+  pushEq parent q' h
+
+end Lean.Meta.Grind

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

@@ -75,8 +75,14 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   match e with
   | .bvar .. => unreachable!
   | .sort .. => return ()
-  | .fvar .. | .letE .. | .lam .. | .forallE .. =>
+  | .fvar .. | .letE .. | .lam .. =>
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
+  | .forallE _ d _ _ =>
+    mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
+    if (← isProp d <&&> isProp e) then
+      internalize d generation
+      registerParent e d
+      propagateUp e
   | .lit .. | .const .. =>
     mkENode e generation
   | .mvar ..

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

@@ -8,6 +8,7 @@ import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Proj
+import Lean.Meta.Tactic.Grind.ForallProp
 
 namespace Lean.Meta.Grind
 
@@ -15,6 +16,7 @@ def mkMethods : CoreM Methods := do
   let builtinPropagators ← builtinPropagatorsRef.get
   return {
     propagateUp := fun e => do
+     propagateForallProp e
      let .const declName _ := e.getAppFn | return ()
      propagateProjEq e
      if let some prop := builtinPropagators.up[declName]? then

tests/lean/run/grind_prop_arrow.lean

@@ -0,0 +1,6 @@
+opaque f (a : Array Bool) (i : Nat) (h : i < a.size) : Bool
+
+set_option trace.grind.eqc true
+
+example : (p ∨ ∀ h : i < a.size, f a i h) → (hb : i < b.size) → a = b → ¬p → f b i hb := by
+  grind