feat: normalize Int lt

Author: leodemoura

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

@@ -239,9 +239,14 @@ def assertIneqFalse (c : Cnstr NodeId) (e : Expr) (he : Expr) : OrderM Unit := d
     else
       ``Grind.Order.lt_of_not_le_k
     let h' ← mkLinearOrdRingPrefix declName
-    let k' := -c.k
-    let h  := mkApp6 h' (← getExpr c.u) (← getExpr c.v) (toExpr c.k) (toExpr k') eagerReflBoolTrue h
-    addEdge c.v c.u { k := k', strict := c.kind matches .le } h
+    let mut k' := -c.k
+    let mut h := mkApp6 h' (← getExpr c.u) (← getExpr c.v) (toExpr c.k) (toExpr k') eagerReflBoolTrue h
+    let mut strict := c.kind matches .le
+    if (← isInt) && strict then
+      h := mkApp6 (mkConst ``Grind.Order.int_lt) (← getExpr c.v) (← getExpr c.u) (toExpr k') (toExpr (k'-1)) eagerReflBoolTrue h
+      k'     := k' - 1
+      strict := !strict
+    addEdge c.v c.u { k := k', strict } h
   else if c.kind matches .lt then
     let h' ← mkLeLtLinearPrefix ``Grind.Order.le_of_not_lt
     let h := mkApp3 h' (← getExpr c.u) (← getExpr c.v) h

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

@@ -66,4 +66,7 @@ def isLinearPreorder : OrderM Bool :=
 def hasLt : OrderM Bool :=
   return (← getStruct).lawfulOrderLTInst?.isSome
 
+def isInt : OrderM Bool :=
+  return isSameExpr (← getStruct).type (← getIntExpr)
+
 end Lean.Meta.Grind.Order

tests/lean/run/grind_order_3.lean

@@ -15,3 +15,6 @@ example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] [CommRi
 example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] [CommRing α] [OrderedRing α]
     (a b c d : α) : a - b ≤ 5 → ¬ (c < b) → ¬ (d ≤ c + 2) → d ≤ a - 8 → False := by
   grind -linarith (splits := 0)
+
+example (p : Prop) (a b c : Int) : (p ↔ b ≤ a) → (p ↔ c ≤ b) → ¬ p → c ≤ a + 1 → False := by
+  grind -linarith -cutsat (splits := 0)