fix: cutsat counterexamples (#7829)

This PR fixes an issue in the cutsat counterexamples. It removes the
optimization (`Cutsat.State.terms`) that was used to avoid the new
theorem `eq_def`. In the two new tests, prior to this PR, `cutsat`
produced a bogus counterexample with `b := 2`.

src/Init/Data/Int/Linear.lean

@@ -1819,6 +1819,14 @@ theorem not_le_of_le (ctx : Context) (p q : Poly) (k : Nat)
   rw [← Int.add_assoc, ← Int.add_assoc, Int.add_neg_cancel_right, Lean.Omega.Int.add_le_zero_iff_le_neg']
   simp; exact Int.le_trans h (Int.ofNat_zero_le _)
 
+def eq_def_cert (x : Var) (xPoly : Poly) (p : Poly) : Bool :=
+  p == .add (-1) x xPoly
+
+theorem eq_def (ctx : Context) (x : Var) (xPoly : Poly) (p : Poly)
+    : eq_def_cert x xPoly p → x.denote ctx = xPoly.denote' ctx → p.denote' ctx = 0 := by
+  simp [eq_def_cert]; intro _ h; subst p; simp [h]
+  rw [← Int.sub_eq_add_neg, Int.sub_self]
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

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

@@ -226,9 +226,7 @@ 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 p := (← get').terms.find? { expr := a } then
-    return p
-  else if let some var := (← get').varMap.find? { expr := a } then
+  if let some var := (← get').varMap.find? { expr := a } then
     return .add 1 var (.num 0)
   else if let some k ← getIntValue? a then
     return .num k
@@ -342,30 +340,16 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   | _ => unreachable!
 
 private def internalizeInt (e : Expr) : GoalM Unit := do
-  if (← get').terms.contains { expr := e } then return ()
+  if (← hasVar e) then return ()
   let p ← toPoly e
-  trace[grind.debug.cutsat.markTerm] "internalizeInt: {e}"
-  unless (← isVar e) do
-    /-
-    We did not use to have the test `isVar e`. The test was added to prevent redundant invocations
-    to `markAsCutsatTerm` which would trigger equalities of the form `x = x` being propagated.
-    This redundancy only affected performance and "polluted" trace messages with redundant information.
-    Consider the following example:
-    ```
-    set_option trace.grind.debug.cutsat.eq true in
-    example (a b : Nat) : c > a * b → c >= 1 := by
-      grind
-    ```
-    Without this test, it would produce:
-    ```
-    [grind.debug.cutsat.eq] ↑a * ↑b = ↑a * ↑b
-    [grind.debug.cutsat.eq] ↑a * ↑b = ↑a * ↑b
-    [grind.debug.cutsat.eq] c = 0
-    ```
-    -/
-    markAsCutsatTerm e
   trace[grind.cutsat.internalize] "{aquote e}:= {← p.pp}"
-  modify' fun s => { s with terms := s.terms.insert { expr := e } p }
+  let x ← mkVar e
+  if p == .add 1 x (.num 0) then
+    -- It is pointless to assert `x = x`
+    -- This can happen if `e` is a nonlinear term (e.g., `e` is `a*b`)
+    return
+  let c := { p := .add (-1) x p, h := .defn e p : EqCnstr }
+  c.assert
 
 private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
   if b == 0 || b == 1 || b == -1 then
@@ -423,6 +407,7 @@ 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
     discard <| mkForeignVar e .nat

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

@@ -139,6 +139,9 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
     let ctx ← getForeignContext .nat
     let h := mkApp4 (mkConst ``Int.OfNat.of_eq) ctx (← mkNatExprDecl lhs) (← mkNatExprDecl rhs) (← mkEqProof a b)
     return mkApp6 (mkConst ``Int.Linear.eq_norm_expr) (← getContext) (← mkExprDecl lhs') (← mkExprDecl rhs') (← mkPolyDecl c'.p) reflBoolTrue h
+  | .defn e p =>
+    let some x := (← get').varMap.find? { expr := e } | throwError "`grind` internal error, missing cutsat variable{indentExpr e}"
+    return mkApp6 (mkConst ``Int.Linear.eq_def) (← getContext) (toExpr x) (← mkPolyDecl p) (← mkPolyDecl c'.p) reflBoolTrue (← mkEqRefl e)
   | .norm c =>
     return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof)
   | .divCoeffs c =>
@@ -416,7 +419,7 @@ private def markAsFound (fvarId : FVarId) : CollectDecVarsM Unit := do
 mutual
 partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core0 .. | .core .. | .coreNat .. => return () -- Equalities coming from the core never contain cutsat decision variables
+  | .core0 .. | .core .. | .coreNat .. | .defn .. => return () -- Equalities coming from the core never contain cutsat decision variables
   | .norm c | .divCoeffs c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 

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

@@ -89,6 +89,8 @@ inductive EqCnstrProof where
   | divCoeffs (c : EqCnstr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | ofLeGe (c₁ : LeCnstr) (c₂ : LeCnstr)
+  | /-- `e` is `p` -/
+    defn (e : Expr) (p : Poly)
 
 /-- A divisibility constraint and its justification/proof. -/
 structure DvdCnstr where
@@ -230,11 +232,6 @@ structure State where
   /-- Mapping from `Expr` to a variable representing it. -/
   varMap  : PHashMap ENodeKey Var := {}
   /--
-  Mapping from terms (e.g., `x + 2*y + 2`, `3*x`, `5`) to polynomials representing them.
-  These are terms used to propagate equalities between this module and the congruence closure module.
-  -/
-  terms : PHashMap ENodeKey Poly := {}
-  /--
   Mapping from foreign terms to their variable and type (e.g., `Nat`). They are also marked using `markAsCutsatTerm`.
   -/
   foreignVarMap : PHashMap ENodeKey (Var × ForeignType) := {}

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

@@ -60,7 +60,7 @@ def getVar (x : Var) : GoalM Expr :=
   return (← get').vars[x]!
 
 /-- Returns `true` if `e` is already associated with a cutsat variable. -/
-def isVar (e : Expr) : GoalM Bool :=
+def hasVar (e : Expr) : GoalM Bool :=
   return (← get').varMap.contains { expr := e }
 
 /-- Returns `true` if `x` has been eliminated using an equality constraint. -/

tests/lean/run/grind_cutsat_diseq_2.lean

@@ -12,8 +12,10 @@ theorem ex₃ (a b c : Int) : a + b + c = 0 → a = c → b = 4 → c = -2 := by
   grind
 
 /--
-info: [grind.cutsat.assert] a + -2*b + -2*c = 0
-[grind.cutsat.assert] a + -2*b + -2*d ≠ 0
+info: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 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
 [grind.cutsat.diseq] d + -1*c ≠ 0
 [grind.cutsat.assert] -1*d + c = 0
 [grind.cutsat.assert] 0 ≠ 0

tests/lean/run/grind_cutsat_eq_1.lean

@@ -5,7 +5,10 @@ open Int.Linear
 -- set_option trace.grind.cutsat.assert true
 -- set_option trace.grind.cutsat.internalize true
 
-/-- info: [grind.cutsat.eq] b + 「f a」 + 1 = 0 -/
+/--
+info: [grind.cutsat.eq] -1*「b + f a + 1」 + b + 「f a」 + 1 = 0
+[grind.cutsat.eq] b + 「f a」 + 1 = 0
+-/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.eq true in
 example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2)  : False := by

tests/lean/run/grind_mbtc_1.lean

@@ -43,3 +43,24 @@ example (f : Nat → Nat) (x : Nat)
 example (f : Nat → Nat → Nat) (x y : Nat)
     : x ≠ 0 → x ≤ 1 → f x y = 2 → f 1 y = 2 := by
   grind
+
+
+-- `b` must not be `2`. Otherwise, `f (b+1)` and `f 3` must be equal.
+/-- info: [grind.cutsat.model] b := 3 -/
+#guard_msgs (info) in
+set_option trace.grind.cutsat.model true in
+example (f : Int → α) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x = y := by
+  (fail_if_success grind); sorry
+
+-- `b` must not be `2`. Otherwise, `f (b+1)` and `f 3` must be equal.
+/--
+info: [grind.cutsat.model] x := 7
+[grind.cutsat.model] y := 8
+[grind.cutsat.model] b := 3
+[grind.cutsat.model] 「f 3」 := 8
+[grind.cutsat.model] 「f (b + 1)」 := 7
+-/
+#guard_msgs (info) in
+set_option trace.grind.cutsat.model true in
+example (f : Int → Int) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x = y := by
+  (fail_if_success grind); sorry