fix: grind order nontermination and propagation issues (#11026)

This PR fixes a nontermination and missing propagation bug in `grind
order`. It also register relevant case-splits for arithmetic.

Closes #11001

Author: leodemoura

src/Init/Grind/Order.lean

@@ -206,6 +206,30 @@ theorem le_eq_true_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α]
   simp; intro h
   exact Std.le_of_lt h
 
+theorem le_eq_true {α} [LE α] [Std.IsPreorder α]
+    {a : α} : (a ≤ a) = True := by
+  simp; exact Std.le_refl a
+
+theorem le_eq_true_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
+    {a : α} {k : Int} : (0 : Int).ble' k → (a ≤ a + k) = True := by
+  simp
+  intro h
+  replace h := OrderedRing.nonneg_intCast_of_nonneg (R := α) _ h
+  have h₁ := Std.le_refl a
+  replace h₁ := OrderedAdd.add_le_add h₁ h
+  simp [Semiring.add_zero] at h₁
+  assumption
+
+theorem lt_eq_true_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
+    {a : α} {k : Int} : (0 : Int).blt' k → (a < a + k) = True := by
+  simp
+  intro h
+  replace h := OrderedRing.pos_intCast_of_pos (R := α) _ h
+  have h₁ := Std.le_refl a
+  replace h₁ := add_lt_add_of_le_of_lt h₁ h
+  simp [Semiring.add_zero] at h₁
+  assumption
+
 theorem le_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
     {a b : α} {k₁ k₂ : Int} : k₁.ble' k₂ → a ≤ b + k₁ → (a ≤ b + k₂) = True := by
   simp; intro h₁ h₂
@@ -247,6 +271,38 @@ theorem lt_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPr
 
 /-! Theorems for propagating constraints to `False` -/
 
+theorem lt_eq_false {α} [LE α] [LT α] [Std.LawfulOrderLT α]
+    {a : α} : (a < a) = False := by
+  simp; intro h
+  have := Preorder.lt_irrefl a
+  contradiction
+
+theorem le_eq_false_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
+    {a : α} {k : Int} : k.blt' 0 → (a ≤ a + k) = False := by
+  simp
+  intro h
+  replace h := OrderedRing.neg_intCast_of_neg (R := α) _ h
+  have h₁ := Std.le_refl a
+  replace h₁ := add_lt_add_of_le_of_lt h₁ h
+  simp [Semiring.add_zero] at h₁
+  intro h
+  have := Std.lt_of_lt_of_le h₁ h
+  have := Preorder.lt_irrefl (a + k)
+  contradiction
+
+theorem lt_eq_false_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
+    {a : α} {k : Int} : k.ble' 0 → (a < a + k) = False := by
+  simp
+  intro h
+  replace h := OrderedRing.nonpos_intCast_of_nonpos (R := α) _ h
+  have h₁ := Std.le_refl a
+  replace h₁ := OrderedAdd.add_le_add h₁ h
+  simp [Semiring.add_zero] at h₁
+  intro h
+  have := Std.lt_of_le_of_lt h₁ h
+  have := Preorder.lt_irrefl (a + k)
+  contradiction
+
 theorem le_eq_false_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α]
     {a b : α} : a < b → (b ≤ a) = False := by
   simp; intro h₁ h₂

src/Init/Grind/Ordered/Ring.lean

@@ -189,6 +189,13 @@ theorem pos_intCast_of_pos (a : Int) : 0 < a → 0 < (a : R) := by
     assumption
   next => omega
 
+theorem neg_intCast_of_neg (a : Int) : a < 0 → (a : R) < 0 := by
+  intro h
+  have h : 0 < -a := by omega
+  replace h := pos_intCast_of_pos (R := R) _ h
+  simp [Ring.intCast_neg, OrderedAdd.neg_pos_iff] at h
+  assumption
+
 theorem nonneg_intCast_of_nonneg (a : Int) : 0 ≤ a → 0 ≤ (a : R) := by
   cases a
   next n =>
@@ -198,6 +205,13 @@ theorem nonneg_intCast_of_nonneg (a : Int) : 0 ≤ a → 0 ≤ (a : R) := by
     assumption
   next => omega
 
+theorem nonpos_intCast_of_nonpos (a : Int) : a ≤ 0 → (a : R) ≤ 0 := by
+  intro h
+  have h : 0 ≤ -a := by omega
+  replace h := nonneg_intCast_of_nonneg (R := R) _ h
+  simp [Ring.intCast_neg, OrderedAdd.neg_nonneg_iff] at h
+  assumption
+
 instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] :
     IsCharP R 0 := IsCharP.mk' _ _ <| by
   intro x

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

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
+public section
+namespace Lean.Meta.Grind.Arith
+
+def isSupportedType (α  : Expr) : GoalM Bool := do
+  if isNatType α || isIntType α then
+    return true
+  else if (← Cutsat.getToIntId? α).isSome then
+    return true
+  else if (← Linear.getStructId? α).isSome then
+    return true
+  else
+    return false
+
+partial def isRelevantPred (e : Expr) : GoalM Bool :=
+  match_expr e with
+  | Not p => isRelevantPred p
+  | LE.le α _ _ _ => isSupportedType α
+  | LT.lt α _ _ _ => isSupportedType α
+  | Eq α _ _ => isSupportedType α
+  | Dvd.dvd α _ _ _ => isSupportedType α
+  | _ => return false
+
+end Lean.Meta.Grind.Arith

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

