feat: MBTC for linarith

Author: leodemoura

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

@@ -19,6 +19,7 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq
 import Lean.Meta.Tactic.Grind.Arith.Linear.Internalize
 import Lean.Meta.Tactic.Grind.Arith.Linear.Model
 import Lean.Meta.Tactic.Grind.Arith.Linear.PP
+import Lean.Meta.Tactic.Grind.Arith.Linear.MBTC
 
 namespace Lean
 

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

@@ -0,0 +1,62 @@
+/-
+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.Canon
+import Lean.Meta.Tactic.Grind.MBTC
+import Lean.Meta.Tactic.Grind.Arith.Linear.Model
+import Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq
+
+namespace Lean.Meta.Grind.Arith.Linear
+
+private partial def toRatValue? (a : Expr) : Option Rat :=
+  if a.isAppOfArity ``Zero.zero 2 then
+    some 0
+  else if a.isAppOfArity ``One.one 2 then
+    some 1
+  else if a.isAppOfArity ``OfNat.ofNat 3 then
+    toRatValue? (a.getArg! 1)
+  else if a.isAppOfArity ``Neg.neg 3 then
+    (- ·) <$> toRatValue? a.appArg!
+  else if a.isAppOfArity ``HDiv.hDiv 6 then
+    (· / ·) <$> toRatValue? a.appFn!.appArg! <*> toRatValue? a.appArg!
+  else if let .lit (.natVal n) := a then
+    some (Std.Internal.mkRat n 1)
+  else
+    none
+
+private def getAssignmentExt? (s : Struct) (a : Expr) : Option Rat := do
+  if let some v := getAssignment? s a then
+    some v
+  else
+    toRatValue? a
+
+private def hasTheoryVar (e : Expr) : GoalM Bool := do
+  return (← getRootENode e).linarith?.isSome || (toRatValue? e).isSome
+
+private def isInterpreted (e : Expr) : GoalM Bool := do
+  if isInterpretedTerm e then return true
+  let f := e.getAppFn
+  return f.isConstOf ``LE.le || f.isConstOf ``LT.lt || f.isConstOf ``Dvd.dvd
+
+private def eqAssignment (a b : Expr) : GoalM Bool := do
+  let structId₁? := (← get).arith.linear.exprToStructId.find? { expr := a }
+  let structId₂? := (← get).arith.linear.exprToStructId.find? { expr := b }
+  let some structId := structId₁? <|> structId₂? | return false
+  let s := (← get).arith.linear.structs[structId]!
+  -- It is pointless to generate case-splits unless we have support for disequality.
+  unless s.linearInst?.isSome do return false
+  let some v₁ := getAssignmentExt? s a | return false
+  let some v₂ := getAssignmentExt? s b | return false
+  return v₁ == v₂
+
+def mbtc : GoalM Bool := do
+  Grind.mbtc {
+    hasTheoryVar := hasTheoryVar
+    isInterpreted := isInterpreted
+    eqAssignment := eqAssignment
+  }
+
+end Lean.Meta.Grind.Arith.Linear

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

@@ -16,7 +16,7 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.Proof
 
 namespace Lean.Meta.Grind.Arith.Linear
 /-- Returns `some structId` if `a` and `b` are elements of the same structure. -/
-private def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
+def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
   let some structId ← getTermStructId? a | return none
   let some structId' ← getTermStructId? b | return none
   unless structId == structId' do return none -- This can happen when we have heterogeneous equalities

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

@@ -47,7 +47,8 @@ where
           intros gen
         else
           break
-      if (← assertAll <||> Arith.check <||> ematch <||> lookahead <||> splitNext <||> Arith.Cutsat.mbtc <||> tryFallback) then
+      if (← assertAll <||> Arith.check <||> ematch <||> lookahead <||> splitNext <||> Arith.Cutsat.mbtc
+          <||> Arith.Linear.mbtc <||> tryFallback) then
         continue
       return some (← getGoal) -- failed
     return none -- solved

tests/lean/run/grind_linarith_2.lean

@@ -88,3 +88,17 @@ set_option trace.grind.linarith.model true in
 example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
     : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → b = c → a ≠ b → False := by
   grind
+
+/-- trace: [grind.split] x = 0, generation: 0 -/
+#guard_msgs (trace) in
+set_option trace.grind.split true in
+example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (f : α → α) (x : α)
+    : Zero.zero ≤ x → x ≤ 0 → f x = a → f 0 = a := by
+  grind
+
+-- should not split on `x = 0` since `α` is not a linear order
+#guard_msgs (drop error, trace) in
+set_option trace.grind.split true in
+example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (f : α → α) (x : α)
+    : Zero.zero ≤ x → x ≤ 0 → f x = a → f 0 = a := by
+  grind