feat: grind order negative constraints (#10600)

This PR implements support for negative constraints in `grind order`.
Examples:

```lean
open Lean Grind
example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α]
    (a b c d : α) : a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → d < a → False := by
  grind -linarith (splits := 0)

example [LE α] [Std.IsLinearPreorder α]
    (a b c d : α) : a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → ¬ (a ≤ d) → False := by
  grind -linarith (splits := 0)

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)
```

Author: leodemoura

src/Init/Grind/Order.lean

@@ -10,12 +10,17 @@ import Init.Grind.Ring
 public section
 namespace Lean.Grind.Order
 
+attribute [local instance] Ring.intCast
+
 /-!
 Helper theorems to assert constraints
 -/
 theorem eq_mp {p q : Prop} (h₁ : p = q) (h₂ : p) : q := by
   subst p; simp [*]
 
+theorem eq_mp_not {p q : Prop} (h₁ : p = q) (h₂ : ¬ p) : ¬ q := by
+  subst p; simp [*]
+
 theorem eq_trans_true {p q : Prop} (h₁ : p = q) (h₂ : q = True) : p = True := by
   subst p; simp [*]
 
@@ -29,24 +34,24 @@ theorem eq_trans_false' {p q : Prop} (h₁ : p = q) (h₂ : p = False) : q = Fal
   subst p; simp [*]
 
 theorem le_of_eq {α} [LE α] [Std.IsPreorder α]
-    (a b : α) : a = b → a ≤ b := by
+    {a b : α} : a = b → a ≤ b := by
   intro h; subst a; apply Std.IsPreorder.le_refl
 
 theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α]
-    (a b : α) : ¬ a ≤ b → b ≤ a := by
+    {a b : α} : ¬ a ≤ b → b ≤ a := by
   intro h
   have := Std.IsLinearPreorder.le_total a b
   cases this; contradiction; assumption
 
 theorem lt_of_not_le {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α]
-    (a b : α) : ¬ a ≤ b → b < a := by
+    {a b : α} : ¬ a ≤ b → b < a := by
   intro h
   rw [Std.LawfulOrderLT.lt_iff]
   have := Std.IsLinearPreorder.le_total a b
   cases this; contradiction; simp [*]
 
 theorem le_of_not_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α]
-    (a b : α) : ¬ a < b → b ≤ a := by
+    {a b : α} : ¬ a < b → b ≤ a := by
   rw [Std.LawfulOrderLT.lt_iff]
   open Classical in
   rw [Classical.not_and_iff_not_or_not, Classical.not_not]
@@ -56,8 +61,26 @@ theorem le_of_not_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPr
     cases this; contradiction; assumption
   next => assumption
 
