fix: simplify interface between grind core and cutsat (#8564)

This PR simplifies the interface between the `grind` core and the cutsat
procedure. Before this PR, core would try to minimize the number of
numeric literals that have to be internalized in cutsat. This
optimization was buggy (see `grind_cutsat_zero.lean` test), and produced
counterintuitive counterexamples.

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

@@ -228,10 +228,10 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
     { d, p, h := .ofEq x c : DvdCnstr }.assert
 
 private def exprAsPoly (a : Expr) : GoalM Poly := do
-  if let some var := (← get').varMap.find? { expr := a } then
-    return .add 1 var (.num 0)
-  else if let some k ← getIntValue? a then
+  if let some k ← getIntValue? a then
     return .num k
+  else if let some var := (← get').varMap.find? { expr := a } then
+    return .add 1 var (.num 0)
   else
     throwError "internal `grind` error, expression is not relevant to cutsat{indentExpr a}"
 
@@ -259,23 +259,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
   | some .nat, some .nat => processNewNatEq a b
   | _, _ => return ()
 
-private def processNewIntLitEq (a ke : Expr) : GoalM Unit := do
-  let some k ← getIntValue? ke | return ()
-  let p₁ ← exprAsPoly a
-  let c ← if k == 0 then
-    pure { p := p₁, h := .core0 a ke : EqCnstr }
-  else
-    let p₂ ← exprAsPoly ke
-    let p := p₁.combine (p₂.mul (-1))
-    pure { p, h := .core a ke p₁ p₂ : EqCnstr }
-  c.assert
-
-@[export lean_process_cutsat_eq_lit]
-def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
-  match (← foreignTerm? a) with
-  | none => processNewIntLitEq a ke
-  | some .nat => processNewNatEq a ke
-
 private def processNewIntDiseq (a b : Expr) : GoalM Unit := do
   let p₁ ← exprAsPoly a
   let c ← if let some 0 ← getIntValue? b then
@@ -334,7 +317,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   match k with
   | .add => return false
   | .mul => return declName == ``HMul.hMul
-  | .num => return declName == ``HMul.hMul || declName == ``Eq
+  | .num => return declName == ``HMul.hMul
   | _ => unreachable!
 
 private def internalizeInt (e : Expr) : GoalM Unit := do
@@ -413,7 +396,7 @@ Internalizes an integer (and `Nat`) expression. Here are the different cases tha
 
 - `a + b` when `parent?` is not `+`, `≤`, or `∣`
 - `k * a` when `k` is a numeral and `parent?` is not `+`, `*`, `≤`, `∣`
-- numerals when `parent?` is not `+`, `*`, `≤`, `∣`, `=`.
+- numerals when `parent?` is not `+`, `*`, `≤`, `∣`.
   Recall that we must internalize numerals to make sure we can propagate equalities
   back to the congruence closure module. Example: we have `f 5`, `f x`, `x - y = 3`, `y = 2`.
 -/
@@ -425,7 +408,6 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     match k with
     | .div => propagateDiv e
     | .mod => propagateMod e
-    | .num => pure ()
     | _ => internalizeInt e
   else if type.isConstOf ``Nat then
     if (← hasForeignVar e) then return ()
@@ -434,7 +416,6 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     | .sub => propagateNatSub e
     | .natAbs => propagateNatAbs e
     | .toNat => propagateToNat e
-    | .num => pure ()
     | _ => internalizeNat e
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -130,6 +130,7 @@ assert that `e` is nonnegative.
 -/
 def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := withIncRecDepth do
   if e.isAppOf ``NatCast.natCast then return ()
+  if e.isAppOf ``OfNat.ofNat then return () -- we don't want to propagate constraints such as `2 ≥ 0`
   let some rhs ← Int.OfNat.ofDenoteAsIntExpr? e |>.run | return ()
   let gen ← getGeneration e
   let ctx ← getForeignVars .nat
@@ -146,6 +147,7 @@ asserts that it is nonnegative.
 def assertNatCast (e : Expr) (x : Var) : GoalM Unit := do
   let_expr NatCast.natCast _ inst a := e | return ()
   let_expr instNatCastInt := inst | return ()
+  if a.isAppOf ``OfNat.ofNat then return () -- we don't want to propagate constraints such as `2 ≥ 0`
   if (← get').foreignDef.contains { expr := a } then return ()
   let n ← mkForeignVar a .nat
   let p := .add (-1) x (.num 0)

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

@@ -113,14 +113,6 @@ inductive PendingTheoryPropagation where
     none
   | /-- Propagate the equality `lhs = rhs`. -/
     eq (lhs rhs : Expr)
-  |
-    /--
-    Propagate the literal equality `lhs = lit`.
-    This is needed because some solvers do not internalize literal values.
-    Remark: we may remove this optimization in the future because it adds complexity
-    for a small performance gain.
-    -/
-    eqLit (lhs lit : Expr)
   | /-- Propagate the disequalities in `ps`. -/
     diseqs (ps : ParentSet)
 
@@ -153,25 +145,19 @@ private def checkCutsatEq (rhsRoot lhsRoot : ENode) : GoalM PendingTheoryPropaga
   | some lhsCutsat =>
     if let some rhsCutsat := rhsRoot.cutsat? then
       return .eq lhsCutsat rhsCutsat
-    else if isNum rhsRoot.self then
-      return .eqLit lhsCutsat rhsRoot.self
     else
       -- We have to retrieve the node because other fields have been updated
       let rhsRoot ← getENode rhsRoot.self
       setENode rhsRoot.self { rhsRoot with cutsat? := lhsCutsat }
       return .diseqs (← getParents rhsRoot.self)
   | none =>
-    if let some rhsCutsat := rhsRoot.cutsat? then
-      if isNum lhsRoot.self then
-        return .eqLit rhsCutsat lhsRoot.self
-      else
-        return .diseqs (← getParents lhsRoot.self)
+    if rhsRoot.cutsat?.isSome then
+      return .diseqs (← getParents lhsRoot.self)
     else
       return .none
 
 def propagateCutsat : PendingTheoryPropagation → GoalM Unit
   | .eq lhs rhs => Arith.Cutsat.processNewEq lhs rhs
-  | .eqLit lhs lit => Arith.Cutsat.processNewEqLit lhs lit
   | .diseqs ps => propagateCutsatDiseqs ps
   | .none => return ()
 

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

@@ -982,13 +982,6 @@ Notifies the cutsat module that `a = b` where
 @[extern "lean_process_cutsat_eq"] -- forward definition
 opaque Arith.Cutsat.processNewEq (a b : Expr) : GoalM Unit
 
-/--
-Notifies the cutsat module that `a = k` where
-`a` is term that has been internalized by this module, and `k` is a numeral.
--/
-@[extern "lean_process_cutsat_eq_lit"] -- forward definition
-opaque Arith.Cutsat.processNewEqLit (a k : Expr) : GoalM Unit
-
 /--
 Notifies the cutsat module that `a ≠ b` where
 `a` and `b` are terms that have been internalized by this module.
@@ -1064,8 +1057,6 @@ def markAsCutsatTerm (e : Expr) : GoalM Unit := do
   let root ← getRootENode e
   if let some e' := root.cutsat? then
     Arith.Cutsat.processNewEq e e'
-  else if isNum root.self && !isSameExpr e root.self then
-    Arith.Cutsat.processNewEqLit e root.self
   else
     setENode root.self { root with cutsat? := some e }
     propagateCutsatDiseqs (← getParents root.self)

tests/lean/run/grind_const_pattern.lean

@@ -18,6 +18,8 @@ h : ¬a = 10
     [prop] ¬a = 10
   [eqc] False propositions
     [prop] a = 10
+  [cutsat] Assignment satisfying linear constraints
+    [assign] a := 1
 -/
 #guard_msgs (error) in
 example : a = 5 + 5 := by
@@ -47,6 +49,9 @@ h : ¬f a = 11
     [prop] ¬f a = 11
   [eqc] False propositions
     [prop] f a = 11
+  [cutsat] Assignment satisfying linear constraints
+    [assign] a := 2
+    [assign] f a := 1
 -/
 #guard_msgs (error) in
 example : f a = 10 + 1 := by
@@ -70,6 +75,10 @@ h : ¬f x = 11
     [prop] f x = 11
   [ematch] E-matching patterns
     [thm] fa: [f `[a]]
+  [cutsat] Assignment satisfying linear constraints
+    [assign] x := 3
+    [assign] a := 2
+    [assign] f x := 1
 -/
 #guard_msgs (error) in
 example : f x = 10 + 1 := by

tests/lean/run/grind_cutsat_diseq_1.lean

@@ -78,10 +78,6 @@ trace: [grind.cutsat.assert] -1*e + 1 ≤ 0
 example (a b c d e : Int) : a = d → c = b → c = e → e > 0 → a + b < 0 → d ≠ c → False := by
   (fail_if_success grind); sorry
 
-#guard_msgs (trace) in -- no propagation to cutsat
-example (a b c d e : Int) : a = d → c = b → c = e → a = 1 → d ≠ c → False := by
-  (fail_if_success grind); sorry
-
 example (a b c : Int) : a + 2*b = 0 → c + b = -b → a = c := by
   grind
 

tests/lean/run/grind_cutsat_diseq_2.lean

@@ -13,6 +13,7 @@ theorem ex₃ (a b c : Int) : a + b + c = 0 → a = c → b = 4 → c = -2 := by
 
 /--
 trace: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
+[grind.cutsat.assert] -1*「0」 = 0
 [grind.cutsat.assert] 「a + -2 * b + -2 * c」 = 0
 [grind.cutsat.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0
 [grind.cutsat.assert] 「a + -2 * b + -2 * d」 ≠ 0

tests/lean/run/grind_cutsat_div_1.lean

@@ -66,6 +66,8 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): Fals
 /--
 trace: [grind.debug.cutsat.search.assign] f 0 := 11
 [grind.debug.cutsat.search.assign] f 1 := 2
+[grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in

tests/lean/run/grind_cutsat_eq_1.lean

@@ -4,6 +4,7 @@ open Int.Linear
 
 /--
 trace: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
+[grind.cutsat.assert] -1*「0」 = 0
 [grind.cutsat.assert] 「b + f a + 1」 = 0
 -/
 #guard_msgs (trace) in

tests/lean/run/grind_cutsat_nat_le.lean

@@ -32,9 +32,11 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
 trace: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
 [grind.cutsat.assert] -1*↑c ≤ 0
 [grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
+[grind.cutsat.assert] -1*↑0 = 0
 [grind.cutsat.assert] ↑c = 0
 [grind.cutsat.assert] 0 ≤ 0
 [grind.cutsat.assert] 「↑a * ↑b」 + 1 ≤ 0
+[grind.cutsat.assert] -1*↑0 + ↑c = 0
 [grind.cutsat.assert] 1 ≤ 0
 -/
 #guard_msgs (trace) in

tests/lean/run/grind_ring_1.lean

@@ -29,7 +29,10 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
   grind +ring
 
 /--
-trace: [grind.ring] new ring: BitVec 8
+trace: [grind.ring] new ring: Int
+[grind.ring] characteristic: 0
+[grind.ring] NoNatZeroDivisors available: true
+[grind.ring] new ring: BitVec 8
 [grind.ring] characteristic: 256
 [grind.ring] NoNatZeroDivisors available: false
 -/

tests/lean/run/grind_split_issue.lean

@@ -25,6 +25,9 @@ h_1 : ⋯ ≍ ⋯
     [eqc] {s, 0}
   [cases] Case analyses
     [cases] [1/2]: X c 0
+  [cutsat] Assignment satisfying linear constraints
+    [assign] c := 1
+    [assign] s := 0
 -/
 #guard_msgs (error) in
 example {c : Nat} (q : X c 0) : False := by

tests/lean/run/grind_t1.lean

@@ -380,6 +380,8 @@ h_1 : b = true
   [eqc] Equivalence classes
     [eqc] {a, if b = true then 10 else 20, 10}
     [eqc] {b, true}
+  [cutsat] Assignment satisfying linear constraints
+    [assign] a := 10
 -/
 #guard_msgs (error) in
 example (b : Bool) : (if b then 10 else 20) = a → b = true → False := by