chore: fix tests

It has been subsumed by `grind order`

src/Init/Grind/Config.lean

@@ -153,11 +153,6 @@ 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
 
 /--

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

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.Util
 public import Lean.Meta.Tactic.Grind.Arith.Types
 public import Lean.Meta.Tactic.Grind.Arith.Main
-public import Lean.Meta.Tactic.Grind.Arith.Offset
 public import Lean.Meta.Tactic.Grind.Arith.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Linear
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat

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

@@ -8,8 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Propagator
 import Lean.Meta.Tactic.Grind.PropagatorAttr
-import Lean.Meta.Tactic.Grind.Arith.Offset.Main
-import Lean.Meta.Tactic.Grind.Arith.Offset.Proof
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
 import Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr
@@ -17,26 +15,11 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.Search
 public section
 namespace Lean.Meta.Grind.Arith
 
-private def Offset.isCnstr? (e : Expr) : GoalM (Option (Cnstr NodeId)) :=
-  return (← get').cnstrs.find? { expr := e }
-
-private def Offset.assertTrue (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
-  addEdge c.u c.v c.k (← mkOfEqTrue p)
-
-private def Offset.assertFalse (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
-  let p := mkOfNegEqFalse (← get').nodes c p
-  let c := c.neg
-  addEdge c.u c.v c.k p
-
 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)
     Cutsat.propagateLe e (eqTrue := true)
     Linear.propagateIneq e (eqTrue := true)
   else if (← isEqFalse e) then
-    if let some c ← Offset.isCnstr? e then
-      Offset.assertFalse c (← mkEqFalseProof e)
     Cutsat.propagateLe e (eqTrue := false)
     Linear.propagateIneq e (eqTrue := false)
 

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

@@ -4,7 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Model
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model

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

@@ -1,34 +0,0 @@
-/-
-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.Arith.Offset.Main
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Proof
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Util
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Types
-public section
-namespace Lean.Meta.Grind.Arith.Offset
-
-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)
-builtin_initialize registerTraceClass `grind.offset.propagate
-builtin_initialize registerTraceClass `grind.offset.eq
-builtin_initialize registerTraceClass `grind.offset.eq.to (inherited := true)
-builtin_initialize registerTraceClass `grind.offset.eq.from (inherited := true)
-builtin_initialize registerTraceClass `grind.offset.model
-
-builtin_initialize registerTraceClass `grind.debug.offset
-builtin_initialize registerTraceClass `grind.debug.offset.proof
-
-builtin_initialize
-  offsetExt.setMethods
-    (internalize := Offset.internalize)
-    (newEq       := Offset.processNewEq)
-    (checkInv    := Offset.checkInvariants)
-
-end Lean.Meta.Grind.Arith.Offset

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

@@ -1,361 +0,0 @@
-/-
-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 Init.Grind.Offset
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Types
-import Lean.Meta.Tactic.Grind.Arith.Offset.Proof
-public section
-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 :=
-  offsetExt.getState
-
-@[inline] def modify' (f : State → State) : GoalM Unit := do
-  offsetExt.modifyState f
-
-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 {}
-  }
-  offsetExt.markTerm expr
-  return nodeId
-
-private def getExpr (u : NodeId) : GoalM Expr := do
-  return (← get').nodes[u]!
-
-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
-
-private def getNodeId (e : Expr) : GoalM NodeId := do
-  let some nodeId := (← get').nodeMap.find? { expr := e }
-    | throwError "internal `grind` error, term has not been internalized by offset module{indentExpr e}"
-  return nodeId
-
-private def getProof (u v : NodeId) : GoalM ProofInfo := do
-  let some p ← getProof? u v
-    | throwError "internal `grind` error, failed to construct proof for{indentExpr (← getExpr u)}\nand{indentExpr (← getExpr v)}"
-  return p
-
-/--
-Returns a proof for `u + k ≤ v` (or `u ≤ v + k`) where `k` is the
-shortest path between `u` and `v`.
--/
-private partial def mkProofForPath (u v : NodeId) : GoalM Expr := do
-  go (← getProof u v)
-where
-  go (p : ProofInfo) : GoalM Expr := do
-    if u == p.w then
-      return p.proof
-    else
-      let p' ← getProof u p.w
-      go (mkTrans (← get').nodes p' p v)
-
-/--
-Given a new edge edge `u --(kuv)--> v` justified by proof `huv` s.t.
-it creates a negative cycle with the existing path `v --{kvu}-->* u`, i.e., `kuv + kvu < 0`,
-this function closes the current goal by constructing a proof of `False`.
--/
-private def setUnsat (u v : NodeId) (kuv : Int) (huv : Expr) (kvu : Int) : GoalM Unit := do
-  assert! kuv + kvu < 0
-  let hvu ← mkProofForPath v u
-  let u ← getExpr u
-  let v ← getExpr v
-  closeGoal (mkUnsatProof u v kuv huv kvu hvu)
-
-/-- Sets the new shortest distance `k` between nodes `u` and `v`. -/
-private def setDist (u v : NodeId) (k : Int) : GoalM Unit := do
-  trace[grind.offset.dist] "{({ u, 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
-
-/-- Returns `true` if `k` is smaller than the shortest distance between `u` and `v` -/
-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
-
-/-- Adds `p` to the list of things to be propagated. -/
-private def pushToPropagate (p : ToPropagate) : GoalM Unit :=
-  modify' fun s => { s with propagate := p :: s.propagate }
-
-private def propagateEqTrue (e : Expr) (u v : NodeId) (k k' : Int) : GoalM Unit := do
-  let kuv ← mkProofForPath u v
-  let u ← getExpr u
-  let v ← getExpr v
-  pushEqTrue e <| mkPropagateEqTrueProof u v k kuv k'
-
-private def propagateEqFalse (e : Expr) (u v : NodeId) (k k' : Int) : GoalM Unit := do
-  let kuv ← mkProofForPath u v
-  let u ← getExpr u
-  let v ← getExpr v
-  pushEqFalse e <| mkPropagateEqFalseProof u v k kuv k'
-
-/-- Propagates all pending constraints and equalities and resets to "to do" list. -/
-private def propagatePending : GoalM Unit := do
-  let todo := (← get').propagate
-  modify' fun s => { s with propagate := [] }
-  for p in todo do
-    match p with
-    | .eqTrue e u v k k' => propagateEqTrue e u v k k'
-    | .eqFalse e u v k k' => propagateEqFalse e u v k k'
-    | .eq u v =>
-      let ue ← getExpr u
-      let ve ← getExpr v
-      unless (← isEqv ue ve) do
-        let huv ← mkProofForPath u v
-        let hvu ← mkProofForPath v u
-        pushEq ue ve <| mkApp4 (mkConst ``Grind.Nat.eq_of_le_of_le) ue ve huv hvu
-
-/--
-Given `e` represented by constraint `c` (from `u` to `v`).
-Checks whether `e = True` can be propagated using the path `u --(k)--> v`.
-If it can, adds a new entry to propagation list.
--/
-private def checkEqTrue (u v : NodeId) (k : Int) (c : Cnstr NodeId) (e : Expr) : GoalM Bool := do
-  if k ≤ c.k then
-    pushToPropagate <| .eqTrue e u v k c.k
-    return true
-  return false
-
-/--
-Given `e` represented by constraint `c` (from `v` to `u`).
-Checks whether `e = False` can be propagated using the path `u --(k)--> v`.
-If it can, adds a new entry to propagation list.
--/
-private def checkEqFalse (u v : NodeId) (k : Int) (c : Cnstr NodeId) (e : Expr) : GoalM Bool := do
-  if k + c.k < 0 then
-    pushToPropagate <| .eqFalse e u v k c.k
-    return true
-  return false
-
-/-- Equality propagation. -/
-private def checkEq (u v : NodeId) (k : Int) : GoalM Unit := do
-  if k != 0 then return ()
-  let some k' ← getDist? v u | return ()
-  if k' != 0 then return ()
-  let ue ← getExpr u
-  let ve ← getExpr v
-  if (← isEqv ue ve) then return ()
-  pushToPropagate <| .eq u v
-
-/--
-Auxiliary function for implementing `propagateAll`.
-Traverses the constraints `c` (representing an expression `e`) s.t.
-`c.u = u` and `c.v = v`, it removes `c` from the list of constraints
-associated with `(u, v)` IF
-- `e` is already assigned, or
-- `f c e` returns true
--/
-@[inline]
-private def updateCnstrsOf (u v : NodeId) (f : Cnstr NodeId → Expr → GoalM Bool) : GoalM Unit := do
-  if let some cs := (← get').cnstrsOf.find? (u, v) then
-    let cs' ← cs.filterM fun (c, e) => do
-      if (← isEqTrue e <||> isEqFalse e) then
-        return false -- constraint was already assigned
-      else
-        return !(← f c e)
-    modify' fun s => { s with cnstrsOf := s.cnstrsOf.insert (u, v) cs' }
-
-/-- Finds constrains and equalities to be propagated. -/
-private def checkToPropagate (u v : NodeId) (k : Int) : GoalM Unit := do
-  updateCnstrsOf u v fun c e => return !(← checkEqTrue u v k c e)
-  updateCnstrsOf v u fun c e => return !(← checkEqFalse u v k c e)
-  checkEq u v k
-
-/--
-If `isShorter u v k`, updates the shortest distance between `u` and `v`.
-`w` is a node in the path from `u` to `v` such that `(← getProof? w v)` is `some`
--/
-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)
-    checkToPropagate u v k
-
-def Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr := do
-  let u := (← get').nodes[c.u]!
-  let v := (← get').nodes[c.v]!
-  if c.k == 0 then
-    return mkNatLE u v
-  else if c.k < 0 then
-    return mkNatLE (mkNatAdd u (Lean.toExpr ((-c.k).toNat))) v
-  else
-    return mkNatLE u (mkNatAdd v (Lean.toExpr c.k.toNat))
-
-def checkInvariants : GoalM Unit := do
-  unless (← isInconsistent) 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 := { u, v, k }
-      trace[grind.debug.offset] "{c}"
-      let p ← mkProofForPath u v
-      trace[grind.debug.offset.proof] "{p} : {← inferType p}"
-      check p
-      unless (← isDefEqD (← inferType p) (← Cnstr.toExpr c)) do
-        throwError "`grind` internal error in the offset constraint module, constraint{indentExpr (← Cnstr.toExpr c)}\nis not definitionally equal to type of its proof{indentExpr (← inferType p)}"
-
-/--
-Adds an edge `u --(k) --> v` justified by the proof term `p`, and then
-if no negative cycle was created, updates the shortest distance of affected
-node pairs.
--/
-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 }
-    checkToPropagate u v k
-    update
-    propagatePending
-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
-
-private def internalizeCnstr (e : Expr) (c : Cnstr Expr) : GoalM Unit := do
-  let u ← mkNode c.u
-  let v ← mkNode c.v
-  let c := { c with u, v }
-  if let some k ← getDist? u v then
-    if k ≤ c.k then
-      propagateEqTrue e u v k c.k
-      return ()
-  if let some k ← getDist? v u then
-    if k + c.k < 0 then
-      propagateEqFalse e v u k c.k
-      return ()
-  trace[grind.offset.internalize] "{e} ↦ {c}"
-  modify' fun s => { s with
-    cnstrs   := s.cnstrs.insert { expr := e } c
-    cnstrsOf :=
-      let cs := if let some cs := s.cnstrsOf.find? (u, v) then (c, e) :: cs else [(c, e)]
-      s.cnstrsOf.insert (u, v) cs
-  }
-
-private def getZeroNode : GoalM NodeId := do
-  mkNode (← getNatZeroExpr)
-
-/-- Internalize `e` of the form `b + k` -/
-private def internalizeTerm (e : Expr) (b : Expr) (k : Nat) : GoalM Unit := do
-  -- `e` is of the form `b + k`
-  let u ← mkNode e
-  let v ← mkNode b
-  -- `u = v + k`. So, we add edges for `u ≤ v + k` and `v + k ≤ u`.
-  let h := mkApp (mkConst ``Nat.le_refl) e
-  addEdge u v k h
-  addEdge v u (-k) h
-  -- `0 + k ≤ u`
-  let z ← getZeroNode
-  addEdge z u (-k) <| mkApp2 (mkConst ``Grind.Nat.le_offset) b (toExpr k)
-
-/--
-Returns `true`, if `parent?` is relevant for internalization.
-For example, we do not want to internalize an offset term that
-is the child of an addition. This kind of term will be processed by the
-more general linear arithmetic module.
--/
-private def isRelevantParent (parent? : Option Expr) : GoalM Bool := do
-  let some parent := parent? | return false
-  let z ← getNatZeroExpr
-  return !isNatAdd parent && (isNatOffsetCnstr? parent z).isNone
-
-private def isEqParent (parent? : Option Expr) : Bool := Id.run do
-  let some parent := parent? | return false
-  return parent.isEq
-
-private def alreadyInternalized (e : Expr) : GoalM Bool := do
-  let s ← get'
-  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
-  if let some c := isNatOffsetCnstr? e z then
-    internalizeCnstr e c
-  else if (← isRelevantParent parent?) then
-    if let some (b, k) := isNatOffset? e then
-      internalizeTerm e b k
-    else if let some k := isNatNum? e then
-      internalizeTerm e z k
-
-def processNewEq (a b : Expr) : GoalM Unit := do
-  unless isSameExpr a b do
-    trace[grind.offset.eq.to] "{a}, {b}"
-    let u ← getNodeId a
-    let v ← getNodeId b
-    let h ← mkEqProof a b
-    addEdge u v 0 <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_1) a b h
-    addEdge v u 0 <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_2) a b h
-
-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}"
-
-end Lean.Meta.Grind.Arith.Offset

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

@@ -1,82 +0,0 @@
-/-
-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.Arith.Offset.Types
-import Lean.Meta.Tactic.Grind.Util
-public section
-namespace Lean.Meta.Grind.Arith.Offset
-
-/-- Construct a model that satisfies all offset constraints -/
-def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
-  let s ← offsetExt.getStateCore goal
-  let dbg := grind.debug.get (← getOptions)
-  let nodes := s.nodes
-  let isInterpreted (u : Nat) : Bool := isNatNum s.nodes[u]!
-  let mut pre : Array (Option Int) := .replicate nodes.size none
-  /-
-  `needAdjust[u]` is true if `u` assignment is not connected to an interpreted value in the graph.
-  That is, its assignment may be negative.
-  -/
-  let mut needAdjust : Array Bool := .replicate nodes.size true
-  -- Initialize `needAdjust`
-  for u in *...nodes.size do
-    if isInterpreted u then
-      -- Interpreted values have a fixed value.
-      needAdjust := needAdjust.set! u false
-    else if s.sources[u]!.any fun v _ => isInterpreted v then
-      needAdjust := needAdjust.set! u false
-    else if s.targets[u]!.any fun v _ => isInterpreted v then
-      needAdjust := needAdjust.set! u false
-  -- Set interpreted values
-  for h : u in *...nodes.size do
-    let e := nodes[u]
-    if let some v ← getNatValue? e then
-      pre := pre.set! u (Int.ofNat v)
-  -- Set remaining values
-  for u in *...nodes.size do
-    let lower? := s.sources[u]!.foldl (init := none) fun val? v k => Id.run do
-      let some va := pre[v]! | return val?
-      let val' := va - k
-      let some val := val? | return val'
-      if val' > val then return val' else val?
-    let upper? := s.targets[u]!.foldl (init := none) fun val? v k => Id.run do
-      let some va := pre[v]! | return val?
-      let val' := va + k
-      let some val := val? | return val'
-      if val' < val then return val' else val?
-    if dbg then
-      let some upper := upper? | pure ()
-      let some lower := lower? | pure ()
-      assert! lower ≤ upper
-      let some val := pre[u]! | pure ()
-      assert! lower ≤ val
-      assert! val ≤ upper
-    unless pre[u]!.isSome do
-      let val := lower?.getD (upper?.getD 0)
-      pre := pre.set! u (some val)
-  let min := pre.foldl (init := 0) fun min val? => Id.run do
-    let some val := val? | return min
-    if val < min then val else min
-  let mut r := {}
-  for u in *...nodes.size do
-    let some val := pre[u]! | unreachable!
-    let val := if needAdjust[u]! then (val - min).toNat else val.toNat
-    let e := nodes[u]!
-    /-
-    We should not include the assignment for auxiliary offset terms since
-    they do not provide any additional information.
-    That said, the information is relevant for debugging `grind`.
-    -/
-    if (!(← isLitValue e) && (isNatOffset? e).isNone && isNatNum? e != some 0) || grind.debug.get (← getOptions) then
-      r := r.push (e, val)
-  r := r.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
-  if (← isTracingEnabledFor `grind.offset.model) then
-    for (x, v) in r do
-      trace[grind.offset.model] "{quoteIfArithTerm x} := {v}"
-  return r
-
-end Lean.Meta.Grind.Arith.Offset

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

@@ -1,164 +0,0 @@
-/-
-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.Arith.Offset.Types
-import Init.Grind.Offset
-import Init.Grind.Lemmas
-public section
-namespace Lean.Meta.Grind.Arith.Offset
-/-!
-Helper functions for constructing proof terms in the offset constraint procedure.
--/
-
-/-- Returns a proof for `true = true` -/
-def rfl_true : Expr := mkConst ``Grind.rfl_true
-
-private def toExprN (n : Int) :=
-  assert! n >= 0
-  toExpr n.toNat
-
-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 (toExprN k₂) p₁ p₂
-    else
-      let k₂ := - k₂
-      -- u ≤ w, w + k₂ ≤ v
-      mkApp6 (mkConst ``Nat.le_lo) u w v (toExprN k₂) p₁ p₂
-  else if k₁ < 0 then
-    let k₁ := -k₁
-    if k₂ == 0 then
-      mkApp6 (mkConst ``Nat.lo_le) u w v (toExprN k₁) p₁ p₂
-    else if k₂ < 0 then
-      let k₂ := -k₂
-      mkApp7 (mkConst ``Nat.lo_lo) u w v (toExprN k₁) (toExprN k₂) p₁ p₂
-    else
-      let ke₁ := toExprN k₁
-      let ke₂ := toExprN k₂
-      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₁ := toExprN k₁
-    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₂ := toExprN k₂
-       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₂ := toExprN k₂
-      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.u]!
-  let v := nodes[c.v]!
-  if c.k == 0 then
-    mkApp3 (mkConst ``Nat.of_le_eq_false) u v h
-  else if c.k == -1 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 (toExprN (-c.k)) h
-  else
-    mkApp4 (mkConst ``Nat.of_ro_eq_false) u v (toExprN c.k) h
-
-/--
-Returns a proof of `False` using a negative cycle composed of
-- `u --(kuv)--> v` with proof `huv`
-- `v --(kvu)--> u` with proof `hvu`
--/
-def mkUnsatProof (u v : Expr) (kuv : Int) (huv : Expr) (kvu : Int) (hvu : Expr) : Expr :=
-  if kuv == 0 then
-    assert! kvu < 0
-    mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) u v (toExprN (-kvu)) rfl_true huv hvu
-  else if kvu == 0 then
-    mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) v u (toExprN (-kuv)) rfl_true hvu huv
-  else if kuv < 0 then
-    if kvu > 0 then
-      mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) u v (toExprN (-kuv)) (toExprN kvu) rfl_true huv hvu
-    else
-      assert! kvu < 0
-      mkApp7 (mkConst ``Grind.Nat.unsat_lo_lo) u v (toExprN (-kuv)) (toExprN (-kvu)) rfl_true huv hvu
-  else
-    assert! kuv > 0 && kvu < 0
-    mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) v u (toExprN (-kvu)) (toExprN kuv) rfl_true hvu huv
-
-/--
-Given a path `u --(kuv)--> v` justified by proof `huv`,
-construct a proof of `e = True` where `e` is a term corresponding to the edge `u --(k') --> v`
-s.t. `k ≤ k'`
--/
-def mkPropagateEqTrueProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr :=
-  if k == 0 then
-    if k' == 0 then
-      mkApp3 (mkConst ``Grind.Nat.le_eq_true_of_le) u v huv
-    else
-      assert! k' > 0
-      mkApp4 (mkConst ``Grind.Nat.ro_eq_true_of_le) u v (toExprN k') huv
-  else if k < 0 then
-    let k := -k
-    if k' == 0 then
-      mkApp4 (mkConst ``Grind.Nat.le_eq_true_of_lo) u v (toExprN k) huv
-    else if k' < 0 then
-      let k' := -k'
-      mkApp6 (mkConst ``Grind.Nat.lo_eq_true_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
-    else
-      assert! k' > 0
-      mkApp5 (mkConst ``Grind.Nat.ro_eq_true_of_lo) u v (toExprN k) (toExprN k') huv
-  else
-    assert! k > 0
-    assert! k' > 0
-    mkApp6 (mkConst ``Grind.Nat.ro_eq_true_of_ro) u v (toExprN k) (toExprN k') rfl_true huv
-
-/--
-Given a path `u --(kuv)--> v` justified by proof `huv`,
-construct a proof of `e = False` where `e` is a term corresponding to the edge `v --(k') --> u`
-s.t. `k+k' < 0`
--/
-def mkPropagateEqFalseProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr :=
-  if k == 0 then
-    assert! k' < 0
-    let k' := -k'
-    mkApp5 (mkConst ``Grind.Nat.lo_eq_false_of_le) u v (toExprN k') rfl_true huv
-  else if k < 0 then
-    let k := -k
-    if k' == 0 then
-      mkApp5 (mkConst ``Grind.Nat.le_eq_false_of_lo) u v (toExprN k) rfl_true huv
-    else if k' < 0 then
-      let k' := -k'
-      mkApp6 (mkConst ``Grind.Nat.lo_eq_false_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
-    else
-      assert! k' > 0
-      mkApp6 (mkConst ``Grind.Nat.ro_eq_false_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
-  else
-    assert! k > 0
-    assert! k' < 0
-    let k' := -k'
-    mkApp6 (mkConst ``Grind.Nat.lo_eq_false_of_ro) u v (toExprN k) (toExprN k') rfl_true huv
-
-end Lean.Meta.Grind.Arith.Offset

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

@@ -1,75 +0,0 @@
-/-
-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
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Util
-public section
-namespace Lean.Meta.Grind.Arith.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
-
-/--
-Auxiliary inductive type for representing constraints and equalities
-that should be propagated to core.
-Recall that we cannot compute proofs until the short-distance
-data-structures have been fully updated when a new edge is inserted.
-Thus, we store the information to be propagated into a list.
-See field `propagate` in `State`.
--/
-inductive ToPropagate where
-  | eqTrue (e : Expr) (u v : NodeId) (k k' : Int)
-  | eqFalse (e : Expr) (u v : NodeId) (k k' : Int)
-  | eq (u v : NodeId)
-  deriving Inhabited
-
-/-- State of the constraint offset procedure. -/
-structure State where
-  /-- Mapping from `NodeId` to the `Expr` represented by the node. -/
-  nodes    : PArray Expr := {}
-  /-- Mapping from `Expr` to a node representing it. -/
-  nodeMap  : PHashMap ExprPtr NodeId := {}
-  /-- Mapping from `Expr` representing inequalities to constraints. -/
-  cnstrs   : PHashMap ExprPtr (Cnstr NodeId) := {}
-  /--
-  Mapping from pairs `(u, v)` to a list of offset constraints on `u` and `v`.
-  We use this mapping to implement exhaustive constraint propagation.
-  -/
-  cnstrsOf : PHashMap (NodeId × NodeId) (List (Cnstr NodeId × Expr)) := {}
-  /--
-  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) := {}
-  /-- Truth values and equalities to propagate to core. -/
-  propagate : List ToPropagate := []
-  deriving Inhabited
-
-builtin_initialize offsetExt : SolverExtension State ← registerSolverExtension (return {})
-
-end Lean.Meta.Grind.Arith.Offset

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

@@ -1,65 +0,0 @@
-/-
-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.Arith.Util
-
-public section
-
-namespace Lean.Meta.Grind.Arith.Offset
-
-/-- 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 Cnstr (α : Type) where
-  u  : α
-  v  : α
-  k  : Int := 0
-  deriving Inhabited
-
-def Cnstr.neg : Cnstr α → Cnstr α
-  | { u, v, k } => { u := v, v := u, k := -k - 1 }
-
-example (c : Cnstr α) : c.neg.neg = c := by
-  cases c; simp [Cnstr.neg]; omega
-
-def toMessageData [inst : ToMessageData α] (c : Cnstr α) : MessageData :=
-  match c.k with
-  | .ofNat 0   => m!"{c.u} ≤ {c.v}"
-  | .ofNat k   => m!"{c.u} ≤ {c.v} + {k}"
-  | .negSucc k => m!"{c.u} + {k + 1} ≤ {c.v}"
-
-instance : ToMessageData (Cnstr Expr) where
-  toMessageData c := Offset.toMessageData c
-
-/--
-Returns `some cnstr` if `e` is offset constraint.
-Remark: `z` is `0` numeral. It is an extra argument because we
-want to be able to provide the one that has already been internalized.
--/
-def isNatOffsetCnstr? (e : Expr) (z : Expr) : Option (Cnstr Expr) :=
-  match_expr e with
-  | LE.le _ inst a b => if isInstLENat inst then go a b else none
-  | _ => none
-where
-  go (u v : Expr) :=
-    if let some (u, k) := isNatOffset? u then
-      some { u, k := - k, v }
-    else if let some (v, k) := isNatOffset? v then
-      some { u, v, k }
-    else if let some k := isNatNum? u then
-      some { u := z, v, k := - k }
-    else if let some k := isNatNum? v then
-      some { u, v := z, k }
-    else
-      some { u, v }
-
-end Lean.Meta.Grind.Arith.Offset

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

@@ -197,20 +197,6 @@ private def ppActiveTheoremPatterns : M Unit := do
   unless m.isEmpty do
     pushMsg <| .trace { cls := `ematch } "E-matching patterns" m
 
-private def ppOffset : M Unit := do
-  unless grind.debug.get (← getOptions) do
-    return ()
-  let goal ← read
-  let s ← Arith.Offset.offsetExt.getStateCore goal
-  let nodes := s.nodes
-  if nodes.isEmpty then return ()
-  let model ← Arith.Offset.mkModel goal
-  if model.isEmpty then return ()
-  let mut ms := #[]
-  for (e, val) in model do
-    ms := ms.push <| .trace { cls := `assign } m!"{Arith.quoteIfArithTerm e} := {val}" #[]
-  pushMsg <| .trace { cls := `offset } "Assignment satisfying offset constraints" ms
-
 def Arith.Cutsat.pp? (goal : Goal) : MetaM (Option MessageData) := do
   let s ← Arith.Cutsat.cutsatExt.getStateCore goal
   let nodes := s.varMap
@@ -279,7 +265,6 @@ where
     ppEqcs (collapsedProps := collapsedMain)
     ppCasesTrace
     ppActiveTheoremPatterns
-    ppOffset
     ppCutsat
     ppLinarith
     ppCommRing

tests/lean/run/grind_dep_match_overlap.lean

@@ -18,9 +18,3 @@ example (a b : Vec α 2) : h a b = 20 := by
 
 example (a b : Vec α 2) : h a b = 20 := by
   grind (splits := 4) [h.eq_def, Vec]
-
-example (a b : Vec α 2) : h a b = 20 := by
-  grind -offset [h.eq_def, Vec]
-
-example (a b : Vec α 2) : h a b = 20 := by
-  grind -offset (splits := 4) [h.eq_def, Vec]

tests/lean/run/grind_fun_singleton.lean

@@ -39,6 +39,3 @@ example [Inhabited α] : ((fun (_ : α) => x = a + 1) = fun (_ : α) => True)
 
 example : c = 5 → ((fun (_ : Nat × Nat) => { down := a + c = b + 5 : ULift Prop }) = fun (_ : Nat × Nat) => { down := c < 10 : ULift Prop }) → a = b := by
   grind
-
-example : c = 5 → ((fun (_ : Nat × Nat) => { down := a + c = b + 5 : ULift Prop }) = fun (_ : Nat × Nat) => { down := c < 10 : ULift Prop }) → a = b := by
-  grind -offset

tests/lean/run/grind_indexmap_trace.lean

@@ -240,14 +240,14 @@ info: Try these:
       instantiate only [usr getElem_indices_lt]
       instantiate only [size]
       cases #ffdf
-      · instantiate only [=_ WF]
-        instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
+      · instantiate only [usr getElem_indices_lt, =_ WF]
+        instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set, = Array.getElem_set]
         instantiate only [WF']
       · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
   [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set,
-    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF, WF',
-    #f590, #ffdf]
+    size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, usr getElem_indices_lt, =_ WF,
+    = Array.size_set, WF', #f590, #ffdf]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
@@ -260,26 +260,21 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
     cases #f590
-    next =>
-      cases #ffdf
-      next =>
-        instantiate only
+    · cases #ffdf
+      · instantiate only
         instantiate only [= Array.getElem_set]
-      next =>
-        instantiate only
+      · instantiate only
         instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert,
           = Array.getElem_push]
-    next =>
-      instantiate only [= mem_indices_of_mem, = getElem_def]
+    · instantiate only [= mem_indices_of_mem, = getElem_def]
       instantiate only [usr getElem_indices_lt]
       instantiate only [size]
       cases #ffdf
-      next =>
-        instantiate only [=_ WF]
-        instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
+      · instantiate only [usr getElem_indices_lt, =_ WF]
+        instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set,
+          = Array.getElem_set]
         instantiate only [WF']
-      next =>
-        instantiate only
+      · instantiate only
         instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
 
 /--

tests/lean/run/grind_match_eq_propagation.lean

@@ -73,9 +73,6 @@ def h (v w : Vec α n) : Nat :=
 example : h a b > 0 := by
   grind [h.eq_def]
 
-example : h a b > 0 := by
-  grind -offset [h.eq_def]
-
 -- TODO: introduce casts while instantiating equation theorems for `h.match_1`
 -- example (a b : Vec α 2) : h a b = 20 := by
 --  unfold h

tests/lean/run/grind_offset_cnstr.lean

@@ -1,401 +0,0 @@
-module
-set_option grind.debug true
-set_option warn.sorry false
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [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 (trace) 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
-
-/--
-trace: [grind.debug.proof] intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4)
-      (iff_eq p (a2 ≤ a1)) fun h h_1 h_2 =>
-      intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun h_3 =>
-        Classical.byContradiction
-          (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun h_4 =>
-            id
-              (Eq.mp
-                (Eq.trans (Eq.symm (eq_true h_4))
-                  (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true
-                    (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm h) (eq_false h_1)))
-                      (Nat.lo_lo a2 a3 a4 3 3 h_2
-                        (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1)))))))
-                True.intro))
--/
-#guard_msgs in
-open Lean Grind in
-set_option trace.grind.debug.proof true in
-theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 := by
-  grind -order
-
-/-! Propagate `cnstr = False` tests -/
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p q r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → p ∧ q ∧ r ∧ s := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c → (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → p ∧ q := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c + 1 → (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → p ∧ q := by
-  grind (splits := 0)
-
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → ¬p ∧ ¬r ∧ ¬s := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c → (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → ¬p ∧ ¬r := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p r : Prop) (a b : Nat) : a  ≤ b → b ≤ c + 3 → (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → ¬p ∧ ¬r := by
-  grind (splits := 0)
-
-/-! Propagate `cnstr = False` tests, but with different internalization order -/
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p q : Prop) (a b : Nat) : (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → a ≤ b → b ≤ c → p ∧ q := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p q : Prop) (a b : Nat) : (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → a ≤ b → b ≤ c + 1 → p ∧ q := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p r s : Prop) (a b : Nat) : (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → a ≤ b → b + 2 ≤ c → ¬p ∧ ¬r ∧ ¬s := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p r : Prop) (a b : Nat) : (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → a ≤ b → b ≤ c → ¬p ∧ ¬r := by
-  grind (splits := 0)
-
--- The following example is solved by `grind` using constraint propagation and 0 case-splits.
-#guard_msgs (trace) in
-set_option trace.grind.split true in
-example (p r : Prop) (a b : Nat) : (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → a ≤ b → b ≤ c + 3 → ¬p ∧ ¬r := by
-  grind (splits := 0)
-
-example (a b c d: Nat) : a ≤ b → b + 2 = c → c < d → a + 2 < d := by
-  grind
-
-example (a b c : Nat) : a + 2 = b → b + 3 = c → a + 5 ≤ c := by
-  grind
-
-example (a b c : Nat) : a + 2 = b → c ≤ a + 2 → a + 2 ≤ c → c = b := by
-  grind
-
-example (a b c : Nat) : a + 2 = b → b + 3 = c → a + 5 = c := by
-  grind
-
-example (f : Nat → Nat) (a b c d e : Nat) :
-        f (a + 3) = b →
-        f (c + 1) = d →
-        c ≤ a + 2 →
-        a + 1 ≤ e →
-        e < c →
-        b = d := by
-  grind
-
-example (a : Nat) : a < 2 → a < 5 := by
-  grind
-
-example (a b : Nat) : 2 < a → a ≤ b → 2 < b := by
-  grind
-
-example (a b : Nat) : 2 < a → a ≤ b → 0 < b := by
-  grind
-
-example (f : Nat → Nat) : f 1 = a → b ≤ 1 → b ≥ 1 → f b = a := by
-  grind
-
-example (f : Nat → Nat) : f 2 = a → b ≤ 1 → b ≥ 1 → c = b + 1 → f c = a := by
-  grind
-
-example (a : Nat) : a < 2 → a = 5 → False := by
-  grind
-
-example (a : Nat) : a < 2 → a = b → b = c → c = 5 → False := by
-  grind
-
-example (a b : Nat) : a + 1 = b → b = 0 → False := by
-  grind

tests/lean/run/grind_offset_model.lean

@@ -1,59 +0,0 @@
-module
-def g (i : Nat) (j : Nat) := i + j
-
-set_option grind.debug true
-set_option grind.debug.proofs true
-set_option trace.grind.offset.model true
-
-/--
-trace: [grind.offset.model] i := 1
-[grind.offset.model] j := 0
-[grind.offset.model] 「0」 := 0
-[grind.offset.model] 「i + 1」 := 2
--/
-#guard_msgs (trace) in
-example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = i + 1 := by
-  fail_if_success grind
-  sorry
-
-/--
-trace: [grind.offset.model] i := 101
-[grind.offset.model] 「0」 := 0
--/
-#guard_msgs (trace) in
-example (i : Nat) : i ≤ 100 := by
-  fail_if_success grind
-  sorry
-
-/--
-trace: [grind.offset.model] i := 99
-[grind.offset.model] 「0」 := 0
--/
-#guard_msgs (trace) in
-example (i : Nat) : 100 ≤ i := by
-  fail_if_success grind
-  sorry
-
-/--
-trace: [grind.offset.model] n := 0
-[grind.offset.model] j := 0
-[grind.offset.model] i := 99
-[grind.offset.model] 「0」 := 0
-[grind.offset.model] 「n + 1」 := 1
--/
-#guard_msgs (trace) in
-example (i : Nat) : g (n + 1) m = a → 100 + j ≤ i := by
-  fail_if_success grind
-  sorry
-
-/--
-trace: [grind.offset.model] n := 0
-[grind.offset.model] j := 101
-[grind.offset.model] i := 0
-[grind.offset.model] 「0」 := 0
-[grind.offset.model] 「n + 1」 := 1
--/
-#guard_msgs (trace) in
-example (i : Nat) : g (n + 1) m = a → j ≤ i + 100 := by
-  fail_if_success grind
-  sorry

tests/lean/run/grind_order_2.lean

@@ -1,13 +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 -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)
 
 example (a b c : Nat) : a ≤ b → b ≤ c → c < a → False := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)
 
 example (a b : Nat) : a ≤ 5 → b ≤ 8 → a > 6 ∨ b > 10 → False := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)
 
 example (a b c d : Nat) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by
-  grind -linarith -lia -offset (splits := 0)
+  grind -linarith -lia (splits := 0)

tests/lean/run/grind_order_eq.lean

@@ -11,22 +11,22 @@ example (a b : Int) (f : Int → Int) : a ≤ b + 1 → b ≤ a - 1 → f a = f
   grind -mbtc -lia -linarith (splits := 0)
 
 example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f a = f (1 + b + 0) := by
-  grind -offset -mbtc -lia -linarith (splits := 0)
+  grind -mbtc -lia -linarith (splits := 0)
 
 example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ c → c ≤ a → f a = f c := by
-  grind -offset -mbtc -lia -linarith (splits := 0)
+  grind -mbtc -lia -linarith (splits := 0)
 
 example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f (1 + a) = f (1 + b + 1) := by
-  grind -offset -mbtc -lia -linarith (splits := 0)
+  grind -mbtc -lia -linarith (splits := 0)
 
 example
     : 2*n_1 + a = 1 → 2*n_1 + a = n_2 + 1 → n = 1 → n = n_3 + 1 → n_2 ≠ n_3 → False := by
-  grind -lia -linarith -offset -ring (splits := 0)
+  grind -lia -linarith -ring (splits := 0)
 
 example
     : a = b → a ≤ b + 1 := by
-  grind -lia -linarith -offset -ring (splits := 0) only
+  grind -lia -linarith -ring (splits := 0) only
 
 example
     : a = b + 1 → a ≤ b + 2 := by
-  grind -lia -linarith -offset -ring (splits := 0) only
+  grind -lia -linarith -ring (splits := 0) only

tests/lean/run/grind_order_issue.lean

@@ -99,7 +99,7 @@ attribute [local grind] getIdx findIdx insert
 
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
-  grind -offset -ring -linarith -lia =>
+  grind -ring -linarith -lia =>
     instantiate only [= getElem_def, insert]
     cases #f590
     next =>
@@ -114,7 +114,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
 
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
-  grind -offset -ring -linarith -lia =>
+  grind -ring -linarith -lia =>
     instantiate only [= getElem_def, insert]
     cases #f590
     next =>

tests/lean/run/grind_pre.lean

@@ -91,20 +91,6 @@ end
 
 def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
 
-/--
-trace: [grind.offset.model] i := 1
-[grind.offset.model] j := 0
-[grind.offset.model] 「0」 := 0
-[grind.offset.model] 「i + j」 := 0
-[grind.offset.model] 「i + 1」 := 2
-[grind.offset.model] 「i + j + 1」 := 1
--/
-#guard_msgs (trace) in
-set_option trace.grind.offset.model true in
-example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
-  fail_if_success grind
-  sorry
-
 structure Point where
   x : Nat
   y : Int