-theorem int_lt {x y k : Int} : x < y + k → x ≤ y + (k-1) := by
-  omega
+theorem le_of_not_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] [Ring α] [OrderedRing α]
+    {a b : α} {k k' : Int} : k'.beq' (-k) → ¬ a < b + k → b ≤ a + k'  := by
+  simp; intro _ h; subst k'
+  replace h := le_of_not_lt h
+  replace h := OrderedAdd.add_le_left h (-k)
+  rw [Semiring.add_assoc, AddCommGroup.add_neg_cancel, Semiring.add_zero] at h
+  rw [Ring.intCast_neg]
+  assumption
+
+theorem lt_of_not_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] [Ring α] [OrderedRing α]
+    {a b : α} {k k' : Int} : k'.beq' (-k) → ¬ a ≤ b + k → b < a + k'  := by
+  simp; intro _ h; subst k'
+  replace h := lt_of_not_le h
+  replace h := OrderedAdd.add_lt_left h (-k)
+  rw [Semiring.add_assoc, AddCommGroup.add_neg_cancel, Semiring.add_zero] at h
+  rw [Ring.intCast_neg]
+  assumption
+
+theorem int_lt {x y k k' : Int} : k'.beq' (k-1) → x < y + k → x ≤ y + k' := by
+  simp; intro; subst k'; omega
 
 /-!
 Helper theorem for equality propagation
@@ -89,8 +112,6 @@ theorem lt_unsat {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α]
 Transitivity with offsets
 -/
 
-attribute [local instance] Ring.intCast
-
 theorem le_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
     {a b c : α} {k₁ k₂ : Int} (k : Int) (h₁ : a ≤ b + k₁) (h₂ : b ≤ c + k₂) : k == k₂ + k₁ → a ≤ c + k := by
   intro h; simp at h; subst k

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

@@ -226,8 +226,39 @@ def assertIneqTrue (c : Cnstr NodeId) (e : Expr) (he : 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
+def assertIneqFalse (c : Cnstr NodeId) (e : Expr) (he : Expr) : OrderM Unit := do
+  unless (← isLinearPreorder) do return ()
   trace[grind.order.assert] "¬ {← c.pp}"
+  let h ←  if let some h := c.h? then
+    pure <| mkApp4 (mkConst ``Grind.Order.eq_mp_not) e c.e h (mkOfEqFalseCore e he)
+  else
+    pure <| mkOfEqFalseCore e he
+  if (← isRing) then
+    let declName := if c.kind matches .lt then
+      ``Grind.Order.le_of_not_lt_k
+    else
+      ``Grind.Order.lt_of_not_le_k
+    let h' ← mkLinearOrdRingPrefix declName
+    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
+    addEdge c.v c.u { strict := false } h
+  else if (← hasLt) then
+    let h' ← mkLeLtLinearPrefix ``Grind.Order.lt_of_not_le
+    let h := mkApp3 h' (← getExpr c.u) (← getExpr c.v) h
+    addEdge c.v c.u { strict := true } h
+  else
+    let h' ← mkLeLinearPrefix ``Grind.Order.le_of_not_le
+    let h := mkApp3 h' (← getExpr c.u) (← getExpr c.v) h
+    addEdge c.v c.u { strict := false } h
 
 def getStructIdOf? (e : Expr) : GoalM (Option Nat) := do
   return (← get').exprToStructId.find? { expr := e }

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

@@ -209,9 +209,6 @@ def internalizeCnstr (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) : OrderM Uni
       s.cnstrsOf.insert (u, v) cs
   }
 
-def hasLt : OrderM Bool :=
-  return (← getStruct).ltFn?.isSome
-
 open Arith.Cutsat in
 def adaptNat (e : Expr) : GoalM Expr := do
   let (eNew, h) ← match_expr e with

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

@@ -60,4 +60,13 @@ def isRing : OrderM Bool :=
 def isPartialOrder : OrderM Bool :=
   return (← getStruct).isPartialInst?.isSome
 
+def isLinearPreorder : OrderM Bool :=
+  return (← getStruct).isLinearPreInst?.isSome
+
+def hasLt : OrderM Bool :=
+  return (← getStruct).lawfulOrderLTInst?.isSome
+
+def isInt : OrderM Bool :=
+  return isSameExpr (← getStruct).type (← getIntExpr)
+
 end Lean.Meta.Grind.Order

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

@@ -44,6 +44,13 @@ public def mkLeLtLinearPrefix (declName : Name) : OrderM Expr := do
   let s ← getStruct
   return mkApp (← mkLeLtPrefix declName) s.isLinearPreInst?.get!
 
+/--
+Returns `declName α leInst isLinearPreorderInst`
+-/
+public def mkLeLinearPrefix (declName : Name) : OrderM Expr := do
+  let s ← getStruct
+  return mkApp3 (mkConst declName [s.u]) s.type s.leInst s.isLinearPreInst?.get!
+
 /--
 Returns `declName α leInst ltInst lawfulOrderLtInst isPreorderInst ringInst ordRingInst`
 -/
@@ -52,6 +59,14 @@ def mkOrdRingPrefix (declName : Name) : OrderM Expr := do
   let h ← mkLeLtPreorderPrefix declName
   return mkApp2 h s.ringInst?.get! s.orderedRingInst?.get!
 
+/--
+Returns `declName α leInst ltInst lawfulOrderLtInst isLinearPreorderInst ringInst ordRingInst`
+-/
+public def mkLinearOrdRingPrefix (declName : Name) : OrderM Expr := do
+  let s ← getStruct
+  let h ← mkLeLtLinearPrefix declName
+  return mkApp2 h s.ringInst?.get! s.orderedRingInst?.get!
+
 def mkTransCoreProof (u v w : Expr) (strict₁ strict₂ : Bool) (h₁ h₂ : Expr) : OrderM Expr := do
   let h ← match strict₁, strict₂ with
     | false, false => mkLePreorderPrefix ``Grind.Order.le_trans

tests/lean/run/grind_offset_cnstr.lean

@@ -1,6 +1,6 @@
 module
 set_option grind.debug true
-
+set_option warn.sorry false
 /--
 trace: [grind.offset.internalize.term] a1 ↦ #0
 [grind.offset.internalize.term] a2 ↦ #1
@@ -274,7 +274,7 @@ trace: [grind.debug.proof] intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬
 open Lean Grind in
 set_option trace.grind.debug.proof true in
 theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 := by
-  grind
+  grind -order
 
 /-! Propagate `cnstr = False` tests -/
 

tests/lean/run/grind_order_3.lean

@@ -0,0 +1,20 @@
+open Lean Grind
+
+example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α]
+    (a b c d : α) : a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → d < a → False := by
+  grind -linarith (splits := 0)
+
+example [LE α] [Std.IsLinearPreorder α]
+    (a b c d : α) : a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → ¬ (a ≤ d) → False := by
+  grind -linarith (splits := 0)
+
+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 [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)