fix: mbtc and cast issue in grind (#7907)

This PR fixes two bugs in `grind`. 
1. Model-based theory combination was creating type incorrect terms.
2. `Nat.cast` vs `NatCast.natCast` issue during normalization.

src/Init/Grind/Norm.lean

@@ -74,11 +74,11 @@ theorem bne_eq_decide_not_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b :
 theorem xor_eq (a b : Bool) : (a ^^ b) = (a != b) := by
   rfl
 
-theorem natCast_div (a b : Nat) : (↑(a / b) : Int) = ↑a / ↑b := by
-  rfl
-
-theorem natCast_mod (a b : Nat) : (↑(a % b) : Int) = ↑a % ↑b := by
-  rfl
+theorem natCast_eq [NatCast α] (a : Nat) : (Nat.cast a : α) = (NatCast.natCast a : α) := rfl
+theorem natCast_div (a b : Nat) : (NatCast.natCast (a / b) : Int) = (NatCast.natCast a) / (NatCast.natCast b) := rfl
+theorem natCast_mod (a b : Nat) : (NatCast.natCast (a % b) : Int) = (NatCast.natCast a) % (NatCast.natCast b) := rfl
+theorem natCast_add (a b : Nat) : (NatCast.natCast (a + b : Nat) : Int) = (NatCast.natCast a : Int) + (NatCast.natCast b : Int) := rfl
+theorem natCast_mul (a b : Nat) : (NatCast.natCast (a * b : Nat) : Int) = (NatCast.natCast a : Int) * (NatCast.natCast b : Int) := rfl
 
 theorem Nat.pow_one (a : Nat) : a ^ 1 = a := by
   simp
@@ -153,8 +153,10 @@ init_grind_norm
   Int.emod_neg Int.ediv_neg
   Int.ediv_zero Int.emod_zero
   Int.ediv_one Int.emod_one
-  Int.natCast_add Int.natCast_mul Int.natCast_pow
-  Int.natCast_zero natCast_div natCast_mod
+
+  natCast_eq natCast_div natCast_mod
+  natCast_add natCast_mul
+
   Int.pow_zero Int.pow_one
   -- GT GE
   ge_eq gt_eq

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -71,6 +71,7 @@ def isArithTerm (e : Expr) : Bool :=
   | HMul.hMul _ _ _ _ _ _ => true
   | HDiv.hDiv _ _ _ _ _ _ => true
   | HMod.hMod _ _ _ _ _ _ => true
+  | HPow.hPow _ _ _ _ _ _ => true
   | Neg.neg _ _ _ => true
   | OfNat.ofNat _ _ _ => true
   | _ => false

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

@@ -60,8 +60,9 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do
             unless others.any (isSameExpr arg ·) do
               for other in others do
                 if (← ctx.eqAssignment arg other) then
-                  let k := mkCandidateKey arg other
-                  candidates := candidates.insert k
+                  if (← hasSameType arg other) then
+                    let k := mkCandidateKey arg other
+                    candidates := candidates.insert k
               map := map.insert (f, i) (arg :: others)
           else
             map := map.insert (f, i) [arg]

tests/lean/run/grind_cutsat_natCast_propagation.lean

@@ -0,0 +1,13 @@
+set_option grind.warning false
+
+example (a b : Nat) : a  = a + b - b := by
+  grind
+
+example (a b : Int) : a = a + b - b := by
+  grind
+
+example (a b : Nat) : a = a + 2^b - 2^b := by
+  grind
+
+example (a b : Nat) : 2^a = 2^a + b - b := by
+  grind