feat: add support for OrderedRing.natCast_nonneg in grind (#11664)

This PR adds support for `Nat.cast` in `grind linarith`. It now uses
`Grind.OrderedRing.natCast_nonneg`. Example:
```lean
open Lean Grind Std
attribute [instance] Semiring.natCast

variable [Lean.Grind.CommRing R] [LE R] [LT R] [LawfulOrderLT R] [IsLinearOrder R] [OrderedRing R]

example (a : Nat) : 0 ≤ (a : R) := by grind
example (a b : Nat) : 0 ≤ (a : R) + (b : R) := by grind
example (a : Nat) : 0 ≤ 2 * (a : R) := by grind
example (a : Nat) : 0 ≥ -3 * (a : R) := by grind
```

src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean

@@ -33,6 +33,12 @@ def isNegInst (struct : Struct) (inst : Expr) : Bool :=
 def reportInstIssue (e : Expr) : GoalM Unit := do
   reportIssue! "`grind linarith` term with unexpected instance{indentExpr e}"
 
+private def assertNatCastNonneg (a : Expr) : LinearM Unit := do
+  let s ← getStruct
+  let h := mkApp8 (mkConst ``Grind.OrderedRing.natCast_nonneg [s.u]) s.type s.ringInst?.get!
+    s.leInst?.get! s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst?.get! s.orderedRingInst?.get! a
+  addNewRawFact h (← inferType h) (← getGeneration a) (.ematch (.decl ``Grind.OrderedRing.natCast_nonneg))
+
 /--
 Converts a Lean `IntModule` expression `e` into a `LinExpr`
 
@@ -54,11 +60,11 @@ partial def reify? (e : Expr) (skipVar : Bool) (generation : Nat := 0) : LinearM
     if isZeroInst (← getStruct) i then return some .zero else asTopVar e
   | OfNat.ofNat _ _ _ =>
     if (← isOfNatZero e) then return some .zero else asTopVar e
-  | _ =>
-    if skipVar then
-      return none
-    else
-      return some (← toVar e)
+  | NatCast.natCast _ _ a =>
+    if (← getStruct).orderedRingInst?.isSome then
+      assertNatCastNonneg a
+    toTopVar e
+  | _ => toTopVar e
 where
   toVar (e : Expr) : LinearM LinExpr := do
     if (← alreadyInternalized e) then
@@ -69,6 +75,11 @@ where
   asVar (e : Expr) : LinearM LinExpr := do
     reportInstIssue e
     toVar e
+  toTopVar (e : Expr) : LinearM (Option LinExpr) := do
+    if skipVar then
+      return none
+    else
+      return some (← toVar e)
   asTopVar (e : Expr) : LinearM (Option LinExpr) := do
     reportInstIssue e
     if skipVar then
@@ -100,6 +111,10 @@ where
       if isZeroInst (← getStruct) i then return .zero else asVar e
     | OfNat.ofNat _ _ _ =>
       if (← isOfNatZero e) then return .zero else toVar e
+    | NatCast.natCast _ _ a =>
+      if (← getStruct).orderedRingInst?.isSome then
+        assertNatCastNonneg a
+      toVar e
     | _ => toVar e
 
 end  Lean.Meta.Grind.Arith.Linear

tests/lean/run/grind_natCast_nonneg_ring.lean

@@ -0,0 +1,16 @@
+open Lean Grind Std
+attribute [instance] Semiring.natCast
+
+variable [Lean.Grind.CommRing R] [LE R] [LT R] [LawfulOrderLT R] [IsLinearOrder R] [OrderedRing R]
+
+example (a : Nat) : 0 ≤ (a : R) := by
+  grind
+
+example (a b : Nat) : 0 ≤ (a : R) + (b : R) := by
+  grind
+
+example (a : Nat) : 0 ≤ 2 * (a : R) := by
+  grind
+
+example (a : Nat) : 0 ≥ -3 * (a : R) := by
+  grind