@@ -78,17 +78,6 @@ def isNatNum? (e : Expr) : Option Nat := Id.run do
   let .lit (.natVal k) := k | none
   some k
 
-def isSupportedType (e : Expr) : Bool :=
-  isNatType e || isIntType e
-
-partial def isRelevantPred (e : Expr) : Bool :=
-  match_expr e with
-  | Not p => isRelevantPred p
-  | LE.le α _ _ _ => isSupportedType α
-  | Eq α _ _ => isSupportedType α
-  | Dvd.dvd α _ _ _ => isSupportedType α
-  | _ => false
-
 def isArithTerm (e : Expr) : Bool :=
   match_expr e with
   | HAdd.hAdd _ _ _ _ _ _ => true

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+import Lean.Meta.Tactic.Grind.Arith.IsRelevant
 import Lean.Meta.Match.MatchEqs
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Beta
@@ -120,7 +121,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
     if (← getConfig).splitImp then
       if (← isProp d) then
         addSplitCandidate (.imp e (h ▸ rfl) currSplitSource)
-    else if Arith.isRelevantPred d then
+    else if (← Arith.isRelevantPred d) then
       -- TODO: should we keep lookahead after we implement non-chronological backtracking?
       if (← getConfig).lookahead then
         addLookaheadCandidate (.imp e (h ▸ rfl) currSplitSource)

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

