From 40e1e097c171a6ef1addb607446950e10eedbb9d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Oct 2025 19:12:51 -0400 Subject: [PATCH] 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 --- src/Init/Grind/Order.lean | 56 +++++++++ src/Init/Grind/Ordered/Ring.lean | 14 +++ .../Meta/Tactic/Grind/Arith/IsRelevant.lean | 34 ++++++ src/Lean/Meta/Tactic/Grind/Arith/Util.lean | 11 -- src/Lean/Meta/Tactic/Grind/Internalize.lean | 3 +- src/Lean/Meta/Tactic/Grind/Order/Assert.lean | 28 +++++ .../Meta/Tactic/Grind/Order/Internalize.lean | 6 + src/Lean/Meta/Tactic/Grind/Order/Proof.lean | 66 +++++++++++ tests/lean/run/grind_11001.lean | 34 ++++++ tests/lean/run/grind_order_propagation.lean | 106 ++++++++++++++++++ 10 files changed, 346 insertions(+), 12 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Grind/Arith/IsRelevant.lean create mode 100644 tests/lean/run/grind_11001.lean create mode 100644 tests/lean/run/grind_order_propagation.lean diff --git a/src/Init/Grind/Order.lean b/src/Init/Grind/Order.lean index 03ce5daec9..234fd004d0 100644 --- a/src/Init/Grind/Order.lean +++ b/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₂ diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index 34114e2257..490bd0c5c6 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/IsRelevant.lean b/src/Lean/Meta/Tactic/Grind/Arith/IsRelevant.lean new file mode 100644 index 0000000000..a30f4a0e91 --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean index db1e495043..02efac9aa4 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 7a5de029e2..b894c3085a 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/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) diff --git a/src/Lean/Meta/Tactic/Grind/Order/Assert.lean b/src/Lean/Meta/Tactic/Grind/Order/Assert.lean index 32ddeb5b28..e2158a346f 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Assert.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean index 5005ec03b0..49b8a7a132 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Internalize.lean +++ b/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' diff --git a/src/Lean/Meta/Tactic/Grind/Order/Proof.lean b/src/Lean/Meta/Tactic/Grind/Order/Proof.lean index 17485c13fa..ac07915ce2 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Proof.lean +++ b/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 diff --git a/tests/lean/run/grind_11001.lean b/tests/lean/run/grind_11001.lean new file mode 100644 index 0000000000..2718eb8f59 --- /dev/null +++ b/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 diff --git a/tests/lean/run/grind_order_propagation.lean b/tests/lean/run/grind_order_propagation.lean new file mode 100644 index 0000000000..f4602f5cc4 --- /dev/null +++ b/tests/lean/run/grind_order_propagation.lean @@ -0,0 +1,106 @@ +/-! +Test propagation rules for `grind order` +-/ + +example (p q : Prop) : ((0 : Rat) < (1 : Rat) → p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q : Prop) : ((0 : Rat) ≤ (1 : Rat) → p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) : (if (0 : Rat) < (1 : Rat) then p else s) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) : (if (0 : Rat) ≤ (0 : Rat) then p else s) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) : (if (0 : Rat) > (1 : Rat) then s else p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) : (if (0 : Rat) >= (1 : Rat) then s else p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +----- +example (p q : Prop) (a : Rat) : (a < a + 1 → p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q : Prop) (a : Rat) : (a ≤ a → p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) (a : Rat) : (if a < a + 1 then p else s) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) (a : Rat) : (if a ≤ a then p else s) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) (a : Rat) : (if a > a + 1 then s else p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +example (p q s : Prop) (a : Rat) : (if a >= a + 1 then s else p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind -linarith (splits := 0) + +----- + +example [LE α] [Std.IsPreorder α] [DecidableLE α] (a : α) (p q s : Prop) + : (if a ≤ a then p else s) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind (splits := 0) + +example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [DecidableLT α] (a : α) (p q s : Prop) + : (if a < a then s else p) + → ¬ p ∨ q + → ¬ p ∨ ¬q + → False + := by + grind (splits := 0)