chore: minor

Co-authored-by: Kim Morrison <scott.morrison@gmail.com>

src/Init/Grind/Offset.lean

@@ -7,159 +7,44 @@ prelude
 import Init.Core
 import Init.Omega
 
-namespace Lean.Grind.Offset
+namespace Lean.Grind
+def isLt (x y : Nat) : Bool := x < y
 
-abbrev Var := Nat
-abbrev Context := Lean.RArray Nat
+theorem Nat.le_ro (u w v k : Nat) : u ≤ w → w ≤ v + k → u ≤ v + k := by
+  omega
+theorem Nat.le_lo (u w v k : Nat) : u ≤ w → w + k ≤ v → u + k ≤ v := by
+  omega
+theorem Nat.lo_le (u w v k : Nat) : u + k ≤ w → w ≤ v → u + k ≤ v := by
+  omega
+theorem Nat.lo_lo (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v := by
+  omega
+theorem Nat.lo_ro_1 (u w v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v := by
+  simp [isLt]; omega
+theorem Nat.lo_ro_2 (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁) := by
+  omega
+theorem Nat.ro_le (u w v k : Nat) : u ≤ w + k → w ≤ v → u ≤ v + k := by
+  omega
+theorem Nat.ro_lo_1 (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂) := by
+  omega
+theorem Nat.ro_lo_2 (u w v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v := by
+  simp [isLt]; omega
+theorem Nat.ro_ro (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂) := by
+  omega
 
-def fixedVar := 100000000 -- Any big number should work here
+theorem Nat.of_le_eq_false (u v : Nat) : ((u ≤ v) = False) → v + 1 ≤ u := by
+  simp; omega
+theorem Nat.of_lo_eq_false_1 (u v : Nat) : ((u + 1 ≤ v) = False) → v ≤ u := by
+  simp; omega
+theorem Nat.of_lo_eq_false (u v k : Nat) : ((u + k ≤ v) = False) → v ≤ u + (k-1) := by
+  simp; omega
+theorem Nat.of_ro_eq_false (u v k : Nat) : ((u ≤ v + k) = False) → v + (k+1) ≤ u := by
+  simp; omega
 
-def Var.denote (ctx : Context) (v : Var) : Nat :=
-  bif v == fixedVar then 1 else ctx.get v
+theorem Nat.unsat_le_lo (u v k : Nat) : isLt 0 k = true → u ≤ v → v + k ≤ u → False := by
+  simp [isLt]; omega
+theorem Nat.unsat_lo_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False := by
+  simp [isLt]; omega
+theorem Nat.unsat_lo_ro (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False := by
+  simp [isLt]; omega
 
-structure Cnstr where
-  x : Var
-  y : Var
-  k : Nat  := 0
-  l : Bool := true
-  deriving Repr, DecidableEq, Inhabited
-
-def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
-  if c.l then
-    c.x.denote ctx + c.k ≤ c.y.denote ctx
-  else
-    c.x.denote ctx ≤ c.y.denote ctx + c.k
-
-def trivialCnstr : Cnstr := { x := 0, y := 0, k := 0, l := true }
-
-@[simp] theorem denote_trivial (ctx : Context) : trivialCnstr.denote ctx := by
-  simp [Cnstr.denote, trivialCnstr]
-
-def Cnstr.trans (c₁ c₂ : Cnstr) : Cnstr :=
-  if c₁.y = c₂.x then
-    let { x, k := k₁, l := l₁, .. } := c₁
-    let { y, k := k₂, l := l₂, .. } := c₂
-    match l₁, l₂ with
-    | false, false =>
-      { x, y, k := k₁ + k₂, l := false }
-    | false, true =>
-      if k₁ < k₂ then
-        { x, y, k := k₂ - k₁, l := true }
-      else
-        { x, y, k := k₁ - k₂, l := false }
-    | true, false =>
-      if k₁ < k₂ then
-        { x, y, k := k₂ - k₁, l := false }
-      else
-        { x, y, k := k₁ - k₂, l := true }
-    | true, true =>
-      { x, y, k := k₁ + k₂, l := true }
-  else
-    trivialCnstr
-
-@[simp] theorem Cnstr.denote_trans_easy (ctx : Context) (c₁ c₂ : Cnstr) (h : c₁.y ≠ c₂.x) : (c₁.trans c₂).denote ctx := by
-  simp [*, Cnstr.trans]
-
-@[simp] theorem Cnstr.denote_trans (ctx : Context) (c₁ c₂ : Cnstr) : c₁.denote ctx → c₂.denote ctx → (c₁.trans c₂).denote ctx := by
-  by_cases c₁.y = c₂.x
-  case neg => simp [*]
-  simp [trans, *]
-  let { x, k := k₁, l := l₁, .. } := c₁
-  let { y, k := k₂, l := l₂, .. } := c₂
-  simp_all; split
-  · simp [denote]; omega
-  · split <;> simp [denote] <;> omega
-  · split <;> simp [denote] <;> omega
-  · simp [denote]; omega
-
-def Cnstr.isTrivial (c : Cnstr) : Bool := c.x == c.y && c.k == 0
-
-theorem Cnstr.of_isTrivial (ctx : Context) (c : Cnstr) : c.isTrivial = true → c.denote ctx := by
-  cases c; simp [isTrivial]; intros; simp [*, denote]
-
-def Cnstr.isFalse (c : Cnstr) : Bool := c.x == c.y && c.k != 0 && c.l == true
-
-theorem Cnstr.of_isFalse (ctx : Context) {c : Cnstr} : c.isFalse = true → ¬c.denote ctx := by
-  cases c; simp [isFalse]; intros; simp [*, denote]; omega
-
-def Cnstrs := List Cnstr
-
-def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
-  match c₂ with
-  | [] => c₁.denote ctx
-  | c::cs => c₁.denote ctx ∧ Cnstrs.denoteAnd' ctx c cs
-
-theorem Cnstrs.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Cnstrs) : c₁.denote ctx → denoteAnd' ctx c cs → denoteAnd' ctx (c₁.trans c) cs := by
-  induction cs
-  next => simp [denoteAnd', *]; apply Cnstr.denote_trans
-  next c cs ih => simp [denoteAnd']; intros; simp [*]
-
-def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
-  match c₂ with
-  | [] => c₁
-  | c::c₂ => trans' (c₁.trans c) c₂
-
-@[simp] theorem Cnstrs.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : denoteAnd' ctx c₁ c₂ → (trans' c₁ c₂).denote ctx := by
-  induction c₂ generalizing c₁
-  next => intros; simp_all [trans', denoteAnd']
-  next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
-
-def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
-  match c with
-  | [] => True
-  | c::cs => denoteAnd' ctx c cs
-
-def Cnstrs.trans (c : Cnstrs) : Cnstr :=
-  match c with
-  | []    => trivialCnstr
-  | c::cs => trans' c cs
-
-theorem Cnstrs.of_denoteAnd_trans {ctx : Context} {c : Cnstrs} : c.denoteAnd ctx → c.trans.denote ctx := by
-  cases c <;> simp [*, trans, denoteAnd] <;> intros <;> simp [*]
-
-def Cnstrs.isFalse (c : Cnstrs) : Bool :=
-  c.trans.isFalse
-
-theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true → ¬ c.denoteAnd ctx := by
-  simp [isFalse]; intro h₁ h₂
-  have := of_denoteAnd_trans h₂
-  have := Cnstr.of_isFalse ctx h₁
-  contradiction
-
-/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
-def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
-  match cs with
-  | [] => C
-  | c::cs => c.denote ctx → denote ctx cs C
-
-theorem Cnstrs.not_denoteAnd'_eq (ctx : Context) (c : Cnstr) (cs : Cnstrs) (C : Prop) : (denoteAnd' ctx c cs → C) = denote ctx (c::cs) C := by
-  simp [denote]
-  induction cs generalizing c
-  next => simp [denoteAnd', denote]
-  next c' cs ih =>
-    simp [denoteAnd', denote, *]
-
-theorem Cnstrs.not_denoteAnd_eq (ctx : Context) (cs : Cnstrs) (C : Prop) : (denoteAnd ctx cs → C) = denote ctx cs C := by
-  cases cs
-  next => simp [denoteAnd, denote]
-  next c cs => apply not_denoteAnd'_eq
-
-def Cnstr.isImpliedBy (cs : Cnstrs) (c : Cnstr) : Bool :=
-  cs.trans == c
-
-/-! Main theorems used by `grind`. -/
-
-/-- Auxiliary theorem used by `grind` to prove that a system of offset inequalities is unsatisfiable. -/
-theorem Cnstrs.unsat (ctx : Context) (cs : Cnstrs) : cs.isFalse = true → cs.denote ctx False := by
-  intro h
-  rw [← not_denoteAnd_eq]
-  apply unsat'
-  assumption
-
-/-- Auxiliary theorem used by `grind` to prove an implied offset inequality. -/
-theorem Cnstrs.imp (ctx : Context) (cs : Cnstrs) (c : Cnstr) (h : c.isImpliedBy cs = true)  : cs.denote ctx (c.denote ctx) := by
-  rw [← eq_of_beq h]
-  rw [← not_denoteAnd_eq]
-  apply of_denoteAnd_trans
-
-end Lean.Grind.Offset
+end Lean.Grind

src/Lean/Data/AssocList.lean

@@ -24,7 +24,7 @@ abbrev empty : AssocList α β :=
 
 instance : EmptyCollection (AssocList α β) := ⟨empty⟩
 
-abbrev insert (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
+abbrev insertNew (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
   m.cons k v
 
 def isEmpty : AssocList α β → Bool
@@ -77,6 +77,12 @@ def replace [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β
     | true  => cons a b es
     | false => cons k v (replace a b es)
 
+def insert [BEq α] (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
+  if m.contains k then
+    m.replace k v
+  else
+    m.insertNew k v
+
 def erase [BEq α] (a : α) : AssocList α β → AssocList α β
   | nil         => nil
   | cons k v es => match k == a with

src/Lean/Meta/AppBuilder.lean

@@ -569,12 +569,16 @@ def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
   mkAppM ``let_body_congr #[a, h]
 
 /-- Return `of_eq_true h` -/
-def mkOfEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``of_eq_true #[h]
+def mkOfEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | eq_true _ h => return h
+  | _ => mkAppM ``of_eq_true #[h]
 
 /-- Return `eq_true h` -/
-def mkEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``eq_true #[h]
+def mkEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | of_eq_true _ h => return h
+  | _ => return mkApp2 (mkConst ``eq_true) (← inferType h) h
 
 /--
   Return `eq_false h`

src/Lean/Meta/Tactic/FVarSubst.lean

@@ -35,7 +35,7 @@ def insert (s : FVarSubst) (fvarId : FVarId) (v : Expr) : FVarSubst :=
   if s.contains fvarId then s
   else
     let map := s.map.mapVal fun e => e.replaceFVarId fvarId v;
-    { map := map.insert fvarId v }
+    { map := map.insertNew fvarId v }
 
 def erase (s : FVarSubst) (fvarId : FVarId) : FVarSubst :=
   { map := s.map.erase fvarId }

src/Lean/Meta/Tactic/Grind.lean

@@ -24,6 +24,7 @@ import Lean.Meta.Tactic.Grind.EMatchTheorem
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.CasesMatch
+import Lean.Meta.Tactic.Grind.Arith
 
 namespace Lean
 
@@ -42,6 +43,10 @@ builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate
 builtin_initialize registerTraceClass `grind.split.resolved
+builtin_initialize registerTraceClass `grind.offset
+builtin_initialize registerTraceClass `grind.offset.dist
+builtin_initialize registerTraceClass `grind.offset.internalize
+builtin_initialize registerTraceClass `grind.offset.internalize.term (inherited := true)
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -54,4 +59,6 @@ builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
+builtin_initialize registerTraceClass `grind.debug.offset
+builtin_initialize registerTraceClass `grind.debug.offset.proof
 end Lean

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

@@ -0,0 +1,10 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Types
+import Lean.Meta.Tactic.Grind.Arith.Offset
+import Lean.Meta.Tactic.Grind.Arith.Main

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

@@ -0,0 +1,33 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Offset
+
+namespace Lean.Meta.Grind.Arith
+
+namespace Offset
+
+def internalizeTerm (_e : Expr) (_a : Expr) (_k : Nat) : GoalM Unit := do
+  -- TODO
+  return ()
+
+def internalizeCnstr (e : Expr) : GoalM Unit := do
+  let some c := isNatOffsetCnstr? e | return ()
+  let c := { c with
+    a := (← mkNode c.a)
+    b := (← mkNode c.b)
+  }
+  trace[grind.offset.internalize] "{e} ↦ {c}"
+  modify' fun s => { s with
+    cnstrs := s.cnstrs.insert { expr := e } c
+  }
+
+end Offset
+
+def internalize (e : Expr) : GoalM Unit := do
+  Offset.internalizeCnstr e
+
+end Lean.Meta.Grind.Arith

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

@@ -0,0 +1,14 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Offset
+
+namespace Lean.Meta.Grind.Arith
+
+def checkInvariants : GoalM Unit :=
+  Offset.checkInvariants
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Main.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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Arith.Offset
+
+namespace Lean.Meta.Grind.Arith
+
+namespace Offset
+def isCnstr? (e : Expr) : GoalM (Option (Cnstr NodeId)) :=
+  return (← get).arith.offset.cnstrs.find? { expr := e }
+
+def assertTrue (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
+  addEdge c.a c.b c.k (← mkOfEqTrue p)
+
+def assertFalse (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
+  let p := mkOfNegEqFalse (← get').nodes c p
+  let c := c.neg
+  addEdge c.a c.b c.k p
+
+end Offset
+
+builtin_grind_propagator propagateLE ↓LE.le := fun e => do
+  if (← isEqTrue e) then
+    if let some c ← Offset.isCnstr? e then
+      Offset.assertTrue c (← mkEqTrueProof e)
+  if (← isEqFalse e) then
+    if let some c ← Offset.isCnstr? e then
+      Offset.assertFalse c (← mkEqFalseProof e)
+
+end Lean.Meta.Grind.Arith

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

@@ -0,0 +1,173 @@
+/-
+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
+-/
+prelude
+import Init.Grind.Offset
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
+
+namespace Lean.Meta.Grind.Arith.Offset
+/-!
+This module implements a decision procedure for offset constraints of the form:
+```
+x + k ≤ y
+x ≤ y + k
+```
+where `k` is a numeral.
+Each constraint is represented as an edge in a weighted graph.
+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.
+This module can also handle offset equalities of the form `x + k = y` by representing them with two edges:
+```
+x + k ≤ y
+y ≤ x + k
+```
+The main advantage of this module over a full linear integer arithmetic procedure is
+its ability to efficiently detect all implied equalities and inequalities.
+-/
+
+def get' : GoalM State := do
+  return (← get).arith.offset
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  modify fun s => { s with arith.offset := f s.arith.offset }
+
+def mkNode (expr : Expr) : GoalM NodeId := do
+  if let some nodeId := (← get').nodeMap.find? { expr } then
+    return nodeId
+  let nodeId : NodeId := (← get').nodes.size
+  trace[grind.offset.internalize.term] "{expr} ↦ #{nodeId}"
+  modify' fun s => { s with
+    nodes   := s.nodes.push expr
+    nodeMap := s.nodeMap.insert { expr } nodeId
+    sources := s.sources.push {}
+    targets := s.targets.push {}
+    proofs  := s.proofs.push {}
+  }
+  return nodeId
+
+private def getDist? (u v : NodeId) : GoalM (Option Int) := do
+  return (← get').targets[u]!.find? v
+
+private def getProof? (u v : NodeId) : GoalM (Option ProofInfo) := do
+  return (← get').proofs[u]!.find? v
+
+partial def extractProof (u v : NodeId) : GoalM Expr := do
+  go (← getProof? u v).get!
+where
+  go (p : ProofInfo) : GoalM Expr := do
+    if u == p.w then
+      return p.proof
+    else
+      let p' := (← getProof? u p.w).get!
+      go (mkTrans (← get').nodes p' p v)
+
+private def setUnsat (u v : NodeId) (kuv : Int) (huv : Expr) (kvu : Int) : GoalM Unit := do
+  assert! kuv + kvu < 0
+  let hvu ← extractProof v u
+  let u := (← get').nodes[u]!
+  let v := (← get').nodes[v]!
+  if kuv == 0 then
+    assert! kvu < 0
+    closeGoal (mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) u v (toExpr (-kvu).toNat) rfl_true huv hvu)
+  else if kvu == 0 then
+    assert! kuv < 0
+    closeGoal (mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) v u (toExpr (-kuv).toNat) rfl_true hvu huv)
+  else if kuv < 0 then
+    if kvu > 0 then
+      closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) u v (toExpr (-kuv).toNat) (toExpr kvu.toNat) rfl_true huv hvu)
+    else
+      assert! kvu < 0
+      closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_lo) u v (toExpr (-kuv).toNat) (toExpr (-kvu).toNat) rfl_true huv hvu)
+  else
+    assert! kuv > 0 && kvu < 0
+    closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) v u (toExpr (-kvu).toNat) (toExpr kuv.toNat) rfl_true hvu huv)
+
+private def setDist (u v : NodeId) (k : Int) : GoalM Unit := do
+  trace[grind.offset.dist] "{({ a := u, b := v, k : Cnstr NodeId})}"
+  modify' fun s => { s with
+    targets := s.targets.modify u fun es => es.insert v k
+    sources := s.sources.modify v fun es => es.insert u k
+  }
+
+private def setProof (u v : NodeId) (p : ProofInfo) : GoalM Unit := do
+  modify' fun s => { s with
+    proofs := s.proofs.modify u fun es => es.insert v p
+  }
+
+@[inline]
+private def forEachSourceOf (u : NodeId) (f : NodeId → Int → GoalM Unit) : GoalM Unit := do
+  (← get').sources[u]!.forM f
+
+@[inline]
+private def forEachTargetOf (u : NodeId) (f : NodeId → Int → GoalM Unit) : GoalM Unit := do
+  (← get').targets[u]!.forM f
+
+private def isShorter (u v : NodeId) (k : Int) : GoalM Bool := do
+  if let some k' ← getDist? u v then
+    return k < k'
+  else
+    return true
+
+private def updateIfShorter (u v : NodeId) (k : Int) (w : NodeId) : GoalM Unit := do
+  if (← isShorter u v k) then
+    setDist u v k
+    setProof u v (← getProof? w v).get!
+
+def addEdge (u : NodeId) (v : NodeId) (k : Int) (p : Expr) : GoalM Unit := do
+  if (← isInconsistent) then return ()
+  if let some k' ← getDist? v u then
+    if k'+k < 0 then
+      setUnsat u v k p k'
+      return ()
+  if (← isShorter u v k) then
+    setDist u v k
+    setProof u v { w := u, k, proof := p }
+    update
+where
+  update : GoalM Unit := do
+    forEachTargetOf v fun j k₂ => do
+      /- Check whether new path: `u -(k)-> v -(k₂)-> j` is shorter -/
+      updateIfShorter u j (k+k₂) v
+    forEachSourceOf u fun i k₁ => do
+      /- Check whether new path: `i -(k₁)-> u -(k)-> v` is shorter -/
+      updateIfShorter i v (k₁+k) u
+      forEachTargetOf v fun j k₂ => do
+        /- Check whether new path: `i -(k₁)-> u -(k)-> v -(k₂) -> j` is shorter -/
+        updateIfShorter i j (k₁+k+k₂) v
+
+def traceDists : GoalM Unit := do
+  let s ← get'
+  for u in [:s.targets.size], es in s.targets.toArray do
+    for (v, k) in es do
+      trace[grind.offset.dist] "#{u} -({k})-> #{v}"
+
+def Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr := do
+  let a := (← get').nodes[c.a]!
+  let b := (← get').nodes[c.b]!
+  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
+    return mk a (mkNatAdd b (Lean.toExpr c.k.toNat))
+
+def checkInvariants : GoalM Unit := do
+  let s ← get'
+  for u in [:s.targets.size], es in s.targets.toArray do
+    for (v, k) in es do
+      let c : Cnstr NodeId := { a := u, b := v, k }
+      trace[grind.debug.offset] "{c}"
+      let p ← extractProof u v
+      trace[grind.debug.offset.proof] "{p} : {← inferType p}"
+      check p
+      unless (← withDefault <| isDefEq (← inferType p) (← Cnstr.toExpr c)) do
+        trace[grind.debug.offset.proof] "failed: {← inferType p} =?= {← Cnstr.toExpr c}"
+        unreachable!
+
+end Lean.Meta.Grind.Arith.Offset

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

@@ -0,0 +1,89 @@
+/-
+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
+-/
+prelude
+import Init.Grind.Offset
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind.Arith
+
+/-!
+Helper functions for constructing proof terms in the arithmetic procedures.
+-/
+
+namespace Offset
+
+/-- `Eq.refl true` -/
+def rfl_true : Expr := mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
+
+open Lean.Grind in
+/--
+Assume `pi₁` is `{ w := u, k := k₁, proof := p₁ }` and `pi₂` is `{ w := w, k := k₂, proof := p₂ }`
+`p₁` is the proof for edge `u -(k₁) → w` and `p₂` the proof for edge `w -(k₂)-> v`.
+Then, this function returns a proof for edge `u -(k₁+k₂) -> v`.
+-/
+def mkTrans (nodes : PArray Expr) (pi₁ : ProofInfo) (pi₂ : ProofInfo) (v : NodeId) : ProofInfo :=
+  let { w := u, k := k₁, proof := p₁ } := pi₁
+  let { w, k := k₂, proof := p₂ } := pi₂
+  let u := nodes[u]!
+  let w := nodes[w]!
+  let v := nodes[v]!
+  let p := if k₁ == 0 then
+    if k₂ == 0 then
+      -- u ≤ w, w ≤ v
+      mkApp5 (mkConst ``Nat.le_trans) u w v p₁ p₂
+    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
+    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
+      let k₂ := -k₂
+      mkApp7 (mkConst ``Nat.lo_lo) u w v (toExpr k₁.toNat) (toExpr k₂.toNat) p₁ p₂
+    else
+      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 ke₁ := toExpr k₁.toNat
+    if k₂ == 0 then
+      mkApp6 (mkConst ``Nat.ro_le) u w v ke₁ p₁ p₂
+    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
+      mkApp7 (mkConst ``Nat.ro_ro) u w v ke₁ ke₂ p₁ p₂
+  { w := pi₁.w, k := k₁+k₂, proof := p }
+
+open Lean.Grind in
+def mkOfNegEqFalse (nodes : PArray Expr) (c : Cnstr NodeId) (h : Expr) : Expr :=
+  let u := nodes[c.a]!
+  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
+    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
+    mkApp4 (mkConst ``Nat.of_ro_eq_false) u v (toExpr c.k.toNat) h
+
+end Offset
+
+end Lean.Meta.Grind.Arith

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

@@ -0,0 +1,58 @@
+/-
+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
+-/
+prelude
+import Lean.Data.PersistentArray
+import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.Arith.Util
+
+namespace Lean.Meta.Grind.Arith
+
+namespace Offset
+
+abbrev NodeId := Nat
+
+instance : ToMessageData (Offset.Cnstr NodeId) where
+  toMessageData c := Offset.toMessageData (α := NodeId) (inst := { toMessageData n := m!"#{n}" }) c
+
+/-- Auxiliary structure used for proof extraction.  -/
+structure ProofInfo where
+  w     : NodeId
+  k     : Int
+  proof : Expr
+  deriving Inhabited
+
+/-- State of the constraint offset procedure. -/
+structure State where
+  nodes   : PArray Expr := {}
+  nodeMap : PHashMap ENodeKey NodeId := {}
+  cnstrs  : PHashMap ENodeKey (Cnstr NodeId) := {}
+  /--
+  For each node with id `u`, `sources[u]` contains
+  pairs `(v, k)` s.t. there is a path from `v` to `u` with weight `k`.
+  -/
+  sources : PArray (AssocList NodeId Int) := {}
+  /--
+  For each node with id `u`, `targets[u]` contains
+  pairs `(v, k)` s.t. there is a path from `u` to `v` with weight `k`.
+  -/
+  targets : PArray (AssocList NodeId Int) := {}
+  /--
+  Proof reconstruction information. For each node with id `u`, `proofs[u]` contains
+  pairs `(v, { w, proof })` s.t. there is a path from `u` to `v`, and
+  `w` is the penultimate node in the path, and `proof` is the justification for
+  the last edge.
+  -/
+  proofs  : PArray (AssocList NodeId ProofInfo) := {}
+  deriving Inhabited
+
+end Offset
+
+/-- State for the arithmetic procedures. -/
+structure State where
+  offset : Offset.State := {}
+  deriving Inhabited
+
+end Lean.Meta.Grind.Arith

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

@@ -0,0 +1,89 @@
+/-
+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
+-/
+prelude
+import Lean.Expr
+import Lean.Message
+
+namespace Lean.Meta.Grind.Arith
+
+/-- Returns `true` if `e` is of the form `Nat` -/
+def isNatType (e : Expr) : Bool :=
+  e.isConstOf ``Nat
+
+/-- Returns `true` if `e` is of the form `@instHAdd Nat instAddNat` -/
+def isInstAddNat (e : Expr) : Bool :=
+  let_expr instHAdd a b := e | false
+  isNatType a && b.isConstOf ``instAddNat
+
+/-- Returns `true` if `e` is `instLENat` -/
+def isInstLENat (e : Expr) : Bool :=
+  e.isConstOf ``instLENat
+
+/--
+Returns `some (a, b)` if `e` is of the form
+```
+@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b
+```
+-/
+def isNatAdd? (e : Expr) : Option (Expr × Expr) :=
+  let_expr HAdd.hAdd _ _ _ i a b := e | none
+  if isInstAddNat i then some (a, b) else none
+
+/-- Returns `some k` if `e` `@OfNat.ofNat Nat _ (instOfNatNat k)` -/
+def isNatNum? (e : Expr) : Option Nat := Id.run do
+  let_expr OfNat.ofNat _ _ inst := e | none
+  let_expr instOfNatNat k := inst | none
+  let .lit (.natVal k) := k | none
+  some k
+
+/-- Returns `some (a, k)` if `e` is of the form `a + k`.  -/
+def isNatOffset? (e : Expr) : Option (Expr × Nat) := Id.run do
+  let some (a, b) := isNatAdd? e | none
+  let some k := isNatNum? b | none
+  some (a, k)
+
+/-- An offset constraint. -/
+structure Offset.Cnstr (α : Type) where
+  a  : α
+  b  : α
+  k  : Int := 0
+  le : Bool := true
+  deriving Inhabited
+
+def Offset.Cnstr.neg : Cnstr α → Cnstr α
+  | { 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
+
+def Offset.toMessageData [inst : ToMessageData α] (c : Offset.Cnstr α) : MessageData :=
+  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} ≤ {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
+
+/-- Returns `some cnstr` if `e` is offset constraint. -/
+def isNatOffsetCnstr? (e : Expr) : Option (Offset.Cnstr Expr) :=
+  match_expr e with
+  | LE.le _ inst a b => if isInstLENat inst then go a b true else none
+  | Eq α a b => if isNatType α then go a b false else none
+  | _ => none
+where
+  go (a b : Expr) (le : Bool) :=
+    if let some (a, k) := isNatOffset? a then
+      some { a, k := - k, b, le }
+    else if let some (b, k) := isNatOffset? b then
+      some { a, b, k := k, le }
+    else
+      some { a, b, le }
+
+end Lean.Meta.Grind.Arith

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

@@ -0,0 +1,30 @@
+/-
+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
+-/
+prelude
+import Lean.Expr
+
+namespace Lean.Meta.Grind
+
+@[inline] def isSameExpr (a b : Expr) : Bool :=
+  -- It is safe to use pointer equality because we hashcons all expressions
+  -- inserted into the E-graph
+  unsafe ptrEq a b
+
+/--
+Key for the `ENodeMap` and `ParentMap` map.
+We use pointer addresses and rely on the fact all internalized expressions
+have been hash-consed, i.e., we have applied `shareCommon`.
+-/
+structure ENodeKey where
+  expr : Expr
+
+instance : Hashable ENodeKey where
+  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
+
+instance : BEq ENodeKey where
+  beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
+
+end Lean.Meta.Grind

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

@@ -11,6 +11,7 @@ import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 namespace Lean.Meta.Grind
 
@@ -196,6 +197,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       mkENode e generation
       addCongrTable e
       updateAppMap e
+      Arith.internalize e
       propagateUp e
 end
 

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.Arith.Inv
 
 namespace Lean.Meta.Grind
 
@@ -103,6 +104,7 @@ def checkInvariants (expensive := false) : GoalM Unit := do
         checkEqc node
     if expensive then
       checkPtrEqImpliesStructEq
+    Arith.checkInvariants
   if expensive && grind.debug.proofs.get (← getOptions) then
     checkProofs
 

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

@@ -13,17 +13,14 @@ import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Grind.ENodeKey
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.Attr
+import Lean.Meta.Tactic.Grind.Arith.Types
 import Lean.Meta.Tactic.Grind.EMatchTheorem
 
 namespace Lean.Meta.Grind
 
-@[inline] def isSameExpr (a b : Expr) : Bool :=
-  -- It is safe to use pointer equality because we hashcons all expressions
-  -- inserted into the E-graph
-  unsafe ptrEq a b
-
 /-- We use this auxiliary constant to mark delayed congruence proofs. -/
 def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
@@ -224,20 +221,6 @@ structure NewEq where
   proof : Expr
   isHEq : Bool
 
-/--
-Key for the `ENodeMap` and `ParentMap` map.
-We use pointer addresses and rely on the fact all internalized expressions
-have been hash-consed, i.e., we have applied `shareCommon`.
--/
-private structure ENodeKey where
-  expr : Expr
-
-instance : Hashable ENodeKey where
-  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
-
-instance : BEq ENodeKey where
-  beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
-
 abbrev ENodeMap := PHashMap ENodeKey ENode
 
 /--
@@ -368,6 +351,8 @@ structure Goal where
   gmt          : Nat := 0
   /-- Next unique index for creating ENodes -/
   nextIdx      : Nat := 0
+  /-- State of arithmetic procedures -/
+  arith        : Arith.State := {}
   /-- Active theorems that we have performed ematching at least once. -/
   thms         : PArray EMatchTheorem := {}
   /-- Active theorems that we have not performed any round of ematching yet. -/

tests/lean/run/grind_offset_cnstr.lean

@@ -0,0 +1,257 @@
+set_option grind.debug true
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.internalize] a1 + 1 ≤ a2 ↦ #0 + 1 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.internalize] a2 ≤ a3 + 2 ↦ #1 ≤ #2 + 2
+[grind.offset.internalize.term] a4 ↦ #3
+[grind.offset.internalize] a3 ≤ a4 ↦ #2 ≤ #3
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize true in
+example (a1 a2 a3) :
+        a1 + 1 ≤ a2 → a2 ≤ a3 + 2 → a3 ≤ a4 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 + 1 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 ≤ #2
+[grind.offset.dist] #0 + 1 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 + 1 ≤ a2 → a2 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 + 1 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 + 2 ≤ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 + 1 ≤ a2 → a2 + 2 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 + 1 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 ≤ #2 + 2
+[grind.offset.dist] #0 ≤ #2 + 1
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 + 1 ≤ a2 → a2 ≤ a3 + 2 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 ≤ #2
+[grind.offset.dist] #0 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 → a2 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 + 2 ≤ #2
+[grind.offset.dist] #0 + 2 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 → a2 + 2 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 ≤ #2 + 5
+[grind.offset.dist] #0 ≤ #2 + 5
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 → a2 ≤ a3 + 5 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1 + 5
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 ≤ #2
+[grind.offset.dist] #0 ≤ #2 + 5
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 + 5 → a2 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1 + 5
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 + 2 ≤ #2
+[grind.offset.dist] #0 ≤ #2 + 3
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 + 5 → a2 + 2 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1 + 5
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 ≤ #2 + 2
+[grind.offset.dist] #0 ≤ #2 + 7
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
+  fail_if_success grind
+  sorry
+
+
+set_option trace.grind.debug.offset.proof true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1 + 2
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 + 3 ≤ #2
+[grind.offset.dist] #0 + 1 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) : a1 ≤ a2 + 2 → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 + 3 ≤ #0
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 6 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1 + 2) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 ≤ #0 + 1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 2 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 + 1 ≤ #0
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 4 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 ≤ #0
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 3 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 1 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+example (a b c : Nat) : a ≤ b → b + 2 ≤ c → a + 1 ≤ c := by
+  grind
+example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
+  grind
+example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 2 ≤ c := by
+  grind
+example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 1 ≤ c := by
+  grind
+example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
+  grind
+example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
+  grind

tests/lean/run/grind_offset_ineq_thms.lean

@@ -1,31 +0,0 @@
-import Lean
-
-elab tk:"#R[" ts:term,* "]" : term => do
-  let ts : Array Lean.Syntax := ts
-  let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
-  if h : 0 < es.size then
-    return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
-  else
-    throwErrorAt tk "RArray cannot be empty"
-
-open Lean.Grind.Offset
-
-macro "C[" "#" x:term:max " ≤ " "#" y:term:max "]" : term => `({ x := $x, y := $y : Cnstr })
-macro "C[" "#" x:term:max " + " k:term:max " ≤ " "#" y:term:max "]" : term => `({ x := $x, y := $y, k := $k : Cnstr })
-macro "C[" "#" x:term:max " ≤ " "#"y:term:max " + " k:term:max "]" : term => `({ x := $x, y := $y, k := $k, l := false : Cnstr })
-
-example (x y z : Nat) : x + 2 ≤ y → y ≤ z → z + 1 ≤ x → False :=
-  Cnstrs.unsat #R[x, y, z] [
-    C[ #0 + 2 ≤ #1 ],
-    C[ #1 ≤ #2 ],
-    C[ #2 + 1 ≤ #0 ]
-  ] rfl
-
-example (x y z w : Nat) : x + 2 ≤ y → y ≤ z → z ≤ w + 7 → x ≤ w + 5 :=
-  Cnstrs.imp #R[x, y, z, w] [
-    C[ #0 + 2 ≤ #1 ],
-    C[ #1 ≤ #2 ],
-    C[ #2 ≤ #3 + 7]
-  ]
-  C[ #0 ≤ #3 + 5 ]
-  rfl