feat: combine two cutsat proof steps (#7371)

This PR combines two cutsat proof steps that often appear together.

src/Init/Data/Int/Linear.lean

@@ -846,6 +846,26 @@ theorem le_combine (ctx : Context) (p₁ p₂ p₃ : Poly)
   · rw [← Int.zero_mul (Poly.denote ctx p₂)]; apply Int.mul_le_mul_of_nonpos_right <;> simp [*]
   · rw [← Int.zero_mul (Poly.denote ctx p₁)]; apply Int.mul_le_mul_of_nonpos_right <;> simp [*]
 
+def le_combine_coeff_cert (p₁ p₂ p₃ : Poly) (k : Int) : Bool :=
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  let p  := p₁.mul a₂ |>.combine (p₂.mul a₁)
+  k > 0 && (p.divCoeffs k && p₃ == p.div k)
+
+theorem le_combine_coeff (ctx : Context) (p₁ p₂ p₃ : Poly) (k : Int)
+    : le_combine_coeff_cert p₁ p₂ p₃ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
+  simp only [le_combine_coeff_cert, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, and_imp]
+  let a₁ := p₁.leadCoeff.natAbs
+  let a₂ := p₂.leadCoeff.natAbs
+  generalize h : (p₁.mul a₂ |>.combine (p₂.mul a₁)) = p
+  intro h₁ h₂ h₃ h₄ h₅
+  have := le_combine ctx p₁ p₂ p
+  simp only [le_combine_cert, beq_iff_eq] at this
+  have aux₁ := this h.symm h₄ h₅
+  have := le_coeff ctx p p₃ k
+  simp only [le_coeff_cert, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, and_imp] at this
+  exact this h₁ h₂ h₃ aux₁
+
 theorem le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe → p.denote' ctx ≤ 0 → False := by
   simp [Poly.isUnsatLe]; split <;> simp
 

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

@@ -105,6 +105,11 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
       (← getContext) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
       reflBoolTrue
       (← c₁.toExprProof) (← c₂.toExprProof)
+  | .combineDivCoeffs c₁ c₂ k =>
+    return mkApp8 (mkConst ``Int.Linear.le_combine_coeff)
+      (← getContext) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) (toExpr k)
+      reflBoolTrue
+      (← c₁.toExprProof) (← c₂.toExprProof)
   | .subst x c₁ c₂ =>
     let a := c₁.p.coeff x
     let thm := if a ≥ 0 then
@@ -285,7 +290,7 @@ partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do u
   | .expr h => collectExpr h
   | .notExpr .. => return () -- This kind of proof is used for connecting with the `grind` core.
   | .cooper c | .norm c | .divCoeffs c => c.collectDecVars
-  | .combine c₁ c₂ | .subst _ c₁ c₂ | .ofLeDiseq c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
+  | .combine c₁ c₂ | .combineDivCoeffs c₁ c₂ _ | .subst _ c₁ c₂ | .ofLeDiseq c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
   | .ofDiseqSplit (decVars := decVars) .. => decVars.forM markAsFound
 
 partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do

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

@@ -275,7 +275,11 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
     trace[grind.cutsat.conflict] "not resolved"
     return false
   else
-    let c := { p, h := .combine c₁ c₂ : LeCnstr }
+    let k := p.gcdCoeffs'
+    let c := if k == 1 then
+      { p, h := .combine c₁ c₂ : LeCnstr }
+    else
+      { p := p.div k, h := .combineDivCoeffs c₁ c₂ k : LeCnstr }
     trace[grind.cutsat.conflict] "resolved: {← c.pp}"
     c.assert
     return true

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

@@ -153,6 +153,7 @@ inductive LeCnstrProof where
   | norm (c : LeCnstr)
   | divCoeffs (c : LeCnstr)
   | combine (c₁ c₂ : LeCnstr)
+  | combineDivCoeffs (c₁ c₂ : LeCnstr) (k : Int)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : LeCnstr)
   | ofLeDiseq (c₁ : LeCnstr) (c₂ : DiseqCnstr)
   | ofDiseqSplit (c₁ : DiseqCnstr) (decVar : FVarId) (h : UnsatProof) (decVars : Array FVarId)