feat: missing cases for equality propagation from core to cutsat (#7220)

This PR implements the missing cases for equality propagation from the
`grind` core to the cutsat module.

src/Init/Data/Int/Linear.lean

@@ -997,6 +997,15 @@ theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
   rw [Int.mul_comm]
   assumption
 
+def eq_of_core_cert (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
+  p₃ == p₁.combine (p₂.mul (-1))
+
+theorem eq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
+    : eq_of_core_cert p₁ p₂ p₃ → p₁.denote' ctx = p₂.denote' ctx → p₃.denote' ctx = 0 := by
+  simp [eq_of_core_cert]
+  intro; subst p₃; simp
+  intro h; rw [h, ←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

@@ -139,24 +139,36 @@ def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
     elimStack := x :: s.elimStack
   }
 
+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
+    return .add 1 var (.num 0)
+  else if let some k ← getIntValue? a then
+    return .num k
+  else
+    throwError "internal `grind` error, expression is not relevant to cutsat{indentExpr a}"
+
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
-  trace[grind.cutsat.eq] "{mkIntEq a b}"
-  -- TODO
-  return ()
+  let p₁ ← exprAsPoly a
+  let p₂ ← exprAsPoly b
+  let p := p₁.combine (p₂.mul (-1))
+  let c ← mkEqCnstr p (.core p₁ p₂ (← mkEqProof a b))
+  c.assert
 
 @[export lean_process_new_cutsat_lit]
 def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
   let some k ← getIntValue? ke | return ()
-  if let some p := (← get').terms.find? { expr := a } then
-    if k == 0 then
-      (← mkEqCnstr p (.expr (← mkEqProof a ke))).assert
-    else
-      -- TODO
-      return ()
+  let p₁ ← exprAsPoly a
+  let h ← mkEqProof a ke
+  let c ← if k == 0 then
+    mkEqCnstr p₁ (.expr h)
   else
-    -- TODO: `a` is a variable
-    return ()
+    let p₂ ← exprAsPoly ke
+    let p := p₁.combine (p₂.mul (-1))
+    mkEqCnstr p (.core p₁ p₂ h)
+  c.assert
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where

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

@@ -77,6 +77,8 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
   match c'.h with
   | .expr h =>
     return h
+  | .core p₁ p₂ h =>
+    return mkApp6 (mkConst ``Int.Linear.eq_of_core) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c'.p) reflBoolTrue h
   | .norm c =>
     return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (toExpr c.p) (toExpr c'.p) reflBoolTrue (← c.toExprProof)
   | .divCoeffs c =>

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

@@ -58,6 +58,7 @@ structure EqCnstr where
 
 inductive EqCnstrProof where
   | expr (h : Expr)
+  | core (p₁ p₂ : Poly) (h : Expr)
   | norm (c : EqCnstr)
   | divCoeffs (c : EqCnstr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)

tests/lean/run/grind_cutsat_eq_1.lean

@@ -48,6 +48,22 @@ example (a b c : Int) (_ : a + c > 1) (_ : a + 2*b = 0) (_ : -c + 2*b = 0) : Fal
 example (a b c : Int) (_ : -a + -c > 1) (_ : a + 2*b = 0) (_ : -c + 2*b = 0) : False := by
   grind
 
+example {p : Prop} (a c : Int) :
+        a + 2*c > 10 →
+        p ∨ [a + c] = [5 - c] →
+        ¬p →
+        False := by
+  grind
+
+example (a : Int) : a > 2 → a = 0 → False := by
+  grind
+
+example (a b : Int) : a = 0 → b = 1 → a + b > 2 → False := by
+  grind
+
+example (a b c : Int) : a = 0 → a + b > 2 → b = c → 1 = c → False := by
+  grind
+
 #print ex₁
 #print ex₂
 #print ex₃