feat: improves Fin n support in grind (#11319)

This PR improves the support for `Fin n` in `grind` when `n` is not a
numeral.

- `toInt (0 : Fin n) = 0` in `grind lia`.
- `Fin.mk`-applications are treated as interpreted terms in `grind lia`.
- `Fin.val` applications are suppressed from `grind lia`
counterexamples.

src/Init/GrindInstances/ToInt.lean

@@ -116,6 +116,9 @@ instance [NeZero n] : ToInt.Zero (Fin n) (.co 0 n) where
 instance [NeZero n] : ToInt.OfNat (Fin n) (.co 0 n) where
   toInt_ofNat x := by simp; rfl
 
+theorem ofNat_FinZero (n : Nat) [NeZero n] : ToInt.toInt (OfNat.ofNat 0 : Fin n) = 0 := by
+  rw [ToInt.toInt, instToIntFinCoOfNatIntCast, Fin.instOfNat, Fin.ofNat]; simp
+
 instance : ToInt.Add (Fin n) (.co 0 n) where
   toInt_add x y := by rfl
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -500,27 +500,28 @@ def processNewDiseq (a b : Expr) : GoalM Unit := do
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where
-  | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast | neg | toInt | finVal
+  | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast | neg | toInt | finVal | finMk
   deriving BEq, Repr
 
-private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
+private def getKindAndType? (e : Expr) : GrindM (Option (SupportedTermKind × Expr)) :=
   match_expr e with
-  | HAdd.hAdd α _ _ _ _ _ => some (.add, α)
-  | HSub.hSub α _ _ _ _ _ => some (.sub, α)
-  | HMul.hMul α _ _ _ _ _ => some (.mul, α)
-  | HDiv.hDiv α _ _ _ _ _ => some (.div, α)
-  | HMod.hMod α _ _ _ _ _ => some (.mod, α)
-  | HPow.hPow α _ _ _ _ _ => some (.pow, α)
-  | OfNat.ofNat α _ _     => some (.num, α)
+  | HAdd.hAdd α _ _ _ _ _ => return some (.add, α)
+  | HSub.hSub α _ _ _ _ _ => return some (.sub, α)
+  | HMul.hMul α _ _ _ _ _ => return some (.mul, α)
+  | HDiv.hDiv α _ _ _ _ _ => return some (.div, α)
+  | HMod.hMod α _ _ _ _ _ => return some (.mod, α)
+  | HPow.hPow α _ _ _ _ _ => return some (.pow, α)
+  | OfNat.ofNat α _ _     => return some (.num, α)
   | Neg.neg α _ a =>
-    let_expr OfNat.ofNat _ _ _ := a | some (.neg, α)
-    some (.num, α)
-  | Int.natAbs _ => some (.natAbs, Nat.mkType)
-  | Int.toNat _ => some (.toNat, Nat.mkType)
-  | NatCast.natCast α _ _ => some (.natCast, α)
-  | Fin.val _ _ => some (.finVal, Nat.mkType)
-  | Grind.ToInt.toInt _ _ _ _ => some (.toInt, Int.mkType)
-  | _ => none
+    let_expr OfNat.ofNat _ _ _ := a | return some (.neg, α)
+    return some (.num, α)
+  | Int.natAbs _ => return some (.natAbs, Nat.mkType)
+  | Int.toNat _ => return some (.toNat, Nat.mkType)
+  | NatCast.natCast α _ _ => return some (.natCast, α)
+  | Fin.val _ _ => return some (.finVal, Nat.mkType)
+  | Grind.ToInt.toInt _ _ _ _ => return some (.toInt, Int.mkType)
+  | Fin.mk n _ _ => return some (.finMk, ← shareCommon (mkApp (mkConst ``Fin) n))
+  | _ => return none
 
 private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) : Bool := Id.run do
   let some parent := parent? | return false
@@ -528,7 +529,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   -- TODO: document `NatCast.natCast` case.
   -- Remark: we added it to prevent natCast_sub from being expanded twice.
   if declName == ``NatCast.natCast then return true
-  if k matches .div | .mod | .sub | .pow | .neg | .natAbs | .toNat | .natCast | .toInt | .finVal then return false
+  if k matches .div | .mod | .sub | .pow | .neg | .natAbs | .toNat | .natCast | .toInt | .finVal | .finMk then return false
   if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
   match k with
   | .add => return false
@@ -626,11 +627,11 @@ private def propagateToNat (e : Expr) : GoalM Unit := do
   let_expr Int.toNat a := e | return ()
   pushNewFact <| mkApp (mkConst ``Nat.ToInt.ofNat_toNat) a
 
-private def isToIntForbiddenParent (parent? : Option Expr) : Bool :=
+private def isToIntForbiddenParent (parent? : Option Expr) : GrindM Bool := do
   if let some parent := parent? then
-    getKindAndType? parent |>.isSome
+    return (← getKindAndType? parent).isSome
   else
-    false
+    return false
 
 private def internalizeIntTerm (e type : Expr) (parent? : Option Expr) (k : SupportedTermKind) : GoalM Unit := do
   if isForbiddenParent parent? k then return ()
