max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: proof terms for grind ring and grind cutsat (#9710)

Browse source 
This PR improves some of the proof terms produced by `grind ring` and
`grind cutsat`.
This commit is contained in:
Leonardo de Moura 2025-08-04 14:27:11 +02:00 • committed by GitHub
parent 3eab35ef22
commit ae728d84f0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 66 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Data/Int/Basic.lean
View file

@ -410,6 +410,20 @@ instance : Max Int := maxOfLe
(fun a => Int.rec (fun b => Nat.beq a b) (fun _ => false) b)
(fun a => Int.rec (fun _ => false) (fun b => Nat.beq a b) b) a
/-- `x ≤ y` for kernel reduction. -/
@[expose] protected noncomputable def ble' (a b : Int) : Bool :=
Int.rec
(fun a => Int.rec (fun b => Nat.ble a b) (fun _ => false) b)
(fun a => Int.rec (fun _ => true) (fun b => Nat.ble b a) b)
a
/-- `x < y` for kernel reduction. -/
@[expose] protected noncomputable def blt' (a b : Int) : Bool :=
Int.rec
(fun a => Int.rec (fun b => Nat.blt a b) (fun _ => false) b)
(fun a => Int.rec (fun _ => true) (fun b => Nat.blt b a) b)
a
end Int
/--

12
src/Init/Data/Int/LemmasAux.lean
View file

@ -69,6 +69,18 @@ theorem natCast_succ_pos (n : Nat) : 0 < (n.succ : Int) := natCast_pos.2 n.succ_
@[simp, norm_cast] theorem cast_id {n : Int} : Int.cast n = n := rfl
@[simp] theorem ble'_eq_true (a b : Int) : (Int.ble' a b = true) = (a ≤ b) := by
cases a <;> cases b <;> simp [Int.ble'] <;> omega
@[simp] theorem blt'_eq_true (a b : Int) : (Int.blt' a b = true) = (a < b) := by
cases a <;> cases b <;> simp [Int.blt'] <;> omega
@[simp] theorem ble'_eq_false (a b : Int) : (Int.ble' a b = false) = ¬(a ≤ b) := by
simp [← Bool.not_eq_true]
@[simp] theorem blt'_eq_false (a b : Int) : (Int.blt' a b = false) = ¬ (a < b) := by
simp [← Bool.not_eq_true]
/-! ### toNat -/
@[simp] theorem toNat_sub' (a : Int) (b : Nat) : (a - b).toNat = a.toNat - b := by

32
src/Init/Data/Int/Linear.lean
View file

