From 409daac2cb5f72c8b49d558d29f0ac686cd8181f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Sep 2025 17:26:37 -0700 Subject: [PATCH] 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 | 6 +++ src/Init/Grind/Tactics.lean | 5 +++ .../Meta/Tactic/Grind/Arith/Offset/Main.lean | 1 + src/Lean/Meta/Tactic/Grind/Order/Assert.lean | 37 ++++++++++++++----- tests/lean/run/grind_order_2.lean | 13 +++++++ 5 files changed, 52 insertions(+), 10 deletions(-) create mode 100644 tests/lean/run/grind_order_2.lean diff --git a/src/Init/Grind/Order.lean b/src/Init/Grind/Order.lean index b329252414..e46761b674 100644 --- a/src/Init/Grind/Order.lean +++ b/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 diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index a53831435f..d2f56b23fd 100644 --- a/src/Init/Grind/Tactics.lean +++ b/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 /-- diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean index 52cf0dc6b0..1f5a4133c5 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Order/Assert.lean b/src/Lean/Meta/Tactic/Grind/Order/Assert.lean index 53636e6932..867e37cd3a 100644 --- a/src/Lean/Meta/Tactic/Grind/Order/Assert.lean +++ b/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 diff --git a/tests/lean/run/grind_order_2.lean b/tests/lean/run/grind_order_2.lean new file mode 100644 index 0000000000..81052fabdc --- /dev/null +++ b/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)