feat: add support for other cast-like operations

This PR ensures that `cast h a` and `a` are in the same equivalence
class in goals generated by the `grind` tactic.

src/Init/Grind/Lemmas.lean

@@ -78,4 +78,21 @@ theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = Tr
 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₂]
 
+/-! Casts -/
+
+theorem eqRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
+        {motive : (x : α) → a = x → Sort u_1} (v : motive a (Eq.refl a)) {b : α} (h : a = b)
+        : HEq (@Eq.rec α a motive v b h) v := by
+ subst h; rfl
+
+theorem eqRecOn_heq.{u_1, u_2} {α : Sort u_2} {a : α}
+        {motive : (x : α) → a = x → Sort u_1} {b : α} (h : a = b) (v : motive a (Eq.refl a))
+        : HEq (@Eq.recOn α a motive b h v) v := by
+ subst h; rfl
+
+theorem eqNDRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
+        {motive : α → Sort u_1} (v : motive a) {b : α} (h : a = b)
+        : HEq (@Eq.ndrec α a motive v b h) v := by
+ subst h; rfl
+
 end Lean.Grind

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

@@ -245,8 +245,10 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
     let v := c.assignment[numParams - i - 1]!
     unless isSameExpr v unassigned do
       let mvarId := mvars[i].mvarId!
-      unless (← isDefEq (← mvarId.getType) (← inferType v) <&&> mvarId.checkedAssign v) do
-        trace_goal[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}"
+      let mvarIdType ← mvarId.getType
+      let vType ← inferType v
+      unless (← isDefEq mvarIdType vType <&&> mvarId.checkedAssign v) do
+        trace_goal[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
         return ()
   -- Synthesize instances
   for mvar in mvars, bi in bis do

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Util
+import Init.Grind.Lemmas
 import Lean.Meta.LitValues
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
@@ -72,6 +73,19 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
     if (← isInductivePredicate declName) then
       addSplitCandidate e
 
+/--
+If `e` is a `cast`-like term (e.g., `cast h a`), add `HEq e a` to the to-do list.
+It could be an E-matching theorem, but we want to ensure it is always applied since
+we want to rely on the fact that `cast h a` and `a` are in the same equivalence class.
+-/
+private def pushCastHEqs (e : Expr) : GoalM Unit := do
+  match_expr e with
+  | f@cast α β h a => pushHEq e a (mkApp4 (mkConst ``cast_heq f.constLevels!) α β h a)
+  | f@Eq.rec α a motive v b h => pushHEq e v (mkApp6 (mkConst ``Grind.eqRec_heq f.constLevels!) α a motive v b h)
+  | f@Eq.ndrec α a motive v b h => pushHEq e v (mkApp6 (mkConst ``Grind.eqNDRec_heq f.constLevels!) α a motive v b h)
+  | f@Eq.recOn α a motive b h v => pushHEq e v (mkApp6 (mkConst ``Grind.eqRecOn_heq f.constLevels!) α a motive b h v)
+  | _ => return ()
+
 mutual
 /-- Internalizes the nested ground terms in the given pattern. -/
 private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
@@ -150,6 +164,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       mkENode e generation
     else e.withApp fun f args => do
       checkAndAddSplitCandidate e
+      pushCastHEqs e
       addMatchEqns f generation
       if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
         -- We only internalize the proposition. We can skip the proof because of

tests/lean/run/grind_t1.lean

@@ -133,3 +133,43 @@ info: [grind.eqc] x = 2 * a
 set_option trace.grind.eqc true in
 example (a : Nat) : let_fun x := a + a; y = x → y = a + a := by
   grind
+
+example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
+        (h₁ : α = β)
+        (h₂ : cast h₁ a₁ = b₁)
+        (h₃ : a₁ = a₂)
+        (h₄ : b₁ = b₂)
+        : HEq a₂ b₂ := by
+  grind
+
+example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
+        (h₁ : α = β)
+        (h₂ : h₁ ▸ a₁ = b₁)
+        (h₃ : a₁ = a₂)
+        (h₄ : b₁ = b₂)
+        : HEq a₂ b₂ := by
+  grind
+
+example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
+        (h₁ : α = β)
+        (h₂ : Eq.recOn h₁ a₁ = b₁)
+        (h₃ : a₁ = a₂)
+        (h₄ : b₁ = b₂)
+        : HEq a₂ b₂ := by
+  grind
+
+example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
+        (h₁ : α = β)
+        (h₂ : Eq.ndrec (motive := id) a₁ h₁ = b₁)
+        (h₃ : a₁ = a₂)
+        (h₄ : b₁ = b₂)
+        : HEq a₂ b₂ := by
+  grind
+
+example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
+        (h₁ : α = β)
+        (h₂ : Eq.rec (motive := fun x _ => x) a₁ h₁ = b₁)
+        (h₃ : a₁ = a₂)
+        (h₄ : b₁ = b₂)
+        : HEq a₂ b₂ := by
+  grind