fix: offset constraint edge sign

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

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

@@ -34,38 +34,40 @@ 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
         mkApp8 (mkConst ``Nat.lo_ro_1) u w v ke₁ ke₂ rfl_true p₁ p₂
       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
 

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 }