fix: Nat adapter in grind order (#10599)

This PR fixes the support for `Nat` in `grind order`. This module uses
the `Nat.ToInt` adapter.

src/Init/Grind/Order.lean

@@ -22,6 +22,12 @@ theorem eq_trans_true {p q : Prop} (h₁ : p = q) (h₂ : q = True) : p = True :
 theorem eq_trans_false {p q : Prop} (h₁ : p = q) (h₂ : q = False) : p = False := by
   subst p; simp [*]
 
+theorem eq_trans_true' {p q : Prop} (h₁ : p = q) (h₂ : p = True) : q = True := by
+  subst p; simp [*]
+
+theorem eq_trans_false' {p q : Prop} (h₁ : p = q) (h₂ : p = False) : q = False := by
+  subst p; simp [*]
+
 theorem le_of_eq {α} [LE α] [Std.IsPreorder α]
     (a b : α) : a = b → a ≤ b := by
   intro h; subst a; apply Std.IsPreorder.le_refl

src/Init/Grind/Tactics.lean

@@ -149,6 +149,11 @@ structure Config where
   at least `Std.IsPreorder`
   -/
   order := true
+  /--
+  When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
+  the future.
+  -/
+  offset := true
   deriving Inhabited, BEq
 
 /--

src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean

@@ -332,6 +332,7 @@ private def alreadyInternalized (e : Expr) : GoalM Bool := do
   return s.cnstrs.contains { expr := e } || s.nodeMap.contains { expr := e }
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+  unless (← getConfig).offset do return ()
   if (← alreadyInternalized e) then
     return ()
   let z ← getNatZeroExpr

src/Lean/Meta/Tactic/Grind/Order/Assert.lean

@@ -211,9 +211,11 @@ where
         /- Check whether new path: `i -(k₁)-> u -(k)-> v -(k₂) -> j` is shorter -/
         updateIfShorter i j (k₁+k+k₂) v
 
-def assertIneqTrue (c : Cnstr NodeId) (e : Expr) : OrderM Unit := do
+/--
+Asserts constraint `c` associated with `e` where `he : e = True`.
+-/
+def assertIneqTrue (c : Cnstr NodeId) (e : Expr) (he : Expr) : OrderM Unit := do
   trace[grind.order.assert] "{← c.pp}"
-  let he ← mkEqTrueProof e
   let h ←  if let some h := c.h? then
     pure <| mkApp4 (mkConst ``Grind.Order.eq_mp) e c.e h (mkOfEqTrueCore e he)
   else
@@ -221,20 +223,35 @@ def assertIneqTrue (c : Cnstr NodeId) (e : Expr) : OrderM Unit := do
   let k : Weight := { k := c.k, strict := c.kind matches .lt }
   addEdge c.u c.v k h
 
-def assertIneqFalse (c : Cnstr NodeId) (_e : Expr) : OrderM Unit := do
+/--
+Asserts constraint `c` associated with `e` where `he : e = False`.
+-/
+def assertIneqFalse (c : Cnstr NodeId) (_e : Expr) (_he : Expr) : OrderM Unit := do
   trace[grind.order.assert] "¬ {← c.pp}"
 
 def getStructIdOf? (e : Expr) : GoalM (Option Nat) := do
   return (← get').exprToStructId.find? { expr := e }
 
 def propagateIneq (e : Expr) : GoalM Unit := do
-  let some structId ← getStructIdOf? e | return ()
-  OrderM.run structId do
-  let some c ← getCnstr? e | return ()
-  if (← isEqTrue e) then
-    assertIneqTrue c e
-  else if (← isEqFalse e) then
-    assertIneqFalse c e
+  if let some (e', he) := (← get').cnstrsMap.find? { expr := e } then
+    go e' (some he)
+  else
+    go e none
+where
+  go (e' : Expr) (he? : Option Expr) : GoalM Unit := do
+    let some structId ← getStructIdOf? e' | return ()
+    OrderM.run structId do
+    let some c ← getCnstr? e' | return ()
+    if (← isEqTrue e) then
+      let mut h ← mkEqTrueProof e
+      if let some he := he? then
+        h := mkApp4 (mkConst ``Grind.Order.eq_trans_true') e e' he h
+      assertIneqTrue c e' h
+    else if (← isEqFalse e) then
+      let mut h ← mkEqFalseProof e
+      if let some he := he? then
+        h := mkApp4 (mkConst ``Grind.Order.eq_trans_false') e e' he h
+      assertIneqFalse c e' h
 
 builtin_grind_propagator propagateLE ↓LE.le := propagateIneq
 builtin_grind_propagator propagateLT ↓LT.lt := propagateIneq

tests/lean/run/grind_order_2.lean

@@ -0,0 +1,13 @@
+open Lean Grind
+
+example (a b : Nat) (h : a + b > 5) : (if a + b ≤ 2 then b else a) = a := by
+  grind -linarith -cutsat -offset (splits := 0)
+
+example (a b c : Nat) : a ≤ b → b ≤ c → c < a → False := by
+  grind -linarith -cutsat -offset (splits := 0)
+
+example (a b : Nat) : a ≤ 5 → b ≤ 8 → a > 6 ∨ b > 10 → False := by
+  grind -linarith -cutsat -offset (splits := 0)
+
+example (a b c d : Nat) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by
+  grind -linarith -cutsat -offset (splits := 0)