From 3d730e35cb2b04cbf563fad80eb2daaa0b0cc5d0 Mon Sep 17 00:00:00 2001 From: Alexander Hicks Date: Tue, 14 Jul 2026 13:05:11 +0100 Subject: [PATCH 1/2] bump 4.32 --- CompPoly/Bivariate/ToPoly.lean | 2 - .../Binary/AdditiveNTT/Correctness.lean | 5 +- CompPoly/Fields/Binary/BF128Ghash/Basic.lean | 17 ++++--- CompPoly/Fields/Binary/BF128Ghash/Impl.lean | 20 +++++--- .../Fields/Binary/Tower/Concrete/Basis.lean | 2 +- CompPoly/Multivariate/MvPolyEquiv/Core.lean | 5 +- .../Multivariate/MvPolyEquiv/Instances.lean | 51 +++++++++++-------- CompPoly/Multivariate/Operations.lean | 4 +- CompPoly/Multivariate/Rename.lean | 6 +-- CompPoly/ToMathlib/MvPolynomial/Equiv.lean | 11 ++-- .../ToMathlib/Polynomial/BivariateDegree.lean | 3 +- CompPoly/Univariate/CMvEquiv.lean | 2 + CompPoly/Univariate/DivisionCorrectness.lean | 27 ++++++---- .../Univariate/NTTFast/Correctness/Basic.lean | 8 +-- .../Univariate/NTTFast/Correctness/Pair.lean | 14 ++--- CompPoly/Univariate/Quotient/Core.lean | 3 +- CompPoly/Univariate/ToPoly/Core.lean | 4 +- lake-manifest.json | 20 ++++---- lakefile.lean | 2 +- lean-toolchain | 2 +- 20 files changed, 120 insertions(+), 88 deletions(-) diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 576f890c..c83dd623 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -313,8 +313,6 @@ lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] ofPoly (0 : R[X][Y]) = 0 := by unfold CBivariate.ofPoly simp +decide [ Polynomial.support ] - erw [Finsupp.support_zero] - exact Finset.sum_empty /-- Ring hom from computable bivariates to Mathlib bivariates. -/ noncomputable def toPolyRingHom diff --git a/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean b/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean index 8c57bcf4..0339dff9 100644 --- a/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean +++ b/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean @@ -660,6 +660,7 @@ lemma initial_tiled_coeffs_correctness (h_ℓ : ℓ ≤ r) (a : Fin (2 ^ ℓ) simp only [Nat.getLowBits_eq_mod_two_pow] omit [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 in +set_option maxHeartbeats 10000000 in lemma NTTStage_correctness (i : Fin (ℓ)) (input_buffer : Fin (2 ^ (ℓ + R_rate)) → L) (original_coeffs : Fin (2 ^ ℓ) → L) : additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate (evaluation_buffer := input_buffer) @@ -762,7 +763,7 @@ lemma NTTStage_correctness (i : Fin (ℓ)) conv_lhs => enter [1] simp only [h_j_div_2_pow_left] - congr + congr 1 simp only [even_coeffs_poly, cur_coeffs] have h_res := evenRefinement_eq_novel_poly_of_0_leading_suffix 𝔽q β h_ℓ_add_R_rate ⟨i, by omega⟩ ⟨Nat.getLowBits i.val j.val, by @@ -848,7 +849,7 @@ lemma NTTStage_correctness (i : Fin (ℓ)) simp only [h_k, ↓reduceIte] rw [h_get_lsb_eq] apply Nat.sum_of_and_eq_zero_is_or h_lsb_and_two_pow_eq_zero - congr + simp only [h_v_eq] rw [h_even_split, h_odd_split] rw [h_P_i_split_even_odd] have h_x0_eq_cur_evaluation_point : x0 = cur_evaluation_point := by diff --git a/CompPoly/Fields/Binary/BF128Ghash/Basic.lean b/CompPoly/Fields/Binary/BF128Ghash/Basic.lean index 02a4673f..519a4a5d 100644 --- a/CompPoly/Fields/Binary/BF128Ghash/Basic.lean +++ b/CompPoly/Fields/Binary/BF128Ghash/Basic.lean @@ -184,15 +184,19 @@ def ofGF2 : ZMod 2 →+* BF128Ghash := algebraMap (ZMod 2) BF128Ghash /-- The generator of the field (root of the GHASH polynomial). -/ def root : BF128Ghash := AdjoinRoot.root ghashPoly +set_option maxRecDepth 100000 in /-- The root satisfies the GHASH polynomial equation: root^128 + root^7 + root^2 + root + 1 = 0 -/ theorem root_satisfies_poly : root^128 + root^7 + root^2 + root + 1 = 0 := by - unfold root ghashPoly - have h := AdjoinRoot.eval₂_root ghashPoly - unfold ghashPoly at h - simp only [eval₂_add, eval₂_X, eval₂_one] at h - erw [eval₂_pow, eval₂_X, eval₂_pow, eval₂_X, eval₂_pow, eval₂_X] at h - exact h + calc + _ = (AdjoinRoot.mk ghashPoly X)^128 + (AdjoinRoot.mk ghashPoly X)^7 + + (AdjoinRoot.mk ghashPoly X)^2 + AdjoinRoot.mk ghashPoly X + 1 := by + simp only [root, AdjoinRoot.mk_X] + _ = AdjoinRoot.mk ghashPoly (X^128 + X^7 + X^2 + X + 1) := by + rw [map_add, map_add, map_add, map_add, map_pow, map_pow, map_pow, map_one] + _ = 0 := by + change AdjoinRoot.mk ghashPoly ghashPoly = 0 + exact AdjoinRoot.mk_self /-- BF128Ghash is a finite type. -/ instance : Fintype BF128Ghash := by @@ -204,6 +208,7 @@ instance : Fintype BF128Ghash := by exact Finite.of_equiv (Fin pb.dim →₀ ZMod 2) (pb.basis.repr.toEquiv.symm) exact Fintype.ofFinite BF128Ghash +set_option maxRecDepth 100000 in /-- The cardinality of BF128Ghash is 2^128. -/ theorem BF128Ghash_card : Fintype.card BF128Ghash = 2^128 := by -- Use the fact that AdjoinRoot of an irreducible polynomial of degree d diff --git a/CompPoly/Fields/Binary/BF128Ghash/Impl.lean b/CompPoly/Fields/Binary/BF128Ghash/Impl.lean index 9e150ed9..e1cfa98f 100644 --- a/CompPoly/Fields/Binary/BF128Ghash/Impl.lean +++ b/CompPoly/Fields/Binary/BF128Ghash/Impl.lean @@ -420,10 +420,10 @@ instance : AddCommGroup ConcreteBF128Ghash where nsmul := fun n x => if n % 2 = 0 then 0 else x zsmul := fun n x => if n % 2 = 0 then 0 else x nsmul_zero := fun x => by - simp only [Nat.zero_mod, ↓reduceIte, ofNat_eq_ofNat] + rfl nsmul_succ := nsmul_succ zsmul_zero' := fun x => by - simp only [EuclideanDomain.zero_mod, ↓reduceIte, ofNat_eq_ofNat] + rfl zsmul_succ' := zsmul_succ zsmul_neg' := zsmul_neg @@ -605,7 +605,10 @@ lemma intCast_negSucc (n : ℕ) : intCast (Int.negSucc n) = -(↑(n + 1) : Concr simp only [natCast_eq, natCast, h_mod]; rfl rw [h_nat]; rfl -instance : Ring ConcreteBF128Ghash where +instance instSemigroupConcreteBF128Ghash : Semigroup ConcreteBF128Ghash where + mul_assoc := mul_assoc + +instance instRingConcreteBF128Ghash : Ring ConcreteBF128Ghash where mul_assoc := mul_assoc one_mul := one_mul mul_one := mul_one @@ -613,6 +616,9 @@ instance : Ring ConcreteBF128Ghash where right_distrib := right_distrib zero_mul := zero_mul mul_zero := mul_zero + npow := npowRecAuto + npow_zero := by intro x; rfl + npow_succ := by intro n x; rfl natCast := natCast natCast_zero := natCast_zero natCast_succ := natCast_succ @@ -825,8 +831,10 @@ instance instHDivConcreteBF128Ghash : HDiv (ConcreteBF128Ghash) (ConcreteBF128Gh lemma div_eq_mul_inv (a b : ConcreteBF128Ghash) : a / b = a * b⁻¹ := by rfl -instance : DivisionRing ConcreteBF128Ghash where - toRing := inferInstance +set_option maxRecDepth 100000 in +set_option maxHeartbeats 10000000 in +instance instDivisionRingConcreteBF128Ghash : DivisionRing ConcreteBF128Ghash where + toRing := instRingConcreteBF128Ghash inv := Inv.inv exists_pair_ne := exists_pair_ne mul_inv_cancel := mul_inv_cancel @@ -841,7 +849,7 @@ lemma mul_comm (a b : ConcreteBF128Ghash) : a * b = b * a := by exact _root_.mul_comm (toQuot a) (toQuot b) instance instFieldConcreteBF128Ghash : Field ConcreteBF128Ghash where - toDivisionRing := inferInstance + toDivisionRing := instDivisionRingConcreteBF128Ghash mul_comm := mul_comm end DivisionRing_Field_Instances diff --git a/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean b/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean index 34a15e1b..b224f35d 100644 --- a/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean +++ b/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean @@ -235,7 +235,7 @@ theorem minPoly_of_powerBasisSucc_generator (k : ℕ) : let r := q.coeff 0 have hc : c = q.leadingCoeff := by rw [Polynomial.leadingCoeff] - exact congrArg q.toFinsupp.2 (id (Eq.symm hqNatDeg)) + exact congrArg q.toFinsupp.coeff (id (Eq.symm hqNatDeg)) have hc_ne_zero : c ≠ 0 := by rw [hc] by_contra h_c_eq_zero diff --git a/CompPoly/Multivariate/MvPolyEquiv/Core.lean b/CompPoly/Multivariate/MvPolyEquiv/Core.lean index 37f12aac..ab88766b 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Core.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Core.lean @@ -31,7 +31,7 @@ def fromCMvPolynomial (p : CMvPolynomial n R) : MvPolynomial (Fin n) R := let support : List (Fin n →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp let toFun (f : Fin n →₀ ℕ) : R := p[CMvMonomial.ofFinsupp f]?.getD 0 let mem_support_fun {a : Fin n →₀ ℕ} : a ∈ support ↔ toFun a ≠ 0 := by grind - Finsupp.mk support.toFinset toFun (by simp [mem_support_fun]) + AddMonoidAlgebra.ofCoeff <| Finsupp.mk support.toFinset toFun (by simp [mem_support_fun]) noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n R := let ⟨s, f, _⟩ := p @@ -114,7 +114,8 @@ lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _ omit [BEq R] [LawfulBEq R] in lemma coeff_eq {m} (a : CMvPolynomial n R) : - MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := rfl + MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := by + rfl @[aesop simp] lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial n R} : diff --git a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean index 89a99996..b537df6a 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean @@ -191,7 +191,8 @@ lemma foldl_eq_sum {β : Type*} [AddCommMonoid β] {t : CMvPolynomial n R} {f : CMvMonomial n → R → β} : ExtTreeMap.foldl (fun x m c => (f m c) + x) 0 t.1 = - Finsupp.sum (fromCMvPolynomial t) (f ∘ CMvMonomial.ofFinsupp) := by + Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial t)) + (f ∘ CMvMonomial.ofFinsupp) := by unfold Finsupp.sum Finset.sum simp only [Function.comp_apply, add_comm] rw [ExtTreeMap.foldl_eq_foldl_toList] @@ -221,8 +222,9 @@ lemma coeff_sum [AddCommMonoid α] lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial {f : (Fin n →₀ ℕ) → R → Lawful n R } {a : CMvPolynomial n R} : - fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) f) = - Finsupp.sum (fromCMvPolynomial a) (fun m c ↦ fromCMvPolynomial (f m c)) := by + fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) f) = + Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) + (fun m c ↦ fromCMvPolynomial (f m c)) := by unfold Finsupp.sum; ext simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum] @@ -231,34 +233,40 @@ lemma map_mul (a b : CMvPolynomial n R) : fromCMvPolynomial (a * b) = fromCMvPolynomial a * fromCMvPolynomial b := by dsimp only [HMul.hMul, Mul.mul, Lawful.mul, Unlawful.mul] simp only [CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful] - unfold MonoidAlgebra.mul' + unfold AddMonoidAlgebra.mul' rw [foldl_eq_sum]; simp_rw [foldl_eq_sum] let F₀ (p q) : CMvMonomial n → R → Lawful n R := fun p_1 q_1 ↦ Lawful.fromUnlawful {(p + p_1 , q * q_1)} set F₁ : (Fin n →₀ ℕ) → R → Lawful n R := - (fun p q ↦ Finsupp.sum (fromCMvPolynomial b) (F₀ p q ∘ CMvMonomial.ofFinsupp)) + (fun p q ↦ Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial b)) + (F₀ p q ∘ CMvMonomial.ofFinsupp)) ∘ CMvMonomial.ofFinsupp with eqF₁ let F₂ a₁ b₁ : - Multiplicative (Fin n →₀ ℕ) → R → MonoidAlgebra R (Multiplicative (Fin n →₀ ℕ)) := - fun a₂ b₂ ↦ MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂) - set F₃ : Multiplicative (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R := - fun a₁ b₁ ↦ Finsupp.sum (fromCMvPolynomial b) (F₂ a₁ b₁) with eqF₃ - have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Multiplicative (Fin n →₀ ℕ)} {c₁ : R} : + (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R := + fun a₂ b₂ ↦ AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂) + set F₃ : (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R := + fun a₁ b₁ ↦ Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial b)) (F₂ a₁ b₁) with eqF₃ + have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Fin n →₀ ℕ} {c₁ : R} : fromCMvPolynomial (F₁ m₁ c₁) = F₃ m₁ c₁ := by dsimp only [Function.comp_apply, F₁, F₀, F₃, F₂] rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial] simp only [Function.comp_apply] congr - ext (m₂ : Multiplicative _) c₂ m + ext (m₂ : Fin n →₀ ℕ) c₂ m rw [coeff_eq] unfold coeff Lawful.fromUnlawful - erw [Unlawful.filter_get, ←CMvMonomial.map_mul, ExtTreeMap.singleton_eq_insert] + erw [Unlawful.filter_get, + ←CMvMonomial.map_mul (m₁ := Multiplicative.ofAdd m₁) (m₂ := Multiplicative.ofAdd m₂), + ExtTreeMap.singleton_eq_insert] erw [ExtTreeMap.getElem?_insert] - by_cases m_in : m = m₁ * m₂ - · rw [←m_in] + by_cases m_in : m = m₁ + m₂ + · subst m + have hmono : CMvMonomial.ofFinsupp (Multiplicative.ofAdd m₁ * Multiplicative.ofAdd m₂) = + CMvMonomial.ofFinsupp (m₁ + m₂) := rfl + rw [hmono] simp only [compare_self] - unfold MvPolynomial.coeff MonoidAlgebra.single - simp only [m_in, ite_true, Option.getD_some] + unfold MvPolynomial.coeff AddMonoidAlgebra.single + simp only [ite_true, Option.getD_some] erw [Finsupp.single_eq_same] · simp only [ Std.compare_eq_iff_eq, @@ -266,7 +274,7 @@ lemma map_mul (a b : CMvPolynomial n R) : not_false_eq_true, getElem?_neg ] - unfold MvPolynomial.coeff MonoidAlgebra.single + unfold MvPolynomial.coeff AddMonoidAlgebra.single erw [Finsupp.single_eq_of_ne (by symm; grind)] split next h contra => @@ -274,8 +282,8 @@ lemma map_mul (a b : CMvPolynomial n R) : apply CMvMonomial.injective_ofFinsupp contra next h => simp_all only [Option.getD_none] -- Lean 4.29 may beta-reduce F₃; fold it back then rewrite - change fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) F₁) = - Finsupp.sum (fromCMvPolynomial a) F₃ + change fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) F₁) = + Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) F₃ rw [show F₃ = fun σ x ↦ fromCMvPolynomial (F₁ σ x) from by ext x; rw [fromCMvPolynomial_F₁_eq_F₃]] rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial] @@ -309,7 +317,10 @@ instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where natCast_zero := rfl natCast_succ := by intro n; simp npow_zero := by intro x; simp [npowRecAuto, npowRec] - npow_succ := by intro n x; simp [npowRecAuto, npowRec] + npow_succ := by + intro n x + change x ^ (n + 1) = x ^ n * x + exact pow_succ x n mul_comm a b := by apply fromCMvPolynomial_injective simp [mul_comm] diff --git a/CompPoly/Multivariate/Operations.lean b/CompPoly/Multivariate/Operations.lean index 4a39078e..4587da5c 100644 --- a/CompPoly/Multivariate/Operations.lean +++ b/CompPoly/Multivariate/Operations.lean @@ -413,8 +413,8 @@ lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {k : ℕ} lemma fromCMvPolynomial_finsupp_sum {n k : ℕ} [CommSemiring R] [BEq R] [LawfulBEq R] (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) (a : CMvPolynomial n R) : - fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) = - Finsupp.sum (fromCMvPolynomial a) + fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) g) = + Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) (fun μ c => fromCMvPolynomial (g μ c)) := by unfold Finsupp.sum; ext simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum] diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean index 2ceb3975..ed40a0ec 100644 --- a/CompPoly/Multivariate/Rename.lean +++ b/CompPoly/Multivariate/Rename.lean @@ -108,8 +108,8 @@ lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) : lemma fromCMvPolynomial_finsupp_sum {k : ℕ} (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) (a : CMvPolynomial n R) : - fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) = - Finsupp.sum (fromCMvPolynomial a) + fromCMvPolynomial (Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) g) = + Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) (fun μ c => fromCMvPolynomial (g μ c)) := by unfold Finsupp.sum; ext simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum] @@ -124,7 +124,7 @@ lemma fromCMvPolynomial_rename (f : Fin n → Fin m) MvPolynomial.rename f (fromCMvPolynomial p) := by -- Express rename as a `Finsupp.sum` via `foldl_eq_sum` have step1 : CMvPolynomial.rename f p = - Finsupp.sum (fromCMvPolynomial p) (fun μ c => + Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial p)) (fun μ c => CMvPolynomial.monomial (CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by show Std.ExtTreeMap.foldl diff --git a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean index 4c200b57..24e02e45 100644 --- a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean +++ b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean @@ -150,16 +150,13 @@ variable. -/ theorem support_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) : (finSuccEquivNth R p f).support = Finset.image (fun m : Fin (n + 1) →₀ ℕ => m p) f.support := by ext i - rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff] + simp only [Polynomial.mem_support_iff, ne_eq, MvPolynomial.ext_iff, coeff_zero, not_forall, + Finset.mem_image, mem_support_iff, finSuccEquivNth_coeff_coeff] constructor · rintro ⟨m, hm⟩ - refine ⟨m.insertNth p i, ?_, insertNth_apply_same _ _ _⟩ - rw [← support_coeff_finSuccEquivNth] - simpa [mem_support_iff, coeff] using hm + exact ⟨m.insertNth p i, hm, insertNth_apply_same _ _ _⟩ · rintro ⟨m, h, rfl⟩ - refine ⟨m.removeNth p, ?_⟩ - rwa [← coeff, zero_apply, ← mem_support_iff, support_coeff_finSuccEquivNth, - insertNth_self_removeNth] + exact ⟨m.removeNth p, by simpa using h⟩ theorem mem_support_finSuccEquivNth {f : MvPolynomial (Fin (n + 1)) R} {x} : x ∈ (finSuccEquivNth R p f).support ↔ x ∈ (fun m : Fin (n + 1) →₀ _ ↦ m p) '' f.support := by diff --git a/CompPoly/ToMathlib/Polynomial/BivariateDegree.lean b/CompPoly/ToMathlib/Polynomial/BivariateDegree.lean index 7e6526df..949bd613 100644 --- a/CompPoly/ToMathlib/Polynomial/BivariateDegree.lean +++ b/CompPoly/ToMathlib/Polynomial/BivariateDegree.lean @@ -436,7 +436,8 @@ theorem degreeX_mul [IsDomain F] (f g : F[X][Y]) (hf : f ≠ 0) (hg : g ≠ 0) : /-- The evaluation at a point of a bivariate polynomial in the first variable `X`. -/ def evalX (a : F) (f : F[X][Y]) : Polynomial F := - ⟨Finsupp.mapRange (Polynomial.eval a) eval_zero f.toFinsupp⟩ + ⟨AddMonoidAlgebra.ofCoeff + (Finsupp.mapRange (Polynomial.eval a) eval_zero f.toFinsupp.coeff)⟩ /-- The evaluation at a point of a bivariate polynomial in the second variable `Y`. -/ def evalY (a : F) (f : F[X][Y]) : Polynomial F := diff --git a/CompPoly/Univariate/CMvEquiv.lean b/CompPoly/Univariate/CMvEquiv.lean index 175857e0..85a9c827 100644 --- a/CompPoly/Univariate/CMvEquiv.lean +++ b/CompPoly/Univariate/CMvEquiv.lean @@ -63,6 +63,8 @@ private lemma mvToUnivariate_eq_map_finSuccEquiv [CommSemiring R] · intro r simp [MvPolynomial.finSuccEquiv_apply, Polynomial.map_C, MvPolynomial.isEmptyRingEquiv] + change r = MvPolynomial.coeff (0 : Fin 0 →₀ ℕ) (MvPolynomial.C r) + simp [MvPolynomial.coeff_C] · intro i have hi : i = 0 := Subsingleton.elim _ _ subst hi diff --git a/CompPoly/Univariate/DivisionCorrectness.lean b/CompPoly/Univariate/DivisionCorrectness.lean index c90b2020..bdec9f2e 100644 --- a/CompPoly/Univariate/DivisionCorrectness.lean +++ b/CompPoly/Univariate/DivisionCorrectness.lean @@ -407,6 +407,7 @@ private lemma raw_toPoly_degree_lt_of_size_lt (p q : Raw R) have hp : p.size ≤ m := by omega simp [Raw.coeff, hp] +set_option maxHeartbeats 10000000 in private theorem raw_divModByMonicAux_go_spec (q : Raw R) (hqtrim : q.trim = q) (hqmonic : q.leadingCoeff = 1) (hqpos : 0 < q.size) (hqdegree : q.toPoly.degree = ((q.size - 1 : Nat) : WithBot Nat)) : @@ -435,7 +436,7 @@ private theorem raw_divModByMonicAux_go_spec (q : Raw R) · rw [Raw.toPoly_zero] ring · exact raw_toPoly_degree_lt_of_size_lt p q hsize hqdegree - · simp [hsize] + · simp only [hsize, ↓reduceIte] let step := (p - Raw.C p.leadingCoeff * (q * Raw.X ^ (p.size - q.size))).trim have hstep_size : step.size < p.size := by exact div_step_size_lt p q hptrim hqtrim hqmonic hsize hqpos @@ -444,20 +445,26 @@ private theorem raw_divModByMonicAux_go_spec (q : Raw R) have hstep_fuel : step.size ≤ fuel := by omega have ihstep := ih step hstep_trim hstep_fuel rcases ihstep with ⟨hrel, hdeg⟩ + have hrel' := hrel + dsimp only [step] at hrel' + change + (Raw.divModByMonicAux.go fuel + (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly + + q.toPoly * + (Raw.divModByMonicAux.go fuel + (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).1.toPoly = + (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim.toPoly at hrel' constructor - · change - (Raw.divModByMonicAux.go fuel step q).2.toPoly + - q.toPoly * - ((Raw.divModByMonicAux.go fuel step q).1 + - Raw.C p.leadingCoeff * Raw.X ^ (p.size - q.size)).toPoly = - p.toPoly - rw [Raw.toPoly_add, _root_.mul_add, ← _root_.add_assoc, hrel] - dsimp only [step] + · rw [Raw.toPoly_add, _root_.mul_add, ← _root_.add_assoc, hrel'] rw [Raw.toPoly_trim, Raw.toPoly_sub, Raw.toPoly_mul, Raw.toPoly_C, Raw.toPoly_mul, Raw.toPoly_pow, Raw.toPoly_X] rw [Raw.toPoly_mul, Raw.toPoly_C, Raw.toPoly_pow, Raw.toPoly_X] ring - · exact hdeg + · change + (Raw.divModByMonicAux.go fuel + (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly.degree < + q.toPoly.degree at hdeg + exact hdeg private theorem raw_divModByMonicAux_toPoly_eq (p q : CPolynomial R) (hq_monic : q.toPoly.Monic) : diff --git a/CompPoly/Univariate/NTTFast/Correctness/Basic.lean b/CompPoly/Univariate/NTTFast/Correctness/Basic.lean index 99c26057..f00f23c7 100644 --- a/CompPoly/Univariate/NTTFast/Correctness/Basic.lean +++ b/CompPoly/Univariate/NTTFast/Correctness/Basic.lean @@ -31,8 +31,8 @@ def WellFormed (P : Plan R) : Prop := private theorem foldl_push_size (wm : R) : ∀ xs : List Nat, ∀ (powers : Array R) (w : R), - (List.foldl (fun (b : MProd (Array R) R) (_ : Nat) ↦ - ⟨b.fst.push b.snd, b.snd * wm⟩) ⟨powers, w⟩ xs).fst.size = + (List.foldl (fun (b : Array R × R) (_ : Nat) ↦ + (b.1.push b.2, b.2 * wm)) (powers, w) xs).1.size = powers.size + xs.length | [], powers, _ => by simp | _ :: xs, powers, w => by @@ -45,8 +45,8 @@ private theorem foldl_push_getD (wm : R) : (∀ i, i < offset → powers.getD i 0 = base * wm ^ i) → w = base * wm ^ offset → ∀ i, i < offset + xs.length → - (List.foldl (fun (b : MProd (Array R) R) (_ : Nat) ↦ - ⟨b.fst.push b.snd, b.snd * wm⟩) ⟨powers, w⟩ xs).fst.getD i 0 = + (List.foldl (fun (b : Array R × R) (_ : Nat) ↦ + (b.1.push b.2, b.2 * wm)) (powers, w) xs).1.getD i 0 = base * wm ^ i | [], powers, _w, base, offset, _hsize, hvals, _hw, i, hi => by exact hvals i (by simpa using hi) diff --git a/CompPoly/Univariate/NTTFast/Correctness/Pair.lean b/CompPoly/Univariate/NTTFast/Correctness/Pair.lean index b5ba3021..4c0556bb 100644 --- a/CompPoly/Univariate/NTTFast/Correctness/Pair.lean +++ b/CompPoly/Univariate/NTTFast/Correctness/Pair.lean @@ -195,7 +195,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair have hfoldFst : ∀ xs (accA accB : Array R), (List.foldl - (fun (acc : MProd (Array R) (Array R)) pass ↦ + (fun (acc : Array R × Array R) pass ↦ ⟨(butterflyRadix4StageDIFPairWithTwiddles D (D.logN - 1 - 2 * pass - 1) ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) @@ -206,7 +206,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) ((twiddleTable D)[D.logN - 1 - 2 * pass - 1]?.getD #[]) acc.fst acc.snd).2⟩) - (⟨accA, accB⟩ : MProd (Array R) (Array R)) xs).fst = + (accA, accB) xs).1 = List.foldl (fun acc pass ↦ butterflyRadix4StageDIFWithTwiddles D (D.logN - 1 - 2 * pass - 1) @@ -230,7 +230,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair (D.logN - 1 - 2 * pass - 1) ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) ((twiddleTable D)[D.logN - 1 - 2 * pass - 1]?.getD #[]) accA accB).2⟩ : - MProd (Array R) (Array R)) = + Array R × Array R) = ⟨butterflyRadix4StageDIFWithTwiddles D (D.logN - 1 - 2 * pass - 1) ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) ((twiddleTable D)[D.logN - 1 - 2 * pass - 1]?.getD #[]) accA, @@ -248,7 +248,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair have hfoldSnd : ∀ xs (accA accB : Array R), (List.foldl - (fun (acc : MProd (Array R) (Array R)) pass ↦ + (fun (acc : Array R × Array R) pass ↦ ⟨(butterflyRadix4StageDIFPairWithTwiddles D (D.logN - 1 - 2 * pass - 1) ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) @@ -259,7 +259,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) ((twiddleTable D)[D.logN - 1 - 2 * pass - 1]?.getD #[]) acc.fst acc.snd).2⟩) - (⟨accA, accB⟩ : MProd (Array R) (Array R)) xs).snd = + (accA, accB) xs).2 = List.foldl (fun acc pass ↦ butterflyRadix4StageDIFWithTwiddles D (D.logN - 1 - 2 * pass - 1) @@ -283,7 +283,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair (D.logN - 1 - 2 * pass - 1) ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) ((twiddleTable D)[D.logN - 1 - 2 * pass - 1]?.getD #[]) accA accB).2⟩ : - MProd (Array R) (Array R)) = + Array R × Array R) = ⟨butterflyRadix4StageDIFWithTwiddles D (D.logN - 1 - 2 * pass - 1) ((twiddleTable D)[D.logN - 1 - 2 * pass]?.getD #[]) ((twiddleTable D)[D.logN - 1 - 2 * pass - 1]?.getD #[]) accA, @@ -311,7 +311,7 @@ theorem runStagesDIFRadix4PairWithTwiddles_eq_pair hfoldSnd (List.range' 0 (D.logN / 2)) (NTT.loadNaturalArray D a) (NTT.loadNaturalArray D b) · simp [runStagesDIFRadix4PairWithTwiddles, runStagesDIFRadix4WithTwiddles, hodd] - constructor + apply Prod.ext · simpa only [Prod.fst, Prod.snd] using hfoldFst (List.range' 0 (D.logN / 2)) (NTT.loadNaturalArray D a) (NTT.loadNaturalArray D b) diff --git a/CompPoly/Univariate/Quotient/Core.lean b/CompPoly/Univariate/Quotient/Core.lean index 4fbd0cec..8d72cafb 100644 --- a/CompPoly/Univariate/Quotient/Core.lean +++ b/CompPoly/Univariate/Quotient/Core.lean @@ -548,7 +548,8 @@ instance : AddCommGroup (QuotientCPolynomial R) where zsmul_zero' := nsmul_zero zsmul_succ' := by intro n a - simpa [zsmulRec] using nsmul_succ n a + change nsmul n.succ a = nsmul n a + a + exact nsmul_succ n a zsmul_neg' := by intro n a rfl diff --git a/CompPoly/Univariate/ToPoly/Core.lean b/CompPoly/Univariate/ToPoly/Core.lean index bf1ce3b4..fa0b2872 100644 --- a/CompPoly/Univariate/ToPoly/Core.lean +++ b/CompPoly/Univariate/ToPoly/Core.lean @@ -43,13 +43,13 @@ noncomputable def Raw.toPoly [Semiring R] (p : CPolynomial.Raw R) : Polynomial R /-- Alternative definition of `toPoly` using `Finsupp`; currently unused. -/ noncomputable def Raw.toPoly' [Semiring R] (p : CPolynomial.Raw R) : Polynomial R := - Polynomial.ofFinsupp (Finsupp.onFinset (Finset.range p.size) p.coeff (by + Polynomial.ofFinsupp (AddMonoidAlgebra.ofCoeff (Finsupp.onFinset (Finset.range p.size) p.coeff (by intro n hn rw [Finset.mem_range] by_contra! h have h' : p.coeff n = 0 := by simp [h] contradiction - )) + ))) /-- Convert a canonical polynomial to a (mathlib) `Polynomial`. -/ noncomputable def toPoly [Semiring R] (p : CPolynomial R) : Polynomial R := p.val.toPoly diff --git a/lake-manifest.json b/lake-manifest.json index 364325ac..eff8144d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", + "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", + "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", + "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa08db58b30eb033edcdab331bba000827f9f785", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", + "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "CompPoly", diff --git a/lakefile.lean b/lakefile.lean index d54c9d27..92b962f4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ package CompPoly where version := v!"0.1.0" testDriver := "CompPolyTests" -require "leanprover-community" / mathlib @ git "v4.31.0" +require "leanprover-community" / mathlib @ git "v4.32.0" @[default_target] lean_lib CompPoly diff --git a/lean-toolchain b/lean-toolchain index 18640c8b..2544c30c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 +leanprover/lean4:v4.32.0 \ No newline at end of file From eca0eeedb26184ebd7da47009a9151bd38fc0a25 Mon Sep 17 00:00:00 2001 From: Alexander Hicks Date: Tue, 14 Jul 2026 13:17:58 +0100 Subject: [PATCH 2/2] fix lint, line length --- CompPoly/Univariate/DivisionCorrectness.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/CompPoly/Univariate/DivisionCorrectness.lean b/CompPoly/Univariate/DivisionCorrectness.lean index bdec9f2e..6f4fec71 100644 --- a/CompPoly/Univariate/DivisionCorrectness.lean +++ b/CompPoly/Univariate/DivisionCorrectness.lean @@ -452,7 +452,8 @@ private theorem raw_divModByMonicAux_go_spec (q : Raw R) (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly + q.toPoly * (Raw.divModByMonicAux.go fuel - (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).1.toPoly = + (p - Raw.C p.leadingCoeff * + (q * Raw.pow Raw.X (p.size - q.size))).trim q).1.toPoly = (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim.toPoly at hrel' constructor · rw [Raw.toPoly_add, _root_.mul_add, ← _root_.add_assoc, hrel'] @@ -462,7 +463,8 @@ private theorem raw_divModByMonicAux_go_spec (q : Raw R) ring · change (Raw.divModByMonicAux.go fuel - (p - Raw.C p.leadingCoeff * (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly.degree < + (p - Raw.C p.leadingCoeff * + (q * Raw.pow Raw.X (p.size - q.size))).trim q).2.toPoly.degree < q.toPoly.degree at hdeg exact hdeg