@@ -81,6 +81,18 @@ public def propagateEqTrue (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' :
   else
     pushEqTrue e h
 
+public def propagateSelfEqTrue (c : Cnstr NodeId) (e : Expr) : OrderM Unit := do
+  let u ← getExpr c.u
+  assert! c.u == c.v
+  let mut h ← mkPropagateSelfEqTrueProof u c.getWeight
+  if let some he := c.h? then
+    h := mkApp4 (mkConst ``Grind.Order.eq_trans_true) e c.e he h
+  if let some (e', he) := (← get').cnstrsMapInv.find? { expr := e } then
+    h := mkApp4 (mkConst ``Grind.Order.eq_trans_true) e' e he h
+    pushEqTrue e' h
+  else
+    pushEqTrue e h
+
 public def propagateEqFalse (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : OrderM Unit := do
   let kuv ← mkProofForPath u v
   let u ← getExpr u
@@ -94,6 +106,18 @@ public def propagateEqFalse (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' :
   else
     pushEqFalse e h
 
+public def propagateSelfEqFalse (c : Cnstr NodeId) (e : Expr) : OrderM Unit := do
+  let u ← getExpr c.u
+  assert! c.u == c.v
+  let mut h ← mkPropagateSelfEqFalseProof u c.getWeight
+  if let some he := c.h? then
+    h := mkApp4 (mkConst ``Grind.Order.eq_trans_false) e c.e he h
+  if let some (e', he) := (← get').cnstrsMapInv.find? { expr := e } then
+    h := mkApp4 (mkConst ``Grind.Order.eq_trans_false) e' e he h
+    pushEqFalse e' h
+  else
+    pushEqFalse e h
+
 /-- Propagates all pending constraints and equalities and resets to "to do" list. -/
 def propagatePending : OrderM Unit := do
   let todo := (← getStruct).propagate
@@ -199,6 +223,10 @@ node pairs.
 -/
 def addEdge (u : NodeId) (v : NodeId) (k : Weight) (h : Expr) : OrderM Unit := do
   if (← isInconsistent) then return ()
+  if u == v then
+    if k.isNeg then
+      closeGoal (← mkSelfUnsatProof (← getExpr u) k h)
+    return ()
   trace[grind.debug.order.add_edge] "{← getExpr u}, {← getExpr v}, {k}"
   if let some k' ← getDist? v u then
     if (k + k').isNeg then

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

@@ -184,6 +184,12 @@ def internalizeCnstr (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) : OrderM Uni
   let v ← mkNode c.v
   let c := { c with u, v }
   let k' := c.getWeight
+  if u == v then
+    if k'.isNeg then
+      propagateSelfEqFalse c e
+    else
+      propagateSelfEqTrue c e
+    return ()
   if let some k ← getDist? u v then
     if k ≤ k' then
       propagateEqTrue c e u v k k'

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

@@ -153,6 +153,28 @@ public def mkPropagateEqTrueProof (u v : Expr) (k : Weight) (huv : Expr) (k' : W
   else
     mkPropagateEqTrueProofCore u v k huv k'
 
+def mkPropagateSelfEqTrueProofOffset (u : Expr) (k : Weight) : OrderM Expr := do
+  let declName := match k.strict with
+    | false => ``Grind.Order.le_eq_true_k
+    | true  => ``Grind.Order.lt_eq_true_k
+  let h ← mkOrdRingPrefix declName
+  return mkApp3 h u (toExpr k.k) eagerReflBoolTrue
+
+def mkPropagateSelfEqTrueProofCore (u : Expr) : OrderM Expr := do
+  let h ← mkLePreorderPrefix ``Grind.Order.le_eq_true
+  return mkApp h u
+
+/--
+Constructs a proof of `e = True` where `e` is a term corresponding to the edge `u --(k) --> u`
+with `k` non-negative
+-/
+public def mkPropagateSelfEqTrueProof (u : Expr) (k : Weight) : OrderM Expr := do
+  if (← isRing) then
+    mkPropagateSelfEqTrueProofOffset u k
+  else
+    assert! !k.strict
+    mkPropagateSelfEqTrueProofCore u
+
 /--
 `u < v → (v ≤ u) = False
 -/
@@ -184,6 +206,50 @@ public def mkPropagateEqFalseProof (u v : Expr) (k : Weight) (huv : Expr) (k' :
   else
     mkPropagateEqFalseProofCore u v k huv k'
 
+def mkPropagateSelfEqFalseProofOffset (u : Expr) (k : Weight) : OrderM Expr := do
+  let declName := match k.strict with
+    | false => ``Grind.Order.le_eq_false_k
+    | true  => ``Grind.Order.lt_eq_false_k
+  let h ← mkOrdRingPrefix declName
+  return mkApp3 h u (toExpr k.k) eagerReflBoolTrue
+
+def mkPropagateSelfEqFalseProofCore (u : Expr) : OrderM Expr := do
+  let h ← mkLeLtPrefix ``Grind.Order.lt_eq_false
+  return mkApp h u
+
+/--
+Constructs a proof of `e = False` where `e` is a term corresponding to the edge `u --(k) --> u` and
+`k` is negative.
+-/
+public def mkPropagateSelfEqFalseProof (u : Expr) (k : Weight) : OrderM Expr := do
+  if (← isRing) then
+    mkPropagateSelfEqFalseProofOffset u k
+  else
+    assert! k.strict
+    mkPropagateSelfEqFalseProofCore u
+
+def mkSelfUnsatProofCore (u : Expr) (h : Expr) : OrderM Expr := do
+  let hf ← mkLeLtPreorderPrefix ``Grind.Order.lt_unsat
+  return mkApp2 hf u h
+
+def mkSelfUnsatProofOffset (u : Expr) (k : Weight) (h : Expr) : OrderM Expr := do
+  let declName := if k.strict then
+    ``Grind.Order.lt_unsat_k
+  else
+    ``Grind.Order.le_unsat_k
+  let hf ← mkOrdRingPrefix declName
+  return mkApp4 hf u (toExpr k.k) eagerReflBoolTrue h
+
+/--
+Returns a proof of `False` using
+`u --(k)--> u` with proof `h` where `k` is negative
+-/
+public def mkSelfUnsatProof (u : Expr) (k : Weight) (h : Expr) : OrderM Expr := do
+  if (← isRing) then
+    mkSelfUnsatProofOffset u k h
+  else
+    mkSelfUnsatProofCore u h
+
 def mkUnsatProofCore (u v : Expr) (k₁ : Weight) (h₁ : Expr) (k₂ : Weight) (h₂ : Expr) : OrderM Expr := do
   let h ← mkTransCoreProof u v u k₁.strict k₂.strict h₁ h₂
   assert! k₁.strict || k₂.strict

tests/lean/run/grind_11001.lean

@@ -0,0 +1,34 @@
+example (n : Nat)
+    (f : Nat → Rat → Rat)
+    (x : Rat)
+    (H : ∀ (x : Rat), 0 ≤ x →
+         (4 < x → f n x < 2 * x) ∧ (x = 4 → f n x = 2 * x) ∧ (x < 4 → 2 * x < f n x)) :
+    x ∈ [4] ↔ f n x = 2 * x := by
+  fail_if_success grind
+  sorry
+
+example (n : Nat)
+    (f : Nat → Rat → Rat)
+    (x : Rat)
+    (_ : x ≥ 0)
+    (H : ∀ (x : Rat), 0 ≤ x →
+         (4 < x → f n x < 2 * x) ∧ (x = 4 → f n x = 2 * x) ∧ (x < 4 → 2 * x < f n x)) :
+    x ∈ [4] ↔ f n x = 2 * x := by
+  grind
+
+example (n : Nat)
+    (f : Nat → Rat → Rat)
+    (x : Rat)
+    (_ : x ≥ 0)
+    (H : ∀ (x : Rat), 0 ≤ x →
+         (4 < x → f n x < 2 * x) ∧ (x = 4 → f n x = 2 * x) ∧ (x < 4 → 2 * x < f n x)) :
+    f n x = 2 * x → x ∈ [4] := by
+  grind
+
+example (n : Nat)
+    (f : Nat → Rat → Rat)
+    (x : Rat)
+    (H : ∀ (x : Rat), 0 ≤ x →
+         (4 < x → f n x < 2 * x) ∧ (x = 4 → f n x = 2 * x) ∧ (x < 4 → 2 * x < f n x)) :
+    x ∈ [4] → f n x = 2 * x := by
+  grind