@@ -707,13 +708,13 @@ Internalizes an integer (and `Nat`) expression. Here are the different cases tha
 -/
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).lia do return ()
-  if let some (k, type) := getKindAndType? e then
+  if let some (k, type) ← getKindAndType? e then
     if type.isConstOf ``Int then
       internalizeIntTerm e type parent? k
     else if type.isConstOf ``Nat then
       internalizeNatTerm e type parent? k
     else
-      if isToIntForbiddenParent parent? then return ()
+      if (← isToIntForbiddenParent parent?) then return ()
       internalizeToIntTerm e type
   else
     /-

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Init.Grind.ToIntLemmas
+import Init.GrindInstances.ToInt
 import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.EvalNum
@@ -385,6 +386,11 @@ private def ToIntThms.mkResult (toIntThms : ToIntThms) (mkBinOp : Expr → Expr
   | none,     some b'' => if let some f := toIntThms.c_wr? then mk f a' b'' else mk f a' b'
   | some a'', some b'' => if let some f := toIntThms.c_ww? then mk f a'' b'' else mk f a' b'
 
+/-- Returns `some (n, neZeroInst)` if `inst` is of the form `Fin.instOfNat n neZeroInst _` -/
+private def isFinInstOfNat? (inst : Expr) : MetaM (Option (Expr × Expr)) := do
+  let_expr Fin.instOfNat n neZeroInst _ := inst | return none
+  return some (n, neZeroInst)
+
 private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
   match_expr e with
   | HAdd.hAdd α β γ _ a b =>
@@ -410,9 +416,13 @@ private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
   | Zero.zero _ _ =>
     let some thm ← getZeroThm? | mkToIntVar e
     return (mkIntLit 0, thm)
-  | OfNat.ofNat _ n _ =>
-    let some thm ← getOfNatThm? | mkToIntVar e
+  | OfNat.ofNat _ n inst =>
     let some n ← getNatValue? n | mkToIntVar e
+    if n == 0 then
+      if let some (k, neZeroInst) ← isFinInstOfNat? inst then
+        let h := mkApp2 (mkConst ``Lean.Grind.ofNat_FinZero) k neZeroInst
+        return (mkIntLit 0, h)
+    let some thm ← getOfNatThm? | mkToIntVar e
     let h := mkApp thm (toExpr n)
     if (← hasNumericLoHi) then
       let r ← (← getInfo).range.wrap (mkIntLit n)

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

@@ -60,7 +60,7 @@ def isInterpretedTerm (e : Expr) : Bool :=
   isNatNum e || isIntNum e || e.isAppOf ``HAdd.hAdd || e.isAppOf ``HMul.hMul || e.isAppOf ``HSub.hSub || e.isAppOf ``HSMul.hSMul
   || e.isAppOf ``Neg.neg || e.isAppOf ``HDiv.hDiv || e.isAppOf ``HMod.hMod || e.isAppOf ``One.one || e.isAppOf ``Zero.zero
   || e.isAppOf ``Inv.inv || e.isAppOf ``NatCast.natCast || e.isIte || e.isDIte || e.isAppOf ``OfNat.ofNat || e.isAppOf ``Grind.ToInt.toInt
-  || e.isAppOf ``Grind.IntModule.OfNatModule.toQ || e matches .lit (.natVal _)
+  || e.isAppOf ``Fin.val || e.isAppOf ``Grind.IntModule.OfNatModule.toQ || e matches .lit (.natVal _)
 
 /--
 Adds the assignments `e' := v` to `a` for each `e'` in the equivalence class os `e`.

tests/lean/run/grind_cutsat_toint_1.lean

@@ -83,11 +83,6 @@ example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := by
 /--
 trace: [grind.lia.model] a := 2
 [grind.lia.model] b := 0
-[grind.lia.model] ↑a := 2
-[grind.lia.model] ↑b := 0
-[grind.lia.model] ↑0 := 0
-[grind.lia.model] ↑1 := 1
-[grind.lia.model] ↑(a + b) := 2
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.lia.model true in
@@ -95,10 +90,7 @@ example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → Fa
   grind
 
 -- We use `↑a` when pretty printing `ToInt.toInt a`
-/--
-trace: [grind.debug.ring.basis] ↑a + ↑b + -1 * ((↑a + ↑b) % 3) + -3 * ((↑a + ↑b) / 3) = 0
-[grind.debug.ring.basis] b = 0
--/
+/-- trace: [grind.debug.ring.basis] ↑a + ↑b + -1 * ((↑a + ↑b) % 3) + -3 * ((↑a + ↑b) / 3) = 0 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.debug.ring.basis true in
 example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → False := by

tests/lean/run/grind_fin_zero.lean

@@ -0,0 +1,6 @@
+/-
+Tests `grind` "knows" `toInt (0 : Fin n) = 0` even if `n` is not a numeral.
+-/
+
+example {n a : Nat} [NeZero n] {ha : a < n}  (h₁ : a ≠ 0) (h₂ : (⟨a, ha⟩ : Fin n) = 0) : False := by
+  grind