chore: remove grind offset (#11051)

This PR removes the `grind offset` module because it is (now) subsumed
by `grind order`.

Author: leodemoura

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,35 +8,18 @@ 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
 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