@ -586,7 +586,7 @@ theorem norm_eq_coeff' (ctx : Context) (p p' : Poly) (k : Int) : p = p'.mul k
@[expose]
noncomputable def norm_eq_coeff_cert (lhs rhs : Expr) (p : Poly) (k : Int) : Bool :=
(lhs.sub rhs).norm.beq' (p.mul_k k) |>.and' (k > 0)
(lhs.sub rhs).norm.beq' (p.mul_k k) |>.and' (Int.blt' 0 k)
theorem norm_eq_coeff (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int)
: norm_eq_coeff_cert lhs rhs p k → (lhs.denote ctx = rhs.denote ctx) = (p.denote' ctx = 0) := by
@ -653,7 +653,7 @@ private theorem eq_of_norm_eq_of_divCoeffs {ctx : Context} {p₁ p₂ : Poly} {k
@[expose]
noncomputable def norm_le_coeff_tight_cert (lhs rhs : Expr) (p : Poly) (k : Int) : Bool :=
let p' := lhs.sub rhs |>.norm
(k > 0 : Bool) |>.and' (p'.divCoeffs k |>.and' (p.beq' (p'.div k)))
(Int.blt' 0 k) |>.and' (p'.divCoeffs k |>.and' (p.beq' (p'.div k)))
theorem norm_le_coeff_tight (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int)
: norm_le_coeff_tight_cert lhs rhs p k → (lhs.denote ctx ≤ rhs.denote ctx) = (p.denote' ctx ≤ 0) := by
@ -765,7 +765,7 @@ private theorem poly_eq_zero_eq_false (ctx : Context) {p : Poly} {k : Int} : p.d
@[expose]
noncomputable def unsatEqDivCoeffCert (lhs rhs : Expr) (k : Int) : Bool :=
let p := (lhs.sub rhs).norm
p.divCoeffs k |>.and' ((k > 0 : Bool) |>.and' (cmod p.getConst k < 0))
p.divCoeffs k |>.and' (Int.blt' 0 k |>.and' (cmod p.getConst k < 0))
theorem eq_eq_false_of_divCoeff (ctx : Context) (lhs rhs : Expr) (k : Int) : unsatEqDivCoeffCert lhs rhs k → (lhs.denote ctx = rhs.denote ctx) = False := by
simp [unsatEqDivCoeffCert]
@ -997,7 +997,7 @@ theorem le_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm.beq' p₂) : p
@[expose]
noncomputable def le_coeff_cert (p₁ p₂ : Poly) (k : Int) : Bool :=
(k > 0 : Bool).and' (p₁.divCoeffs k |>.and' (p₂.beq' (p₁.div k)))
Int.blt' 0 k |>.and' (p₁.divCoeffs k |>.and' (p₂.beq' (p₁.div k)))
theorem le_coeff (ctx : Context) (p₁ p₂ : Poly) (k : Int) : le_coeff_cert p₁ p₂ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
simp [le_coeff_cert]
@ -1042,12 +1042,12 @@ noncomputable 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₁.combine_mul_k a₂ a₁ p₂
(k > 0 : Bool).and' (p.divCoeffs k |>.and' (p₃.beq' (p.div k)))
Int.blt' 0 k |>.and' (p.divCoeffs k |>.and' (p₃.beq' (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, Bool.and'_eq_and,
Poly.beq'_eq, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, and_imp]
Poly.beq'_eq, Bool.and_eq_true, and_imp]
let a₁ := p₁.leadCoeff.natAbs
let a₂ := p₂.leadCoeff.natAbs
generalize h : (p₁.combine_mul_k a₂ a₁ p₂) = p
@ -1056,7 +1056,7 @@ theorem le_combine_coeff (ctx : Context) (p₁ p₂ p₃ : Poly) (k : Int)
simp only [le_combine_cert, Poly.beq'_eq] at this
have aux₁ := this h.symm h₄ h₅
have := le_coeff ctx p p₃ k
simp only [le_coeff_cert, Bool.and'_eq_and, Poly.beq'_eq, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, and_imp] at this
simp only [le_coeff_cert, Bool.and'_eq_and, Poly.beq'_eq, Bool.and_eq_true, 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
@ -1081,7 +1081,7 @@ theorem eq_unsat (ctx : Context) (p : Poly) : p.isUnsatEq → p.denote' ctx = 0
@[expose]
noncomputable def eq_unsat_coeff_cert (p : Poly) (k : Int) : Bool :=
p.divCoeffs k |>.and' ((k > 0 : Bool).and' (cmod p.getConst k < 0))
p.divCoeffs k |>.and' (Int.blt' 0 k |>.and' (cmod p.getConst k < 0))
theorem eq_unsat_coeff (ctx : Context) (p : Poly) (k : Int) : eq_unsat_coeff_cert p k → p.denote' ctx = 0 → False := by
simp [eq_unsat_coeff_cert]
@ -1208,7 +1208,7 @@ theorem eq_eq_subst' (ctx : Context) (a b : Int) (p₁ : Poly) (p₂ : Poly) (p
noncomputable def eq_le_subst_nonneg_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
let a := p₁.coeff x
let b := p₂.coeff x
(a ≥ 0 : Bool).and' (p₃.beq' (p₂.combine_mul_k a (-b) p₁))
Int.ble' 0 a |>.and' (p₃.beq' (p₂.combine_mul_k a (-b) p₁))
theorem eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
: eq_le_subst_nonneg_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
@ -1224,7 +1224,7 @@ theorem eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
noncomputable def eq_le_subst_nonpos_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
let a := p₁.coeff x
let b := p₂.coeff x
(a ≤ 0 : Bool).and' (p₃.beq' (p₁.combine_mul_k b (-a) p₂))
Int.ble' a 0 |>.and' (p₃.beq' (p₁.combine_mul_k b (-a) p₂))
theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
: eq_le_subst_nonpos_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
@ -1933,12 +1933,12 @@ noncomputable def dvd_le_tight_cert (d : Int) (p₁ p₂ p₃ : Poly) : Bool :=
let b₁ := p₁.getConst
let b₂ := p₂.getConst
let p := p₁.addConst_k (-b₁)
(d > 0 : Bool) |>.and' (p₂.beq' (p.addConst_k b₂) |>.and' (p₃.beq' (p.addConst_k (b₁ - d*((b₁ - b₂)/d)))))
Int.blt' 0 d |>.and' (p₂.beq' (p.addConst_k b₂) |>.and' (p₃.beq' (p.addConst_k (b₁ - d*((b₁ - b₂)/d)))))
theorem dvd_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly)
: dvd_le_tight_cert d p₁ p₂ p₃ → d ∣ p₁.denote' ctx → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
simp only [dvd_le_tight_cert, gt_iff_lt, Bool.and'_eq_and, Poly.beq'_eq, Bool.and_eq_true,
Poly.addConst_k_eq_addConst, decide_eq_true_eq, and_imp]
simp only [dvd_le_tight_cert, Bool.and'_eq_and, Poly.beq'_eq, Bool.and_eq_true,
Poly.addConst_k_eq_addConst, Int.blt'_eq_true, and_imp]
generalize p₂.getConst = b₂
intro hd _ _; subst p₂ p₃
have := eq_neg_addConst_add ctx p₁
@ -1957,7 +1957,7 @@ noncomputable def dvd_neg_le_tight_cert (d : Int) (p₁ p₂ p₃ : Poly) : Bool
let p := p₁.addConst_k (-b₁)
let b₁ := -b₁
let p := p.mul_k (-1)
(d > 0 : Bool) |>.and' (p₂.beq' (p.addConst_k b₂) |>.and' (p₃.beq' (p.addConst_k (b₁ - d*((b₁ - b₂)/d)))))
Int.blt' 0 d |>.and' (p₂.beq' (p.addConst_k b₂) |>.and' (p₃.beq' (p.addConst_k (b₁ - d*((b₁ - b₂)/d)))))
theorem Poly.mul_minus_one_getConst_eq (p : Poly) : (p.mul (-1)).getConst = -p.getConst := by
simp [Poly.mul]
@ -1965,8 +1965,8 @@ theorem Poly.mul_minus_one_getConst_eq (p : Poly) : (p.mul (-1)).getConst = -p.g
theorem dvd_neg_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly)
: dvd_neg_le_tight_cert d p₁ p₂ p₃ → d ∣ p₁.denote' ctx → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
simp only [dvd_neg_le_tight_cert, gt_iff_lt, Poly.beq'_eq, Bool.and'_eq_and, Bool.and_eq_true,
decide_eq_true_eq, and_imp]
simp only [dvd_neg_le_tight_cert, Poly.beq'_eq, Bool.and'_eq_and, Bool.and_eq_true,
Int.blt'_eq_true, and_imp]
generalize p₂.getConst = b₂
intro hd _ _; subst p₂ p₃
simp only [Poly.denote'_eq_denote, Int.reduceNeg, Poly.addConst_k_eq_addConst, Poly.denote_addConst, Poly.denote_mul, Poly.mul_k_eq_mul,

45
src/Init/Grind/Ring/Poly.lean
View file

@ -7,6 +7,7 @@ module
prelude
public import Init.Data.Nat.Lemmas
public import Init.Data.Int.LemmasAux
public import Init.Data.Hashable
public import all Init.Data.Ord
public import Init.Data.RArray
@ -41,23 +42,25 @@ def Var.denote {α} (ctx : Context α) (v : Var) : α :=
ctx.get v
@[expose]
def denoteInt {α} [Ring α] (k : Int) : α :=
bif k < 0 then
- OfNat.ofNat (α := α) k.natAbs
else
OfNat.ofNat (α := α) k.natAbs
noncomputable def denoteInt {α} [Ring α] (k : Int) : α :=
Bool.rec
(OfNat.ofNat (α := α) k.natAbs)
(- OfNat.ofNat (α := α) k.natAbs)
(Int.blt' k 0)
@[expose]
def Expr.denote {α} [Ring α] (ctx : Context α) : Expr → α
| .add a b => denote ctx a + denote ctx b
| .sub a b => denote ctx a - denote ctx b
| .mul a b => denote ctx a * denote ctx b
| .neg a => -denote ctx a
| .num k => denoteInt k
| .natCast k => NatCast.natCast (R := α) k
| .intCast k => IntCast.intCast (R := α) k
| .var v => v.denote ctx
| .pow a k => denote ctx a ^ k
noncomputable def Expr.denote {α} [Ring α] (ctx : Context α) (e : Expr) : α :=
Expr.rec
(fun k => denoteInt k)
(fun k => NatCast.natCast (R := α) k)
(fun k => IntCast.intCast (R := α) k)
(fun x => x.denote ctx)
(fun _ ih => - ih)
(fun _ _ ih₁ ih₂ => ih₁ + ih₂)
(fun _ _ ih₁ ih₂ => ih₁ - ih₂)
(fun _ _ ih₁ ih₂ => ih₁ * ih₂)
(fun _ k ih => ih ^ k)
e
structure Power where
x : Var
@ -797,7 +800,7 @@ q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
```
-/
@[expose]
def NullCert.denote {α} [CommRing α] (ctx : Context α) : NullCert → α
noncomputable def NullCert.denote {α} [CommRing α] (ctx : Context α) : NullCert → α
| .empty => 0
| .add q lhs rhs nc => (q.denote ctx)*(lhs.denote ctx - rhs.denote ctx) + nc.denote ctx
@ -840,9 +843,9 @@ open Ring hiding sub_eq_add_neg
open CommSemiring
theorem denoteInt_eq {α} [CommRing α] (k : Int) : denoteInt (α := α) k = k := by
simp [denoteInt, cond_eq_if] <;> split
next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← intCast_neg, ← Int.eq_neg_natAbs_of_nonpos (Int.le_of_lt h)]
next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← Int.eq_natAbs_of_nonneg (Int.le_of_not_gt h)]
simp [denoteInt] <;> cases h : k.blt' 0 <;> simp <;> simp at h
next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← Int.eq_natAbs_of_nonneg h]
next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← Ring.intCast_neg, ← Int.eq_neg_natAbs_of_nonpos (Int.le_of_lt h)]
theorem Power.denote_eq {α} [Semiring α] (ctx : Context α) (p : Power)
: p.denote ctx = p.x.denote ctx ^ p.k := by
@ -1596,14 +1599,14 @@ theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx :
theorem not_le_norm' {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
: core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by
simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
replace h := add_le_right (rhs.denote ctx) h
replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) ≤ _ := add_le_right (rhs.denote ctx) h
rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
contradiction
theorem not_lt_norm' {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
: core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by
simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
replace h := add_lt_right (rhs.denote ctx) h
replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) < _ := add_lt_right (rhs.denote ctx) h
rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
contradiction