diff --git a/CompPoly/Bivariate/ToPoly.lean b/CompPoly/Bivariate/ToPoly.lean index 0c4a86d8..f2794b5f 100644 --- a/CompPoly/Bivariate/ToPoly.lean +++ b/CompPoly/Bivariate/ToPoly.lean @@ -49,7 +49,7 @@ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] Extracts each Y-coefficient via `p.coeff`, converts to `CPolynomial R` via `toImpl` and trimming, then builds the canonical bivariate sum. -/ -def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] +noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : R[X][Y]) : CBivariate R := (p.support).sum (fun j ↦ let cj := p.coeff j @@ -171,9 +171,10 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (show q.support ⊆ p.support ∪ q.support from Finset.subset_union_right) ] · rw [ ← Finset.sum_add_distrib ] refine' Finset.sum_congr rfl fun x hx ↦ _ - rw [ ← CPolynomial.monomial_add ] - congr - exact Eq.symm (toImpl_add (p.coeff x) (q.coeff x)) + erw [ ← CPolynomial.monomial_add ] + congr 1 + apply Subtype.ext + exact (toImpl_add (p.coeff x) (q.coeff x)).symm · aesop · aesop · aesop @@ -195,7 +196,8 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring unfold CBivariate.ofPoly induction' p.support using Finset.induction with j s hj ih · exact CPolynomial.eq_iff_coeff.mpr (congrFun rfl) - · rw [ Finset.sum_insert hj, CPolynomial.coeff_add, ih, Finset.sum_insert hj ] + · rw [Finset.sum_insert hj] + erw [CPolynomial.coeff_add, ih, Finset.sum_insert hj] rw [ h_coeff_sum, Finset.sum_eq_single n ] · rw [ CPolynomial.coeff_monomial ] simp +decide [ CPolynomial.toPoly ] @@ -237,7 +239,8 @@ theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] toPoly (p * q) = toPoly p * toPoly q := by have h_mul : (p * q).toPoly = (CPolynomial.toPoly (p * q)).map (CPolynomial.ringEquiv (R := R)) := toPoly_eq_map (p * q) - rw [ h_mul, CPolynomial.toPoly_mul ] + rw [ h_mul ] + erw [CPolynomial.toPoly_mul] rw [ Polynomial.map_mul, ← toPoly_eq_map, ← toPoly_eq_map ] end ToPolyCore @@ -310,6 +313,8 @@ 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 @@ -743,7 +748,7 @@ theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semi CPolynomial.coeff (swap (R := R) f) j = ∑ x ∈ f.supportY, CPolynomial.monomial x ((f.val.coeff x).coeff j) := by unfold CBivariate.swap CBivariate.supportY - rw [hCoeffSumOuter] + erw [hCoeffSumOuter] exact Finset.sum_congr rfl (fun x hx => hInner x) change CPolynomial.coeff (CPolynomial.coeff (swap (R := R) f) j) i = CPolynomial.coeff (CPolynomial.coeff f i) j diff --git a/CompPoly/Data/Nat/Bitwise.lean b/CompPoly/Data/Nat/Bitwise.lean index 588a52b6..2830ee72 100644 --- a/CompPoly/Data/Nat/Bitwise.lean +++ b/CompPoly/Data/Nat/Bitwise.lean @@ -35,7 +35,7 @@ lemma ENat.le_floor_NNReal_iff (x : ENat) (y : ℝ≥0) (hx_ne_top : x ≠ ⊤) (x : ENat) ≤ ((Nat.floor y) : ENat) ↔ x.toNat ≤ Nat.floor y := by lift x to ℕ using hx_ne_top -- y : ℝ≥0, x : ℕ, ⊢ ↑x ≤ ↑⌊y⌋₊ ↔ (↑x).toNat ≤ ⌊y⌋₊ - simp only [Nat.cast_le, toNat_coe] + simp only [ENat.coe_le_coe, toNat_coe] section ENNReal open ENNReal @@ -49,29 +49,11 @@ variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0} -- lemma ENNReal.div_lt_div_right (hc₀ : c ≠ 0) (hc : c ≠ ∞) (hab : a < b) : a / c < b / c := -- (ENNReal.div_lt_div_iff_left hc₀ hc).2 hab -theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : - ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ := by --- Let x = ↑a and y = ↑b for readability - let x : ENNReal := a - let y : ENNReal := b - -- Prove x and y are non-zero and finite (needed for inv_cancel) - have hx_ne_zero : x ≠ 0 := by exact Nat.cast_ne_zero.mpr ha - have hy_ne_zero : y ≠ 0 := by exact Nat.cast_ne_zero.mpr hb - have hx_ne_top : x ≠ ∞ := by exact ENNReal.natCast_ne_top a - have hy_ne_top : y ≠ ∞ := by exact ENNReal.natCast_ne_top b - have ha_NNReal_ne0 : (a : ℝ≥0) ≠ 0 := by exact Nat.cast_ne_zero.mpr ha - have hb_NNReal_ne0 : (b : ℝ≥0) ≠ 0 := by exact Nat.cast_ne_zero.mpr hb - -- (a * b)⁻¹ = b⁻¹ * a⁻¹ - have hlhs : ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ℝ≥0)⁻¹ * (b : ℝ≥0)⁻¹) := by - rw [coe_inv (hr := by exact ha_NNReal_ne0)] - rw [coe_inv (hr := by exact hb_NNReal_ne0)] - rw [ENNReal.coe_natCast, ENNReal.coe_natCast] - have hrhs : ((a : ENNReal) * (b : ENNReal))⁻¹ = ((a : ℝ≥0) * (b : ℝ≥0))⁻¹ := by - rw [coe_inv (hr := (mul_ne_zero_iff_right hb_NNReal_ne0).mpr (ha_NNReal_ne0))] - simp only [coe_mul, coe_natCast] - rw [hlhs, hrhs] - rw [mul_inv_rev (a := (a : ℝ≥0)) (b := (b : ℝ≥0))] - rw [coe_mul, mul_comm] +theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) : + ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ := + (ENNReal.mul_inv + (Or.inl (Nat.cast_ne_zero.mpr ha)) + (Or.inl (ENNReal.natCast_ne_top a))).symm lemma ENNReal.coe_le_of_NNRat {a b : ℚ≥0} : ((a : ENNReal)) ≤ (b) ↔ a ≤ b := by exact ENNReal.coe_le_coe.trans (by norm_cast) diff --git a/CompPoly/Data/Polynomial/Frobenius.lean b/CompPoly/Data/Polynomial/Frobenius.lean index 6a1b393f..e3768c43 100644 --- a/CompPoly/Data/Polynomial/Frobenius.lean +++ b/CompPoly/Data/Polynomial/Frobenius.lean @@ -486,7 +486,7 @@ theorem degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X have h_exponent_dvd : Monoid.exponent Kˣ ∣ q ^ n - 1 := Monoid.exponent_dvd_of_forall_pow_eq_one h_units_pow_eq_one have h_order_K : Fintype.card Kˣ = q ^ d - 1 := by - rw [Fintype.card_units, h_card_K] + erw [Fintype.card_units, h_card_K] have h_exp_eq_order : Monoid.exponent Kˣ = Fintype.card Kˣ := by rw [IsCyclic.exponent_eq_card, Nat.card_eq_fintype_card] rw [h_exp_eq_order, h_order_K] at h_exponent_dvd diff --git a/CompPoly/Data/RingTheory/AlgebraTower.lean b/CompPoly/Data/RingTheory/AlgebraTower.lean index 18b891e3..e7213b68 100644 --- a/CompPoly/Data/RingTheory/AlgebraTower.lean +++ b/CompPoly/Data/RingTheory/AlgebraTower.lean @@ -41,7 +41,7 @@ variable {ι : Type*} [Preorder ι] {B : ι → Type*} [∀ i, CommSemiring (B i)] [AlgebraTower B] {C : ι → Type*} [∀ i, CommSemiring (C i)] [AlgebraTower C] -@[simp] +@[simp, reducible] def AlgebraTower.toAlgebra {i j : ι} (h : i ≤ j) : Algebra (A i) (A j) := (AlgebraTower.algebraMap (i:=i) (j:=j) (h:=h)).toAlgebra @@ -102,11 +102,11 @@ def AlgebraTowerEquiv.algebraMapLeftUp (e : AlgebraTowerEquiv A B) (i j : ι) have hjRingEquiv: RingEquiv (B i) (A i) := (e.toRingEquiv i).symm exact hAij.comp hjRingEquiv.toRingHom -def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι) +@[reducible] def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : Algebra (A i) (B j) := by exact (e.algebraMapRightUp i j h).toAlgebra -def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι) +@[reducible] def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : Algebra (B i) (A j) := by exact (e.algebraMapLeftUp i j h).toAlgebra diff --git a/CompPoly/Data/Vector/Basic.lean b/CompPoly/Data/Vector/Basic.lean index ab107aa8..6bfd70c2 100644 --- a/CompPoly/Data/Vector/Basic.lean +++ b/CompPoly/Data/Vector/Basic.lean @@ -89,7 +89,7 @@ lemma cons_empty_tail_eq_nil {α} (hd : α) (tl : Vector α 0) : theorem tail_cons {α} {n : ℕ} (hd : α) (tl : Vector α n) : (cons hd tl).tail = tl := by rw [cons, Vector.insertIdx] simp only [Nat.add_one_sub_one, Array.insertIdx_zero, tail_eq_cast_extract, extract_mk, - Array.extract_append, List.extract_toArray, List.extract_eq_drop_take, add_tsub_cancel_right, + Array.extract_append, List.extract_toArray, List.extract_eq_take_drop, add_tsub_cancel_right, List.drop_succ_cons, List.drop_nil, List.take_nil, List.size_toArray, List.length_cons, List.length_nil, tsub_self, Array.take_eq_extract, Array.empty_append, cast_mk, mk_eq, Array.extract_eq_self_iff, size_toArray, le_refl, and_self, or_true] diff --git a/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean b/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean index 1f84afba..66943dcb 100644 --- a/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean +++ b/CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean @@ -501,12 +501,13 @@ theorem additiveNTT_correctness (h_ℓ : ℓ ≤ r) have res := output_foldl_correctness j unfold output_foldl at res simp only [Fin.zero_eta, Nat.sub_zero, pow_zero, Nat.div_one, Fin.eta, - Nat.pow_zero, Nat.getLowBits_zero_eq_zero (n := j.val), Fin.isValue, base_coeffsBySuffix] at res + Nat.pow_zero, Nat.getLowBits_zero_eq_zero (n := j.val), Fin.isValue] at res simp only [← intermediate_poly_P_base 𝔽q β h_ℓ_add_R_rate h_ℓ original_coeffs, Fin.zero_eta] - rw [← res] + erw [base_coeffsBySuffix] at res + erw [← res] simp_rw [Nat.sub_right_comm] end AlgorithmCorrectness diff --git a/CompPoly/Fields/Binary/AdditiveNTT/Impl.lean b/CompPoly/Fields/Binary/AdditiveNTT/Impl.lean index 879aa0b8..8882445f 100644 --- a/CompPoly/Fields/Binary/AdditiveNTT/Impl.lean +++ b/CompPoly/Fields/Binary/AdditiveNTT/Impl.lean @@ -399,7 +399,7 @@ abbrev BTF₃ := ConcreteBTField 3 -- 8 bits instance : NeZero (2^3) := ⟨by norm_num⟩ instance : Field BTF₃ := instFieldConcrete instance : DecidableEq BTF₃ := (inferInstance : DecidableEq (ConcreteBTField 3)) -instance : Fintype BTF₃ := (inferInstance : Fintype (ConcreteBTField 3)) +noncomputable instance : Fintype BTF₃ := (inferInstance : Fintype (ConcreteBTField 3)) /-- Test of the computable additive NTT over BTF₃ (an 8-bit binary tower field `BTF₃`). **Input polynomial:** p(x) = x (novel coefficients [7, 1, 0, 0]) of size `2^ℓ` in `BTF₃` diff --git a/CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean b/CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean index 28e023f7..d0b8675c 100644 --- a/CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean +++ b/CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean @@ -380,7 +380,7 @@ lemma getSDomainBasisCoeff_of_iteratedQuotientMap simp only [zero_add] omega⟩) simp only [Fin.zero_eta, Fin.coe_ofNat_eq_mod, Nat.sub_zero] at h_interW_comp - rw [h_interW_comp] + erw [h_interW_comp] have h_index : 0 + i.val = i.val := by omega rw! (castMode := .all) [h_index] rfl @@ -480,7 +480,7 @@ theorem base_intermediateNovelBasisX (j : Fin (2 ^ ℓ)) : simp only [Fin.mk_zero'] at h_res conv_lhs => enter [2, x, 1] - rw [h_res ⟨x, by omega⟩] + erw [h_res ⟨x, by omega⟩] congr omit [DecidableEq L] [DecidableEq 𝔽q] h_Fq_char_prime hF₂ hβ_lin_indep h_β₀_eq_1 in diff --git a/CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean b/CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean index d0ed0c19..8e59ac57 100644 --- a/CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean +++ b/CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean @@ -368,7 +368,7 @@ lemma W₀_eq_X : W 𝔽q β 0 = X := by rw [W] have : (univ : Finset (U 𝔽q β 0)) = {0} := by ext x - simp only [U, Set.Ico, mem_univ, mem_singleton, true_iff] + simp only [mem_univ, mem_singleton, true_iff] --x : ↥(U 𝔽q β 0), ⊢ x = 0 unfold U at x have h_empty : Set.Ico 0 (0: Fin r) = ∅ := by @@ -1340,11 +1340,19 @@ lemma degree_Xⱼ (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (j : Fin (2 ^ ℓ)) : -- We use the `Nat.digits` API for this. rw [Finset.sum_congr rfl deg_each] -- .degree introduces (WithBot ℕ) -- ⊢ ⊢ ∑ x, ↑(if bit ↑x ↑j = 1 then 2 ^ ↑x else 0) = ↑↑j - set f:= fun x: ℕ => if Nat.getBit x j = 1 then (2: ℕ) ^ (x: ℕ) else 0 - norm_cast -- from WithBot ℕ to ℕ - change (∑ x : Fin ℓ, f x) = (j.val: WithBot ℕ) - norm_cast - -- ⊢ (∑ x ∈ Icc 0 (ℓ - 1), if bit x j = 1 then 2 ^ x else 0) = ↑j => in Withbot ℕ + -- The goal is: ∑ x, ↑(if ... then 2^↑x else 0) = ↑↑j in WithBot ℕ + -- Reduce to ℕ equality via suffices and cast lemma + set f := fun x : ℕ => if Nat.getBit x j = 1 then (2 : ℕ) ^ x else 0 + suffices h : (∑ x : Fin ℓ, f x.val) = j.val by + simp only [f] at h + have h2 := congrArg (fun n : ℕ => (n : WithBot ℕ)) h + simp only [Nat.cast_sum, Nat.cast_ite, Nat.cast_pow, Nat.cast_ofNat, + Nat.cast_zero] at h2 + convert h2 using 1 + apply Finset.sum_congr rfl + intro x _ + simp only [Nat.cast_ite, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_zero] + -- ⊢ (∑ x, f x.val) = j.val in ℕ rw [Fin.sum_univ_eq_sum_range (n:=ℓ)] -- switch to sum over Finset.range ℓ have h_range: range ℓ = Icc 0 (ℓ-1) := by rw [←Nat.range_succ_eq_Icc_zero (n:=ℓ - 1)] @@ -1385,10 +1393,6 @@ noncomputable def basisVectors (ℓ : Nat) (h_ℓ : ℓ ≤ r) : /-- The vector space of coefficients for polynomials of degree < 2^ℓ. -/ abbrev CoeffVecSpace (L : Type u) (ℓ : Nat) := Fin (2^ℓ) → L -noncomputable instance (ℓ : Nat) : AddCommGroup (CoeffVecSpace L ℓ) := by - unfold CoeffVecSpace - infer_instance -- default additive group for `Fin (2^ℓ) → L` - noncomputable instance finiteDimensionalCoeffVecSpace (ℓ : ℕ) : FiniteDimensional (K := L) (V := CoeffVecSpace L ℓ) := by unfold CoeffVecSpace @@ -1398,7 +1402,10 @@ noncomputable instance finiteDimensionalCoeffVecSpace (ℓ : ℕ) : def toCoeffsVec (ℓ : Nat) : L⦃<2^ℓ⦄[X] →ₗ[L] CoeffVecSpace L ℓ where toFun := fun p => fun i => p.val.coeff i.val map_add' := fun p q => by ext i; simp [coeff_add] - map_smul' := fun c p => by ext i; simp [coeff_smul, smul_eq_mul] + map_smul' := fun c p => by + ext i + simp only [Pi.smul_apply, RingHom.id_apply, smul_eq_mul] + rw [Submodule.coe_smul, Polynomial.coeff_smul, smul_eq_mul] /-- The rows of a square lower-triangular matrix with non-zero diagonal entries are linearly independent. -/ diff --git a/CompPoly/Fields/Binary/BF128Ghash/Basic.lean b/CompPoly/Fields/Binary/BF128Ghash/Basic.lean index f28bf78a..bfefead8 100644 --- a/CompPoly/Fields/Binary/BF128Ghash/Basic.lean +++ b/CompPoly/Fields/Binary/BF128Ghash/Basic.lean @@ -189,7 +189,8 @@ def root : BF128Ghash := AdjoinRoot.root ghashPoly theorem root_satisfies_poly : root^128 + root^7 + root^2 + root + 1 = 0 := by unfold root ghashPoly have h := AdjoinRoot.eval₂_root ghashPoly - simp only [ghashPoly, eval₂_add, eval₂_pow, eval₂_X, eval₂_one] at h + simp only [ghashPoly, 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 /-- BF128Ghash is a finite type. -/ diff --git a/CompPoly/Fields/Binary/Common.lean b/CompPoly/Fields/Binary/Common.lean index 5915da30..7c6f6b85 100644 --- a/CompPoly/Fields/Binary/Common.lean +++ b/CompPoly/Fields/Binary/Common.lean @@ -556,13 +556,12 @@ lemma toPoly_128_extend_256 (a : B128) : intro (i : Fin (128)) hi_mem_univ dsimp only [BitVec.getLsb] simp_rw [to256_toNat] - simp only [Fin.val_castAdd, Fin.val_addNat, add_eq_left, ite_eq_right_iff, ne_eq, - Nat.add_eq_zero_iff, Fin.val_eq_zero_iff, Fin.isValue, OfNat.ofNat_ne_zero, and_false, - not_false_eq_true, pow_eq_zero_iff, X_ne_zero, imp_false, Bool.not_eq_true] - -- ⊢ (BitVec.toNat a).testBit (↑i + 128) = false - apply Nat.testBit_lt_two_pow + simp only [Fin.val_castAdd, Fin.val_addNat] have h_toNat_lt := BitVec.toNat_lt_twoPow_of_le (n := i.val + 128) (x := a) (h := by omega) - exact h_toNat_lt + have h_testBit_false : (BitVec.toNat a).testBit (↑i + 128) = false := + Nat.testBit_lt_two_pow h_toNat_lt + simp only [h_testBit_false, Bool.false_eq_true, ↓reduceIte, add_zero] + rfl -- Lemma: Left Shift corresponds to Multiplication by X^k theorem BitVec_getLsb_eq_false_of_toNat_lt_two_pow {w d : ℕ} (a : BitVec w) (ha : a.toNat < 2 ^ d) diff --git a/CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean b/CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean index 1f251c19..7c3d3519 100644 --- a/CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean +++ b/CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean @@ -83,9 +83,8 @@ lemma towerAlgebraMap_succ_1 (k : ℕ) : towerAlgebraMap (l:=k) (r:=k+1) (h_le:=by omega) = canonicalEmbedding k := by unfold towerAlgebraMap simp only [Nat.left_eq_add, one_ne_zero, ↓reduceDIte, - Nat.add_one_sub_one, eq_mp_eq_cast, cast_eq] - rw [towerAlgebraMap_id] - rw [RingHom.comp_id] + Nat.add_one_sub_one, eq_mp_eq_cast] + erw [cast_eq, towerAlgebraMap_id, RingHom.comp_id] /-! Right associativity of the Tower Map -/ lemma towerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) : @@ -96,8 +95,8 @@ lemma towerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) : conv_lhs => rw [towerAlgebraMap] have h_l_ne_eq_r_add_1 : l ≠ r + 1 := by omega simp only [h_l_ne_eq_r_add_1, ↓reduceDIte, Nat.add_one_sub_one, - eq_mp_eq_cast, cast_eq, RingHom.coe_comp, Function.comp_apply] - rw [towerAlgebraMap_succ_1] + eq_mp_eq_cast, RingHom.coe_comp, Function.comp_apply] + erw [cast_eq, towerAlgebraMap_succ_1]; congr 1 /-! Left associativity of the Tower Map -/ theorem towerAlgebraMap_succ_last (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → @@ -136,7 +135,7 @@ theorem BTField.RingHom_comp_cast {α β γ δ : ℕ} (f : BTField α →+* BTFi have h_heq : HEq ((cast (h1) g).comp f) (cast (h2) (g.comp f)) := by subst h -- this simplifies h1 h2 in cast which makes them trivial equality -- => hence it becomes easier to simplify - simp only [BTField, BTFieldIsField, cast_eq, heq_eq_eq] + simp only [BTField, cast_eq, heq_eq_eq] apply eq_of_heq h_heq theorem towerAlgebraMap_assoc : ∀ r mid l : ℕ, (h_l_le_mid : l ≤ mid) → (h_mid_le_r : mid ≤ r) → @@ -177,7 +176,7 @@ instance : AlgebraTower (BTField) where exact CommMonoid.mul_comm ((towerAlgebraMap i j h) r) x coherence' := by exact fun i j k h1 h2 ↦ towerAlgebraMap_assoc k j i h1 h2 -def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) := by +@[reducible] def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) := by exact AlgebraTower.toAlgebra h_le lemma binaryTowerAlgebra_def (l r : ℕ) (h_le : l ≤ r) : @@ -213,7 +212,7 @@ theorem binaryTowerAlgebra_apply_assoc (l mid r : ℕ) (h_l_le_mid : l ≤ mid) (h_l_le_mid:=h_l_le_mid) (h_mid_le_r:=h_mid_le_r)] /-- This also provides the corresponding Module instance. -/ -def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r) := +@[reducible] def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r) := (binaryAlgebraTower (h_le:=h_le)).toModule instance (priority := 1000) algebra_adjacent_tower (l : ℕ) : diff --git a/CompPoly/Fields/Binary/Tower/Abstract/Basis.lean b/CompPoly/Fields/Binary/Tower/Abstract/Basis.lean index d1b13526..3e358a74 100644 --- a/CompPoly/Fields/Binary/Tower/Abstract/Basis.lean +++ b/CompPoly/Fields/Binary/Tower/Abstract/Basis.lean @@ -38,7 +38,7 @@ def hli_level_diff_0 (l : ℕ) : smul_eq_mul, Finset.sum_singleton] at hg -- hg : g 0 = 0 ∨ 1 = 0 have h_one_ne_zero : (1 : BTField l) ≠ (0 : BTField l) := by exact BTFieldNeZero1 (k:=l).out - simp only [BTField, BTFieldIsField, Fin.isValue] at hg + simp only [BTField, Fin.isValue] at hg rw [Subsingleton.elim j 0] -- j must be 0 rw [hg.symm] exact Eq.symm (MulOneClass.mul_one (g 0)) @@ -50,7 +50,7 @@ def hli_level_diff_0 (l : ℕ) : rw [Ideal.submodule_span_eq] rw [Ideal.span_singleton_one] -def BTField.isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) := +@[reducible] def BTField.isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) := instAlgebraTowerNatBTField.toIsScalarTower (i:=l) (j:=r) (k:=r+1) (h1:=by omega) (h2:=by omega) @@ -126,6 +126,7 @@ theorem BTField.PowerBasis.dim_of_eq_rec subst h_r rfl +set_option backward.isDefEq.respectTransparency false in @[simp] theorem PowerBasis.cast_basis_succ_of_eq_rec_apply (r1 r : ℕ) (h_r : r = r1 + 1) @@ -145,7 +146,7 @@ theorem PowerBasis.cast_basis_succ_of_eq_rec_apply have h_pb'_dim : bCast.dim = 2 := by dsimp [bCast] - rw [BTField.PowerBasis.dim_of_eq_rec (r1:=r1) (r:=r) (h_r:=h_r) (b:=b)] + erw [BTField.PowerBasis.dim_of_eq_rec (r1:=r1) (r:=r) (h_r:=h_r) (b:=b)] exact h_pb_dim have h_pb_type_eq : Basis (Fin bCast.dim) (BTField r1) (BTField r) = @@ -159,8 +160,12 @@ theorem PowerBasis.cast_basis_succ_of_eq_rec_apply left k = right := by -- The proof of the theorem itself remains simple. subst h_r - simp only [binaryTowerAlgebra_id, - Algebra.algebraMap_self, PowerBasis.coe_basis, Fin.val_cast, RingHom.id_apply] + simp only [PowerBasis.coe_basis, Fin.val_cast] + -- algebraMap from BTField (r1+1) to itself is identity, but the instance is binaryAlgebraTower + -- which simp can't rewrite. Use erw to bridge the instance gap. + conv_rhs => erw [show @algebraMap _ _ _ _ (binaryAlgebraTower (by omega : r1 + 1 ≤ r1 + 1)) + ((powerBasisSucc r1).gen ^ (k : ℕ)) = (powerBasisSucc r1).gen ^ (k : ℕ) from by + erw [binaryTowerAlgebra_id (rfl : r1 + 1 = r1 + 1)]; rfl] rw [BTField.Basis_cast_index_apply (h_eq:=by exact powerBasisSucc_dim r1) (h_le:=by omega)] simp only [PowerBasis.coe_basis, Fin.val_cast] @@ -177,7 +182,8 @@ lemma algebraMap_𝕏_eq_of_index_eq (r k m : ℕ) (h_k_le : k + 1 ≤ r) (h_m_l The basis element at index `j` is the product of the tower generators at the ON bits in binary representation of `j`. -/ -set_option maxHeartbeats 350000 +set_option maxHeartbeats 800000 +set_option backward.isDefEq.respectTransparency false in theorem multilinearBasis_apply (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → ∀ (j : Fin (2 ^ (r - l))), multilinearBasis (l:=l) (r:=r) (h_le:=h_le) j = (Finset.univ : Finset (Fin (r - l))).prod (fun i => @@ -217,14 +223,14 @@ theorem multilinearBasis_apply (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → ∀ else rw [multilinearBasis] -- key to remove Eq.rec : dif_neg h_r_sub_l - simp only [Nat.pow_zero, eq_mp_eq_cast, cast_eq, + simp (config := { maxSteps := 100000 }) only [Nat.pow_zero, eq_mp_eq_cast, cast_eq, eq_mpr_eq_cast, dif_neg h_r_sub_l] have h2 : 2 ^ (r - l - 1) * 2 = 2 ^ (r - l) := by rw [←Nat.pow_succ, Nat.succ_eq_add_one, Nat.sub_add_cancel (by omega)] - rw [BTField.Basis_cast_index_apply (h_eq:=by omega) (h_le:=by omega)] + erw [BTField.Basis_cast_index_apply (h_eq:=by omega) (h_le:=by omega)] simp only [Basis.coe_reindex, Function.comp_apply, revFinProdFinEquiv_symm_apply] - rw [BTField.Basis_cast_dest_apply (h_eq:=by omega) (h_le1:=by omega) (h_le2:=by omega)] + erw [BTField.Basis_cast_dest_apply (h_eq:=by omega) (h_le1:=by omega) (h_le2:=by omega)] set prevDiff := r - l - 1 with h_prevDiff have h_r_sub_l : r - l = prevDiff + 1 := by omega @@ -300,9 +306,9 @@ theorem multilinearBasis_apply (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → ∀ conv_lhs => rw [←Fin.prod_congr' (b:=r1-l) (a:=prevDiff) (h:=by omega)] simp only [Fin.val_cast] - simp_rw [algebraMap, instAlgebraSucc, algebra_adjacent_tower] - rw [RingHom.map_pow] - simp_rw [←binaryTowerAlgebra_apply_assoc] + simp (config := { failIfUnchanged := false }) only [algebraMap, instAlgebraSucc] + erw [RingHom.map_pow] + simp (config := { failIfUnchanged := false }) only [←binaryTowerAlgebra_apply_assoc] ------------------ Equality of bit-based powers of generators ----------------- --- The outtermost term have hfinProd_msb := bit_revFinProdFinEquiv_symm_2_pow_succ (n:=prevDiff) diff --git a/CompPoly/Fields/Binary/Tower/Abstract/Split.lean b/CompPoly/Fields/Binary/Tower/Abstract/Split.lean index d8781eef..50934803 100644 --- a/CompPoly/Fields/Binary/Tower/Abstract/Split.lean +++ b/CompPoly/Fields/Binary/Tower/Abstract/Split.lean @@ -95,7 +95,7 @@ lemma powerBasisSucc_gen (k : ℕ) : lemma powerBasisSucc_dim (k : ℕ) : powerBasisSucc (k:=k).dim = 2 := by - simp only [BTField, CommRing, BTFieldIsField, powerBasisSucc, poly, PowerBasis.map_dim, + simp only [BTField, BTFieldIsField, powerBasisSucc, poly, PowerBasis.map_dim, powerBasis_dim] exact natDegree_definingPoly (Z k) @@ -201,15 +201,28 @@ theorem unique_linear_decomposition_succ (k : ℕ) : -- Last, we prove the equality : `•` => `*`, `lo_btf` and `hi_btf` => `algebraMap` unfold join_via_add_smul simp only [Nat.add_one_sub_one] - simp only [Algebra.smul_def] have unique_linear_combination : ∀ (c1 : AdjoinRoot (poly k)), ∃! (p : BTField k × BTField k), c1 = (of (poly k)) p.1 * root (poly k) + (of (poly k)) p.2 := by apply unique_linear_form_of_elements_in_adjoined_commring · apply BinaryTower.poly_natDegree_eq_2 · apply BinaryTower.polyMonic let px := unique_linear_combination (c1:=x) - simp_rw [algebraMap_adjacent_tower_succ_eq_Adjoin_of k] - convert px + have h_alg : (algebraMap (BTField k) (BTField (k + 1))) = of (poly k) := + algebraMap_adjacent_tower_succ_eq_Adjoin_of k + have h_eq : ∀ p : BTField k × BTField k, + ((of (poly k)) p.1 * root (poly k) + (of (poly k)) p.2) = + (p.1 • Z (k + 1) + (algebraMap (BTField k) (BTField (k + 1))) p.2) := by + intro p; simp only [Z_succ_eq_adjointRoot_root] + erw [Algebra.smul_def, h_alg]; rfl + obtain ⟨p, hp, hu⟩ := px + refine ⟨p, ?_, fun q hq => hu q ?_⟩ + · show x = p.1 • Z (k + 1) + (algebraMap (BTField k) (BTField (k + 1))) p.2 + erw [Z_succ_eq_adjointRoot_root, Algebra.smul_def, + algebraMap_adjacent_tower_succ_eq_Adjoin_of k]; exact hp + · change x = (of (poly k)) q.1 * root (poly k) + (of (poly k)) q.2 + change x = q.1 • Z (k + 1) + (algebraMap (BTField k) (BTField (k + 1))) q.2 at hq + erw [Z_succ_eq_adjointRoot_root, Algebra.smul_def, + algebraMap_adjacent_tower_succ_eq_Adjoin_of k] at hq; exact hq def split (k : ℕ) (h_k : k > 0) (x : BTField k) : BTField (k-1) × BTField (k-1) := by have h_eq : k - 1 + 1 = k := by omega @@ -313,12 +326,15 @@ lemma split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1)) rw [Algebra.smul_def', map_zero, zero_mul, zero_add] have h := algebraMap_adjacent_tower_def (l:=k-1) rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h - simp only [algebra_adjacent_tower, eqRec_eq_cast] at h + simp only [eqRec_eq_cast] at h rw [algebraMap, Algebra.algebraMap] at ⊢ h rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h simp only [cast_eq] at h - conv_rhs => rw [h] - rw [eqRec_eq_cast] + unfold binaryAlgebraTower AlgebraTower.toAlgebra AlgebraTower.algebraMap + instAlgebraTowerNatBTField + simp only [] -- normalize eqRec before rewrite + -- Both sides reduce to (cast ⋯ (canonicalEmbedding (k-1))) x through different paths + erw [h_concrete_embedding_succ_1]; simp only [eqRec_eq_cast] lemma algebraMap_succ_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1)) : letI instAlgebra := binaryAlgebraTower (l:=k-1) (r:=k) (h_le:=by omega) @@ -350,7 +366,7 @@ lemma algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : BTField i) : set r := towerAlgebraMap (l:=i) (r:=i+d') (h_le:=by omega) x with h_r have h := algebraMap_succ_eq_zero_x (k:=i+d'+1) (h_pos:=by omega) r simp only [Nat.add_one_sub_one] at h - rw [←h] + erw [←h] rfl @[simp] diff --git a/CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean b/CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean index cd095c15..16c3d417 100644 --- a/CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean +++ b/CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean @@ -12,6 +12,8 @@ import CompPoly.Fields.Binary.Tower.Concrete.Field Algebra maps and embeddings for the concrete bitvector binary tower. -/ +set_option backward.isDefEq.respectTransparency false + namespace ConcreteBinaryTower open Polynomial @@ -207,7 +209,7 @@ instance instAlgebraTowerConcreteBTF : AlgebraTower (ConcreteBTField) where intro i j k h1 h2 exact concreteTowerAlgebraMap_assoc k j i h1 h2 -def ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : +@[reducible] def ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : Algebra (ConcreteBTField l) (ConcreteBTField r) := instAlgebraTowerConcreteBTF.toAlgebra h_le -- Since `join_via_add_smul` is equal `join`, it is also inverse of `split` @@ -409,7 +411,7 @@ theorem ConcreteBTFieldAlgebra_apply_assoc (l mid r : ℕ) (h_l_le_mid:=h_l_le_mid) (h_mid_le_r:=h_mid_le_r)] /-- This also provides the corresponding Module instance. -/ -def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : +@[reducible] def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (ConcreteBTField l) (ConcreteBTField r) := (ConcreteBTFieldAlgebra (h_le:=h_le)).toModule diff --git a/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean b/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean index b139d9c4..70750465 100644 --- a/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean +++ b/CompPoly/Fields/Binary/Tower/Concrete/Basis.lean @@ -12,6 +12,7 @@ import CompPoly.Fields.Binary.Tower.Concrete.Algebra Basis constructions for the concrete bitvector binary tower. -/ +set_option backward.isDefEq.respectTransparency false namespace ConcreteBinaryTower open Polynomial @@ -299,7 +300,7 @@ def hli_level_diff_0 (l : ℕ) : rw [Ideal.submodule_span_eq] rw [Ideal.span_singleton_one] -def isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) := +@[reducible] def isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) := instAlgebraTowerConcreteBTF.toIsScalarTower (i:=l) (j:=r) (k:=r+1) (h1:=by omega) (h2:=by omega) /-- @@ -407,12 +408,9 @@ theorem PowerBasis.cast_basis_succ_of_eq_rec_apply (b.basis (Fin.cast h_pb_dim.symm k)) left k = right := by -- The proof of the theorem itself remains simple. - subst h_r - simp only [ConcreteBTFieldAlgebra_id, - Algebra.algebraMap_self, PowerBasis.coe_basis, Fin.val_cast, RingHom.id_apply] - rw [Basis_cast_index_apply (h_eq:=by - exact powerBasisSucc_dim r1) (h_le:=by omega)] - simp only [PowerBasis.coe_basis, Fin.val_cast] + subst h_r; dsimp only + convert rfl using 2 + rw [ConcreteBTFieldAlgebra_id rfl]; rfl @[simp] theorem coe_basis_apply {R S : Type*} [CommRing R] [Ring S] [Algebra R S] @@ -554,9 +552,9 @@ theorem multilinearBasis_apply (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → ∀ conv_lhs => rw [←Fin.prod_congr' (b:=r1 - l) (a:=prevDiff) (h:=by omega)] simp only [Fin.val_cast] - simp_rw [algebraMap, instAlgebraSucc, algebra_adjacent_tower] - rw [RingHom.map_pow] - simp_rw [←ConcreteBTFieldAlgebra_apply_assoc] + simp (config := { failIfUnchanged := false }) only [algebraMap, instAlgebraSucc] + erw [RingHom.map_pow] + simp (config := { failIfUnchanged := false }) only [←ConcreteBTFieldAlgebra_apply_assoc] ------------------ Equality of bit-based powers of generators ----------------- have hfinProd_msb := bit_revFinProdFinEquiv_symm_2_pow_succ (n:=prevDiff) (i:=⟨prevDiff, by omega⟩) (j:=⟨j, by omega⟩) diff --git a/CompPoly/Fields/Binary/Tower/Concrete/Core.lean b/CompPoly/Fields/Binary/Tower/Concrete/Core.lean index 5f7f77f6..a530256a 100644 --- a/CompPoly/Fields/Binary/Tower/Concrete/Core.lean +++ b/CompPoly/Fields/Binary/Tower/Concrete/Core.lean @@ -314,7 +314,7 @@ instance (k : ℕ) : Add (ConcreteBTField k) where theorem sum_fromNat_eq_from_xor_Nat {k : ℕ} (x y : Nat) : fromNat (k:=k) (x ^^^ y) = fromNat (k:=k) x + fromNat (k:=k) y := by unfold fromNat - simp only [instHAddConcreteBTField, add, BitVec.xor_eq] + show BitVec.ofNat _ (x ^^^ y) = (BitVec.ofNat _ x) ^^^ (BitVec.ofNat _ y) rw [BitVec.ofNat_xor] -- Basic lemmas for addition @@ -535,7 +535,7 @@ instance {k : ℕ} : NeZero (1 : ConcreteBTField k) := by unfold ConcreteBTField exact {out := concrete_one_ne_zero (k:=k) } -def mkAddCommGroupInstance {k : ℕ} : AddCommGroup (ConcreteBTField k) := { +@[reducible] def mkAddCommGroupInstance {k : ℕ} : AddCommGroup (ConcreteBTField k) := { zero := zero neg := neg sub := fun x y => add x y @@ -950,17 +950,15 @@ theorem split_sum_eq_sum_split {k : ℕ} (h_pos : k > 0) (x₀ x₁ : ConcreteBT have h_nat_eq : BitVec.toNat x₀ >>> 2 ^ (k - 1) ^^^ BitVec.toNat x₁ >>> 2 ^ (k - 1) = BitVec.toNat (x₀ + x₁) >>> 2 ^ (k - 1) := by -- unfold Concrete BTF addition into BitVec.xor - simp only [instHAddConcreteBTField, add, BitVec.xor_eq] + erw [BitVec.toNat_xor] rw [Nat.shiftRight_xor_distrib.symm] - rw [BitVec.toNat_xor] -- distribution of BitVec.xor over BitVec.toNat rw [h_nat_eq] have h_sum_lo : (lo₀ + lo₁) = fromNat (BitVec.toNat (x₀ + x₁) &&& 2 ^ 2 ^ (k - 1) - 1) := by rw [h₀.2, h₁.2] rw [←sum_fromNat_eq_from_xor_Nat] have h_nat_eq : BitVec.toNat x₀ &&& 2 ^ 2 ^ (k - 1) - 1 ^^^ BitVec.toNat x₁ &&& 2 ^ 2 ^ (k - 1) - 1 = BitVec.toNat (x₀ + x₁) &&& 2 ^ 2 ^ (k - 1) - 1 := by - simp only [instHAddConcreteBTField, add, BitVec.xor_eq] - rw [BitVec.toNat_xor] + erw [BitVec.toNat_xor] rw [Nat.and_xor_distrib_right.symm] rw [h_nat_eq] have h_sum_hi_lo : (hi₀ + hi₁, lo₀ + lo₁) = split h_pos (x₀ + x₁) := by @@ -1234,7 +1232,7 @@ theorem concrete_eq_zero_or_eq_one {k : ℕ} {a : ConcreteBTField k} (h_k_zero : -- zero (k:=k) = Eq.mpr ... (zero (k:=0)) have : zero = Eq.mpr (congrArg ConcreteBTField h_k_zero) (zero (k:=0)) := by simp only [zero, eq_mpr_eq_cast, BitVec.zero] - rw [←dcast_eq_root_cast] + erw [←dcast_eq_root_cast] simp only [BitVec.ofNatLT_zero, Nat.pow_zero] rw [BitVec.dcast_zero] -- ⊢ 1 = 2 ^ k exact h_2_pow_k_eq_1.symm @@ -1246,7 +1244,7 @@ theorem concrete_eq_zero_or_eq_one {k : ℕ} {a : ConcreteBTField k} (h_k_zero : rw [this, ha1] have : one = Eq.mpr (congrArg ConcreteBTField h_k_zero) (one (k:=0)) := by simp only [one, eq_mpr_eq_cast] - rw [←dcast_eq_root_cast] + erw [←dcast_eq_root_cast] simp only [Nat.pow_zero] rw [BitVec.dcast_one] -- ⊢ 1 = 2 ^ k exact h_2_pow_k_eq_1.symm @@ -1256,9 +1254,9 @@ theorem concrete_eq_zero_or_eq_one {k : ℕ} {a : ConcreteBTField k} (h_k_zero : lemma add_eq_one_iff (a b : ConcreteBTField 0) : a + b = 1 ↔ (a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 0) := by - rcases eq_zero_or_eq_one (a := a) with (ha | ha) - · simp [ha, zero_is_0] -- a = zero - · simp [ha, one_is_1] + rcases eq_zero_or_eq_one (a := a) with (ha | ha) <;> + rcases eq_zero_or_eq_one (a := b) with (hb | hb) <;> + simp_all [zero_is_0, one_is_1, add_self_cancel] instance instInvConcreteBTF {k : ℕ} : Inv (ConcreteBTField k) where inv := concrete_inv @@ -1346,9 +1344,7 @@ lemma concrete_mul_left_distrib0 (a b c : ConcreteBTField 0) : simp only [c_cases, ne_eq, one_ne_zero, not_false_eq_true] rw [if_neg c_ne_0] exact c_cases.symm - · rw [one_is_1] at hb; simp [hb]; - simp [hb] at c_cases - exact c_cases + · rw [one_is_1] at hb; simp [hb] at c_cases; simp [hb, c_cases] lemma concrete_mul_right_distrib0 (a b c : ConcreteBTField 0) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c := by @@ -1369,7 +1365,7 @@ def natCast_succ {k : ℕ} (n : ℕ) : natCast (k:=k) (n + 1) = natCast (k:=k) n by_cases h : n % 2 = 0 · -- If n % 2 = 0, then (n + 1) % 2 = 1 have h_succ : (n + 1) % 2 = 1 := by omega - simp only [natCast, h, h_succ]; norm_num; rw [one_is_1, zero_is_0]; norm_num + simp only [natCast, h, h_succ]; norm_num; rw [one_is_1, zero_is_0, zero_add] · -- If n % 2 = 1, then (n + 1) % 2 = 0 have h_succ : (n + 1) % 2 = 0 := by omega simp only [natCast, h, h_succ]; norm_num; rw [one_is_1, zero_is_0, add_self_cancel] @@ -1492,7 +1488,8 @@ structure ConcreteBTFieldProps (k : ℕ) extends (ConcreteBTFDivisionRingProps k -- Commutativity (what makes it a Field vs just a DivisionRing) mul_comm : ∀ a b : ConcreteBTField k, concrete_mul a b = concrete_mul b a -def mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBTField k) where +@[reducible] def mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : + Ring (ConcreteBTField k) where toAddCommGroup := mkAddCommGroupInstance toOne := inferInstance mul := concrete_mul @@ -1511,7 +1508,7 @@ def mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBT intCast_ofNat n := intCast_ofNat n intCast_negSucc n := intCast_negSucc n -def mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : +@[reducible] def mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : DivisionRing (ConcreteBTField k) where toRing := mkRingInstance (k:=k) props inv := concrete_inv @@ -1521,7 +1518,8 @@ def mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : qsmul := (Rat.castRec · * ·) nnqsmul := (NNRat.castRec · * ·) -def mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Field (ConcreteBTField k) where +@[reducible] def mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : + Field (ConcreteBTField k) where toDivisionRing := mkDivisionRingInstance (k:=k) props mul_comm := props.mul_comm diff --git a/CompPoly/Fields/Binary/Tower/Concrete/Field.lean b/CompPoly/Fields/Binary/Tower/Concrete/Field.lean index 740c4ff8..33aae64c 100644 --- a/CompPoly/Fields/Binary/Tower/Concrete/Field.lean +++ b/CompPoly/Fields/Binary/Tower/Concrete/Field.lean @@ -12,6 +12,7 @@ import CompPoly.Fields.Binary.Tower.Concrete.Core Field-structure lemmas for successive levels of the concrete binary tower. -/ +set_option backward.isDefEq.respectTransparency false namespace ConcreteBinaryTower open Polynomial @@ -586,7 +587,7 @@ def liftBTFieldProps (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k := k)) (h_k:=h_k) } -def liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k := k)) : +@[reducible] def liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k := k)) : Field (ConcreteBTField (k + 1)) := by exact mkFieldInstance (k:=k + 1) (props:=liftBTFieldProps (k:=k) (prevBTFResult:=prevBTFResult)) @@ -712,7 +713,7 @@ lemma sum_inv_Z_next_eq rw [h_mul_inv, Z_square_mul_form (k:=k) (prev:=prev), add_assoc] rw [add_self_cancel, add_zero] ------------------------------------------------------------------------------------------- -def getBTFResult (k : ℕ) : ConcreteBTFStepResult k := +noncomputable def getBTFResult (k : ℕ) : ConcreteBTFStepResult k := match k with | 0 => let base : ConcreteBTFieldProps 0 := { @@ -920,9 +921,10 @@ instance instFieldConcrete {k : ℕ} : Field (ConcreteBTField k) := instance instCharP2 {k : ℕ} : CharP (ConcreteBTField k) 2 := charP_eq_2_of_add_self_eq_zero (F:=(ConcreteBTField k)) (sumZeroIffEq:=add_eq_zero_iff_eq) -instance (k : ℕ) : Fintype (ConcreteBTField k) := (getBTFResult k).instFintype +noncomputable instance (k : ℕ) : Fintype (ConcreteBTField k) := (getBTFResult k).instFintype -instance instFintype {k : ℕ} : Fintype (ConcreteBTField k) := (getBTFResult k).instFintype +noncomputable instance instFintype {k : ℕ} : Fintype (ConcreteBTField k) := + (getBTFResult k).instFintype /-- adjoined root of poly k, generator of successor field BTField (k + 1) -/ @[simp] diff --git a/CompPoly/Fields/Binary/Tower/Equiv.lean b/CompPoly/Fields/Binary/Tower/Equiv.lean index 39b51928..dd182015 100644 --- a/CompPoly/Fields/Binary/Tower/Equiv.lean +++ b/CompPoly/Fields/Binary/Tower/Equiv.lean @@ -12,6 +12,7 @@ import CompPoly.Fields.Binary.Tower.Concrete.Basis Equivalences between the abstract and concrete binary tower constructions. -/ +set_option backward.isDefEq.respectTransparency false namespace ConcreteBinaryTower open Polynomial diff --git a/CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean b/CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean index 718a5b32..588a329e 100644 --- a/CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean +++ b/CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean @@ -388,6 +388,7 @@ theorem unique_linear_sum_repr (R : Type*) [CommRing R] (S : Type*) [CommRing S] _ = b := by rw [b_def] exact Prod.ext y1_eq_a y2_eq_b +set_option backward.isDefEq.respectTransparency false in theorem linear_form_of_elements_in_adjoined_commring {R : Type*} [CommRing R] (f : R[X]) (hf_deg : f.natDegree = 2) (hf_monic : Monic f) (c1 : AdjoinRoot f) : @@ -409,6 +410,7 @@ theorem linear_form_of_elements_in_adjoined_commring rw [oleft, oright] at c1_linear_comb_over_a_b exact c1_linear_comb_over_a_b +set_option backward.isDefEq.respectTransparency false in theorem unique_linear_form_of_elements_in_adjoined_commring {R : Type*} [CommRing R] (f : R[X]) (hf_deg : f.natDegree = 2) (hf_monic : Monic f) (c1 : AdjoinRoot f) : diff --git a/CompPoly/Multilinear/Basic.lean b/CompPoly/Multilinear/Basic.lean index c81b969e..576b97d9 100644 --- a/CompPoly/Multilinear/Basic.lean +++ b/CompPoly/Multilinear/Basic.lean @@ -600,7 +600,7 @@ theorem mobius_apply_zeta_apply_eq_id (n : ℕ) [NeZero n] (r : Fin n) (l : Fin rw [lagrangeToMonoSegment, monoToLagrangeSegment, forwardRange] simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, Fin.val_eq_zero, tsub_self, zero_add, List.ofFn_succ, Fin.isValue, Fin.cast_zero, Nat.mod_succ, add_zero, Fin.mk_zero', - Fin.cast_succ_eq, Fin.val_succ, Fin.val_cast, List.ofFn_zero, List.foldl_cons, List.foldl_nil, + Fin.val_cast, List.ofFn_zero, List.foldl_cons, List.foldl_nil, List.foldr_cons, List.foldr_nil] exact lagrangeToMonoLevel_monoToLagrangeLevel_id v 0 | succ r1 r1_lt_n h_r1 => @@ -645,7 +645,7 @@ lemma zeta_apply_mobius_apply_eq_id (n : ℕ) (r : Fin n) (l : Fin (r.val + 1)) rw [lagrangeToMonoSegment, monoToLagrangeSegment, forwardRange] simp only [add_tsub_cancel_right, tsub_self, zero_add, List.ofFn_succ, Nat.add_one_sub_one, Fin.isValue, Fin.cast_zero, Fin.coe_ofNat_eq_mod, Nat.mod_succ, add_zero, Fin.eta, - Fin.cast_succ_eq, Fin.val_succ, Fin.val_cast, List.ofFn_zero, List.foldr_cons, List.foldr_nil, + Fin.val_cast, List.ofFn_zero, List.foldr_cons, List.foldr_nil, List.foldl_cons, List.foldl_nil] exact monoToLagrangeLevel_lagrangeToMonoLevel_id v r | succ l1 l1_gt_0 h_l1 => diff --git a/CompPoly/Multilinear/Equiv.lean b/CompPoly/Multilinear/Equiv.lean index 4ecde84c..95fd1c10 100644 --- a/CompPoly/Multilinear/Equiv.lean +++ b/CompPoly/Multilinear/Equiv.lean @@ -301,13 +301,12 @@ noncomputable def linearEquivMvPolynomialDeg1 : -- coeff i ↑(p.toMvPolynomialDeg1 + q.toMvPolynomialDeg1) unfold equivMvPolynomialDeg1 toMvPolynomialDeg1 simp only [AddMemClass.mk_add_mk, coeff_add] + erw [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := p + q)] simp only [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := p)] - simp only [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := p + q)] simp only [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := q)] if h_binary: (∀ j: Fin n, i j ≤ 1) then simp only [h_binary, implies_true, ↓reduceDIte] - conv_lhs => enter [1]; change CMlPolynomial.add p q - simp only [add, Vector.getElem_zipWith] + erw [Vector.getElem_zipWith] else simp only [h_binary, ↓reduceDIte, add_zero] map_smul' := by @@ -315,12 +314,11 @@ noncomputable def linearEquivMvPolynomialDeg1 : ext i unfold equivMvPolynomialDeg1 toMvPolynomialDeg1 simp only [RingHom.id_apply, SetLike.mk_smul_mk, coeff_smul, smul_eq_mul] + erw [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := r • p)] simp only [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := p)] - simp only [coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial (p := r • p)] if h_binary: (∀ j: Fin n, i j ≤ 1) then simp only [h_binary, implies_true, ↓reduceDIte] - conv_lhs => enter [1]; change CMlPolynomial.smul r p - simp only [smul, Vector.getElem_map] + erw [Vector.getElem_map]; rfl else simp only [h_binary, ↓reduceDIte, mul_zero] } diff --git a/CompPoly/Multivariate/CMvMonomial.lean b/CompPoly/Multivariate/CMvMonomial.lean index 2d283fd2..1ee327df 100644 --- a/CompPoly/Multivariate/CMvMonomial.lean +++ b/CompPoly/Multivariate/CMvMonomial.lean @@ -164,11 +164,11 @@ lemma map_mul {m₁ m₂ : Multiplicative (Fin n →₀ ℕ)} : end CMvMonomial -abbrev MonoR (n : ℕ) (R : Type) := CMvMonomial n × R +abbrev MonoR (n : ℕ) (R : Type*) := CMvMonomial n × R namespace MonoR -variable {n : ℕ} {R : Type} +variable {n : ℕ} {R : Type*} instance [DecidableEq R] : DecidableEq (CMvMonomial n × R) := instDecidableEqProd @@ -195,7 +195,7 @@ instance {t₁ t₂ : MonoR n R} : Decidable (t₁ ∣ t₂) := by end -def evalMonomial {R : Type} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvMonomial n → R := +def evalMonomial {R : Type*} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvMonomial n → R := fun vals m => ∏ (i : Fin n), (vals i) ^ m.get i end MonoR diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean index a412497e..ad51f71a 100644 --- a/CompPoly/Multivariate/CMvPolynomial.lean +++ b/CompPoly/Multivariate/CMvPolynomial.lean @@ -39,24 +39,24 @@ namespace CPoly open Std /-- A computable multivariate polynomial in `n` variables with coefficients in `R`. -/ -abbrev CMvPolynomial (n : ℕ) (R : Type) [Zero R] : Type := Lawful n R +abbrev CMvPolynomial (n : ℕ) (R : Type*) [Zero R] : Type _ := Lawful n R -variable {R : Type} +variable {R : Type*} namespace CMvPolynomial /-- Construct a constant polynomial. -/ -def C {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] (c : R) : CMvPolynomial n R := +def C {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (c : R) : CMvPolynomial n R := Lawful.C (n := n) (R := R) c /-- Construct the polynomial $X_i$. -/ -def X {n : ℕ} {R : Type} [Zero R] [One R] [BEq R] [LawfulBEq R] +def X {n : ℕ} {R : Type*} [Zero R] [One R] [BEq R] [LawfulBEq R] (i : Fin n) : CMvPolynomial n R := let monomial : CMvMonomial n := Vector.ofFn (fun j => if j = i then 1 else 0) Lawful.fromUnlawful <| .ofList [(monomial, (1 : R))] /-- Extract the coefficient of a monomial. -/ -def coeff {R : Type} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : CMvPolynomial n R) : R := +def coeff {R : Type*} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : CMvPolynomial n R) : R := p.1[m]?.getD 0 attribute [grind =] coeff.eq_def @@ -125,26 +125,26 @@ end /-- Evaluate a polynomial at a point given by a ring homomorphism `f` and variable assignments `vs`. -/ -def eval₂ {R S : Type} {n : ℕ} [Semiring R] [CommSemiring S] : +def eval₂ {R S : Type*} {n : ℕ} [Semiring R] [CommSemiring S] : (R →+* S) → (Fin n → S) → CMvPolynomial n R → S := fun f vs p => ExtTreeMap.foldl (fun s m c => (f c * MonoR.evalMonomial vs m) + s) 0 p.1 /-- Evaluate a polynomial at a given point. -/ -def eval {R : Type} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvPolynomial n R → R := +def eval {R : Type*} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvPolynomial n R → R := eval₂ (RingHom.id _) /-- The support of a polynomial (set of monomials with non-zero coefficients), represented as Finsupps. -/ -def support {R : Type} {n : ℕ} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n →₀ ℕ) := +def support {R : Type*} {n : ℕ} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n →₀ ℕ) := (Lawful.monomials p).map CMvMonomial.toFinsupp |>.toFinset /-- The total degree of a polynomial (maximum total degree of its monomials). -/ -def totalDegree {R : Type} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ := +def totalDegree {R : Type*} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ := fun p => Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p))) (fun s => Finsupp.sum s (fun _ e => e)) /-- The degree of a polynomial in a specific variable. -/ -def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ := +noncomputable def degreeOf {R : Type*} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ := fun p => Multiset.count i (Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p))) @@ -154,7 +154,7 @@ def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → Creates a polynomial with a single monomial term. If `c = 0`, returns the zero polynomial. -/ -def monomial {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] +def monomial {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (m : CMvMonomial n) (c : R) : CMvPolynomial n R := if c == 0 then 0 else Lawful.fromUnlawful <| Unlawful.ofList [(m, c)] @@ -162,11 +162,11 @@ def monomial {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] Each variable `i` appears `degreeOf i p` times in the multiset. -/ -def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) := +noncomputable def degrees {n : ℕ} {R : Type*} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) := Finset.univ.sum fun i => Multiset.replicate (p.degreeOf i) i /-- `degreeOf` is the multiplicity of a variable in `degrees`. -/ -lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type} [Zero R] +lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type*} [Zero R] (i : Fin n) (p : CMvPolynomial n R) : p.degreeOf i = Multiset.count i p.degrees := by classical @@ -187,11 +187,11 @@ lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type} [Zero R] Returns the set of variable indices `i : Fin n` such that `degreeOf i p > 0`. -/ -def vars {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) := +noncomputable def vars {n : ℕ} {R : Type*} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) := Finset.univ.filter fun i => 0 < p.degreeOf i /-- Filter a polynomial, keeping only monomials for which `keep m` is true. -/ -def restrictBy {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] +def restrictBy {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (keep : CMvMonomial n → Prop) [DecidablePred keep] (p : CMvPolynomial n R) : CMvPolynomial n R := Lawful.fromUnlawful <| p.1.filter (fun m _ => decide (keep m)) @@ -200,7 +200,7 @@ def restrictBy {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] Filters out all monomials where `m.totalDegree > d`. -/ -def restrictTotalDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] +def restrictTotalDegree {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (d : ℕ) (p : CMvPolynomial n R) : CMvPolynomial n R := restrictBy (fun m => m.totalDegree ≤ d) p @@ -208,7 +208,7 @@ def restrictTotalDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] Filters out all monomials where `m.degreeOf i > d` for some variable `i`. -/ -def restrictDegree {n : ℕ} {R : Type} [BEq R] [LawfulBEq R] [Zero R] +def restrictDegree {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (d : ℕ) (p : CMvPolynomial n R) : CMvPolynomial n R := restrictBy (fun m => ∀ i : Fin n, m.degreeOf i ≤ d) p diff --git a/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean b/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean index 2b08135c..8fedb94c 100644 --- a/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean +++ b/CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean @@ -17,7 +17,7 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] variable (vals : Fin n → R) @[simp] diff --git a/CompPoly/Multivariate/FinSuccEquiv.lean b/CompPoly/Multivariate/FinSuccEquiv.lean index bfc8704a..4d3be5d0 100644 --- a/CompPoly/Multivariate/FinSuccEquiv.lean +++ b/CompPoly/Multivariate/FinSuccEquiv.lean @@ -37,7 +37,7 @@ namespace CPoly open Std CMvPolynomial -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-! ### Polynomial-level ring equivalence -/ diff --git a/CompPoly/Multivariate/Lawful.lean b/CompPoly/Multivariate/Lawful.lean index 69ef49ed..509d8ee3 100644 --- a/CompPoly/Multivariate/Lawful.lean +++ b/CompPoly/Multivariate/Lawful.lean @@ -18,6 +18,8 @@ computable multivariate polynomials. * `CPoly.Lawful n R`: The subtype of `Unlawful n R` with no zero coefficients. -/ +set_option allowUnsafeReducibility true in +attribute [local reducible] instDecidableEqOfLawfulBEq attribute [local instance 5] instDecidableEqOfLawfulBEq namespace CPoly @@ -25,10 +27,10 @@ namespace CPoly open Std /-- The subtype of polynomials with no zero coefficients. -/ -def Lawful (n : ℕ) (R : Type) [Zero R] := +def Lawful (n : ℕ) (R : Type*) [Zero R] : Type _ := {p : Unlawful n R // p.isNoZeroCoef} -variable {n : ℕ} {R : Type} [Zero R] +variable {n : ℕ} {R : Type*} [Zero R] section Instances @@ -64,7 +66,7 @@ lemma mem_iff_cast : x ∈ p.1 ↔ x ∈ p := by rfl @[grind =] lemma mem_iff : x ∈ p ↔ ∃ v, v ≠ 0 ∧ p[x]? = .some v := by - rw [←mem_iff_cast, ExtTreeMap.mem_iff_isSome_getElem?, Option.isSome_iff_exists] + erw [←mem_iff_cast, ExtTreeMap.mem_iff_isSome_getElem?, Option.isSome_iff_exists] rcases p with ⟨p, hp⟩ specialize hp x grind @@ -111,7 +113,9 @@ lemma C_zero' : C (n := n) (0 : ℕ) = 0 := rfl lemma zero_eq_zero : (0 : Lawful n R) = ⟨0, by grind⟩ := rfl -lemma zero_eq_empty : (0 : Lawful n R) = ∅ := by unfold_projs; simp [C, Unlawful.zero_eq_empty] +lemma zero_eq_empty : (0 : Lawful n R) = ∅ := by + unfold_projs + simp [C, Unlawful.zero_eq_empty] @[simp, grind .] lemma not_mem_C_zero : x ∉ C 0 := by simp [zero_eq_empty]; unfold_projs; grind @@ -167,7 +171,7 @@ abbrev monomials (p : Lawful n R) : List (CMvMonomial n) := p.1.monomials /-- Check if a polynomial is a non-zero constant. -/ -def NZConst {n : ℕ} {R : Type} [Zero R] (p : Lawful n R) : Prop := +def NzConst {n : ℕ} {R : Type*} [Zero R] (p : Lawful n R) : Prop := p.val.size = 1 ∧ p.val.contains CMvMonomial.zero omit [BEq R] [LawfulBEq R] in @@ -175,8 +179,8 @@ omit [BEq R] [LawfulBEq R] in lemma mem_monomials_iff {w : CMvMonomial n} : w ∈ Lawful.monomials p ↔ w ∈ p := by grind -instance {p : Lawful n R} : Decidable (NZConst p) := by - dsimp [NZConst] +instance {p : Lawful n R} : Decidable (NzConst p) := by + dsimp [NzConst] infer_instance end diff --git a/CompPoly/Multivariate/MvPolyEquiv/Core.lean b/CompPoly/Multivariate/MvPolyEquiv/Core.lean index f63523dd..37f12aac 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Core.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Core.lean @@ -25,7 +25,7 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] def fromCMvPolynomial (p : CMvPolynomial n R) : MvPolynomial (Fin n) R := let support : List (Fin n →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp @@ -43,8 +43,12 @@ noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n obtain ⟨elem, h₁⟩ : ∃ (h : m ∈ unlawful), unlawful[m] = 0 := ExtTreeMap.getElem?_eq_some_iff.1 contra obtain ⟨a, ha₁, ⟨rfl⟩⟩ : ∃ a ∈ s, .ofFinsupp a = m := by - simp [unlawful] at elem; rw [ExtTreeMap.mem_ofList] at elem; simp at elem - exact elem + have elem' : + m ∈ ExtTreeMap.ofList + (s.toList.map fun m => (CMvMonomial.ofFinsupp m, f m)) compare := by + simpa [unlawful] using elem + rw [ExtTreeMap.mem_ofList] at elem' + simpa using elem' have : f a = 0 := by dsimp [unlawful] at h₁ erw [ExtTreeMap.getElem_ofList_of_mem (v := f a) @@ -57,7 +61,7 @@ noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n grind ⟩ -instance {n : ℕ} {R : Type} : Membership (Vector ℕ n) (Unlawful n R) := inferInstance +instance {n : ℕ} {R : Type*} : Membership (Vector ℕ n) (Unlawful n R) := inferInstance omit [BEq R] [LawfulBEq R] in @[grind =, simp] @@ -67,20 +71,18 @@ theorem toCMvPolynomial_fromCMvPolynomial {p : CMvPolynomial n R} : dsimp ext m; simp only [CMvPolynomial.coeff]; congr 1 by_cases eq : m ∈ p <;> simp [eq] - · erw [ExtTreeMap.getElem?_ofList_of_mem (k := m) - (k_eq := by simp) - (v := p[m]) - (mem := by simp; grind) - (distinct := ?distinct)] + · erw [ExtTreeMap.getElem_ofList_of_mem (k := m) + (k_eq := by simp) + (v := p[m]) + (mem := by simp; grind) + (distinct := ?distinct)] grind case distinct => simp only [Std.compare_eq_iff_eq, List.pairwise_map] exact List.distinct_of_inj_nodup CMvMonomial.injective_ofFinsupp (Finset.nodup_toList _) - · erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false] - simpa omit [BEq R] [LawfulBEq R] in -@[grind=, simp] +@[grind =, simp] theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial (Fin n) R} : fromCMvPolynomial (toCMvPolynomial p) = p := by dsimp [fromCMvPolynomial, toCMvPolynomial, toCMvPolynomial, fromCMvPolynomial] @@ -93,7 +95,9 @@ theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial (Fin n) R} : aesop have : f m' ≠ 0 := by grind obtain ⟨rfl⟩ : m' = m := CMvMonomial.injective_ofFinsupp hm'₂ - suffices p[CMvMonomial.ofFinsupp m] = f m by simpa [eq₁] + suffices p[CMvMonomial.ofFinsupp m] = f m by + erw [show p[CMvMonomial.ofFinsupp m]? = some (f m) from + ExtTreeMap.getElem?_eq_some_iff.mpr ⟨eq₁, this⟩]; rfl simp_rw [←eq] rw [ExtTreeMap.getElem_ofList_of_mem (k := CMvMonomial.ofFinsupp m) (k_eq := by simp) (mem := by simp; use m) (distinct := ?distinct)] diff --git a/CompPoly/Multivariate/MvPolyEquiv/Eval.lean b/CompPoly/Multivariate/MvPolyEquiv/Eval.lean index 079b6482..649e0e3e 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Eval.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Eval.lean @@ -19,10 +19,10 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] omit [BEq R] [LawfulBEq R] in -lemma eval₂_equiv {S : Type} {p : CMvPolynomial n R} [CommSemiring S] {f : (R →+* S)} +lemma eval₂_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] {f : (R →+* S)} {vals : Fin n → S} : p.eval₂ f vals = (fromCMvPolynomial p).eval₂ f vals := by unfold CMvPolynomial.eval₂ MvPolynomial.eval₂ rw [foldl_eq_sum] @@ -53,11 +53,11 @@ lemma eval_equiv {p : CMvPolynomial n R} {vals : Fin n → R} : exact eval₂_equiv omit [BEq R] [LawfulBEq R] in -lemma totalDegree_equiv {S : Type} {p : CMvPolynomial n R} [CommSemiring S] : +lemma totalDegree_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] : p.totalDegree = (fromCMvPolynomial p).totalDegree := by rfl omit [BEq R] [LawfulBEq R] in -lemma degreeOf_equiv {S : Type} {p : CMvPolynomial n R} [CommSemiring S] : +lemma degreeOf_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] : p.degreeOf = (fromCMvPolynomial p).degreeOf := by ext i unfold MvPolynomial.degreeOf MvPolynomial.degrees @@ -83,10 +83,10 @@ end namespace CMvPolynomial -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-- `eval₂` as a ring homomorphism. -/ -def eval₂Hom {S : Type} [CommSemiring S] +def eval₂Hom {S : Type*} [CommSemiring S] (f : R →+* S) (vs : Fin n → S) : CMvPolynomial n R →+* S where toFun := eval₂ f vs map_zero' := by simp [eval₂_equiv] @@ -95,7 +95,7 @@ def eval₂Hom {S : Type} [CommSemiring S] map_mul' _ _ := by simp [eval₂_equiv, MvPolynomial.eval₂_mul] @[simp] -lemma eval₂Hom_apply {S : Type} [CommSemiring S] +lemma eval₂Hom_apply {S : Type*} [CommSemiring S] (f : R →+* S) (vs : Fin n → S) (p : CMvPolynomial n R) : eval₂Hom f vs p = eval₂ f vs p := rfl diff --git a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean index 3c234441..fd6ba948 100644 --- a/CompPoly/Multivariate/MvPolyEquiv/Instances.lean +++ b/CompPoly/Multivariate/MvPolyEquiv/Instances.lean @@ -19,7 +19,7 @@ open CMvPolynomial section -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] @[simp] lemma map_add (a b : CMvPolynomial n R) : @@ -176,7 +176,7 @@ instance {n : ℕ} : AddCommMonoid (CPoly.CMvPolynomial n R) where simp [add_comm] omit [BEq R] [LawfulBEq R] in -lemma toList_pairs_monomial_coeff {β : Type} [AddCommMonoid β] +lemma toList_pairs_monomial_coeff {β : Type*} [AddCommMonoid β] {t : Unlawful n R} {f : CMvMonomial n → R → β} : t.toList.map (fun term => f term.1 term.2) = @@ -187,7 +187,7 @@ lemma toList_pairs_monomial_coeff {β : Type} [AddCommMonoid β] grind omit [BEq R] [LawfulBEq R] in -lemma foldl_eq_sum {β : Type} [AddCommMonoid β] +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 = @@ -258,8 +258,8 @@ lemma map_mul (a b : CMvPolynomial n R) : · rw [←m_in] simp only [compare_self] unfold MvPolynomial.coeff MonoidAlgebra.single - simp only [m_in, Finsupp.single_eq_same] - rfl + simp only [m_in, ite_true, Option.getD_some] + erw [Finsupp.single_eq_same] · simp only [ Std.compare_eq_iff_eq, ExtTreeMap.not_mem_empty, @@ -267,18 +267,18 @@ lemma map_mul (a b : CMvPolynomial n R) : getElem?_neg ] unfold MvPolynomial.coeff MonoidAlgebra.single - rw [Finsupp.single_eq_of_ne (by symm; grind)] + erw [Finsupp.single_eq_of_ne (by symm; grind)] split next h contra => exfalso; apply m_in; symm apply CMvMonomial.injective_ofFinsupp contra next h => simp_all only [Option.getD_none] - have : F₃ = fun σ x ↦ fromCMvPolynomial (F₁ σ x) := by - ext x - rw [fromCMvPolynomial_F₁_eq_F₃] - rw [this] + -- Lean 4.29 may beta-reduce F₃; fold it back then rewrite + change fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) F₁) = + Finsupp.sum (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] - rfl instance {n : ℕ} : MonoidWithZero (CPoly.CMvPolynomial n R) where zero_mul a := by @@ -316,7 +316,7 @@ instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where section CommRing -variable {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommRing R] [BEq R] [LawfulBEq R] @[simp] lemma map_neg (a : CMvPolynomial n R) : @@ -362,7 +362,7 @@ end namespace CMvPolynomial -variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-- Ring equivalence between `CMvPolynomial 0 R` and `R`. -/ noncomputable def isEmptyRingEquiv : CMvPolynomial 0 R ≃+* R := diff --git a/CompPoly/Multivariate/Operations.lean b/CompPoly/Multivariate/Operations.lean index e3c0b5a5..862c9b56 100644 --- a/CompPoly/Multivariate/Operations.lean +++ b/CompPoly/Multivariate/Operations.lean @@ -29,7 +29,7 @@ namespace CPoly open Std -variable {R : Type} +variable {R : Type*} namespace CMvPolynomial @@ -55,7 +55,7 @@ def MonomialOrder.degree {n : ℕ} (m : CMvMonomial n) : ℕ := Returns `none` for the zero polynomial. -/ -def leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] +def leadingMonomial {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : Option (CMvMonomial n) := ExtTreeMap.foldl (fun acc m _ => @@ -72,7 +72,7 @@ def leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] Returns `0` for the zero polynomial, and otherwise returns the monomial with leading monomial and leading coefficient. -/ -def leadingTerm {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] +def leadingTerm {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] (p : CMvPolynomial n R) : CMvPolynomial n R := match leadingMonomial p with | none => 0 @@ -82,37 +82,37 @@ def leadingTerm {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrd Returns `0` for the zero polynomial. -/ -def leadingCoeff {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] +def leadingCoeff {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : R := match leadingMonomial p with | none => 0 | some m => coeff m p @[simp] lemma leadingCoeff_eq_zero_of_leadingMonomial_eq_none - {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} + {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} (h : leadingMonomial p = none) : leadingCoeff p = 0 := by simp [leadingCoeff, h] lemma leadingCoeff_eq_coeff_of_leadingMonomial_eq_some - {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} + {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} {m : CMvMonomial n} (h : leadingMonomial p = some m) : leadingCoeff p = coeff m p := by simp [leadingCoeff, h] /-- Packaged form of `leadingCoeff`: it is the coefficient at the optional leading monomial, defaulting to `0` when no leading monomial exists. -/ lemma leadingCoeff_eq_coeff_leadingMonomial - {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : + {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : leadingCoeff p = (leadingMonomial p).elim 0 (fun m => coeff m p) := by grind [leadingCoeff] @[simp] lemma leadingTerm_eq_zero_of_leadingMonomial_eq_none - {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] + {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] {p : CMvPolynomial n R} (h : leadingMonomial p = none) : leadingTerm p = 0 := by grind [leadingTerm] @[simp] lemma leadingTerm_eq_monomial_of_leadingMonomial_eq_some - {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] + {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] {p : CMvPolynomial n R} {m : CMvMonomial n} (h : leadingMonomial p = some m) : leadingTerm p = monomial m (coeff m p) := by grind [leadingTerm] @@ -123,16 +123,16 @@ lemma leadingCoeff_eq_coeff_leadingMonomial Given an algebra `σ` over `R` and a function `f : Fin n → σ`, evaluates the polynomial. -/ -def aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R σ] +def aeval {n : ℕ} {R σ : Type*} [CommSemiring R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) : σ := eval₂ (algebraMap R σ) f p -@[simp] lemma aeval_eq_eval₂ {n : ℕ} {R σ : Type} +@[simp] lemma aeval_eq_eval₂ {n : ℕ} {R σ : Type*} [CommSemiring R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) : aeval f p = eval₂ (algebraMap R σ) f p := rfl -@[simp] lemma aeval_C {n : ℕ} {R σ : Type} +@[simp] lemma aeval_C {n : ℕ} {R σ : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (c : R) : @@ -141,7 +141,7 @@ def aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R rw [eval₂_equiv (p := CMvPolynomial.C (n := n) c) (f := algebraMap R σ) (vals := f)] simp [CMvPolynomial.fromCMvPolynomial_C] -@[simp] lemma aeval_add {n : ℕ} {R σ : Type} +@[simp] lemma aeval_add {n : ℕ} {R σ : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p q : CMvPolynomial n R) : @@ -150,7 +150,7 @@ def aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R simpa [CMvPolynomial.eval₂Hom_apply] using (CMvPolynomial.eval₂Hom (S := σ) (algebraMap R σ) f).map_add p q -@[simp] lemma aeval_mul {n : ℕ} {R σ : Type} +@[simp] lemma aeval_mul {n : ℕ} {R σ : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p q : CMvPolynomial n R) : @@ -163,14 +163,14 @@ def aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R Given `f : Fin n → CMvPolynomial m R`, substitutes `f i` for variable `X i`. -/ -def bind₁ {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +def bind₁ {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : CMvPolynomial m R := ExtTreeMap.foldl (fun acc mono c => CMvPolynomial.C (n := m) c * MonoR.evalMonomial f mono + acc) 0 p.1 /-- The computable substitution `bind₁` agrees with algebraic evaluation. -/ -lemma bind₁_eq_aeval {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma bind₁_eq_aeval {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : bind₁ f p = aeval (σ := CMvPolynomial m R) f p := by have hmap : ∀ c : R, @@ -180,19 +180,19 @@ lemma bind₁_eq_aeval {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBE unfold bind₁ aeval CMvPolynomial.eval₂ simp [hmap] -@[simp] lemma bind₁_C {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +@[simp] lemma bind₁_C {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (c : R) : bind₁ f (CMvPolynomial.C (n := n) c) = CMvPolynomial.C (n := m) c := by rw [bind₁_eq_aeval] simpa using (aeval_C (n := n) (R := R) (σ := CMvPolynomial m R) f c) -@[simp] lemma bind₁_add {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +@[simp] lemma bind₁_add {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p q : CMvPolynomial n R) : bind₁ f (p + q) = bind₁ f p + bind₁ f q := by repeat rw [bind₁_eq_aeval] simpa using (aeval_add (n := n) (R := R) (σ := CMvPolynomial m R) f p q) -@[simp] lemma bind₁_mul {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +@[simp] lemma bind₁_mul {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p q : CMvPolynomial n R) : bind₁ f (p * q) = bind₁ f p * bind₁ f q := by repeat rw [bind₁_eq_aeval] @@ -204,7 +204,7 @@ lemma bind₁_eq_aeval {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBE Given `f : Fin n → Fin m`, renames variable `X i` to `X (f i)`. -/ -def rename {n m : ℕ} {R : Type} [Zero R] [Add R] [BEq R] [LawfulBEq R] +def rename {n m : ℕ} {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] (f : Fin n → Fin m) (p : CMvPolynomial n R) : CMvPolynomial m R := let renameMonomial (mono : CMvMonomial n) : CMvMonomial m := Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i)) @@ -213,13 +213,13 @@ def rename {n m : ℕ} {R : Type} [Zero R] [Add R] [BEq R] [LawfulBEq R] -- `renameEquiv` is defined in `CompPoly.Multivariate.Rename` /-- Iterative reconstruction of a polynomial by folding over terms. -/ -def sumToIter {n : ℕ} {R : Type} [Zero R] [Add R] [BEq R] [LawfulBEq R] +def sumToIter {n : ℕ} {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : CMvPolynomial n R := ExtTreeMap.foldl (fun acc m c => acc + monomial m c) 0 p.1 /-! ## Bridge and transport lemmas (technical) -/ -lemma X_eq_monomial {k : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma X_eq_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (i : Fin k) : CMvPolynomial.X (R := R) i = CMvPolynomial.monomial (Vector.ofFn (fun j => if j = i then 1 else 0)) @@ -241,7 +241,7 @@ lemma toFinsupp_unitMono {k : ℕ} simp [CMvMonomial.toFinsupp, Vector.get, Finsupp.single_apply, eq_comm] -lemma fromCMvPolynomial_monomial {k : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma fromCMvPolynomial_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (mono : CMvMonomial k) (c : R) : fromCMvPolynomial (CMvPolynomial.monomial mono c) = MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by @@ -268,14 +268,14 @@ lemma fromCMvPolynomial_monomial {k : ℕ} {R : Type} [CommSemiring R] [BEq R] [ (by simp [hne])] rfl -lemma fromCMvPolynomial_X {k : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma fromCMvPolynomial_X {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (i : Fin k) : fromCMvPolynomial (CMvPolynomial.X (R := R) i) = MvPolynomial.X i := by rw [X_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_unitMono] rfl -@[simp] lemma aeval_X {n : ℕ} {R σ : Type} +@[simp] lemma aeval_X {n : ℕ} {R σ : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (i : Fin n) : @@ -284,13 +284,13 @@ lemma fromCMvPolynomial_X {k : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulB rw [eval₂_equiv (p := CMvPolynomial.X (R := R) i) (f := algebraMap R σ) (vals := f)] simp [fromCMvPolynomial_X] -@[simp] lemma bind₁_X {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +@[simp] lemma bind₁_X {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (i : Fin n) : bind₁ f (CMvPolynomial.X (R := R) i) = f i := by rw [bind₁_eq_aeval] simpa using (aeval_X (n := n) (R := R) (σ := CMvPolynomial m R) f i) -@[simp] lemma bind₁_id {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +@[simp] lemma bind₁_id {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : bind₁ (fun i => CMvPolynomial.X (R := R) i) p = p := by rw [bind₁_eq_aeval] @@ -345,7 +345,7 @@ lemma fromCMvPolynomial_X {k : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulB simp [MvPolynomial.eval₂_eta (p := fromCMvPolynomial p)] _ = CPoly.polyRingEquiv (n := n) (R := R) p := rfl -lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β] +lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] (g : K → V → β) (l : List (K × V)) (init : β) : List.foldl (fun acc pair => acc + g pair.1 pair.2) init l = List.foldl (fun acc pair => g pair.1 pair.2 + acc) init l := by @@ -356,8 +356,8 @@ lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β] rw [show init + g h.1 h.2 = g h.1 h.2 + init from add_comm _ _] exact ih _ -lemma foldl_add_comm {β : Type} [AddCommMonoid β] {k : ℕ} - {R' : Type} (g : CMvMonomial k → R' → β) +lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {k : ℕ} + {R' : Type*} (g : CMvMonomial k → R' → β) (t : Std.ExtTreeMap (CMvMonomial k) R') : Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t = Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by @@ -375,7 +375,7 @@ lemma fromCMvPolynomial_finsupp_sum {n k : ℕ} [CommSemiring R] [BEq R] [Lawful /-! ## API lemmas for `sumToIter` -/ -lemma sumToIter_eq {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma sumToIter_eq {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : sumToIter p = p := by rw [eq_iff_fromCMvPolynomial] unfold sumToIter @@ -386,21 +386,21 @@ lemma sumToIter_eq {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] rw [Finsupp.sum] exact MvPolynomial.support_sum_monomial_coeff (fromCMvPolynomial p) -lemma coeff_sumToIter {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma coeff_sumToIter {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (m : CMvMonomial n) (p : CMvPolynomial n R) : coeff m (sumToIter p) = coeff m p := by simp [sumToIter_eq (p := p)] -@[simp] lemma sumToIter_zero {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] : +@[simp] lemma sumToIter_zero {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] : sumToIter (0 : CMvPolynomial n R) = 0 := by simpa using sumToIter_eq (p := (0 : CMvPolynomial n R)) -lemma sumToIter_add {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +lemma sumToIter_add {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CMvPolynomial n R) : sumToIter (p + q) = sumToIter p + sumToIter q := by simp [sumToIter_eq] -@[simp] lemma sumToIter_idempotent {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +@[simp] lemma sumToIter_idempotent {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : sumToIter (sumToIter p) = sumToIter p := by simp [sumToIter_eq] diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean index e104ec4a..84d29b23 100644 --- a/CompPoly/Multivariate/Rename.lean +++ b/CompPoly/Multivariate/Rename.lean @@ -27,13 +27,13 @@ namespace CPoly open Std CMvPolynomial -variable {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] +variable {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] /-! ### Helper lemmas for `fromCMvPolynomial_rename` -/ /-- In a commutative additive monoid, the order of addition in a list fold does not matter. -/ -lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β] +lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] (g : K → V → β) (l : List (K × V)) (init : β) : List.foldl (fun acc pair => acc + g pair.1 pair.2) init l = List.foldl (fun acc pair => g pair.1 pair.2 + acc) init l := by @@ -45,8 +45,8 @@ lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β] exact ih _ /-- Swapping addition order in `ExtTreeMap.foldl` does not change the result. -/ -lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ} - {R' : Type} (g : CMvMonomial k → R' → β) +lemma foldl_add_comm' {β : Type*} [AddCommMonoid β] {k : ℕ} + {R' : Type*} (g : CMvMonomial k → R' → β) (t : Std.ExtTreeMap (CMvMonomial k) R') : Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t = Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by @@ -180,6 +180,7 @@ lemma toFinsupp_zero {k : ℕ} : CMvMonomial.toFinsupp (0 : CMvMonomial k) = 0 := by ext i simp [CMvMonomial.toFinsupp, Vector.get] + exact Vector.getElem_zero i.val i.isLt /-- `fromCMvPolynomial` maps `CMvPolynomial.C` to `MvPolynomial.C`. -/ lemma fromCMvPolynomial_C {k : ℕ} (c : R) : diff --git a/CompPoly/Multivariate/Restrict.lean b/CompPoly/Multivariate/Restrict.lean index 5bd49176..18c6a13a 100644 --- a/CompPoly/Multivariate/Restrict.lean +++ b/CompPoly/Multivariate/Restrict.lean @@ -20,7 +20,7 @@ namespace CPoly open CMvPolynomial -variable {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] +variable {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] /-- Coefficient of `restrictBy keep p` at `m`: `p.coeff m` if `keep m`, else `0`. -/ lemma coeff_restrictBy (keep : CMvMonomial n → Prop) [DecidablePred keep] @@ -152,7 +152,7 @@ private lemma vector_ofFn_sum_eq_finSum {n : ℕ} (s : Fin n → ℕ) : (Vector.ofFn s).sum = (Array.ofFn s).sum := by simp [Vector.sum, Vector.toArray_ofFn] _ = (Array.ofFn s).toList.sum := by - exact (Array.sum_eq_sum_toList (as := Array.ofFn s)).symm + exact (Array.sum_toList (as := Array.ofFn s)).symm _ = (List.ofFn s).sum := by exact congrArg List.sum (Array.toList_ofFn (f := s)) _ = ∑ i : Fin n, s i := list_ofFn_sum_eq_finSum s @@ -171,7 +171,7 @@ private lemma totalDegree_eq_finsupp_sum {n : ℕ} (m : CMvMonomial n) : /-- `restrictTotalDegree d p` has `totalDegree ≤ d`. -/ lemma totalDegree_restrictTotalDegree_le - {R' : Type} [CommSemiring R'] [BEq R'] [LawfulBEq R'] + {R' : Type*} [CommSemiring R'] [BEq R'] [LawfulBEq R'] (d : ℕ) (p : CMvPolynomial n R') : (CMvPolynomial.restrictTotalDegree d p).totalDegree ≤ d := by classical diff --git a/CompPoly/Multivariate/Unlawful.lean b/CompPoly/Multivariate/Unlawful.lean index 1b5ea739..a8b61872 100644 --- a/CompPoly/Multivariate/Unlawful.lean +++ b/CompPoly/Multivariate/Unlawful.lean @@ -5,9 +5,8 @@ Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdusa -/ import CompPoly.Multivariate.CMvMonomial import CompPoly.Multivariate.Wheels -import Mathlib.Algebra.Lie.OfAssociative -import Std.Data.ExtTreeMap import ExtTreeMapLemmas.ExtTreeMap +import Mathlib.Algebra.Lie.OfAssociative /-! # Unlawful multivariate polynomials @@ -20,6 +19,8 @@ the absence of zero coefficients. * `CPoly.Unlawful n R`: A map from `CMvMonomial n` to `R`, implemented using `Std.ExtTreeMap`. -/ +set_option allowUnsafeReducibility true in +attribute [local reducible] instDecidableEqOfLawfulBEq attribute [local instance 5] instDecidableEqOfLawfulBEq namespace CPoly @@ -30,13 +31,12 @@ open Std Polynomial in `n` variables with coefficients in `R`. Internally represented as a tree map from monomials to coefficients. -/ -@[grind =] -def Unlawful (n : ℕ) (R : Type) : Type := +abbrev Unlawful (n : ℕ) (R : Type*) : Type _ := Std.ExtTreeMap (CMvMonomial n) R (Ord.compare (α := CMvMonomial n)) section Instances -variable {n : ℕ} {R : Type} +variable {n : ℕ} {R : Type*} instance : EmptyCollection (Unlawful n R) := ⟨(∅ : Std.ExtTreeMap (CMvMonomial n) R compare)⟩ @@ -76,7 +76,7 @@ lemma ext_getElem? {n R} {t₁ t₂ : Unlawful n R} (h : ∀ (k : CMvMonomial n), t₁[k]? = t₂[k]?) : t₁ = t₂ := Std.ExtTreeMap.ext_getElem? h -variable {n : ℕ} {R : Type} +variable {n : ℕ} {R : Type*} /-- Construct an `Unlawful` polynomial from a list of monomial-coefficient pairs. -/ @[simp, grind =] @@ -104,7 +104,7 @@ instance [Repr R] : Repr (Unlawful n R) where reprPrec p _ := if p.isEmpty then "0" else let toFormat : Std.ToFormat (CMvMonomial n × R) := - ⟨λ (m, c) => repr c ++ " * " ++ repr m⟩ + ⟨fun (m, c) => repr c ++ " * " ++ repr m⟩ @Std.Format.joinSep _ toFormat p.toList " + " /-- Constant polynomial. -/ @@ -135,7 +135,9 @@ lemma C_zero' : C (n := n) (0 : ℕ) = 0 := rfl @[simp, grind =] lemma zero_eq_zero : (Zero.zero : R) = 0 := rfl -lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful n R) = ∅ := by unfold_projs; simp [C] +lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful n R) = ∅ := by + unfold_projs + simp [C] @[simp, grind .] lemma not_mem_C_zero : x ∉ C 0 := by grind @@ -145,10 +147,10 @@ section variable [BEq R] [LawfulBEq R] @[simp, grind .] -lemma not_mem_zero : x ∉ (0 : Unlawful n R) := by rw [←C_zero]; grind +lemma not_mem_zero : x ∉ (0 : Unlawful n R) := by rw [← C_zero]; grind @[simp, grind .] -lemma isNoZeroCoef_zero : isNoZeroCoef (n := n) (R := R) 0 := by rw [←C_zero]; grind +lemma isNoZeroCoef_zero : isNoZeroCoef (n := n) (R := R) 0 := by rw [← C_zero]; grind end @@ -160,7 +162,7 @@ def add [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R := instance [Add R] : Add (Unlawful n R) := ⟨add⟩ -@[grind=] +@[grind =] protected lemma grind_add_skip [Add R] {p₁ p₂ : Unlawful n R} : p₁ + p₂ = p₁.mergeWith (fun _ c₁ c₂ ↦ c₁ + c₂) p₂ := rfl @@ -170,11 +172,11 @@ def addMonoR [Add R] (p : Unlawful n R) (term : MonoR n R) : Unlawful n R := /-- Multiply a polynomial by a single monomial term. -/ def mul₀ [Mul R] (t : MonoR n R) (p : Unlawful n R) : Unlawful n R := - .ofList (p.toList.map fun (k, v) ↦ (t.1+k, t.2*v)) + .ofList (p.toList.map fun (k, v) => (t.1 + k, t.2 * v)) -attribute [grind=] ExtTreeMap.ofList_eq_empty_iff List.map_eq_nil_iff ExtTreeMap.toList_eq_nil_iff +attribute [grind =] ExtTreeMap.ofList_eq_empty_iff List.map_eq_nil_iff ExtTreeMap.toList_eq_nil_iff -@[simp, grind=] +@[simp, grind =] lemma mul₀_zero [Zero R] [BEq R] [LawfulBEq R] [Mul R] {t : MonoR n R} : mul₀ t 0 = 0 := by unfold mul₀ grind @@ -218,15 +220,15 @@ instance instDecidableEq [DecidableEq R] : DecidableEq (Unlawful n R) := fun x y then Decidable.isTrue (ExtTreeMap.ext_toList (h ▸ List.perm_rfl)) else Decidable.isFalse (by grind) -def coeff {R : Type} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : Unlawful n R) : R := +def coeff {R : Type*} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : Unlawful n R) : R := p[m]?.getD 0 @[simp, grind =] -lemma filter_get {R : Type} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : +lemma filter_get {R : Type*} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : (ExtTreeMap.filter (fun _ c => c != v) a)[m]?.getD v = a[m]?.getD v := by grind -lemma add_getD? [CommSemiring R] {m : CMvMonomial n} {p q : Unlawful n R} : +lemma add_getD? [AddZeroClass R] {m : CMvMonomial n} {p q : Unlawful n R} : (p.add q)[m]?.getD 0 = p[m]?.getD 0 + q[m]?.getD 0 := by unfold Unlawful.add by_cases m ∈ p <;> by_cases m ∈ q <;> grind [add_zero, zero_add] diff --git a/CompPoly/Multivariate/VarsDegrees.lean b/CompPoly/Multivariate/VarsDegrees.lean index e3e746a6..985d1e40 100644 --- a/CompPoly/Multivariate/VarsDegrees.lean +++ b/CompPoly/Multivariate/VarsDegrees.lean @@ -18,7 +18,7 @@ namespace CPoly open CMvPolynomial -variable {n : ℕ} {R : Type} +variable {n : ℕ} {R : Type*} /-- `i ∈ p.vars` iff `0 < p.degreeOf i`. -/ @[simp] diff --git a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean index f3f1e99a..ab4527e9 100644 --- a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean +++ b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean @@ -143,6 +143,7 @@ theorem totalDegree_coeff_finSuccEquivNth_add_le (f : MvPolynomial (Fin (n + 1)) · rw [totalDegree, hσ2, sum_insertNth _ _ p, add_comm] · rwa [← support_coeff_finSuccEquivNth] +set_option backward.isDefEq.respectTransparency false in /-- The support of `finSuccEquivNth R p f` equals the support of `f` projected onto the `p`-th variable. -/ theorem support_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) : diff --git a/CompPoly/Univariate/Quotient/Core.lean b/CompPoly/Univariate/Quotient/Core.lean index 9a35d2dc..4ced5704 100644 --- a/CompPoly/Univariate/Quotient/Core.lean +++ b/CompPoly/Univariate/Quotient/Core.lean @@ -250,8 +250,7 @@ lemma add_descends [Semiring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPo equiv a₁ a₂ → equiv b₁ b₂ → addDescending a₁ b₁ = addDescending a₂ b₂ := by intros heq_a heq_b unfold addDescending - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] + apply Quotient.sound calc add a₁ b₁ ≈ addRaw a₁ b₁ := add_equiv_raw a₁ b₁ _ ≈ addRaw a₂ b₂ := by @@ -273,8 +272,7 @@ lemma smul_descends [Semiring R] (r : R) (p₁ p₂ : CPolynomial.Raw R) : equiv p₁ p₂ → smulDescending r p₁ = smulDescending r p₂ := by unfold equiv smulDescending intro heq - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] + apply Quotient.sound intro i rw [smul_equiv, smul_equiv, heq i] @@ -294,9 +292,9 @@ lemma nsmul_descends [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) unfold equiv intro heq unfold nsmulDescending - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] - unfold nsmul equiv + apply Quotient.sound + unfold nsmul + show equiv _ _ intro i repeat rw [nsmulRaw_equiv, coeff_eq_coeff] rw [heq i] @@ -316,9 +314,8 @@ lemma neg_descends [NegZeroClass R] (a b : CPolynomial.Raw R) : equiv a b → negDescending a = negDescending b := by unfold equiv negDescending intros heq - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] - unfold equiv + apply Quotient.sound + show equiv _ _ intro i rw [neg_coeff a i, neg_coeff b i, heq i] @@ -336,9 +333,8 @@ lemma sub_descends [Ring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolyno equiv a₁ a₂ → equiv b₁ b₂ → subDescending a₁ b₁ = subDescending a₂ b₂ := by unfold equiv subDescending intros heq_a heq_b - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] - unfold sub equiv + apply Quotient.sound + unfold sub calc a₁.add b₁.neg ≈ a₁.addRaw b₁.neg := add_equiv_raw a₁ b₁.neg _ ≈ a₂.addRaw b₂.neg := by @@ -361,9 +357,8 @@ lemma mulPowX_descends [Zero R] (i : ℕ) (p₁ p₂ : CPolynomial.Raw R) : equiv p₁ p₂ → mulPowXDescending i p₁ = mulPowXDescending i p₂ := by unfold mulPowXDescending intro heq - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] - apply mulPowX_equiv; exact heq + apply Quotient.sound + exact mulPowX_equiv i p₁ p₂ heq /-- Multiplication by `X^i` on the quotient. -/ @[inline, specialize] @@ -384,8 +379,7 @@ lemma mul_descends [Semiring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPo equiv a₁ a₂ → equiv b₁ b₂ → mulDescending a₁ b₁ = mulDescending a₂ b₂ := by unfold mulDescending intros heq_a heq_b - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] + apply Quotient.sound calc a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a _ ≈ a₂.mul b₂ := mul_equiv₂ a₂ b₁ b₂ heq_b @@ -405,8 +399,7 @@ lemma pow_descends [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPo equiv p₁ p₂ → powDescending p₁ n = powDescending p₂ n := by intro heq unfold powDescending - rw [Quotient.eq] - simp [Raw.instSetoidCPolynomial] + apply Quotient.sound unfold pow have mul_pow_succ_equiv (p : CPolynomial.Raw R) (n : ℕ): p.mul^[n + 1] (C 1) ≈ p.mul (p.mul^[n] (C 1)) := by @@ -676,7 +669,6 @@ lemma npow_succ : ∀ (n : ℕ) (x : QuotientCPolynomial R), x.pow (n + 1) = x.p exact Function.iterate_succ_apply' _ _ _] convert commute_pow_self n ( Quotient.mk ( Raw.instSetoidCPolynomial ) p ) using 1 erw [ Quotient.eq ] - rfl /-- `QuotientCPolynomial R` forms a semiring when `R` is a semiring. @@ -741,7 +733,7 @@ instance : Ring (QuotientCPolynomial R) where have h_neg_succ : ∀ n : ℕ, Int.negSucc n = - (n + 1 : ℤ) := by grind convert h_neg_succ convert Quotient.eq using 1 - simp +decide [ Raw.instSetoidCPolynomial ] + simp +decide simp +decide [ Raw.C, Raw.neg ] grind end Ring diff --git a/CompPoly/Univariate/Raw/Proofs.lean b/CompPoly/Univariate/Raw/Proofs.lean index c5abdfc8..cd36d1e4 100644 --- a/CompPoly/Univariate/Raw/Proofs.lean +++ b/CompPoly/Univariate/Raw/Proofs.lean @@ -544,7 +544,7 @@ lemma equiv_mul_one [LawfulBEq R] (p : CPolynomial.Raw R) : Trim.equiv (p * 1) p · simp +decide conv => rw [ ← Array.toList_zipIdx ] conv => rw [ ← Array.toList_map ] - exact Eq.symm Array.sum_eq_sum_toList) + exact Eq.symm Array.sum_toList) exact (by exact mul_one_unwrap p ▸ coeff_sum p i ▸ rfl) exact congrFun (h_mul_one p) diff --git a/lake-manifest.json b/lake-manifest.json index 4d3901d2..170a5d88 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1c21eb1270312fdcdac35d6b6bf07e0863f7ef45", + "rev": "5e5184282f96edc8b71c4c1626e4bb14d7a3cace", "name": "ExtTreeMapLemmas", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-patch-1", + "inputRev": "v4.29.0-rc6-patch-1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", + "rev": "5c8398df528176d9c87ccd9226ba8f7c8852d59c", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.29.0-rc6", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", + "rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", + "rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", + "rev": "2e58165a9dcdca9837b666528f974299ee1a51cc", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.87", + "inputRev": "v0.0.92", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", + "rev": "c3361708f266893de5d1769192b60d4b1831f2bb", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", + "rev": "221e8088e3a066b8676dc471ff10638cf1c10835", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "rev": "bd58e3506632241b59e406902d5e42b73cdeccce", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", + "rev": "3de531c1135f5e3a01f3ac04830996fda476b28e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.29.0-rc6", "inherited": true, "configFile": "lakefile.toml"}], "name": "CompPoly", diff --git a/lakefile.lean b/lakefile.lean index b94a0207..f8024916 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,9 +6,9 @@ package CompPoly where version := v!"0.1.0" testDriver := "CompPolyTests" -require "leanprover-community" / mathlib @ git "v4.28.0" +require "leanprover-community" / mathlib @ git "v4.29.0-rc6" -require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.28.0-patch-1" +require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.29.0-rc6-patch-1" @[default_target] lean_lib CompPoly diff --git a/lean-toolchain b/lean-toolchain index ea6ca7ff..bf718850 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0 \ No newline at end of file +leanprover/lean4:v4.29.0-rc6 \ No newline at end of file diff --git a/tests/CompPolyTests/Univariate/Linear.lean b/tests/CompPolyTests/Univariate/Linear.lean index abcccc9c..62144f07 100644 --- a/tests/CompPolyTests/Univariate/Linear.lean +++ b/tests/CompPolyTests/Univariate/Linear.lean @@ -14,25 +14,23 @@ import CompPoly.Univariate.ToPoly.Degree namespace CompPoly namespace CPolynomial -private def natBeqEq : BEq Nat := ⟨fun a b => decide (a = b)⟩ +@[reducible] private def natBeqEq : BEq Nat := ⟨fun a b => decide (a = b)⟩ private theorem nat_lawful_beq_eq : @LawfulBEq Nat natBeqEq := by letI : BEq Nat := natBeqEq refine { rfl := ?_, eq_of_beq := ?_ } - · intro a - simp [natBeqEq] - · intro a b h - simpa [natBeqEq] using h + · intro a; erw [show natBeqEq.beq a a = decide (a = a) from rfl]; simp + · intro a b h; erw [show natBeqEq.beq a b = decide (a = b) from rfl] at h; simpa using h -private def natBeqSucc : BEq Nat := ⟨fun a b => decide (a.succ = b.succ)⟩ +@[reducible] private def natBeqSucc : BEq Nat := ⟨fun a b => decide (a.succ = b.succ)⟩ private theorem nat_lawful_beq_succ : @LawfulBEq Nat natBeqSucc := by letI : BEq Nat := natBeqSucc refine { rfl := ?_, eq_of_beq := ?_ } - · intro a - simp [natBeqSucc] + · intro a; erw [show natBeqSucc.beq a a = decide (a.succ = a.succ) from rfl]; simp · intro a b h - exact Nat.succ.inj <| by simpa [natBeqSucc] using h + erw [show natBeqSucc.beq a b = decide (a.succ = b.succ) from rfl] at h + exact Nat.succ.inj <| by simpa using h private def leftPoly : CPolynomial Nat := @CPolynomial.monomial Nat _ natBeqEq nat_lawful_beq_eq _ 1 7