From 00a4503c4f63c04001e874cbaa31d744ad00854b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Mar 2025 15:28:49 -0800 Subject: [PATCH] feat: combine two cutsat proof steps (#7371) This PR combines two cutsat proof steps that often appear together. --- src/Init/Data/Int/Linear.lean | 20 +++++++++++++++++++ .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean | 7 ++++++- .../Tactic/Grind/Arith/Cutsat/Search.lean | 6 +++++- .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 1 + 4 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 6d79f71aff..adef51f1a1 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index 91ea44c7ce..1c4b32a04e 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean index 71821f9c12..a673949d19 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index 3f71f3290b..c66d2ece96 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/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)