From 131af27d577dbcf6cdcb8eb0525e46cd3d9e6318 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Jan 2025 11:10:29 -0800 Subject: [PATCH] fix: offset constraint edge sign --- src/Lean/Meta/Tactic/Grind/Arith/Offset.lean | 8 +++---- .../Meta/Tactic/Grind/Arith/ProofUtil.lean | 24 ++++++++++--------- src/Lean/Meta/Tactic/Grind/Arith/Util.lean | 14 +++++------ 3 files changed, 24 insertions(+), 22 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean index 85d32da4a958..4a4e6f1bf9e1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean @@ -17,7 +17,7 @@ x ≤ y + k ``` where `k` is a numeral. Each constraint is represented as an edge in a weighted graph. -The constraint `x ≤ y + k` is represented as a negative edge. +The constraint `x + k ≤ y` is represented as a negative edge. The shortest path between two nodes in the graph corresponds to an implied inequality. When adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle. An incremental Floyd-Warshall algorithm is used to find the shortest paths between all nodes. @@ -141,10 +141,10 @@ def Cnstr.toExpr (c : Cnstr NodeId) : OffsetM Expr := do let mk := if c.le then mkNatLE else mkNatEq if c.k == 0 then return mk a b - else if c.k > 0 then - return mk (mkNatAdd a (Lean.toExpr (c.k.toNat))) b + else if c.k < 0 then + return mk (mkNatAdd a (Lean.toExpr ((-c.k).toNat))) b else - return mk a (mkNatAdd b (Lean.toExpr (- c.k).toNat)) + return mk a (mkNatAdd b (Lean.toExpr c.k.toNat)) def checkInvariants : GoalM Unit := OffsetM.run do let s ← get diff --git a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean index e40d1b63e956..e281f2b813ab 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean @@ -34,19 +34,21 @@ def mkTrans (nodes : PArray Expr) (pi₁ : ProofInfo) (pi₂ : ProofInfo) (v : N if k₂ == 0 then -- u ≤ w, w ≤ v mkApp5 (mkConst ``Nat.le_trans) u w v p₁ p₂ - else if k₂ < 0 then + else if k₂ > 0 then -- u ≤ v, w ≤ v + k₂ mkApp6 (mkConst ``Nat.le_ro) u w v (toExpr k₂.toNat) p₁ p₂ else + let k₂ := - k₂ -- u ≤ w, w + k₂ ≤ v mkApp6 (mkConst ``Nat.le_lo) u w v (toExpr k₂.toNat) p₁ p₂ - else if k₁ > 0 then + else if k₁ < 0 then + let k₁ := -k₁ if k₂ == 0 then mkApp6 (mkConst ``Nat.lo_le) u w v (toExpr k₁.toNat) p₁ p₂ - else if k₂ > 0 then + else if k₂ < 0 then + let k₂ := -k₂ mkApp7 (mkConst ``Nat.lo_lo) u w v (toExpr k₁.toNat) (toExpr k₂.toNat) p₁ p₂ else - let k₂ := -k₂ let ke₁ := toExpr k₁.toNat let ke₂ := toExpr k₂.toNat if k₁ > k₂ then @@ -54,18 +56,18 @@ def mkTrans (nodes : PArray Expr) (pi₁ : ProofInfo) (pi₂ : ProofInfo) (v : N else mkApp7 (mkConst ``Nat.lo_ro_2) u w v ke₁ ke₂ p₁ p₂ else - let k₁ := -k₁ let ke₁ := toExpr k₁.toNat if k₂ == 0 then mkApp6 (mkConst ``Nat.ro_le) u w v ke₁ p₁ p₂ - else if k₂ > 0 then + else if k₂ < 0 then + let k₂ := -k₂ let ke₂ := toExpr k₂.toNat if k₂ > k₁ then mkApp8 (mkConst ``Nat.ro_lo_2) u w v ke₁ ke₂ rfl_true p₁ p₂ else mkApp7 (mkConst ``Nat.ro_lo_1) u w v ke₁ ke₂ p₁ p₂ else - let ke₂ := toExpr (-k₂).toNat + let ke₂ := toExpr k₂.toNat mkApp7 (mkConst ``Nat.ro_ro) u w v ke₁ ke₂ p₁ p₂ { w := pi₁.w, k := k₁+k₂, proof := p } @@ -75,12 +77,12 @@ def mkOfNegEqFalse (nodes : PArray Expr) (c : Cnstr NodeId) (h : Expr) : Expr := let v := nodes[c.b]! if c.k == 0 then mkApp3 (mkConst ``Nat.of_le_eq_false) u v h - else if c.k == 1 && c.le then + else if c.k == -1 && c.le then mkApp3 (mkConst ``Nat.of_lo_eq_false_1) u v h - else if c.k > 0 then - mkApp4 (mkConst ``Nat.of_lo_eq_false) u v (toExpr c.k.toNat) h + else if c.k < 0 then + mkApp4 (mkConst ``Nat.of_lo_eq_false) u v (toExpr (-c.k).toNat) h else - mkApp4 (mkConst ``Nat.of_ro_eq_false) u v (toExpr (-c.k).toNat) h + mkApp4 (mkConst ``Nat.of_ro_eq_false) u v (toExpr c.k.toNat) h end Offset diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean index ca5878e2fd56..13e0ae6de46f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean @@ -54,7 +54,7 @@ structure Offset.Cnstr (α : Type) where deriving Inhabited def Offset.Cnstr.neg : Cnstr α → Cnstr α - | { a, b, k, le } => { a := b, b := a, le, k := -k + 1 } + | { a, b, k, le } => { a := b, b := a, le, k := -k - 1 } example (c : Offset.Cnstr α) : c.neg.neg = c := by cases c; simp [Offset.Cnstr.neg]; omega @@ -63,10 +63,10 @@ def Offset.toMessageData [inst : ToMessageData α] (c : Offset.Cnstr α) : Messa match c.k, c.le with | .ofNat 0, true => m!"{c.a} ≤ {c.b}" | .ofNat 0, false => m!"{c.a} = {c.b}" - | .ofNat k, true => m!"{c.a} + {k} ≤ {c.b}" - | .ofNat k, false => m!"{c.a} + {k} = {c.b}" - | .negSucc k, true => m!"{c.a} ≤ {c.b} + {k + 1}" - | .negSucc k, false => m!"{c.a} = {c.b} + {k + 1}" + | .ofNat k, true => m!"{c.a} ≤ {c.b} + {k}" + | .ofNat k, false => m!"{c.a} = {c.b} + {k}" + | .negSucc k, true => m!"{c.a} + {k + 1} ≤ {c.b}" + | .negSucc k, false => m!"{c.a} + {k + 1} = {c.b}" instance : ToMessageData (Offset.Cnstr Expr) where toMessageData c := Offset.toMessageData c @@ -80,9 +80,9 @@ def isNatOffsetCnstr? (e : Expr) : Option (Offset.Cnstr Expr) := where go (a b : Expr) (le : Bool) := if let some (a, k) := isNatOffset? a then - some { a, k, b, le } + some { a, k := - k, b, le } else if let some (b, k) := isNatOffset? b then - some { a, b, k := - k, le } + some { a, b, k := k, le } else some { a, b, le }