From 0da5723406a6ac9e158a180d5fa9393b45ff88e9 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Fri, 12 Dec 2025 14:05:17 +0000 Subject: [PATCH 01/11] feat: main definitions and theorems for remaining univariate polynomial operations (aside from div, for now); some sorrys that will be resolved --- CompPoly/Univariate/Basic.lean | 138 ++++++++++++++++++++++++++++++++- 1 file changed, 137 insertions(+), 1 deletion(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index c3131d1..2dd7e6e 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -594,6 +594,23 @@ lemma add_equiv_raw [LawfulBEq R] (p q : CPolynomial R) : Trim.equiv (p.add q) ( unfold Trim.equiv add exact Trim.coeff_eq_coeff (p.add_raw q) +def smul_equiv : ∀ (i : ℕ) (r : R), + (smul r p).coeff i = r * (p.coeff i) := by + intro i r + unfold smul mk coeff + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] + +def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), + (nsmul_raw n p).trim.coeff i = n * p.trim.coeff i := by + intro n i + unfold nsmul_raw + repeat rw [Trim.coeff_eq_coeff] + unfold mk + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] + +def mulPowX_equiv : ∀ (i j : ℕ), + (mulPowX i p).coeff j = p.coeff (j - i) := by sorry + omit [BEq R] in lemma neg_coeff : ∀ (p : CPolynomial R) (i : ℕ), p.neg.coeff i = - p.coeff i := by intro p i @@ -926,6 +943,15 @@ def QuotientCPolynomial (R : Type*) [Ring R] [BEq R] := Quotient (@instSetoidCPo -- operations on `CPolynomial` descend to `QuotientCPolynomial` namespace QuotientCPolynomial +lemma mul_equiv (a₁ a₂ b : CPolynomial R) : + equiv a₁ a₂ → equiv (a₁.mul b) (a₂.mul b) := by sorry + +lemma mul_comm (a b : CPolynomial R) : + a.mul b ≈ b.mul a := by sorry + +lemma pow_equiv : ∀ (p : CPolynomial R) (n : ℕ), + (p.mul^[n + 1] (C 1)) ≈ (p.mul (p.mul^[n] (C 1))) := by sorry + -- Addition: add descends to `QuotientCPolynomial` def add_descending (p q : CPolynomial R) : QuotientCPolynomial R := Quotient.mk _ (add p q) @@ -947,6 +973,46 @@ lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : def add {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift₂ add_descending add_descends p q +-- Scalar multiplication: smul descends to `QuotientCPolynomial` +def smul_descending (r : R) (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (smul r p) + +lemma smul_descends [LawfulBEq R] (r : R) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → smul_descending r p₁ = smul_descending r p₂ := by + unfold equiv smul_descending + intro heq + rw [Quotient.eq] + simp [instSetoidCPolynomial] + intro i + rw [smul_equiv p₁, smul_equiv p₂] + rw [heq i] + +@[inline, specialize] +def smul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (r : R) (p : QuotientCPolynomial R) + : QuotientCPolynomial R := + Quotient.lift (smul_descending r) (smul_descends r) p + +-- Scalar multiplication: nsmul_raw descends to `QuotientCPolynomial` +def nsmul_descending (n : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (nsmul n p) + +lemma nsmul_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → nsmul_descending n p₁ = nsmul_descending n p₂ := by + unfold equiv + intro heq + unfold nsmul_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + unfold nsmul equiv + intro i + repeat rw [nsmul_raw_equiv, coeff_eq_coeff] + rw [heq i] + +@[inline, specialize] +def nsmul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : QuotientCPolynomial R) + : QuotientCPolynomial R := + Quotient.lift (nsmul_descending n) (nsmul_descends n) p + -- Negation: neg descends to `QuotientCPolynomial` def neg_descending (p : CPolynomial R) : QuotientCPolynomial R := Quotient.mk _ (neg p) @@ -987,7 +1053,77 @@ lemma sub_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : def sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift₂ sub_descending sub_descends p q --- TODO the other operations ... +-- Multiplication by `X ^ i`: mulPowX descends to `QuotientCPolynomial` +def mulPowX_descending (i : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (mulPowX i p) + +lemma mulPowX_descends (i : ℕ) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → mulPowX_descending i p₁ = mulPowX_descending i p₂ := by + unfold equiv + intro heq + unfold mulPowX_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + intro j + rw [mulPowX_equiv p₁, mulPowX_equiv p₂] + rw [heq] + +@[inline, specialize] +def mulPowX {R : Type*} [Ring R] [BEq R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift (mulPowX_descending i) (mulPowX_descends i) p + +-- Multiplication of a `CPolynomial` by `X`, reduces to `mulPowX 1`. +@[inline, specialize] +def mulX (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 + +-- Multiplication: mul descends to `QuotientPoly` +def mul_descending (p q : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (mul p q) + +lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : + equiv a₁ a₂ → equiv b₁ b₂ → mul_descending a₁ b₁ = mul_descending a₂ b₂ := by + unfold mul_descending + intros heq_a heq_b + rw [Quotient.eq] + simp [instSetoidCPolynomial] + calc + a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a + _ ≈ b₁.mul a₂ := mul_comm a₂ b₁ + _ ≈ b₂.mul a₂ := mul_equiv b₁ b₂ a₂ heq_b + _ ≈ a₂.mul b₂ := mul_comm b₂ a₂ + +@[inline, specialize] +def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift₂ mul_descending mul_descends p q + +-- Exponentiation: pow descends to `QuotientCPolynomial` +def pow_descending (p : CPolynomial R) (n : ℕ) : QuotientCPolynomial R := + Quotient.mk _ (pow p n) + +lemma pow_descends (n : ℕ) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → pow_descending p₁ n = pow_descending p₂ n := by + intro heq + unfold pow_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + unfold pow + -- intro i + induction n with + | zero => simp + | succ n ih => + calc + p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := pow_equiv p₁ n + _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := mul_comm p₁ (p₁.mul^[n] (C 1)) + _ ≈ (p₂.mul^[n] (C 1)).mul p₁ := mul_equiv _ _ p₁ ih + _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_comm (p₂.mul^[n] (C 1)) p₁ + _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq + _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (pow_equiv p₂ n) + +@[inline, specialize] +def pow {R : Type*} [Ring R] [BEq R] (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := + Quotient.lift (fun p => pow_descending p n) (pow_descends n) p + +-- TODO div? end QuotientCPolynomial From 1085a63188c2ccc478d3e94ac88666711fff3ee0 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 15 Dec 2025 12:52:53 +0000 Subject: [PATCH 02/11] feat: equivalence lemmas over mulPowX and smul --- CompPoly/Univariate/Basic.lean | 42 ++++++++++++++++++++++++++++++---- 1 file changed, 38 insertions(+), 4 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 2dd7e6e..ea1851d 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -574,6 +574,17 @@ theorem add_size {p q : CPolynomial Q} : (add_raw p q).size = max p.size q.size change (Array.zipWith _ _ _ ).size = max p.size q.size rw [zipWith_size matchSize_size_eq, matchSize_size] +-- coeff on list concatenations +lemma concat_coeff₁ (i : ℕ) : i < p.size → + (p ++ q).coeff i = p.coeff i := by + simp + grind + +lemma concat_coeff₂ (i : ℕ) : i ≥ p.size → + (p ++ q).coeff i = q.coeff (i - p.size) := by + simp + grind + theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : (add_raw p q)[i] = p.coeff i + q.coeff i := by @@ -608,8 +619,28 @@ def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), unfold mk rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] -def mulPowX_equiv : ∀ (i j : ℕ), - (mulPowX i p).coeff j = p.coeff (j - i) := by sorry +lemma mulPowX_equiv₁ : ∀ (i j : ℕ), j ≥ i → + (mulPowX i p).coeff j = p.coeff (j - i) := by + intro i j h + unfold mulPowX mk + rw [concat_coeff₂ (Array.replicate i 0) p j] + . simp + have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp + rw [← h_size i] + simp + exact h + +lemma mulPowX_equiv₂ : ∀ (i j : ℕ), j < i → + (mulPowX i p).coeff j = 0 := by + intro i j h + unfold mulPowX mk + rw [concat_coeff₁ (Array.replicate i 0) p j] + . simp + grind + have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp + rw [← h_size i] + simp + exact h omit [BEq R] in lemma neg_coeff : ∀ (p : CPolynomial R) (i : ℕ), p.neg.coeff i = - p.coeff i := by @@ -1065,8 +1096,11 @@ lemma mulPowX_descends (i : ℕ) (p₁ p₂ : CPolynomial R) : rw [Quotient.eq] simp [instSetoidCPolynomial] intro j - rw [mulPowX_equiv p₁, mulPowX_equiv p₂] - rw [heq] + by_cases h : j ≥ i + . rw [mulPowX_equiv₁ p₁ i j h, mulPowX_equiv₁ p₂ i j h] + rw [heq] + . simp at h + rw [mulPowX_equiv₂ p₁ i j h, mulPowX_equiv₂ p₂ i j h] @[inline, specialize] def mulPowX {R : Type*} [Ring R] [BEq R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := From 9671dec0e65eb60fd94a917f7e99e312012f3a13 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 16 Dec 2025 11:26:22 +0000 Subject: [PATCH 03/11] progress on associativity of power-based multiplication lemmas --- CompPoly/Univariate/Basic.lean | 87 +++++++++++++++++++++++++++------- 1 file changed, 70 insertions(+), 17 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index ea1851d..7a17ce2 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -137,7 +137,7 @@ theorem last_nonzero_some_iff [LawfulBEq R] {p : CPolynomial R} {k} : /-- eliminator for `p.last_nonzero`, e.g. use with the induction tactic as follows: ``` - induction p using last_none_zero_elim with + induction p using last_nonzero_induct with | case1 p h_none h_all_zero => ... | case2 p k h_some h_nonzero h_max => ... ``` @@ -157,7 +157,7 @@ theorem last_nonzero_induct [LawfulBEq R] {motive : CPolynomial R → Prop} /-- eliminator for `p.trim`; use with the induction tactic as follows: ``` - induction p using Trim.elim with + induction p using induct with | case1 p h_empty h_all_zero => ... | case2 p k h_extract h_nonzero h_max => ... ``` @@ -974,14 +974,62 @@ def QuotientCPolynomial (R : Type*) [Ring R] [BEq R] := Quotient (@instSetoidCPo -- operations on `CPolynomial` descend to `QuotientCPolynomial` namespace QuotientCPolynomial -lemma mul_equiv (a₁ a₂ b : CPolynomial R) : - equiv a₁ a₂ → equiv (a₁.mul b) (a₂.mul b) := by sorry - lemma mul_comm (a b : CPolynomial R) : - a.mul b ≈ b.mul a := by sorry + a.mul b = b.mul a := by + simp [mul] + -- Array.foldl_induction + -- or Trim induction: + + -- induction p using induct with + -- | case1 p h_empty h_all_zero => ... + -- | case2 p k h_extract h_nonzero h_max => ... + + -- induction p using last_nonzero_induct with + -- | case1 p h_none h_all_zero => ... + -- | case2 p k h_some h_nonzero h_max => ... + + sorry + +lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), + ∀ (q : CPolynomial R) (m l : ℕ), + l + m = n → + p.mul^[n] q = p.mul^[m] (p.mul^[l] q) := by + intro p n + induction n with + | zero => + intro q m l h_sizes + rw [Nat.add_eq_zero_iff] at h_sizes + obtain ⟨hl, hm⟩ := h_sizes + rw [hl, hm] + simp + | succ n₀ ih => + intro q m l h_sizes + cases l with + | zero => + simp at h_sizes + rw [h_sizes] + simp + | succ l₀ => + have h_sizes_simp : l₀ + m = n₀ := by linarith + clear h_sizes + simp + rw [ih (p.mul q) m l₀ h_sizes_simp] + +lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : + a.mul b ≈ a.trim.mul b := by + have h_trim := trim_equiv a + unfold equiv at h_trim + intro i + simp [mul] + sorry -lemma pow_equiv : ∀ (p : CPolynomial R) (n : ℕ), - (p.mul^[n + 1] (C 1)) ≈ (p.mul (p.mul^[n] (C 1))) := by sorry +lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : + equiv a₁ a₂ → a₁.mul b ≈ a₂.mul b := by + intro h + calc + a₁.mul b ≈ a₁.trim.mul b := mul_trim_equiv a₁ b + _ ≈ a₂.trim.mul b := by rw [eq_of_equiv h] + _ ≈ a₂.mul b := equiv_symm (mul_trim_equiv a₂ b) -- Addition: add descends to `QuotientCPolynomial` def add_descending (p q : CPolynomial R) : QuotientCPolynomial R := @@ -1122,9 +1170,9 @@ lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : simp [instSetoidCPolynomial] calc a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a - _ ≈ b₁.mul a₂ := mul_comm a₂ b₁ + _ ≈ b₁.mul a₂ := by rw [mul_comm a₂ b₁] _ ≈ b₂.mul a₂ := mul_equiv b₁ b₂ a₂ heq_b - _ ≈ a₂.mul b₂ := mul_comm b₂ a₂ + _ ≈ a₂.mul b₂ := by rw [mul_comm b₂ a₂] @[inline, specialize] def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := @@ -1134,27 +1182,32 @@ def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) def pow_descending (p : CPolynomial R) (n : ℕ) : QuotientCPolynomial R := Quotient.mk _ (pow p n) -lemma pow_descends (n : ℕ) (p₁ p₂ : CPolynomial R) : +lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : equiv p₁ p₂ → pow_descending p₁ n = pow_descending p₂ n := by intro heq unfold pow_descending rw [Quotient.eq] simp [instSetoidCPolynomial] unfold pow - -- intro i + have mul_pow_equiv : ∀ (p : CPolynomial R) (n : ℕ), + p.mul^[n + 1] (C 1) ≈ p.mul (p.mul^[n] (C 1)) := by + intro p n + rw [mul_pow_assoc p (n + 1) (C 1) 1 n] + . simp + simp induction n with | zero => simp | succ n ih => calc - p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := pow_equiv p₁ n - _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := mul_comm p₁ (p₁.mul^[n] (C 1)) + p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_equiv p₁ n + _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := by rw [mul_comm p₁ (p₁.mul^[n] (C 1))] _ ≈ (p₂.mul^[n] (C 1)).mul p₁ := mul_equiv _ _ p₁ ih - _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_comm (p₂.mul^[n] (C 1)) p₁ + _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := by rw [mul_comm (p₂.mul^[n] (C 1)) p₁] _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq - _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (pow_equiv p₂ n) + _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_equiv p₂ n) @[inline, specialize] -def pow {R : Type*} [Ring R] [BEq R] (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := +def pow {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := Quotient.lift (fun p => pow_descending p n) (pow_descends n) p -- TODO div? From cfe6f92dbd70bef05b22e6992dab2a6a06d9d16f Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 23 Dec 2025 02:42:07 -0900 Subject: [PATCH 04/11] feat: add_coeff proof and progress on mul and other equivalence lemmas --- CompPoly/.DS_Store | Bin 0 -> 6148 bytes CompPoly/Univariate/Basic.lean | 202 +++- CompPoly/Univariate/harmonic-output.lean | 1413 ++++++++++++++++++++++ 3 files changed, 1584 insertions(+), 31 deletions(-) create mode 100644 CompPoly/.DS_Store create mode 100644 CompPoly/Univariate/harmonic-output.lean diff --git a/CompPoly/.DS_Store b/CompPoly/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..8455f972ed6317f53df22d1225ba9246c4ada9d2 GIT binary patch literal 6148 zcmeHKyK2Kg5Zp~%n7C2t@_xa8a0ulKjC%(hOd!Z$V%MttUHLT6J_r$V3Kwb2EbPwR z-p&b4q1B3rwx``nq!E!h+)yqSre^2n6MM>x0^zvhO^)(`_$BX?>e~t9zQ{&;@Xo*a z=k>AwJoNjx`!<PUgD#rGhvt(tClvLk ... - -- | case2 p k h_extract h_nonzero h_max => ... - - -- induction p using last_nonzero_induct with - -- | case1 p h_none h_all_zero => ... - -- | case2 p k h_some h_nonzero h_max => ... - - sorry +section EquivalenceLemmas lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), ∀ (q : CPolynomial R) (m l : ℕ), @@ -1015,22 +997,180 @@ lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), simp rw [ih (p.mul q) m l₀ h_sizes_simp] +/- +Scalar multiplication by 0 is equivalent to the zero polynomial. +-/ +lemma smul_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : + (smul 0 p) ≈ 0 := by + -- By definition of scalar multiplication, multiplying by 0 results in the zero polynomial. + have h_smul_zero : ∀ (p : CPolynomial R), (smul 0 p).coeff = 0 := by + intro p; ext i; simp [CPolynomial.smul]; + cases p[i]? <;> simp +decide; + exact fun i => by simpa using congr_fun ( h_smul_zero p ) i; + +/- +Addition of polynomials respects equivalence. +-/ +lemma add_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (p1 p2 q1 q2 : CPolynomial R) + (hp : equiv p1 p2) (hq : equiv q1 q2) : + equiv (p1.add q1) (p2.add q2) := by + -- By `add_equiv_raw`, `add p1 q1` is equivalent to `add_raw p1 q1`, and similarly for `p2, q2`. + have h_add_equiv_raw : ∀ p q : CPolynomial R, equiv (p.add q) (p.add_raw q) := by + exact? + -- By `add_coeff?`, we have `(add_raw p1 q1).coeff i = p1.coeff i + q1.coeff i` and `(add_raw p2 q2).coeff i = p2.coeff i + q2.coeff i`. + have h_add_coeff : ∀ i, (p1.add_raw q1).coeff i = p1.coeff i + q1.coeff i ∧ (p2.add_raw q2).coeff i = p2.coeff i + q2.coeff i := by + exact fun i => ⟨ add_coeff? p1 q1 i, add_coeff? p2 q2 i ⟩ + simp_all +decide [ equiv ] + +/- +Multiplication by X^i respects equivalence. +-/ +lemma mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (i : ℕ) (p q : CPolynomial R) (h : equiv p q) : + equiv (CPolynomial.mulPowX i p) (CPolynomial.mulPowX i q) := by + unfold equiv at *; + simp +zetaDelta at *; + intro j; by_cases hj : j < i <;> simp_all +decide [ CPolynomial.mulPowX ] ; + · unfold CPolynomial.mk; rw [ Array.getElem?_append, Array.getElem?_append ] ; aesop; + · convert h ( j - i ) using 1 <;> rw [ Array.getElem?_append ] <;> simp +decide [ hj ]; + · rw [ if_neg ( not_lt_of_ge hj ) ]; + · rw [ if_neg ( not_lt_of_ge hj ) ] + +/- +Adding a polynomial equivalent to zero acts as the identity. +-/ +lemma add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (p q : CPolynomial R) (hq : equiv q 0) : + equiv (CPolynomial.add p q) p := by + intro x; + have := add_coeff? p q x; + have hq_zero : q.coeff x = 0 := by + exact hq x; + unfold CPolynomial.add; + rw [ Trim.coeff_eq_coeff ] ; aesop + +/- +Multiplying the zero polynomial by X^i results in a polynomial equivalent to zero. +-/ +lemma mulPowX_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (i : ℕ) : equiv (CPolynomial.mulPowX i (0 : CPolynomial R)) 0 := by + unfold equiv; + simp [CPolynomial.coeff]; + unfold CPolynomial.mulPowX; + grind + +/- +Definition of a single step in the polynomial multiplication algorithm. +-/ +def mul_step {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CPolynomial R) (acc : CPolynomial R) (x : R × ℕ) : CPolynomial R := + acc.add ((CPolynomial.smul x.1 q).mulPowX x.2) + +/- +The multiplication step respects equivalence of the accumulator. +-/ +lemma mul_step_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CPolynomial R) (acc1 acc2 : CPolynomial R) (x : R × ℕ) + (h : equiv acc1 acc2) : + equiv (mul_step q acc1 x) (mul_step q acc2 x) := by + apply_rules [ add_equiv, mulPowX_equiv, CPolynomial.smul_equiv ] + +/- +The multiplication step with a zero coefficient acts as the identity modulo equivalence. +-/ +lemma mul_step_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CPolynomial R) (acc : CPolynomial R) (i : ℕ) : + equiv (mul_step q acc (0, i)) acc := by + -- By definition of `mul_step`, we have `mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i)`. + have h_mul_step : mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i) := by + exact?; + -- By definition of `mulPowX`, we have `mulPowX i (smul 0 q) = smul 0 (mulPowX i q)`. + have h_mulPowX : CPolynomial.mulPowX i (CPolynomial.smul 0 q) = CPolynomial.smul 0 (CPolynomial.mulPowX i q) := by + unfold CPolynomial.mulPowX CPolynomial.smul; aesop; + rw [ h_mul_step, h_mulPowX ]; + exact add_zero_equiv _ _ ( smul_zero_equiv _ ) + +/- +Folding `mul_step` over a list of zero coefficients preserves equivalence. +-/ +lemma foldl_mul_step_zeros {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CPolynomial R) (acc : CPolynomial R) (l : List (R × ℕ)) + (hl : ∀ x ∈ l, x.1 = 0) : + equiv (l.foldl (mul_step q) acc) acc := by + induction' l using List.reverseRecOn with x xs ih generalizing acc; + · exact fun _ => rfl; + · simp_all +decide [ List.foldl_append ]; + -- By the properties of the multiplication step and the induction hypothesis, we can conclude the proof. + have h_mul_step : equiv (mul_step q (List.foldl (mul_step q) acc x) xs) (List.foldl (mul_step q) acc x) := by + convert mul_step_zero q ( List.foldl ( mul_step q ) acc x ) xs.2 using 1; + specialize hl _ _ ( Or.inr rfl ) ; aesop; + exact? + +/- +The `zipIdx` of a polynomial is the `zipIdx` of its trim followed by a list of zero coefficients. +-/ +lemma zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (p : CPolynomial R) : + ∃ l, p.zipIdx.toList = p.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by + -- Let `n` be `p.trim.size`. `p.trim` is the prefix of `p` of length `n`. + set n := p.trim.size with hn_def; + by_cases hn : n = 0; + · unfold n at hn; + -- Since `p.trim` is empty, `p` must be the zero polynomial. + have hp_zero : ∀ i (hi : i < p.size), p[i] = 0 := by + have := Trim.elim p; aesop; + use List.map (fun i => (0, i)) (List.range p.size); + simp +decide [ hp_zero ]; + refine' List.ext_get _ _ <;> aesop; + · -- Since `n` is not zero, `p.last_nonzero` is `some k` and `n = k + 1`. + obtain ⟨k, hk⟩ : ∃ k : Fin p.size, p.trim = p.extract 0 (k.val + 1) ∧ p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by + have := Trim.elim p; + aesop; + refine' ⟨ _, _, _ ⟩; + exact ( Array.zipIdx p ).toList.drop ( k + 1 ); + · rw [ hk.1 ]; + refine' List.ext_get _ _ <;> simp +decide [ List.get ]; + · rw [ min_eq_left ( by linarith [ Fin.is_lt k ] ), add_tsub_cancel_of_le ( by linarith [ Fin.is_lt k ] ) ]; + · intro n h₁ h₂; rw [ List.getElem_append ] ; simp +decide [ h₁, h₂ ] ; + grind; + · simp +decide [ List.mem_iff_get ]; + intro a; specialize hk; have := hk.2.2 ( k + 1 + a ) ; simp_all +decide [ Nat.add_assoc ] ; + lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : a.mul b ≈ a.trim.mul b := by - have h_trim := trim_equiv a - unfold equiv at h_trim - intro i - simp [mul] - sorry + have h_zipIdx_split : ∃ l, a.zipIdx.toList = a.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by + exact?; + obtain ⟨l, hl⟩ := h_zipIdx_split; + have h_foldl_split : ∃ acc, (a.mul b) = (l.foldl (mul_step b) acc) ∧ (a.trim.mul b) = acc := by + -- By definition of `mul`, we can rewrite `a.mul b` using `mul_step` and the foldl operation. + have h_mul_def : a.mul b = (a.zipIdx.toList.foldl (mul_step b) (CPolynomial.C 0)) := by + unfold CPolynomial.mul; + exact?; + have h_mul_def_trim : a.trim.mul b = (a.trim.zipIdx.toList.foldl (mul_step b) (CPolynomial.C 0)) := by + unfold CPolynomial.mul; + exact?; + aesop; + obtain ⟨ acc, h₁, h₂ ⟩ := h_foldl_split; + exact h₁.symm ▸ h₂.symm ▸ foldl_mul_step_zeros b acc l hl.2 lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : - equiv a₁ a₂ → a₁.mul b ≈ a₂.mul b := by + a₁ ≈ a₂ → a₁.mul b ≈ a₂.mul b := by intro h calc a₁.mul b ≈ a₁.trim.mul b := mul_trim_equiv a₁ b _ ≈ a₂.trim.mul b := by rw [eq_of_equiv h] _ ≈ a₂.mul b := equiv_symm (mul_trim_equiv a₂ b) +-- TODO? +-- lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial R) : +-- b₁ ≈ b₂ → a.mul b₁ ≈ a.mul b₂ + +lemma mul_comm_equiv [LawfulBEq R] (a b : CPolynomial R) : + a.mul b ≈ b.mul a := by sorry + +end EquivalenceLemmas + -- Addition: add descends to `QuotientCPolynomial` def add_descending (p q : CPolynomial R) : QuotientCPolynomial R := Quotient.mk _ (add p q) @@ -1170,9 +1310,9 @@ lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : simp [instSetoidCPolynomial] calc a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a - _ ≈ b₁.mul a₂ := by rw [mul_comm a₂ b₁] + _ ≈ b₁.mul a₂ := mul_comm_equiv a₂ b₁ _ ≈ b₂.mul a₂ := mul_equiv b₁ b₂ a₂ heq_b - _ ≈ a₂.mul b₂ := by rw [mul_comm b₂ a₂] + _ ≈ a₂.mul b₂ := mul_comm_equiv b₂ a₂ @[inline, specialize] def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := @@ -1200,9 +1340,9 @@ lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : | succ n ih => calc p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_equiv p₁ n - _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := by rw [mul_comm p₁ (p₁.mul^[n] (C 1))] + _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := mul_comm_equiv p₁ (p₁.mul^[n] (C 1)) _ ≈ (p₂.mul^[n] (C 1)).mul p₁ := mul_equiv _ _ p₁ ih - _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := by rw [mul_comm (p₂.mul^[n] (C 1)) p₁] + _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_comm_equiv (p₂.mul^[n] (C 1)) p₁ _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_equiv p₂ n) diff --git a/CompPoly/Univariate/harmonic-output.lean b/CompPoly/Univariate/harmonic-output.lean new file mode 100644 index 0000000..2fc8d8e --- /dev/null +++ b/CompPoly/Univariate/harmonic-output.lean @@ -0,0 +1,1413 @@ +/- +This file was edited by Aristotle. + +Lean version: leanprover/lean4:v4.24.0 +Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 +This project request had uuid: 95f785fa-5bb7-4083-9638-ce14b5377f15 + +The following was proved by Aristotle: + +- theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : + (add_raw p q)[i] = p.coeff i + q.coeff i + +- lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : + a.mul b ≈ a.trim.mul b +-/ + +/- +Copyright (c) 2025 CompPoly. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen +-/ + +import Mathlib.Algebra.Tropical.Basic +import Mathlib.RingTheory.Polynomial.Basic +import CompPoly.Data.Array.Lemmas + + +/-! + # Computable Univariate Polynomials + + This file contains a computable datatype for univariate polynomial, `CPolynomial R`. This is + internally represented as an array of coefficients. + + Note: this has been ported from ArkLib +-/ + +open Polynomial + +namespace CompPoly + +/-- A type analogous to `Polynomial` that supports computable operations. This defined to be a + wrapper around `Array`. + +For example the Array `#[1,2,3]` represents the polynomial `1 + 2x + 3x^2`. Two arrays may represent +the same polynomial via zero-padding, for example `#[1,2,3] = #[1,2,3,0,0,0,...]`. +-/ +@[reducible, inline, specialize] +def CPolynomial (R : Type*) := Array R + +end CompPoly + +/-- Convert a `Polynomial` to a `CPolynomial`. -/ +def Polynomial.toImpl {R : Type*} [Semiring R] (p : R[X]) : CompPoly.CPolynomial R := + match p.degree with + | ⊥ => #[] + | some d => .ofFn (fun i : Fin (d + 1) => p.coeff i) + +namespace CompPoly + +namespace CPolynomial + +@[reducible] +def mk {R : Type*} (coeffs : Array R) : CPolynomial R := coeffs + +@[reducible] +def coeffs {R : Type*} (p : CPolynomial R) : Array R := p + +variable {R : Type*} [Ring R] [BEq R] + +variable {Q : Type*} [Ring Q] + +@[reducible] +def coeff (p : CPolynomial Q) (i : ℕ) : Q := p.getD i 0 + +/-- The constant polynomial `C r`. -/ +def C (r : R) : CPolynomial R := #[r] + +/-- The variable `X`. -/ +def X : CPolynomial R := #[0, 1] + +/-- Return the index of the last non-zero coefficient of a `CPolynomial` -/ +def last_nonzero (p : CPolynomial R) : Option (Fin p.size) := + p.findIdxRev? (· != 0) + +/-- Remove leading zeroes from a `CPolynomial`. Requires `BEq` to check if the coefficients are zero. -/ +def trim (p : CPolynomial R) : CPolynomial R := + match p.last_nonzero with + | none => #[] + | some i => p.extract 0 (i.val + 1) + +/-- Return the degree of a `CPolynomial`. -/ +def degree (p : CPolynomial R) : Nat := + match p.last_nonzero with + | none => 0 + | some i => i.val + 1 + +/-- Return the leading coefficient of a `CPolynomial` as the last coefficient of the trimmed array, +or `0` if the trimmed array is empty. -/ +def leadingCoeff (p : CPolynomial R) : R := p.trim.getLastD 0 + +namespace Trim + +-- characterize .last_nonzero +theorem last_nonzero_none [LawfulBEq R] {p : CPolynomial R} : + (∀ i, (hi : i < p.size) → p[i] = 0) → p.last_nonzero = none +:= by + intro h + apply Array.findIdxRev?_eq_none + intros + rw [bne_iff_ne, ne_eq, not_not] + apply_assumption + +theorem last_nonzero_some [LawfulBEq R] {p : CPolynomial R} {i} (hi : i < p.size) (h : p[i] ≠ 0) : + ∃ k, p.last_nonzero = some k +:= Array.findIdxRev?_eq_some ⟨i, hi, bne_iff_ne.mpr h⟩ + +theorem last_nonzero_spec [LawfulBEq R] {p : CPolynomial R} {k} : + p.last_nonzero = some k + → p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) +:= by + intro (h : p.last_nonzero = some k) + constructor + · by_contra + have h : p[k] != 0 := Array.findIdxRev?_def h + rwa [‹p[k] = 0›, bne_self_eq_false, Bool.false_eq_true] at h + · intro j hj j_gt_k + have h : ¬(p[j] != 0) := Array.findIdxRev?_maximal h ⟨ j, hj ⟩ j_gt_k + rwa [bne_iff_ne, ne_eq, not_not] at h + +-- the property of `last_nonzero_spec` uniquely identifies an element, +-- and that allows us to prove the reverse as well +def last_nonzero_prop {p : CPolynomial R} (k : Fin p.size) : Prop := + p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) + +lemma last_nonzero_unique {p : CPolynomial Q} {k k' : Fin p.size} : + last_nonzero_prop k → last_nonzero_prop k' → k = k' +:= by + suffices weaker : ∀ k k', last_nonzero_prop k → last_nonzero_prop k' → k ≤ k' by + intro h h' + exact Fin.le_antisymm (weaker k k' h h') (weaker k' k h' h) + intro k k' ⟨ h_nonzero, h ⟩ ⟨ h_nonzero', h' ⟩ + by_contra k_not_le + have : p[k] = 0 := h' k k.is_lt (Nat.lt_of_not_ge k_not_le) + contradiction + +theorem last_nonzero_some_iff [LawfulBEq R] {p : CPolynomial R} {k} : + p.last_nonzero = some k ↔ (p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0)) +:= by + constructor + · apply last_nonzero_spec + intro h_prop + have ⟨ k', h_some'⟩ := last_nonzero_some k.is_lt h_prop.left + have k_is_k' := last_nonzero_unique (last_nonzero_spec h_some') h_prop + rwa [← k_is_k'] + +/-- eliminator for `p.last_nonzero`, e.g. use with the induction tactic as follows: + ``` + induction p using last_nonzero_induct with + | case1 p h_none h_all_zero => ... + | case2 p k h_some h_nonzero h_max => ... + ``` +-/ +theorem last_nonzero_induct [LawfulBEq R] {motive : CPolynomial R → Prop} + (case1 : ∀ p, p.last_nonzero = none → (∀ i, (hi : i < p.size) → p[i] = 0) → motive p) + (case2 : ∀ p : CPolynomial R, ∀ k : Fin p.size, p.last_nonzero = some k → p[k] ≠ 0 → + (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0) → motive p) + (p : CPolynomial R) : motive p +:= by + by_cases h : ∀ i, (hi : i < p.size) → p[i] = 0 + · exact case1 p (last_nonzero_none h) h + · push_neg at h; rcases h with ⟨ i, hi, h ⟩ + obtain ⟨ k, h_some ⟩ := last_nonzero_some hi h + have ⟨ h_nonzero, h_max ⟩ := last_nonzero_spec h_some + exact case2 p k h_some h_nonzero h_max + +/-- eliminator for `p.trim`; use with the induction tactic as follows: + ``` + induction p using induct with + | case1 p h_empty h_all_zero => ... + | case2 p k h_extract h_nonzero h_max => ... + ``` +-/ +theorem induct [LawfulBEq R] {motive : CPolynomial R → Prop} + (case1 : ∀ p, p.trim = #[] → (∀ i, (hi : i < p.size) → p[i] = 0) → motive p) + (case2 : ∀ p : CPolynomial R, ∀ k : Fin p.size, p.trim = p.extract 0 (k + 1) + → p[k] ≠ 0 → (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0) → motive p) + (p : CPolynomial R) : motive p +:= by induction p using last_nonzero_induct with + | case1 p h_none h_all_zero => + have h_empty : p.trim = #[] := by unfold trim; rw [h_none] + exact case1 p h_empty h_all_zero + | case2 p k h_some h_nonzero h_max => + have h_extract : p.trim = p.extract 0 (k + 1) := by unfold trim; rw [h_some] + exact case2 p k h_extract h_nonzero h_max + +/-- eliminator for `p.trim`; e.g. use for case distinction as follows: + ``` + rcases (Trim.elim p) with ⟨ h_empty, h_all_zero ⟩ | ⟨ k, h_extract, h_nonzero, h_max ⟩ + ``` +-/ +theorem elim [LawfulBEq R] (p : CPolynomial R) : + (p.trim = #[] ∧ (∀ i, (hi : i < p.size) → p[i] = 0)) + ∨ (∃ k : Fin p.size, + p.trim = p.extract 0 (k + 1) + ∧ p[k] ≠ 0 + ∧ (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0)) +:= by induction p using induct with + | case1 p h_empty h_all_zero => left; exact ⟨h_empty, h_all_zero⟩ + | case2 p k h_extract h_nonzero h_max => right; exact ⟨k, h_extract, h_nonzero, h_max⟩ + +theorem size_eq_degree (p : CPolynomial R) : p.trim.size = p.degree := by + unfold trim degree + match h : p.last_nonzero with + | none => simp + | some i => simp [Fin.is_lt, Nat.succ_le_of_lt] + +theorem size_le_size (p : CPolynomial R) : p.trim.size ≤ p.size := by + unfold trim + match h : p.last_nonzero with + | none => simp + | some i => simp [Array.size_extract] + +attribute [simp] Array.getElem?_eq_none + +theorem coeff_eq_getElem_of_lt [LawfulBEq R] {p : CPolynomial R} {i} (hi : i < p.size) : + p.trim.coeff i = p[i] := by + induction p using induct with + | case1 p h_empty h_all_zero => + specialize h_all_zero i hi + simp [h_empty, h_all_zero] + | case2 p k h_extract h_nonzero h_max => + simp [h_extract] + -- split between i > k and i <= k + have h_size : k + 1 = (p.extract 0 (k + 1)).size := by + simp [Array.size_extract] + exact Nat.succ_le_of_lt k.is_lt + rcases (Nat.lt_or_ge k i) with hik | hik + · have hik' : i ≥ (p.extract 0 (k + 1)).size := by linarith + rw [Array.getElem?_eq_none hik', Option.getD_none] + exact h_max i hi hik |> Eq.symm + · have hik' : i < (p.extract 0 (k + 1)).size := by linarith + rw [Array.getElem?_eq_getElem hik', Option.getD_some, Array.getElem_extract] + simp only [zero_add] + +theorem coeff_eq_coeff [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : + p.trim.coeff i = p.coeff i := by + rcases (Nat.lt_or_ge i p.size) with hi | hi + · rw [coeff_eq_getElem_of_lt hi] + simp [hi] + · have hi' : i ≥ p.trim.size := by linarith [size_le_size p] + simp [hi, hi'] + +lemma coeff_eq_getElem {p : CPolynomial Q} {i} (hp : i < p.size) : + p.coeff i = p[i] := by + simp [hp] + +/-- Two polynomials are equivalent if they have the same `Nat` coefficients. -/ +def equiv (p q : CPolynomial R) : Prop := + ∀ i, p.coeff i = q.coeff i + +lemma coeff_eq_zero {p : CPolynomial Q} : + (∀ i, (hi : i < p.size) → p[i] = 0) ↔ ∀ i, p.coeff i = 0 +:= by + constructor <;> intro h i + · cases Nat.lt_or_ge i p.size <;> simp [*] + · intro hi; specialize h i; simp [hi] at h; assumption + +lemma eq_degree_of_equiv [LawfulBEq R] {p q : CPolynomial R} : equiv p q → p.degree = q.degree := by + unfold equiv degree + intro h_equiv + induction p using last_nonzero_induct with + | case1 p h_none_p h_all_zero => + have h_zero_p : ∀ i, p.coeff i = 0 := coeff_eq_zero.mp h_all_zero + have h_zero_q : ∀ i, q.coeff i = 0 := by intro i; rw [← h_equiv, h_zero_p] + have h_none_q : q.last_nonzero = none := last_nonzero_none (coeff_eq_zero.mpr h_zero_q) + rw [h_none_p, h_none_q] + | case2 p k h_some_p h_nonzero_p h_max_p => + have h_equiv_k := h_equiv k + have k_lt_q : k < q.size := by + by_contra h_not_lt + have h_ge := Nat.le_of_not_lt h_not_lt + simp [h_ge] at h_equiv_k + contradiction + simp [k_lt_q] at h_equiv_k + have h_nonzero_q : q[k.val] ≠ 0 := by rwa [← h_equiv_k] + have h_max_q : ∀ j, (hj : j < q.size) → j > k → q[j] = 0 := by + intro j hj j_gt_k + have h_eq := h_equiv j + simp [hj] at h_eq + rw [← h_eq] + rcases Nat.lt_or_ge j p.size with hj | hj + · simp [hj, h_max_p j hj j_gt_k] + · simp [hj] + have h_some_q : q.last_nonzero = some ⟨ k, k_lt_q ⟩ := + last_nonzero_some_iff.mpr ⟨ h_nonzero_q, h_max_q ⟩ + rw [h_some_p, h_some_q] + +theorem eq_of_equiv [LawfulBEq R] {p q : CPolynomial R} : equiv p q → p.trim = q.trim := by + unfold equiv + intro h + ext + · rw [size_eq_degree, size_eq_degree] + apply eq_degree_of_equiv h + rw [← coeff_eq_getElem, ← coeff_eq_getElem] + rw [coeff_eq_coeff, coeff_eq_coeff, h _] + +theorem trim_equiv [LawfulBEq R] (p : CPolynomial R) : equiv p.trim p := by + apply coeff_eq_coeff + +theorem trim_twice [LawfulBEq R] (p : CPolynomial R) : p.trim.trim = p.trim := by + apply eq_of_equiv + apply trim_equiv + +theorem canonical_empty : (CPolynomial.mk (R:=R) #[]).trim = #[] := by + have : (CPolynomial.mk (R:=R) #[]).last_nonzero = none := by + simp [last_nonzero]; + apply Array.findIdxRev?_emtpy_none + rfl + rw [trim, this] + +theorem canonical_of_size_zero {p : CPolynomial R} : p.size = 0 → p.trim = p := by + intro h + suffices h_empty : p = #[] by rw [h_empty]; exact canonical_empty + exact Array.eq_empty_of_size_eq_zero h + +theorem canonical_nonempty_iff [LawfulBEq R] {p : CPolynomial R} (hp : p.size > 0) : + p.trim = p ↔ p.last_nonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩ +:= by + unfold trim + induction p using last_nonzero_induct with + | case1 p h_none h_all_zero => + simp [h_none] + by_contra h_empty + subst h_empty + contradiction + | case2 p k h_some h_nonzero h_max => + simp [h_some] + constructor + · intro h + ext + have : p ≠ #[] := Array.ne_empty_of_size_pos hp + simp [this] at h + have : k + 1 ≤ p.size := Nat.succ_le_of_lt k.is_lt + have : p.size = k + 1 := Nat.le_antisymm h this + simp [this] + · intro h + have : k + 1 = p.size := by rw [h]; exact Nat.succ_pred_eq_of_pos hp + rw [this] + right + exact le_refl _ + +theorem last_nonzero_last_iff [LawfulBEq R] {p : CPolynomial R} (hp : p.size > 0) : + p.last_nonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩ ↔ p.getLast hp ≠ 0 +:= by + induction p using last_nonzero_induct with + | case1 => simp [Array.getLast, *] + | case2 p k h_some h_nonzero h_max => + simp only [h_some, Option.some_inj, Array.getLast] + constructor + · intro h + have : k = p.size - 1 := by rw [h] + conv => lhs; congr; case i => rw [← this] + assumption + · intro h + rcases Nat.lt_trichotomy k (p.size - 1) with h_lt | h_eq | h_gt + · specialize h_max (p.size - 1) (Nat.pred_lt_self hp) h_lt + contradiction + · ext; assumption + · have : k < p.size := k.is_lt + have : k ≥ p.size := Nat.le_of_pred_lt h_gt + linarith + +theorem canonical_iff [LawfulBEq R] {p : CPolynomial R} : + p.trim = p ↔ ∀ hp : p.size > 0, p.getLast hp ≠ 0 +:= by + constructor + · intro h hp + rwa [← last_nonzero_last_iff hp, ← canonical_nonempty_iff hp] + · rintro h + rcases Nat.eq_zero_or_pos p.size with h_zero | hp + · exact canonical_of_size_zero h_zero + · rw [canonical_nonempty_iff hp, last_nonzero_last_iff hp] + exact h hp + +theorem non_zero_map [LawfulBEq R] (f : R → R) (hf : ∀ r, f r = 0 → r = 0) (p : CPolynomial R) : + let fp := CPolynomial.mk (p.map f); + p.trim = p → fp.trim = fp +:= by + intro fp p_canon + by_cases hp : p.size > 0 + -- positive case + · apply canonical_iff.mpr + intro hfp + have h_nonzero := canonical_iff.mp p_canon hp + have : fp.getLast hfp = f (p.getLast hp) := by simp [Array.getLast, fp] + rw [this] + by_contra h_zero + specialize hf (p.getLast hp) h_zero + contradiction + -- zero case + have : p.size = 0 := by linarith + have : fp.size = 0 := by simp [this, fp] + apply canonical_of_size_zero this + +/-- Canonical polynomials enjoy a stronger extensionality theorem: + they just need to agree at all coefficients (without assuming equal sizes) +-/ +theorem canonical_ext [LawfulBEq R] {p q : CPolynomial R} (hp : p.trim = p) (hq : q.trim = q) : + equiv p q → p = q := by + intro h_equiv + rw [← hp, ← hq] + exact eq_of_equiv h_equiv + +end Trim + +/-- canonical version of CPolynomial + +TODO: make THIS the `CPolynomial, rename current `CPolynomial` to `CPolynomial.Raw` or something -/ +def CPolynomialC (R : Type*) [BEq R] [Ring R] := { p : CPolynomial R // p.trim = p } + +@[ext] theorem CPolynomialC.ext {p q : CPolynomialC R} (h : p.val = q.val) : p = q := Subtype.eq h + +instance : Coe (CPolynomialC R) (CPolynomial R) where coe := Subtype.val + +instance : Inhabited (CPolynomialC R) := ⟨#[], Trim.canonical_empty⟩ + +section Operations + +variable {S : Type*} + +-- p(x) = a_0 + a_1 x + a_2 x^2 + ... + a_n x^n + +-- eval₂ f x p = f(a_0) + f(a_1) x + f(a_2) x^2 + ... + f(a_n) x^n + +/-- Evaluates a `CPolynomial` at a given value, using a ring homomorphism `f: R →+* S`. +TODO: define an efficient version of this with caching -/ +def eval₂ [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : S := + p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 + +/-- Evaluates a `CPolynomial` at a given value -/ +@[inline, specialize] +def eval (x : R) (p : CPolynomial R) : R := + p.eval₂ (RingHom.id R) x + +/-- Addition of two `CPolynomial`s. Defined as the pointwise sum of the underlying coefficient arrays + (properly padded with zeroes). -/ +@[inline, specialize] +def add_raw (p q : CPolynomial R) : CPolynomial R := + let ⟨p', q'⟩ := Array.matchSize p q 0 + .mk (Array.zipWith (· + ·) p' q' ) + +/-- Addition of two `CPolynomial`s, with result trimmed. -/ +@[inline, specialize] +def add (p q : CPolynomial R) : CPolynomial R := + add_raw p q |> trim + +/-- Scalar multiplication of `CPolynomial` by an element of `R`. -/ +@[inline, specialize] +def smul (r : R) (p : CPolynomial R) : CPolynomial R := + .mk (Array.map (fun a => r * a) p) + +/-- Scalar multiplication of `CPolynomial` by a natural number. -/ +@[inline, specialize] +def nsmul_raw (n : ℕ) (p : CPolynomial R) : CPolynomial R := + .mk (Array.map (fun a => n * a) p) + +/-- Scalar multiplication of `CPolynomial` by a natural number, with result trimmed. -/ +@[inline, specialize] +def nsmul (n : ℕ) (p : CPolynomial R) : CPolynomial R := + nsmul_raw n p |> trim + +/-- Negation of a `CPolynomial`. -/ +@[inline, specialize] +def neg (p : CPolynomial R) : CPolynomial R := p.map (fun a => -a) + +/-- Subtraction of two `CPolynomial`s. -/ +@[inline, specialize] +def sub (p q : CPolynomial R) : CPolynomial R := p.add q.neg + +/-- Multiplication of a `CPolynomial` by `X ^ i`, i.e. pre-pending `i` zeroes to the +underlying array of coefficients. -/ +@[inline, specialize] +def mulPowX (i : Nat) (p : CPolynomial R) : CPolynomial R := .mk (Array.replicate i 0 ++ p) + +/-- Multiplication of a `CPolynomial` by `X`, reduces to `mulPowX 1`. -/ +@[inline, specialize] +def mulX (p : CPolynomial R) : CPolynomial R := p.mulPowX 1 + +/-- Multiplication of two `CPolynomial`s, using the naive `O(n^2)` algorithm. -/ +@[inline, specialize] +def mul (p q : CPolynomial R) : CPolynomial R := + p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc.add <| (smul a q).mulPowX i) (C 0) + +/-- Exponentiation of a `CPolynomial` by a natural number `n` via repeated multiplication. -/ +@[inline, specialize] +def pow (p : CPolynomial R) (n : Nat) : CPolynomial R := (mul p)^[n] (C 1) + +-- TODO: define repeated squaring version of `pow` + +instance : Zero (CPolynomial R) := ⟨#[]⟩ + +instance : One (CPolynomial R) := ⟨CPolynomial.C 1⟩ + +instance : Add (CPolynomial R) := ⟨CPolynomial.add⟩ + +instance : SMul R (CPolynomial R) := ⟨CPolynomial.smul⟩ + +instance : SMul ℕ (CPolynomial R) := ⟨nsmul⟩ + +instance : Neg (CPolynomial R) := ⟨CPolynomial.neg⟩ + +instance : Sub (CPolynomial R) := ⟨CPolynomial.sub⟩ + +instance : Mul (CPolynomial R) := ⟨CPolynomial.mul⟩ + +instance : Pow (CPolynomial R) Nat := ⟨CPolynomial.pow⟩ + +instance : NatCast (CPolynomial R) := ⟨fun n => CPolynomial.C (n : R)⟩ + +instance : IntCast (CPolynomial R) := ⟨fun n => CPolynomial.C (n : R)⟩ + +/-- Return a bound on the degree of a `CPolynomial` as the size of the underlying array +(and `⊥` if the array is empty). -/ +def degreeBound (p : CPolynomial R) : WithBot Nat := + match p.size with + | 0 => ⊥ + | .succ n => n + +/-- Convert `degreeBound` to a natural number by sending `⊥` to `0`. -/ +def natDegreeBound (p : CPolynomial R) : Nat := + (degreeBound p).getD 0 + +/-- Check if a `CPolynomial` is monic, i.e. its leading coefficient is 1. -/ +def monic (p : CPolynomial R) : Bool := p.leadingCoeff == 1 + +/-- Division and modulus of `p : CPolynomial R` by a monic `q : CPolynomial R`. -/ +def divModByMonicAux [Field R] (p : CPolynomial R) (q : CPolynomial R) : + CPolynomial R × CPolynomial R := + go (p.size - q.size) p q +where + go : Nat → CPolynomial R → CPolynomial R → CPolynomial R × CPolynomial R + | 0, p, _ => ⟨0, p⟩ + | n+1, p, q => + let k := p.size - q.size -- k should equal n, this is technically unneeded + let q' := C p.leadingCoeff * (q * X.pow k) + let p' := (p - q').trim + let (e, f) := go n p' q + -- p' = q * e + f + -- Thus p = p' + q' = q * e + f + p.leadingCoeff * q * X^n + -- = q * (e + p.leadingCoeff * X^n) + f + ⟨e + C p.leadingCoeff * X^k, f⟩ + +/-- Division of `p : CPolynomial R` by a monic `q : CPolynomial R`. -/ +def divByMonic [Field R] (p : CPolynomial R) (q : CPolynomial R) : + CPolynomial R := + (divModByMonicAux p q).1 + +/-- Modulus of `p : CPolynomial R` by a monic `q : CPolynomial R`. -/ +def modByMonic [Field R] (p : CPolynomial R) (q : CPolynomial R) : + CPolynomial R := + (divModByMonicAux p q).2 + +/-- Division of two `CPolynomial`s. -/ +def div [Field R] (p q : CPolynomial R) : CPolynomial R := + (C (q.leadingCoeff)⁻¹ • p).divByMonic (C (q.leadingCoeff)⁻¹ * q) + +/-- Modulus of two `CPolynomial`s. -/ +def mod [Field R] (p q : CPolynomial R) : CPolynomial R := + (C (q.leadingCoeff)⁻¹ • p).modByMonic (C (q.leadingCoeff)⁻¹ * q) + +instance [Field R] : Div (CPolynomial R) := ⟨CPolynomial.div⟩ + +instance [Field R] : Mod (CPolynomial R) := ⟨CPolynomial.mod⟩ + +/-- Pseudo-division of a `CPolynomial` by `X`, which shifts all non-constant coefficients +to the left by one. -/ +def divX (p : CPolynomial R) : CPolynomial R := p.extract 1 p.size + +variable (p q r : CPolynomial R) + +-- some helper lemmas to characterize p + q + +lemma matchSize_size_eq {p q : CPolynomial Q} : + let (p', q') := Array.matchSize p q 0 + p'.size = q'.size := by + change (Array.rightpad _ _ _).size = (Array.rightpad _ _ _).size + rw [Array.size_rightpad, Array.size_rightpad] + omega + +lemma matchSize_size {p q : CPolynomial Q} : + let (p', _) := Array.matchSize p q 0 + p'.size = max p.size q.size := by + change (Array.rightpad _ _ _).size = max (Array.size _) (Array.size _) + rw [Array.size_rightpad] + omega + +lemma zipWith_size {R} {f : R → R → R} {a b : Array R} (h : a.size = b.size) : + (Array.zipWith f a b).size = a.size := by + simp; omega + +-- TODO we could generalize the next few lemmas to matchSize + zipWith f for any f + +theorem add_size {p q : CPolynomial Q} : (add_raw p q).size = max p.size q.size := by + change (Array.zipWith _ _ _ ).size = max p.size q.size + rw [zipWith_size matchSize_size_eq, matchSize_size] + +-- coeff on list concatenations +lemma concat_coeff₁ (i : ℕ) : i < p.size → + (p ++ q).coeff i = p.coeff i := by + simp + grind + +lemma concat_coeff₂ (i : ℕ) : i ≥ p.size → + (p ++ q).coeff i = q.coeff (i - p.size) := by + simp + grind + +theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : + (add_raw p q)[i] = p.coeff i + q.coeff i +:= by + simp [add_raw] + sorry + +-- unfold List.matchSize + -- repeat rw [List.rightpad_getElem_eq_getD] + -- simp only [List.getD_eq_getElem?_getD, Array.getElem?_eq_toList] + +theorem add_coeff? (p q : CPolynomial Q) (i : ℕ) : + (add_raw p q).coeff i = p.coeff i + q.coeff i +:= by + rcases (Nat.lt_or_ge i (add_raw p q).size) with h_lt | h_ge + · rw [← add_coeff h_lt]; simp [h_lt] + have h_lt' : i ≥ max p.size q.size := by rwa [← add_size] + have h_p : i ≥ p.size := by omega + have h_q : i ≥ q.size := by omega + simp [h_ge, h_p, h_q] + +lemma add_equiv_raw [LawfulBEq R] (p q : CPolynomial R) : Trim.equiv (p.add q) (p.add_raw q) := by + unfold Trim.equiv add + exact Trim.coeff_eq_coeff (p.add_raw q) + +def smul_equiv : ∀ (i : ℕ) (r : R), + (smul r p).coeff i = r * (p.coeff i) := by + intro i r + unfold smul mk coeff + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] + +def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), + (nsmul_raw n p).trim.coeff i = n * p.trim.coeff i := by + intro n i + unfold nsmul_raw + repeat rw [Trim.coeff_eq_coeff] + unfold mk + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] + +lemma mulPowX_equiv₁ : ∀ (i j : ℕ), j ≥ i → + (mulPowX i p).coeff j = p.coeff (j - i) := by + intro i j h + unfold mulPowX mk + rw [concat_coeff₂ (Array.replicate i 0) p j] + . simp + have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp + rw [← h_size i] + simp + exact h + +lemma mulPowX_equiv₂ : ∀ (i j : ℕ), j < i → + (mulPowX i p).coeff j = 0 := by + intro i j h + unfold mulPowX mk + rw [concat_coeff₁ (Array.replicate i 0) p j] + . simp + grind + have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp + rw [← h_size i] + simp + exact h + +omit [BEq R] in +lemma neg_coeff : ∀ (p : CPolynomial R) (i : ℕ), p.neg.coeff i = - p.coeff i := by + intro p i + unfold neg coeff + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] + +lemma trim_add_trim [LawfulBEq R] (p q : CPolynomial R) : p.trim + q = p + q := by + apply Trim.eq_of_equiv + intro i + rw [add_coeff?, add_coeff?, Trim.coeff_eq_coeff] + +-- algebra theorems about addition + +omit [Ring Q] in +@[simp] theorem zero_def : (0 : CPolynomial Q) = #[] := rfl + +theorem add_comm : p + q = q + p := by + apply congrArg trim + ext + · simp only [add_size]; omega + · simp only [add_coeff] + apply _root_.add_comm + +def canonical (p : CPolynomial R) := p.trim = p + +theorem zero_canonical : (0 : CPolynomial R).trim = 0 := Trim.canonical_empty + +theorem zero_add (hp : p.canonical) : 0 + p = p := by + rw (occs := .pos [2]) [← hp] + apply congrArg trim + ext <;> simp [add_size, add_coeff, *] + +theorem add_zero (hp : p.canonical) : p + 0 = p := by + rw [add_comm, zero_add p hp] + +theorem add_assoc [LawfulBEq R] : p + q + r = p + (q + r) := by + change (add_raw p q).trim + r = p + (add_raw q r).trim + rw [trim_add_trim, add_comm p, trim_add_trim, add_comm _ p] + apply congrArg trim + ext i + · simp only [add_size]; omega + · simp only [add_coeff, add_coeff?] + apply _root_.add_assoc + +theorem nsmul_zero [LawfulBEq R] (p : CPolynomial R) : nsmul 0 p = 0 := by + suffices (nsmul_raw 0 p).last_nonzero = none by simp [nsmul, trim, *] + apply Trim.last_nonzero_none + intros; unfold nsmul_raw + simp only [Nat.cast_zero, zero_mul, Array.getElem_map] + +theorem nsmul_raw_succ (n : ℕ) (p : CPolynomial Q) : + nsmul_raw (n + 1) p = add_raw (nsmul_raw n p) p := by + unfold nsmul_raw + ext + · simp [add_size] + next i _ hi => + simp [add_size] at hi + simp [add_coeff, hi] + rw [_root_.add_mul (R:=Q) n 1 p[i], one_mul] + +theorem nsmul_succ [LawfulBEq R] (n : ℕ) {p : CPolynomial R} : nsmul (n + 1) p = nsmul n p + p := by + unfold nsmul + rw [trim_add_trim] + apply congrArg trim + apply nsmul_raw_succ + +theorem neg_trim [LawfulBEq R] (p : CPolynomial R) : p.trim = p → (-p).trim = -p := by + apply Trim.non_zero_map + simp + +theorem neg_add_cancel [LawfulBEq R] (p : CPolynomial R) : -p + p = 0 := by + rw [← zero_canonical] + apply Trim.eq_of_equiv; unfold Trim.equiv; intro i + rw [add_coeff?] + rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi, Neg.neg, neg] + +end Operations + +namespace OperationsC + +-- additive group on CPolynomialC +variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + +variable (p q r : CPolynomialC R) + +instance : Add (CPolynomialC R) where + add p q := ⟨p.val + q.val, by apply Trim.trim_twice⟩ + +theorem add_comm : p + q = q + p := by + apply CPolynomialC.ext; apply CPolynomial.add_comm + +theorem add_assoc : p + q + r = p + (q + r) := by + apply CPolynomialC.ext; apply CPolynomial.add_assoc + +instance : Zero (CPolynomialC R) := ⟨0, zero_canonical⟩ + +theorem zero_add : 0 + p = p := by + apply CPolynomialC.ext + apply CPolynomial.zero_add p.val p.prop + +theorem add_zero : p + 0 = p := by + apply CPolynomialC.ext + apply CPolynomial.add_zero p.val p.prop + +def nsmul (n : ℕ) (p : CPolynomialC R) : CPolynomialC R := + ⟨CPolynomial.nsmul n p.val, by apply Trim.trim_twice⟩ + +theorem nsmul_zero : nsmul 0 p = 0 := by + apply CPolynomialC.ext; apply CPolynomial.nsmul_zero + +theorem nsmul_succ (n : ℕ) (p : CPolynomialC R) : nsmul (n + 1) p = nsmul n p + p := by + apply CPolynomialC.ext; apply CPolynomial.nsmul_succ + +instance : Neg (CPolynomialC R) where + neg p := ⟨-p.val, neg_trim p.val p.prop⟩ + +instance : Sub (CPolynomialC R) where + sub p q := p + -q + +theorem neg_add_cancel : -p + p = 0 := by + apply CPolynomialC.ext + apply CPolynomial.neg_add_cancel + +instance [LawfulBEq R] : AddCommGroup (CPolynomialC R) where + add_assoc := add_assoc + zero_add := zero_add + add_zero := add_zero + add_comm := add_comm + neg_add_cancel := neg_add_cancel + nsmul := nsmul -- TODO do we actually need this custom implementation? + nsmul_zero := nsmul_zero + nsmul_succ := nsmul_succ + zsmul := zsmulRec + +-- TODO do we want a custom efficient implementation? + +-- TODO: define `SemiRing` structure on `CPolynomialC` + +end OperationsC + +section ToPoly + +/-- Convert a `CPolynomial` to a (mathlib) `Polynomial`. -/ +noncomputable def toPoly (p : CPolynomial R) : Polynomial R := + p.eval₂ Polynomial.C Polynomial.X + +/-- a more low-level and direct definition of `toPoly`; currently unused. -/ +noncomputable def toPoly' (p : CPolynomial R) : Polynomial R := + Polynomial.ofFinsupp (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 + )) + +noncomputable def CPolynomialC.toPoly (p : CPolynomialC R) : Polynomial R := p.val.toPoly + +alias ofPoly := Polynomial.toImpl + +/-- evaluation stays the same after converting to mathlib -/ +theorem eval_toPoly_eq_eval (x : Q) (p : CPolynomial Q) : p.toPoly.eval x = p.eval x := by + unfold toPoly eval eval₂ + rw [← Array.foldl_hom (Polynomial.eval x) + (g₁ := fun acc (t : Q × ℕ) ↦ acc + Polynomial.C t.1 * Polynomial.X ^ t.2) + (g₂ := fun acc (a, i) ↦ acc + a * x ^ i) ] + · congr; exact Polynomial.eval_zero + simp + +/-- characterize `p.toPoly` by showing that its coefficients are exactly the coefficients of `p` -/ +lemma coeff_toPoly {p : CPolynomial Q} {n : ℕ} : p.toPoly.coeff n = p.coeff n := by + unfold toPoly eval₂ + + let f := fun (acc: Q[X]) ((a,i): Q × ℕ) ↦ acc + Polynomial.C a * Polynomial.X ^ i + change (Array.foldl f 0 p.zipIdx).coeff n = p.coeff n + + -- we slightly weaken the goal, to use `Array.foldl_induction` + let motive (size: ℕ) (acc: Q[X]) := acc.coeff n = if (n < size) then p.coeff n else 0 + + have zipIdx_size : p.zipIdx.size = p.size := by simp [Array.zipIdx] + + suffices h : motive p.zipIdx.size (Array.foldl f 0 p.zipIdx) by + rw [h, ite_eq_left_iff, zipIdx_size] + intro hn + replace hn : n ≥ p.size := by linarith + rw [coeff, Array.getD_eq_getD_getElem?, Array.getElem?_eq_none hn, Option.getD_none] + + apply Array.foldl_induction motive + · change motive 0 0 + simp [motive] + + change ∀ (i : Fin p.zipIdx.size) acc, motive i acc → motive (i + 1) (f acc p.zipIdx[i]) + unfold motive f + intros i acc h + have i_lt_p : i < p.size := by linarith [i.is_lt] + have : p.zipIdx[i] = (p[i], ↑i) := by simp [Array.getElem_zipIdx] + rw [this, coeff_add, coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, h] + rcases (Nat.lt_trichotomy i n) with hlt | rfl | hgt + · have h1 : ¬ (n < i) := by linarith + have h2 : ¬ (n = i) := by linarith + have h3 : ¬ (n < i + 1) := by linarith + simp [h1, h2, h3] + · simp [i_lt_p] + · have h1 : ¬ (n = i) := by linarith + have h2 : n < i + 1 := by linarith + simp [hgt, h1, h2] + +/-- helper lemma, to argue about `toImpl` by cases -/ +lemma toImpl_elim (p : Q[X]) : + (p = 0 ∧ p.toImpl = #[]) + ∨ (p ≠ 0 ∧ p.toImpl = .ofFn (fun i : Fin (p.natDegree + 1) => p.coeff i)) := by + unfold toImpl + by_cases hbot : p.degree = ⊥ + · left + use degree_eq_bot.mp hbot + rw [hbot] + right + use degree_ne_bot.mp hbot + have hnat : p.degree = p.natDegree := degree_eq_natDegree (degree_ne_bot.mp hbot) + simp [hnat] + +/-- `toImpl` is a right-inverse of `toPoly`. + that is, the round-trip starting from a mathlib polynomial gets us back to where we were. + in particular, `toPoly` is surjective and `toImpl` is injective. -/ +theorem toPoly_toImpl {p : Q[X]} : p.toImpl.toPoly = p := by + ext n + rw [coeff_toPoly] + rcases toImpl_elim p with ⟨rfl, h⟩ | ⟨_, h⟩ + · simp [h] + rw [h] + by_cases h : n < p.natDegree + 1 + · simp [h] + simp only [Array.getD_eq_getD_getElem?, Array.getElem?_ofFn] + simp only [h, reduceDIte, Option.getD_none] + replace h := Nat.lt_of_succ_le (not_lt.mp h) + symm + exact coeff_eq_zero_of_natDegree_lt h + +/-- `CPolynomial` addition is mapped to `Polynomial` addition -/ +theorem toPoly_add {p q : CPolynomial Q} : (add_raw p q).toPoly = p.toPoly + q.toPoly := by + ext n + rw [coeff_add, coeff_toPoly, coeff_toPoly, coeff_toPoly, add_coeff?] + +/-- trimming doesn't change the `toPoly` image -/ +lemma toPoly_trim [LawfulBEq R] {p : CPolynomial R} : p.trim.toPoly = p.toPoly := by + ext n + rw [coeff_toPoly, coeff_toPoly, Trim.coeff_eq_coeff] + +/-- helper lemma to be able to state the next lemma -/ +lemma toImpl_nonzero {p : Q[X]} (hp : p ≠ 0) : p.toImpl.size > 0 := by + rcases toImpl_elim p with ⟨rfl, _⟩ | ⟨_, h⟩ + · contradiction + suffices h : p.toImpl ≠ #[] from Array.size_pos_iff.mpr h + simp [h] + +/-- helper lemma: the last entry of the `CPolynomial` obtained by `toImpl` is just the `leadingCoeff` -/ +lemma getLast_toImpl {p : Q[X]} (hp : p ≠ 0) : let h : p.toImpl.size > 0 := toImpl_nonzero hp; + p.toImpl[p.toImpl.size - 1] = p.leadingCoeff := by + rcases toImpl_elim p with ⟨rfl, _⟩ | ⟨_, h⟩ + · contradiction + simp [h] + +/-- `toImpl` maps to canonical `CPolynomial`s -/ +theorem trim_toImpl [LawfulBEq R] (p : R[X]) : p.toImpl.trim = p.toImpl := by + rcases toImpl_elim p with ⟨rfl, h⟩ | ⟨h_nz, _⟩ + · rw [h, Trim.canonical_empty] + rw [Trim.canonical_iff] + unfold Array.getLast + intro + rw [getLast_toImpl h_nz] + exact Polynomial.leadingCoeff_ne_zero.mpr h_nz + +/-- on canonical `CPolynomial`s, `toImpl` is also a left-inverse of `toPoly`. + in particular, `toPoly` is a bijection from `CPolynomialC` to `Polynomial`. -/ +lemma toImpl_toPoly_of_canonical [LawfulBEq R] (p : CPolynomialC R) : p.toPoly.toImpl = p := by + -- we will change something slightly more general: `toPoly` is injective on canonical polynomials + suffices h_inj : ∀ q : CPolynomialC R, p.toPoly = q.toPoly → p = q by + have : p.toPoly = p.toPoly.toImpl.toPoly := by rw [toPoly_toImpl] + exact h_inj ⟨ p.toPoly.toImpl, trim_toImpl p.toPoly ⟩ this |> congrArg Subtype.val |>.symm + intro q hpq + apply CPolynomialC.ext + apply Trim.canonical_ext p.property q.property + intro i + rw [← coeff_toPoly, ← coeff_toPoly] + exact hpq |> congrArg (fun p => p.coeff i) + +/-- the roundtrip to and from mathlib maps a `CPolynomial` to its trimmed/canonical representative -/ +theorem toImpl_toPoly [LawfulBEq R] (p : CPolynomial R) : p.toPoly.toImpl = p.trim := by + rw [← toPoly_trim] + exact toImpl_toPoly_of_canonical ⟨ p.trim, Trim.trim_twice p⟩ + +/-- evaluation stays the same after converting a mathlib `Polynomial` to a `CPolynomial` -/ +theorem eval_toImpl_eq_eval [LawfulBEq R] (x : R) (p : R[X]) : p.toImpl.eval x = p.eval x := by + rw [← toPoly_toImpl (p := p), toImpl_toPoly, ← toPoly_trim, eval_toPoly_eq_eval] + +/-- corollary: evaluation stays the same after trimming -/ +lemma eval_trim_eq_eval [LawfulBEq R] (x : R) (p : CPolynomial R) : p.trim.eval x = p.eval x := by + rw [← toImpl_toPoly, eval_toImpl_eq_eval, eval_toPoly_eq_eval] + +end ToPoly + +section Equiv + +open Trim + +/-- Reflexivity of the equivalence relation. -/ +@[simp] theorem equiv_refl (p : CPolynomial Q) : equiv p p := + by simp [equiv] + +/-- Symmetry of the equivalence relation. -/ +@[simp] theorem equiv_symm {p q : CPolynomial Q} : equiv p q → equiv q p := by + simp [equiv] + intro h i + exact Eq.symm (h i) + +/-- Transitivity of the equivalence relation. -/ +@[simp] theorem equiv_trans {p q r : CPolynomial Q} : Trim.equiv p q → equiv q r → equiv p r := by + simp_all [Trim.equiv] + +/-- The `CPolynomial.equiv` is indeed an equivalence relation. -/ +instance instEquivalenceEquiv : Equivalence (equiv (R := R)) where + refl := equiv_refl + symm := equiv_symm + trans := equiv_trans + +/-- The `Setoid` instance for `CPolynomial R` induced by `CPolynomial.equiv`. -/ +instance instSetoidCPolynomial : Setoid (CPolynomial R) where + r := equiv + iseqv := instEquivalenceEquiv + +/-- The quotient of `CPolynomial R` by `CPolynomial.equiv`. This will be changen to be equivalent to + `Polynomial R`. -/ +def QuotientCPolynomial (R : Type*) [Ring R] [BEq R] := Quotient (@instSetoidCPolynomial R _) + +-- operations on `CPolynomial` descend to `QuotientCPolynomial` +namespace QuotientCPolynomial + +/- Aristotle failed to find a proof. -/ +-- lemma mul_comm [LawfulBEq R] (a b : CPolynomial R) : +-- a.mul b = b.mul a + +lemma mul_comm_equiv [LawfulBEq R] (a b : CPolynomial R) : + a.mul b ≈ b.mul a := by sorry + +#check Array.foldl_induction + +#check Polynomial R + +lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), + ∀ (q : CPolynomial R) (m l : ℕ), + l + m = n → + p.mul^[n] q = p.mul^[m] (p.mul^[l] q) := by + intro p n + induction n with + | zero => + intro q m l h_sizes + rw [Nat.add_eq_zero_iff] at h_sizes + obtain ⟨hl, hm⟩ := h_sizes + rw [hl, hm] + simp + | succ n₀ ih => + intro q m l h_sizes + cases l with + | zero => + simp at h_sizes + rw [h_sizes] + simp + | succ l₀ => + have h_sizes_simp : l₀ + m = n₀ := by linarith + clear h_sizes + simp + rw [ih (p.mul q) m l₀ h_sizes_simp] + +noncomputable section AristotleLemmas + +/- +Scalar multiplication by 0 is equivalent to the zero polynomial. +-/ +lemma CompPoly.CPolynomial.smul_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CompPoly.CPolynomial R) : + CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.smul 0 p) 0 := by + -- By definition of scalar multiplication, multiplying by 0 results in the zero polynomial. + have h_smul_zero : ∀ (p : CPolynomial R), (smul 0 p).coeff = 0 := by + intro p; ext i; simp [CompPoly.CPolynomial.smul]; + cases p[i]? <;> simp +decide; + exact fun i => by simpa using congr_fun ( h_smul_zero p ) i; + +/- +Addition of polynomials respects equivalence. +-/ +lemma CompPoly.CPolynomial.add_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (p1 p2 q1 q2 : CompPoly.CPolynomial R) + (hp : CompPoly.CPolynomial.Trim.equiv p1 p2) + (hq : CompPoly.CPolynomial.Trim.equiv q1 q2) : + CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.add p1 q1) (CompPoly.CPolynomial.add p2 q2) := by + -- By `add_equiv_raw`, `add p1 q1` is equivalent to `add_raw p1 q1`, and similarly for `p2, q2`. + have h_add_equiv_raw : ∀ p q : CompPoly.CPolynomial R, Trim.equiv (p.add q) (p.add_raw q) := by + exact?; + -- By `add_coeff?`, we have `(add_raw p1 q1).coeff i = p1.coeff i + q1.coeff i` and `(add_raw p2 q2).coeff i = p2.coeff i + q2.coeff i`. + have h_add_coeff : ∀ i, (p1.add_raw q1).coeff i = p1.coeff i + q1.coeff i ∧ (p2.add_raw q2).coeff i = p2.coeff i + q2.coeff i := by + exact fun i => ⟨ add_coeff? p1 q1 i, add_coeff? p2 q2 i ⟩; + simp_all +decide [ Trim.equiv ] + +/- +Multiplication by X^i respects equivalence. +-/ +lemma CompPoly.CPolynomial.mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (i : ℕ) (p q : CompPoly.CPolynomial R) (h : CompPoly.CPolynomial.Trim.equiv p q) : + CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mulPowX i p) (CompPoly.CPolynomial.mulPowX i q) := by + unfold CompPoly.CPolynomial.Trim.equiv at *; + simp +zetaDelta at *; + intro j; by_cases hj : j < i <;> simp_all +decide [ CompPoly.CPolynomial.mulPowX ] ; + · unfold CompPoly.CPolynomial.mk; rw [ Array.getElem?_append, Array.getElem?_append ] ; aesop; + · convert h ( j - i ) using 1 <;> rw [ Array.getElem?_append ] <;> simp +decide [ hj ]; + · rw [ if_neg ( not_lt_of_ge hj ) ]; + · rw [ if_neg ( not_lt_of_ge hj ) ] + +/- +Adding a polynomial equivalent to zero acts as the identity. +-/ +lemma CompPoly.CPolynomial.add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (p q : CompPoly.CPolynomial R) (hq : CompPoly.CPolynomial.Trim.equiv q 0) : + CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.add p q) p := by + intro x; + have := add_coeff? p q x; + have hq_zero : q.coeff x = 0 := by + exact hq x; + unfold CompPoly.CPolynomial.add; + rw [ Trim.coeff_eq_coeff ] ; aesop + +/- +Multiplying the zero polynomial by X^i results in a polynomial equivalent to zero. +-/ +lemma CompPoly.CPolynomial.mulPowX_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (i : ℕ) : CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mulPowX i (0 : CompPoly.CPolynomial R)) 0 := by + unfold CompPoly.CPolynomial.Trim.equiv; + simp [CompPoly.CPolynomial.coeff]; + unfold CompPoly.CPolynomial.mulPowX; + grind + +/- +Definition of a single step in the polynomial multiplication algorithm. +-/ +def CompPoly.CPolynomial.mul_step {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CompPoly.CPolynomial R) (acc : CompPoly.CPolynomial R) (x : R × ℕ) : CompPoly.CPolynomial R := + acc.add ((CompPoly.CPolynomial.smul x.1 q).mulPowX x.2) + +/- +The multiplication step respects equivalence of the accumulator. +-/ +lemma CompPoly.CPolynomial.mul_step_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CompPoly.CPolynomial R) (acc1 acc2 : CompPoly.CPolynomial R) (x : R × ℕ) + (h : CompPoly.CPolynomial.Trim.equiv acc1 acc2) : + CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mul_step q acc1 x) (CompPoly.CPolynomial.mul_step q acc2 x) := by + apply_rules [ CompPoly.CPolynomial.add_equiv, CompPoly.CPolynomial.mulPowX_equiv, CompPoly.CPolynomial.smul_equiv ] + +/- +The multiplication step with a zero coefficient acts as the identity modulo equivalence. +-/ +lemma CompPoly.CPolynomial.mul_step_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CompPoly.CPolynomial R) (acc : CompPoly.CPolynomial R) (i : ℕ) : + CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mul_step q acc (0, i)) acc := by + -- By definition of `mul_step`, we have `mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i)`. + have h_mul_step : CompPoly.CPolynomial.mul_step q acc (0, i) = acc.add ((CompPoly.CPolynomial.smul 0 q).mulPowX i) := by + exact?; + -- By definition of `mulPowX`, we have `mulPowX i (smul 0 q) = smul 0 (mulPowX i q)`. + have h_mulPowX : CompPoly.CPolynomial.mulPowX i (CompPoly.CPolynomial.smul 0 q) = CompPoly.CPolynomial.smul 0 (CompPoly.CPolynomial.mulPowX i q) := by + unfold CompPoly.CPolynomial.mulPowX CompPoly.CPolynomial.smul; aesop; + rw [ h_mul_step, h_mulPowX ]; + exact add_zero_equiv _ _ ( smul_zero_equiv _ ) + +/- +Folding `mul_step` over a list of zero coefficients preserves equivalence. +-/ +lemma CompPoly.CPolynomial.foldl_mul_step_zeros {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (q : CompPoly.CPolynomial R) (acc : CompPoly.CPolynomial R) (l : List (R × ℕ)) + (hl : ∀ x ∈ l, x.1 = 0) : + CompPoly.CPolynomial.Trim.equiv (l.foldl (CompPoly.CPolynomial.mul_step q) acc) acc := by + induction' l using List.reverseRecOn with x xs ih generalizing acc; + · exact fun _ => rfl; + · simp_all +decide [ List.foldl_append ]; + -- By the properties of the multiplication step and the induction hypothesis, we can conclude the proof. + have h_mul_step : CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mul_step q (List.foldl (CompPoly.CPolynomial.QuotientCPolynomial.CompPoly.CPolynomial.mul_step q) acc x) xs) (List.foldl (CompPoly.CPolynomial.QuotientCPolynomial.CompPoly.CPolynomial.mul_step q) acc x) := by + convert mul_step_zero q ( List.foldl ( CompPoly.CPolynomial.QuotientCPolynomial.CompPoly.CPolynomial.mul_step q ) acc x ) xs.2 using 1; + specialize hl _ _ ( Or.inr rfl ) ; aesop; + exact? + +/- +The `zipIdx` of a polynomial is the `zipIdx` of its trim followed by a list of zero coefficients. +-/ +lemma CompPoly.CPolynomial.zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] + (p : CompPoly.CPolynomial R) : + ∃ l, p.zipIdx.toList = p.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by + -- Let `n` be `p.trim.size`. `p.trim` is the prefix of `p` of length `n`. + set n := p.trim.size with hn_def; + by_cases hn : n = 0; + · unfold n at hn; + -- Since `p.trim` is empty, `p` must be the zero polynomial. + have hp_zero : ∀ i (hi : i < p.size), p[i] = 0 := by + have := Trim.elim p; aesop; + use List.map (fun i => (0, i)) (List.range p.size); + simp +decide [ hp_zero ]; + refine' List.ext_get _ _ <;> aesop; + · -- Since `n` is not zero, `p.last_nonzero` is `some k` and `n = k + 1`. + obtain ⟨k, hk⟩ : ∃ k : Fin p.size, p.trim = p.extract 0 (k.val + 1) ∧ p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by + have := Trim.elim p; + aesop; + refine' ⟨ _, _, _ ⟩; + exact ( Array.zipIdx p ).toList.drop ( k + 1 ); + · rw [ hk.1 ]; + refine' List.ext_get _ _ <;> simp +decide [ List.get ]; + · rw [ min_eq_left ( by linarith [ Fin.is_lt k ] ), add_tsub_cancel_of_le ( by linarith [ Fin.is_lt k ] ) ]; + · intro n h₁ h₂; rw [ List.getElem_append ] ; simp +decide [ h₁, h₂ ] ; + grind; + · simp +decide [ List.mem_iff_get ]; + intro a; specialize hk; have := hk.2.2 ( k + 1 + a ) ; simp_all +decide [ Nat.add_assoc ] ; + +end AristotleLemmas + +lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : + a.mul b ≈ a.trim.mul b := by + have h_zipIdx_split : ∃ l, a.zipIdx.toList = a.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by + exact?; + obtain ⟨l, hl⟩ := h_zipIdx_split; + have h_foldl_split : ∃ acc, (a.mul b) = (l.foldl (CompPoly.CPolynomial.mul_step b) acc) ∧ (a.trim.mul b) = acc := by + -- By definition of `mul`, we can rewrite `a.mul b` using `mul_step` and the foldl operation. + have h_mul_def : a.mul b = (a.zipIdx.toList.foldl (CompPoly.CPolynomial.mul_step b) (CompPoly.CPolynomial.C 0)) := by + unfold CompPoly.CPolynomial.mul; + exact?; + have h_mul_def_trim : a.trim.mul b = (a.trim.zipIdx.toList.foldl (CompPoly.CPolynomial.mul_step b) (CompPoly.CPolynomial.C 0)) := by + unfold CompPoly.CPolynomial.mul; + exact?; + aesop; + obtain ⟨ acc, h₁, h₂ ⟩ := h_foldl_split; + exact h₁.symm ▸ h₂.symm ▸ CompPoly.CPolynomial.foldl_mul_step_zeros b acc l hl.2 + +lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : + equiv a₁ a₂ → a₁.mul b ≈ a₂.mul b := by + intro h + calc + a₁.mul b ≈ a₁.trim.mul b := mul_trim_equiv a₁ b + _ ≈ a₂.trim.mul b := by rw [eq_of_equiv h] + _ ≈ a₂.mul b := equiv_symm (mul_trim_equiv a₂ b) + +-- Addition: add descends to `QuotientCPolynomial` +def add_descending (p q : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (add p q) + +lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : + equiv a₁ a₂ → equiv b₁ b₂ → add_descending a₁ b₁ = add_descending a₂ b₂ := by + intros heq_a heq_b + unfold add_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + calc + add a₁ b₁ ≈ add_raw a₁ b₁ := add_equiv_raw a₁ b₁ + _ ≈ add_raw a₂ b₂ := by + intro i + rw [add_coeff? a₁ b₁ i, add_coeff? a₂ b₂ i, heq_a i, heq_b i] + _ ≈ add a₂ b₂ := equiv_symm (add_equiv_raw a₂ b₂) + +@[inline, specialize] +def add {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift₂ add_descending add_descends p q + +-- Scalar multiplication: smul descends to `QuotientCPolynomial` +def smul_descending (r : R) (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (smul r p) + +lemma smul_descends [LawfulBEq R] (r : R) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → smul_descending r p₁ = smul_descending r p₂ := by + unfold equiv smul_descending + intro heq + rw [Quotient.eq] + simp [instSetoidCPolynomial] + intro i + rw [smul_equiv p₁, smul_equiv p₂] + rw [heq i] + +@[inline, specialize] +def smul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (r : R) (p : QuotientCPolynomial R) + : QuotientCPolynomial R := + Quotient.lift (smul_descending r) (smul_descends r) p + +-- Scalar multiplication: nsmul_raw descends to `QuotientCPolynomial` +def nsmul_descending (n : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (nsmul n p) + +lemma nsmul_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → nsmul_descending n p₁ = nsmul_descending n p₂ := by + unfold equiv + intro heq + unfold nsmul_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + unfold nsmul equiv + intro i + repeat rw [nsmul_raw_equiv, coeff_eq_coeff] + rw [heq i] + +@[inline, specialize] +def nsmul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : QuotientCPolynomial R) + : QuotientCPolynomial R := + Quotient.lift (nsmul_descending n) (nsmul_descends n) p + +-- Negation: neg descends to `QuotientCPolynomial` +def neg_descending (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (neg p) + +lemma neg_descends (a b : CPolynomial R) : equiv a b → neg_descending a = neg_descending b := by + unfold equiv neg_descending + intros heq + rw [Quotient.eq] + simp [instSetoidCPolynomial] + unfold equiv + intro i + rw [neg_coeff a i, neg_coeff b i, heq i] + +@[inline, specialize] +def neg {R : Type*} [Ring R] [BEq R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift neg_descending neg_descends p + +-- Subtraction: sub descends to `QuotientCPolynomial` +def sub_descending (p q : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (sub p q) + +lemma sub_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : + equiv a₁ a₂ → equiv b₁ b₂ → sub_descending a₁ b₁ = sub_descending a₂ b₂ := by + unfold equiv sub_descending + intros heq_a heq_b + rw [Quotient.eq] + simp [instSetoidCPolynomial] + unfold sub equiv + calc + a₁.add b₁.neg ≈ a₁.add_raw b₁.neg := add_equiv_raw a₁ b₁.neg + _ ≈ a₂.add_raw b₂.neg := by + intro i + rw [add_coeff? a₁ b₁.neg i, add_coeff? a₂ b₂.neg i] + rw [neg_coeff b₁ i, neg_coeff b₂ i, heq_a i, heq_b i] + _ ≈ a₂.add b₂.neg := equiv_symm (add_equiv_raw a₂ b₂.neg) + +@[inline, specialize] +def sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift₂ sub_descending sub_descends p q + +-- Multiplication by `X ^ i`: mulPowX descends to `QuotientCPolynomial` +def mulPowX_descending (i : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (mulPowX i p) + +lemma mulPowX_descends (i : ℕ) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → mulPowX_descending i p₁ = mulPowX_descending i p₂ := by + unfold equiv + intro heq + unfold mulPowX_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + intro j + by_cases h : j ≥ i + . rw [mulPowX_equiv₁ p₁ i j h, mulPowX_equiv₁ p₂ i j h] + rw [heq] + . simp at h + rw [mulPowX_equiv₂ p₁ i j h, mulPowX_equiv₂ p₂ i j h] + +@[inline, specialize] +def mulPowX {R : Type*} [Ring R] [BEq R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift (mulPowX_descending i) (mulPowX_descends i) p + +-- Multiplication of a `CPolynomial` by `X`, reduces to `mulPowX 1`. +@[inline, specialize] +def mulX (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 + +-- Multiplication: mul descends to `QuotientPoly` +def mul_descending (p q : CPolynomial R) : QuotientCPolynomial R := + Quotient.mk _ (mul p q) + +lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : + equiv a₁ a₂ → equiv b₁ b₂ → mul_descending a₁ b₁ = mul_descending a₂ b₂ := by + unfold mul_descending + intros heq_a heq_b + rw [Quotient.eq] + simp [instSetoidCPolynomial] + calc + a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a + _ ≈ b₁.mul a₂ := mul_comm_equiv a₂ b₁ + _ ≈ b₂.mul a₂ := mul_equiv b₁ b₂ a₂ heq_b + _ ≈ a₂.mul b₂ := mul_comm_equiv b₂ a₂ + +@[inline, specialize] +def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := + Quotient.lift₂ mul_descending mul_descends p q + +-- Exponentiation: pow descends to `QuotientCPolynomial` +def pow_descending (p : CPolynomial R) (n : ℕ) : QuotientCPolynomial R := + Quotient.mk _ (pow p n) + +lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : + equiv p₁ p₂ → pow_descending p₁ n = pow_descending p₂ n := by + intro heq + unfold pow_descending + rw [Quotient.eq] + simp [instSetoidCPolynomial] + unfold pow + have mul_pow_equiv : ∀ (p : CPolynomial R) (n : ℕ), + p.mul^[n + 1] (C 1) ≈ p.mul (p.mul^[n] (C 1)) := by + intro p n + rw [mul_pow_assoc p (n + 1) (C 1) 1 n] + . simp + simp + induction n with + | zero => simp + | succ n ih => + calc + p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_equiv p₁ n + _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := mul_comm_equiv p₁ (p₁.mul^[n] (C 1)) + _ ≈ (p₂.mul^[n] (C 1)).mul p₁ := mul_equiv _ _ p₁ ih + _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_comm_equiv (p₂.mul^[n] (C 1)) p₁ + _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq + _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_equiv p₂ n) + +@[inline, specialize] +def pow {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := + Quotient.lift (fun p => pow_descending p n) (pow_descends n) p + +-- TODO div? + +end QuotientCPolynomial + +end Equiv + +namespace Lagrange + +end Lagrange + +end CPolynomial + +end CompPoly From 8c6013a6ca8e382a006b9646e157e52129c22abb Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 5 Jan 2026 10:23:40 +0000 Subject: [PATCH 05/11] fix: remove draft code --- CompPoly/Univariate/harmonic-output.lean | 1413 ---------------------- 1 file changed, 1413 deletions(-) delete mode 100644 CompPoly/Univariate/harmonic-output.lean diff --git a/CompPoly/Univariate/harmonic-output.lean b/CompPoly/Univariate/harmonic-output.lean deleted file mode 100644 index 2fc8d8e..0000000 --- a/CompPoly/Univariate/harmonic-output.lean +++ /dev/null @@ -1,1413 +0,0 @@ -/- -This file was edited by Aristotle. - -Lean version: leanprover/lean4:v4.24.0 -Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 -This project request had uuid: 95f785fa-5bb7-4083-9638-ce14b5377f15 - -The following was proved by Aristotle: - -- theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : - (add_raw p q)[i] = p.coeff i + q.coeff i - -- lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : - a.mul b ≈ a.trim.mul b --/ - -/- -Copyright (c) 2025 CompPoly. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Quang Dao, Gregor Mitscha-Baude, Derek Sorensen --/ - -import Mathlib.Algebra.Tropical.Basic -import Mathlib.RingTheory.Polynomial.Basic -import CompPoly.Data.Array.Lemmas - - -/-! - # Computable Univariate Polynomials - - This file contains a computable datatype for univariate polynomial, `CPolynomial R`. This is - internally represented as an array of coefficients. - - Note: this has been ported from ArkLib --/ - -open Polynomial - -namespace CompPoly - -/-- A type analogous to `Polynomial` that supports computable operations. This defined to be a - wrapper around `Array`. - -For example the Array `#[1,2,3]` represents the polynomial `1 + 2x + 3x^2`. Two arrays may represent -the same polynomial via zero-padding, for example `#[1,2,3] = #[1,2,3,0,0,0,...]`. --/ -@[reducible, inline, specialize] -def CPolynomial (R : Type*) := Array R - -end CompPoly - -/-- Convert a `Polynomial` to a `CPolynomial`. -/ -def Polynomial.toImpl {R : Type*} [Semiring R] (p : R[X]) : CompPoly.CPolynomial R := - match p.degree with - | ⊥ => #[] - | some d => .ofFn (fun i : Fin (d + 1) => p.coeff i) - -namespace CompPoly - -namespace CPolynomial - -@[reducible] -def mk {R : Type*} (coeffs : Array R) : CPolynomial R := coeffs - -@[reducible] -def coeffs {R : Type*} (p : CPolynomial R) : Array R := p - -variable {R : Type*} [Ring R] [BEq R] - -variable {Q : Type*} [Ring Q] - -@[reducible] -def coeff (p : CPolynomial Q) (i : ℕ) : Q := p.getD i 0 - -/-- The constant polynomial `C r`. -/ -def C (r : R) : CPolynomial R := #[r] - -/-- The variable `X`. -/ -def X : CPolynomial R := #[0, 1] - -/-- Return the index of the last non-zero coefficient of a `CPolynomial` -/ -def last_nonzero (p : CPolynomial R) : Option (Fin p.size) := - p.findIdxRev? (· != 0) - -/-- Remove leading zeroes from a `CPolynomial`. Requires `BEq` to check if the coefficients are zero. -/ -def trim (p : CPolynomial R) : CPolynomial R := - match p.last_nonzero with - | none => #[] - | some i => p.extract 0 (i.val + 1) - -/-- Return the degree of a `CPolynomial`. -/ -def degree (p : CPolynomial R) : Nat := - match p.last_nonzero with - | none => 0 - | some i => i.val + 1 - -/-- Return the leading coefficient of a `CPolynomial` as the last coefficient of the trimmed array, -or `0` if the trimmed array is empty. -/ -def leadingCoeff (p : CPolynomial R) : R := p.trim.getLastD 0 - -namespace Trim - --- characterize .last_nonzero -theorem last_nonzero_none [LawfulBEq R] {p : CPolynomial R} : - (∀ i, (hi : i < p.size) → p[i] = 0) → p.last_nonzero = none -:= by - intro h - apply Array.findIdxRev?_eq_none - intros - rw [bne_iff_ne, ne_eq, not_not] - apply_assumption - -theorem last_nonzero_some [LawfulBEq R] {p : CPolynomial R} {i} (hi : i < p.size) (h : p[i] ≠ 0) : - ∃ k, p.last_nonzero = some k -:= Array.findIdxRev?_eq_some ⟨i, hi, bne_iff_ne.mpr h⟩ - -theorem last_nonzero_spec [LawfulBEq R] {p : CPolynomial R} {k} : - p.last_nonzero = some k - → p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) -:= by - intro (h : p.last_nonzero = some k) - constructor - · by_contra - have h : p[k] != 0 := Array.findIdxRev?_def h - rwa [‹p[k] = 0›, bne_self_eq_false, Bool.false_eq_true] at h - · intro j hj j_gt_k - have h : ¬(p[j] != 0) := Array.findIdxRev?_maximal h ⟨ j, hj ⟩ j_gt_k - rwa [bne_iff_ne, ne_eq, not_not] at h - --- the property of `last_nonzero_spec` uniquely identifies an element, --- and that allows us to prove the reverse as well -def last_nonzero_prop {p : CPolynomial R} (k : Fin p.size) : Prop := - p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) - -lemma last_nonzero_unique {p : CPolynomial Q} {k k' : Fin p.size} : - last_nonzero_prop k → last_nonzero_prop k' → k = k' -:= by - suffices weaker : ∀ k k', last_nonzero_prop k → last_nonzero_prop k' → k ≤ k' by - intro h h' - exact Fin.le_antisymm (weaker k k' h h') (weaker k' k h' h) - intro k k' ⟨ h_nonzero, h ⟩ ⟨ h_nonzero', h' ⟩ - by_contra k_not_le - have : p[k] = 0 := h' k k.is_lt (Nat.lt_of_not_ge k_not_le) - contradiction - -theorem last_nonzero_some_iff [LawfulBEq R] {p : CPolynomial R} {k} : - p.last_nonzero = some k ↔ (p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0)) -:= by - constructor - · apply last_nonzero_spec - intro h_prop - have ⟨ k', h_some'⟩ := last_nonzero_some k.is_lt h_prop.left - have k_is_k' := last_nonzero_unique (last_nonzero_spec h_some') h_prop - rwa [← k_is_k'] - -/-- eliminator for `p.last_nonzero`, e.g. use with the induction tactic as follows: - ``` - induction p using last_nonzero_induct with - | case1 p h_none h_all_zero => ... - | case2 p k h_some h_nonzero h_max => ... - ``` --/ -theorem last_nonzero_induct [LawfulBEq R] {motive : CPolynomial R → Prop} - (case1 : ∀ p, p.last_nonzero = none → (∀ i, (hi : i < p.size) → p[i] = 0) → motive p) - (case2 : ∀ p : CPolynomial R, ∀ k : Fin p.size, p.last_nonzero = some k → p[k] ≠ 0 → - (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0) → motive p) - (p : CPolynomial R) : motive p -:= by - by_cases h : ∀ i, (hi : i < p.size) → p[i] = 0 - · exact case1 p (last_nonzero_none h) h - · push_neg at h; rcases h with ⟨ i, hi, h ⟩ - obtain ⟨ k, h_some ⟩ := last_nonzero_some hi h - have ⟨ h_nonzero, h_max ⟩ := last_nonzero_spec h_some - exact case2 p k h_some h_nonzero h_max - -/-- eliminator for `p.trim`; use with the induction tactic as follows: - ``` - induction p using induct with - | case1 p h_empty h_all_zero => ... - | case2 p k h_extract h_nonzero h_max => ... - ``` --/ -theorem induct [LawfulBEq R] {motive : CPolynomial R → Prop} - (case1 : ∀ p, p.trim = #[] → (∀ i, (hi : i < p.size) → p[i] = 0) → motive p) - (case2 : ∀ p : CPolynomial R, ∀ k : Fin p.size, p.trim = p.extract 0 (k + 1) - → p[k] ≠ 0 → (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0) → motive p) - (p : CPolynomial R) : motive p -:= by induction p using last_nonzero_induct with - | case1 p h_none h_all_zero => - have h_empty : p.trim = #[] := by unfold trim; rw [h_none] - exact case1 p h_empty h_all_zero - | case2 p k h_some h_nonzero h_max => - have h_extract : p.trim = p.extract 0 (k + 1) := by unfold trim; rw [h_some] - exact case2 p k h_extract h_nonzero h_max - -/-- eliminator for `p.trim`; e.g. use for case distinction as follows: - ``` - rcases (Trim.elim p) with ⟨ h_empty, h_all_zero ⟩ | ⟨ k, h_extract, h_nonzero, h_max ⟩ - ``` --/ -theorem elim [LawfulBEq R] (p : CPolynomial R) : - (p.trim = #[] ∧ (∀ i, (hi : i < p.size) → p[i] = 0)) - ∨ (∃ k : Fin p.size, - p.trim = p.extract 0 (k + 1) - ∧ p[k] ≠ 0 - ∧ (∀ j : ℕ, (hj : j < p.size) → j > k → p[j] = 0)) -:= by induction p using induct with - | case1 p h_empty h_all_zero => left; exact ⟨h_empty, h_all_zero⟩ - | case2 p k h_extract h_nonzero h_max => right; exact ⟨k, h_extract, h_nonzero, h_max⟩ - -theorem size_eq_degree (p : CPolynomial R) : p.trim.size = p.degree := by - unfold trim degree - match h : p.last_nonzero with - | none => simp - | some i => simp [Fin.is_lt, Nat.succ_le_of_lt] - -theorem size_le_size (p : CPolynomial R) : p.trim.size ≤ p.size := by - unfold trim - match h : p.last_nonzero with - | none => simp - | some i => simp [Array.size_extract] - -attribute [simp] Array.getElem?_eq_none - -theorem coeff_eq_getElem_of_lt [LawfulBEq R] {p : CPolynomial R} {i} (hi : i < p.size) : - p.trim.coeff i = p[i] := by - induction p using induct with - | case1 p h_empty h_all_zero => - specialize h_all_zero i hi - simp [h_empty, h_all_zero] - | case2 p k h_extract h_nonzero h_max => - simp [h_extract] - -- split between i > k and i <= k - have h_size : k + 1 = (p.extract 0 (k + 1)).size := by - simp [Array.size_extract] - exact Nat.succ_le_of_lt k.is_lt - rcases (Nat.lt_or_ge k i) with hik | hik - · have hik' : i ≥ (p.extract 0 (k + 1)).size := by linarith - rw [Array.getElem?_eq_none hik', Option.getD_none] - exact h_max i hi hik |> Eq.symm - · have hik' : i < (p.extract 0 (k + 1)).size := by linarith - rw [Array.getElem?_eq_getElem hik', Option.getD_some, Array.getElem_extract] - simp only [zero_add] - -theorem coeff_eq_coeff [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : - p.trim.coeff i = p.coeff i := by - rcases (Nat.lt_or_ge i p.size) with hi | hi - · rw [coeff_eq_getElem_of_lt hi] - simp [hi] - · have hi' : i ≥ p.trim.size := by linarith [size_le_size p] - simp [hi, hi'] - -lemma coeff_eq_getElem {p : CPolynomial Q} {i} (hp : i < p.size) : - p.coeff i = p[i] := by - simp [hp] - -/-- Two polynomials are equivalent if they have the same `Nat` coefficients. -/ -def equiv (p q : CPolynomial R) : Prop := - ∀ i, p.coeff i = q.coeff i - -lemma coeff_eq_zero {p : CPolynomial Q} : - (∀ i, (hi : i < p.size) → p[i] = 0) ↔ ∀ i, p.coeff i = 0 -:= by - constructor <;> intro h i - · cases Nat.lt_or_ge i p.size <;> simp [*] - · intro hi; specialize h i; simp [hi] at h; assumption - -lemma eq_degree_of_equiv [LawfulBEq R] {p q : CPolynomial R} : equiv p q → p.degree = q.degree := by - unfold equiv degree - intro h_equiv - induction p using last_nonzero_induct with - | case1 p h_none_p h_all_zero => - have h_zero_p : ∀ i, p.coeff i = 0 := coeff_eq_zero.mp h_all_zero - have h_zero_q : ∀ i, q.coeff i = 0 := by intro i; rw [← h_equiv, h_zero_p] - have h_none_q : q.last_nonzero = none := last_nonzero_none (coeff_eq_zero.mpr h_zero_q) - rw [h_none_p, h_none_q] - | case2 p k h_some_p h_nonzero_p h_max_p => - have h_equiv_k := h_equiv k - have k_lt_q : k < q.size := by - by_contra h_not_lt - have h_ge := Nat.le_of_not_lt h_not_lt - simp [h_ge] at h_equiv_k - contradiction - simp [k_lt_q] at h_equiv_k - have h_nonzero_q : q[k.val] ≠ 0 := by rwa [← h_equiv_k] - have h_max_q : ∀ j, (hj : j < q.size) → j > k → q[j] = 0 := by - intro j hj j_gt_k - have h_eq := h_equiv j - simp [hj] at h_eq - rw [← h_eq] - rcases Nat.lt_or_ge j p.size with hj | hj - · simp [hj, h_max_p j hj j_gt_k] - · simp [hj] - have h_some_q : q.last_nonzero = some ⟨ k, k_lt_q ⟩ := - last_nonzero_some_iff.mpr ⟨ h_nonzero_q, h_max_q ⟩ - rw [h_some_p, h_some_q] - -theorem eq_of_equiv [LawfulBEq R] {p q : CPolynomial R} : equiv p q → p.trim = q.trim := by - unfold equiv - intro h - ext - · rw [size_eq_degree, size_eq_degree] - apply eq_degree_of_equiv h - rw [← coeff_eq_getElem, ← coeff_eq_getElem] - rw [coeff_eq_coeff, coeff_eq_coeff, h _] - -theorem trim_equiv [LawfulBEq R] (p : CPolynomial R) : equiv p.trim p := by - apply coeff_eq_coeff - -theorem trim_twice [LawfulBEq R] (p : CPolynomial R) : p.trim.trim = p.trim := by - apply eq_of_equiv - apply trim_equiv - -theorem canonical_empty : (CPolynomial.mk (R:=R) #[]).trim = #[] := by - have : (CPolynomial.mk (R:=R) #[]).last_nonzero = none := by - simp [last_nonzero]; - apply Array.findIdxRev?_emtpy_none - rfl - rw [trim, this] - -theorem canonical_of_size_zero {p : CPolynomial R} : p.size = 0 → p.trim = p := by - intro h - suffices h_empty : p = #[] by rw [h_empty]; exact canonical_empty - exact Array.eq_empty_of_size_eq_zero h - -theorem canonical_nonempty_iff [LawfulBEq R] {p : CPolynomial R} (hp : p.size > 0) : - p.trim = p ↔ p.last_nonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩ -:= by - unfold trim - induction p using last_nonzero_induct with - | case1 p h_none h_all_zero => - simp [h_none] - by_contra h_empty - subst h_empty - contradiction - | case2 p k h_some h_nonzero h_max => - simp [h_some] - constructor - · intro h - ext - have : p ≠ #[] := Array.ne_empty_of_size_pos hp - simp [this] at h - have : k + 1 ≤ p.size := Nat.succ_le_of_lt k.is_lt - have : p.size = k + 1 := Nat.le_antisymm h this - simp [this] - · intro h - have : k + 1 = p.size := by rw [h]; exact Nat.succ_pred_eq_of_pos hp - rw [this] - right - exact le_refl _ - -theorem last_nonzero_last_iff [LawfulBEq R] {p : CPolynomial R} (hp : p.size > 0) : - p.last_nonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩ ↔ p.getLast hp ≠ 0 -:= by - induction p using last_nonzero_induct with - | case1 => simp [Array.getLast, *] - | case2 p k h_some h_nonzero h_max => - simp only [h_some, Option.some_inj, Array.getLast] - constructor - · intro h - have : k = p.size - 1 := by rw [h] - conv => lhs; congr; case i => rw [← this] - assumption - · intro h - rcases Nat.lt_trichotomy k (p.size - 1) with h_lt | h_eq | h_gt - · specialize h_max (p.size - 1) (Nat.pred_lt_self hp) h_lt - contradiction - · ext; assumption - · have : k < p.size := k.is_lt - have : k ≥ p.size := Nat.le_of_pred_lt h_gt - linarith - -theorem canonical_iff [LawfulBEq R] {p : CPolynomial R} : - p.trim = p ↔ ∀ hp : p.size > 0, p.getLast hp ≠ 0 -:= by - constructor - · intro h hp - rwa [← last_nonzero_last_iff hp, ← canonical_nonempty_iff hp] - · rintro h - rcases Nat.eq_zero_or_pos p.size with h_zero | hp - · exact canonical_of_size_zero h_zero - · rw [canonical_nonempty_iff hp, last_nonzero_last_iff hp] - exact h hp - -theorem non_zero_map [LawfulBEq R] (f : R → R) (hf : ∀ r, f r = 0 → r = 0) (p : CPolynomial R) : - let fp := CPolynomial.mk (p.map f); - p.trim = p → fp.trim = fp -:= by - intro fp p_canon - by_cases hp : p.size > 0 - -- positive case - · apply canonical_iff.mpr - intro hfp - have h_nonzero := canonical_iff.mp p_canon hp - have : fp.getLast hfp = f (p.getLast hp) := by simp [Array.getLast, fp] - rw [this] - by_contra h_zero - specialize hf (p.getLast hp) h_zero - contradiction - -- zero case - have : p.size = 0 := by linarith - have : fp.size = 0 := by simp [this, fp] - apply canonical_of_size_zero this - -/-- Canonical polynomials enjoy a stronger extensionality theorem: - they just need to agree at all coefficients (without assuming equal sizes) --/ -theorem canonical_ext [LawfulBEq R] {p q : CPolynomial R} (hp : p.trim = p) (hq : q.trim = q) : - equiv p q → p = q := by - intro h_equiv - rw [← hp, ← hq] - exact eq_of_equiv h_equiv - -end Trim - -/-- canonical version of CPolynomial - -TODO: make THIS the `CPolynomial, rename current `CPolynomial` to `CPolynomial.Raw` or something -/ -def CPolynomialC (R : Type*) [BEq R] [Ring R] := { p : CPolynomial R // p.trim = p } - -@[ext] theorem CPolynomialC.ext {p q : CPolynomialC R} (h : p.val = q.val) : p = q := Subtype.eq h - -instance : Coe (CPolynomialC R) (CPolynomial R) where coe := Subtype.val - -instance : Inhabited (CPolynomialC R) := ⟨#[], Trim.canonical_empty⟩ - -section Operations - -variable {S : Type*} - --- p(x) = a_0 + a_1 x + a_2 x^2 + ... + a_n x^n - --- eval₂ f x p = f(a_0) + f(a_1) x + f(a_2) x^2 + ... + f(a_n) x^n - -/-- Evaluates a `CPolynomial` at a given value, using a ring homomorphism `f: R →+* S`. -TODO: define an efficient version of this with caching -/ -def eval₂ [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : S := - p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0 - -/-- Evaluates a `CPolynomial` at a given value -/ -@[inline, specialize] -def eval (x : R) (p : CPolynomial R) : R := - p.eval₂ (RingHom.id R) x - -/-- Addition of two `CPolynomial`s. Defined as the pointwise sum of the underlying coefficient arrays - (properly padded with zeroes). -/ -@[inline, specialize] -def add_raw (p q : CPolynomial R) : CPolynomial R := - let ⟨p', q'⟩ := Array.matchSize p q 0 - .mk (Array.zipWith (· + ·) p' q' ) - -/-- Addition of two `CPolynomial`s, with result trimmed. -/ -@[inline, specialize] -def add (p q : CPolynomial R) : CPolynomial R := - add_raw p q |> trim - -/-- Scalar multiplication of `CPolynomial` by an element of `R`. -/ -@[inline, specialize] -def smul (r : R) (p : CPolynomial R) : CPolynomial R := - .mk (Array.map (fun a => r * a) p) - -/-- Scalar multiplication of `CPolynomial` by a natural number. -/ -@[inline, specialize] -def nsmul_raw (n : ℕ) (p : CPolynomial R) : CPolynomial R := - .mk (Array.map (fun a => n * a) p) - -/-- Scalar multiplication of `CPolynomial` by a natural number, with result trimmed. -/ -@[inline, specialize] -def nsmul (n : ℕ) (p : CPolynomial R) : CPolynomial R := - nsmul_raw n p |> trim - -/-- Negation of a `CPolynomial`. -/ -@[inline, specialize] -def neg (p : CPolynomial R) : CPolynomial R := p.map (fun a => -a) - -/-- Subtraction of two `CPolynomial`s. -/ -@[inline, specialize] -def sub (p q : CPolynomial R) : CPolynomial R := p.add q.neg - -/-- Multiplication of a `CPolynomial` by `X ^ i`, i.e. pre-pending `i` zeroes to the -underlying array of coefficients. -/ -@[inline, specialize] -def mulPowX (i : Nat) (p : CPolynomial R) : CPolynomial R := .mk (Array.replicate i 0 ++ p) - -/-- Multiplication of a `CPolynomial` by `X`, reduces to `mulPowX 1`. -/ -@[inline, specialize] -def mulX (p : CPolynomial R) : CPolynomial R := p.mulPowX 1 - -/-- Multiplication of two `CPolynomial`s, using the naive `O(n^2)` algorithm. -/ -@[inline, specialize] -def mul (p q : CPolynomial R) : CPolynomial R := - p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc.add <| (smul a q).mulPowX i) (C 0) - -/-- Exponentiation of a `CPolynomial` by a natural number `n` via repeated multiplication. -/ -@[inline, specialize] -def pow (p : CPolynomial R) (n : Nat) : CPolynomial R := (mul p)^[n] (C 1) - --- TODO: define repeated squaring version of `pow` - -instance : Zero (CPolynomial R) := ⟨#[]⟩ - -instance : One (CPolynomial R) := ⟨CPolynomial.C 1⟩ - -instance : Add (CPolynomial R) := ⟨CPolynomial.add⟩ - -instance : SMul R (CPolynomial R) := ⟨CPolynomial.smul⟩ - -instance : SMul ℕ (CPolynomial R) := ⟨nsmul⟩ - -instance : Neg (CPolynomial R) := ⟨CPolynomial.neg⟩ - -instance : Sub (CPolynomial R) := ⟨CPolynomial.sub⟩ - -instance : Mul (CPolynomial R) := ⟨CPolynomial.mul⟩ - -instance : Pow (CPolynomial R) Nat := ⟨CPolynomial.pow⟩ - -instance : NatCast (CPolynomial R) := ⟨fun n => CPolynomial.C (n : R)⟩ - -instance : IntCast (CPolynomial R) := ⟨fun n => CPolynomial.C (n : R)⟩ - -/-- Return a bound on the degree of a `CPolynomial` as the size of the underlying array -(and `⊥` if the array is empty). -/ -def degreeBound (p : CPolynomial R) : WithBot Nat := - match p.size with - | 0 => ⊥ - | .succ n => n - -/-- Convert `degreeBound` to a natural number by sending `⊥` to `0`. -/ -def natDegreeBound (p : CPolynomial R) : Nat := - (degreeBound p).getD 0 - -/-- Check if a `CPolynomial` is monic, i.e. its leading coefficient is 1. -/ -def monic (p : CPolynomial R) : Bool := p.leadingCoeff == 1 - -/-- Division and modulus of `p : CPolynomial R` by a monic `q : CPolynomial R`. -/ -def divModByMonicAux [Field R] (p : CPolynomial R) (q : CPolynomial R) : - CPolynomial R × CPolynomial R := - go (p.size - q.size) p q -where - go : Nat → CPolynomial R → CPolynomial R → CPolynomial R × CPolynomial R - | 0, p, _ => ⟨0, p⟩ - | n+1, p, q => - let k := p.size - q.size -- k should equal n, this is technically unneeded - let q' := C p.leadingCoeff * (q * X.pow k) - let p' := (p - q').trim - let (e, f) := go n p' q - -- p' = q * e + f - -- Thus p = p' + q' = q * e + f + p.leadingCoeff * q * X^n - -- = q * (e + p.leadingCoeff * X^n) + f - ⟨e + C p.leadingCoeff * X^k, f⟩ - -/-- Division of `p : CPolynomial R` by a monic `q : CPolynomial R`. -/ -def divByMonic [Field R] (p : CPolynomial R) (q : CPolynomial R) : - CPolynomial R := - (divModByMonicAux p q).1 - -/-- Modulus of `p : CPolynomial R` by a monic `q : CPolynomial R`. -/ -def modByMonic [Field R] (p : CPolynomial R) (q : CPolynomial R) : - CPolynomial R := - (divModByMonicAux p q).2 - -/-- Division of two `CPolynomial`s. -/ -def div [Field R] (p q : CPolynomial R) : CPolynomial R := - (C (q.leadingCoeff)⁻¹ • p).divByMonic (C (q.leadingCoeff)⁻¹ * q) - -/-- Modulus of two `CPolynomial`s. -/ -def mod [Field R] (p q : CPolynomial R) : CPolynomial R := - (C (q.leadingCoeff)⁻¹ • p).modByMonic (C (q.leadingCoeff)⁻¹ * q) - -instance [Field R] : Div (CPolynomial R) := ⟨CPolynomial.div⟩ - -instance [Field R] : Mod (CPolynomial R) := ⟨CPolynomial.mod⟩ - -/-- Pseudo-division of a `CPolynomial` by `X`, which shifts all non-constant coefficients -to the left by one. -/ -def divX (p : CPolynomial R) : CPolynomial R := p.extract 1 p.size - -variable (p q r : CPolynomial R) - --- some helper lemmas to characterize p + q - -lemma matchSize_size_eq {p q : CPolynomial Q} : - let (p', q') := Array.matchSize p q 0 - p'.size = q'.size := by - change (Array.rightpad _ _ _).size = (Array.rightpad _ _ _).size - rw [Array.size_rightpad, Array.size_rightpad] - omega - -lemma matchSize_size {p q : CPolynomial Q} : - let (p', _) := Array.matchSize p q 0 - p'.size = max p.size q.size := by - change (Array.rightpad _ _ _).size = max (Array.size _) (Array.size _) - rw [Array.size_rightpad] - omega - -lemma zipWith_size {R} {f : R → R → R} {a b : Array R} (h : a.size = b.size) : - (Array.zipWith f a b).size = a.size := by - simp; omega - --- TODO we could generalize the next few lemmas to matchSize + zipWith f for any f - -theorem add_size {p q : CPolynomial Q} : (add_raw p q).size = max p.size q.size := by - change (Array.zipWith _ _ _ ).size = max p.size q.size - rw [zipWith_size matchSize_size_eq, matchSize_size] - --- coeff on list concatenations -lemma concat_coeff₁ (i : ℕ) : i < p.size → - (p ++ q).coeff i = p.coeff i := by - simp - grind - -lemma concat_coeff₂ (i : ℕ) : i ≥ p.size → - (p ++ q).coeff i = q.coeff (i - p.size) := by - simp - grind - -theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : - (add_raw p q)[i] = p.coeff i + q.coeff i -:= by - simp [add_raw] - sorry - --- unfold List.matchSize - -- repeat rw [List.rightpad_getElem_eq_getD] - -- simp only [List.getD_eq_getElem?_getD, Array.getElem?_eq_toList] - -theorem add_coeff? (p q : CPolynomial Q) (i : ℕ) : - (add_raw p q).coeff i = p.coeff i + q.coeff i -:= by - rcases (Nat.lt_or_ge i (add_raw p q).size) with h_lt | h_ge - · rw [← add_coeff h_lt]; simp [h_lt] - have h_lt' : i ≥ max p.size q.size := by rwa [← add_size] - have h_p : i ≥ p.size := by omega - have h_q : i ≥ q.size := by omega - simp [h_ge, h_p, h_q] - -lemma add_equiv_raw [LawfulBEq R] (p q : CPolynomial R) : Trim.equiv (p.add q) (p.add_raw q) := by - unfold Trim.equiv add - exact Trim.coeff_eq_coeff (p.add_raw q) - -def smul_equiv : ∀ (i : ℕ) (r : R), - (smul r p).coeff i = r * (p.coeff i) := by - intro i r - unfold smul mk coeff - rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] - -def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), - (nsmul_raw n p).trim.coeff i = n * p.trim.coeff i := by - intro n i - unfold nsmul_raw - repeat rw [Trim.coeff_eq_coeff] - unfold mk - rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] - -lemma mulPowX_equiv₁ : ∀ (i j : ℕ), j ≥ i → - (mulPowX i p).coeff j = p.coeff (j - i) := by - intro i j h - unfold mulPowX mk - rw [concat_coeff₂ (Array.replicate i 0) p j] - . simp - have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp - rw [← h_size i] - simp - exact h - -lemma mulPowX_equiv₂ : ∀ (i j : ℕ), j < i → - (mulPowX i p).coeff j = 0 := by - intro i j h - unfold mulPowX mk - rw [concat_coeff₁ (Array.replicate i 0) p j] - . simp - grind - have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp - rw [← h_size i] - simp - exact h - -omit [BEq R] in -lemma neg_coeff : ∀ (p : CPolynomial R) (i : ℕ), p.neg.coeff i = - p.coeff i := by - intro p i - unfold neg coeff - rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] - -lemma trim_add_trim [LawfulBEq R] (p q : CPolynomial R) : p.trim + q = p + q := by - apply Trim.eq_of_equiv - intro i - rw [add_coeff?, add_coeff?, Trim.coeff_eq_coeff] - --- algebra theorems about addition - -omit [Ring Q] in -@[simp] theorem zero_def : (0 : CPolynomial Q) = #[] := rfl - -theorem add_comm : p + q = q + p := by - apply congrArg trim - ext - · simp only [add_size]; omega - · simp only [add_coeff] - apply _root_.add_comm - -def canonical (p : CPolynomial R) := p.trim = p - -theorem zero_canonical : (0 : CPolynomial R).trim = 0 := Trim.canonical_empty - -theorem zero_add (hp : p.canonical) : 0 + p = p := by - rw (occs := .pos [2]) [← hp] - apply congrArg trim - ext <;> simp [add_size, add_coeff, *] - -theorem add_zero (hp : p.canonical) : p + 0 = p := by - rw [add_comm, zero_add p hp] - -theorem add_assoc [LawfulBEq R] : p + q + r = p + (q + r) := by - change (add_raw p q).trim + r = p + (add_raw q r).trim - rw [trim_add_trim, add_comm p, trim_add_trim, add_comm _ p] - apply congrArg trim - ext i - · simp only [add_size]; omega - · simp only [add_coeff, add_coeff?] - apply _root_.add_assoc - -theorem nsmul_zero [LawfulBEq R] (p : CPolynomial R) : nsmul 0 p = 0 := by - suffices (nsmul_raw 0 p).last_nonzero = none by simp [nsmul, trim, *] - apply Trim.last_nonzero_none - intros; unfold nsmul_raw - simp only [Nat.cast_zero, zero_mul, Array.getElem_map] - -theorem nsmul_raw_succ (n : ℕ) (p : CPolynomial Q) : - nsmul_raw (n + 1) p = add_raw (nsmul_raw n p) p := by - unfold nsmul_raw - ext - · simp [add_size] - next i _ hi => - simp [add_size] at hi - simp [add_coeff, hi] - rw [_root_.add_mul (R:=Q) n 1 p[i], one_mul] - -theorem nsmul_succ [LawfulBEq R] (n : ℕ) {p : CPolynomial R} : nsmul (n + 1) p = nsmul n p + p := by - unfold nsmul - rw [trim_add_trim] - apply congrArg trim - apply nsmul_raw_succ - -theorem neg_trim [LawfulBEq R] (p : CPolynomial R) : p.trim = p → (-p).trim = -p := by - apply Trim.non_zero_map - simp - -theorem neg_add_cancel [LawfulBEq R] (p : CPolynomial R) : -p + p = 0 := by - rw [← zero_canonical] - apply Trim.eq_of_equiv; unfold Trim.equiv; intro i - rw [add_coeff?] - rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi, Neg.neg, neg] - -end Operations - -namespace OperationsC - --- additive group on CPolynomialC -variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - -variable (p q r : CPolynomialC R) - -instance : Add (CPolynomialC R) where - add p q := ⟨p.val + q.val, by apply Trim.trim_twice⟩ - -theorem add_comm : p + q = q + p := by - apply CPolynomialC.ext; apply CPolynomial.add_comm - -theorem add_assoc : p + q + r = p + (q + r) := by - apply CPolynomialC.ext; apply CPolynomial.add_assoc - -instance : Zero (CPolynomialC R) := ⟨0, zero_canonical⟩ - -theorem zero_add : 0 + p = p := by - apply CPolynomialC.ext - apply CPolynomial.zero_add p.val p.prop - -theorem add_zero : p + 0 = p := by - apply CPolynomialC.ext - apply CPolynomial.add_zero p.val p.prop - -def nsmul (n : ℕ) (p : CPolynomialC R) : CPolynomialC R := - ⟨CPolynomial.nsmul n p.val, by apply Trim.trim_twice⟩ - -theorem nsmul_zero : nsmul 0 p = 0 := by - apply CPolynomialC.ext; apply CPolynomial.nsmul_zero - -theorem nsmul_succ (n : ℕ) (p : CPolynomialC R) : nsmul (n + 1) p = nsmul n p + p := by - apply CPolynomialC.ext; apply CPolynomial.nsmul_succ - -instance : Neg (CPolynomialC R) where - neg p := ⟨-p.val, neg_trim p.val p.prop⟩ - -instance : Sub (CPolynomialC R) where - sub p q := p + -q - -theorem neg_add_cancel : -p + p = 0 := by - apply CPolynomialC.ext - apply CPolynomial.neg_add_cancel - -instance [LawfulBEq R] : AddCommGroup (CPolynomialC R) where - add_assoc := add_assoc - zero_add := zero_add - add_zero := add_zero - add_comm := add_comm - neg_add_cancel := neg_add_cancel - nsmul := nsmul -- TODO do we actually need this custom implementation? - nsmul_zero := nsmul_zero - nsmul_succ := nsmul_succ - zsmul := zsmulRec - --- TODO do we want a custom efficient implementation? - --- TODO: define `SemiRing` structure on `CPolynomialC` - -end OperationsC - -section ToPoly - -/-- Convert a `CPolynomial` to a (mathlib) `Polynomial`. -/ -noncomputable def toPoly (p : CPolynomial R) : Polynomial R := - p.eval₂ Polynomial.C Polynomial.X - -/-- a more low-level and direct definition of `toPoly`; currently unused. -/ -noncomputable def toPoly' (p : CPolynomial R) : Polynomial R := - Polynomial.ofFinsupp (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 - )) - -noncomputable def CPolynomialC.toPoly (p : CPolynomialC R) : Polynomial R := p.val.toPoly - -alias ofPoly := Polynomial.toImpl - -/-- evaluation stays the same after converting to mathlib -/ -theorem eval_toPoly_eq_eval (x : Q) (p : CPolynomial Q) : p.toPoly.eval x = p.eval x := by - unfold toPoly eval eval₂ - rw [← Array.foldl_hom (Polynomial.eval x) - (g₁ := fun acc (t : Q × ℕ) ↦ acc + Polynomial.C t.1 * Polynomial.X ^ t.2) - (g₂ := fun acc (a, i) ↦ acc + a * x ^ i) ] - · congr; exact Polynomial.eval_zero - simp - -/-- characterize `p.toPoly` by showing that its coefficients are exactly the coefficients of `p` -/ -lemma coeff_toPoly {p : CPolynomial Q} {n : ℕ} : p.toPoly.coeff n = p.coeff n := by - unfold toPoly eval₂ - - let f := fun (acc: Q[X]) ((a,i): Q × ℕ) ↦ acc + Polynomial.C a * Polynomial.X ^ i - change (Array.foldl f 0 p.zipIdx).coeff n = p.coeff n - - -- we slightly weaken the goal, to use `Array.foldl_induction` - let motive (size: ℕ) (acc: Q[X]) := acc.coeff n = if (n < size) then p.coeff n else 0 - - have zipIdx_size : p.zipIdx.size = p.size := by simp [Array.zipIdx] - - suffices h : motive p.zipIdx.size (Array.foldl f 0 p.zipIdx) by - rw [h, ite_eq_left_iff, zipIdx_size] - intro hn - replace hn : n ≥ p.size := by linarith - rw [coeff, Array.getD_eq_getD_getElem?, Array.getElem?_eq_none hn, Option.getD_none] - - apply Array.foldl_induction motive - · change motive 0 0 - simp [motive] - - change ∀ (i : Fin p.zipIdx.size) acc, motive i acc → motive (i + 1) (f acc p.zipIdx[i]) - unfold motive f - intros i acc h - have i_lt_p : i < p.size := by linarith [i.is_lt] - have : p.zipIdx[i] = (p[i], ↑i) := by simp [Array.getElem_zipIdx] - rw [this, coeff_add, coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, h] - rcases (Nat.lt_trichotomy i n) with hlt | rfl | hgt - · have h1 : ¬ (n < i) := by linarith - have h2 : ¬ (n = i) := by linarith - have h3 : ¬ (n < i + 1) := by linarith - simp [h1, h2, h3] - · simp [i_lt_p] - · have h1 : ¬ (n = i) := by linarith - have h2 : n < i + 1 := by linarith - simp [hgt, h1, h2] - -/-- helper lemma, to argue about `toImpl` by cases -/ -lemma toImpl_elim (p : Q[X]) : - (p = 0 ∧ p.toImpl = #[]) - ∨ (p ≠ 0 ∧ p.toImpl = .ofFn (fun i : Fin (p.natDegree + 1) => p.coeff i)) := by - unfold toImpl - by_cases hbot : p.degree = ⊥ - · left - use degree_eq_bot.mp hbot - rw [hbot] - right - use degree_ne_bot.mp hbot - have hnat : p.degree = p.natDegree := degree_eq_natDegree (degree_ne_bot.mp hbot) - simp [hnat] - -/-- `toImpl` is a right-inverse of `toPoly`. - that is, the round-trip starting from a mathlib polynomial gets us back to where we were. - in particular, `toPoly` is surjective and `toImpl` is injective. -/ -theorem toPoly_toImpl {p : Q[X]} : p.toImpl.toPoly = p := by - ext n - rw [coeff_toPoly] - rcases toImpl_elim p with ⟨rfl, h⟩ | ⟨_, h⟩ - · simp [h] - rw [h] - by_cases h : n < p.natDegree + 1 - · simp [h] - simp only [Array.getD_eq_getD_getElem?, Array.getElem?_ofFn] - simp only [h, reduceDIte, Option.getD_none] - replace h := Nat.lt_of_succ_le (not_lt.mp h) - symm - exact coeff_eq_zero_of_natDegree_lt h - -/-- `CPolynomial` addition is mapped to `Polynomial` addition -/ -theorem toPoly_add {p q : CPolynomial Q} : (add_raw p q).toPoly = p.toPoly + q.toPoly := by - ext n - rw [coeff_add, coeff_toPoly, coeff_toPoly, coeff_toPoly, add_coeff?] - -/-- trimming doesn't change the `toPoly` image -/ -lemma toPoly_trim [LawfulBEq R] {p : CPolynomial R} : p.trim.toPoly = p.toPoly := by - ext n - rw [coeff_toPoly, coeff_toPoly, Trim.coeff_eq_coeff] - -/-- helper lemma to be able to state the next lemma -/ -lemma toImpl_nonzero {p : Q[X]} (hp : p ≠ 0) : p.toImpl.size > 0 := by - rcases toImpl_elim p with ⟨rfl, _⟩ | ⟨_, h⟩ - · contradiction - suffices h : p.toImpl ≠ #[] from Array.size_pos_iff.mpr h - simp [h] - -/-- helper lemma: the last entry of the `CPolynomial` obtained by `toImpl` is just the `leadingCoeff` -/ -lemma getLast_toImpl {p : Q[X]} (hp : p ≠ 0) : let h : p.toImpl.size > 0 := toImpl_nonzero hp; - p.toImpl[p.toImpl.size - 1] = p.leadingCoeff := by - rcases toImpl_elim p with ⟨rfl, _⟩ | ⟨_, h⟩ - · contradiction - simp [h] - -/-- `toImpl` maps to canonical `CPolynomial`s -/ -theorem trim_toImpl [LawfulBEq R] (p : R[X]) : p.toImpl.trim = p.toImpl := by - rcases toImpl_elim p with ⟨rfl, h⟩ | ⟨h_nz, _⟩ - · rw [h, Trim.canonical_empty] - rw [Trim.canonical_iff] - unfold Array.getLast - intro - rw [getLast_toImpl h_nz] - exact Polynomial.leadingCoeff_ne_zero.mpr h_nz - -/-- on canonical `CPolynomial`s, `toImpl` is also a left-inverse of `toPoly`. - in particular, `toPoly` is a bijection from `CPolynomialC` to `Polynomial`. -/ -lemma toImpl_toPoly_of_canonical [LawfulBEq R] (p : CPolynomialC R) : p.toPoly.toImpl = p := by - -- we will change something slightly more general: `toPoly` is injective on canonical polynomials - suffices h_inj : ∀ q : CPolynomialC R, p.toPoly = q.toPoly → p = q by - have : p.toPoly = p.toPoly.toImpl.toPoly := by rw [toPoly_toImpl] - exact h_inj ⟨ p.toPoly.toImpl, trim_toImpl p.toPoly ⟩ this |> congrArg Subtype.val |>.symm - intro q hpq - apply CPolynomialC.ext - apply Trim.canonical_ext p.property q.property - intro i - rw [← coeff_toPoly, ← coeff_toPoly] - exact hpq |> congrArg (fun p => p.coeff i) - -/-- the roundtrip to and from mathlib maps a `CPolynomial` to its trimmed/canonical representative -/ -theorem toImpl_toPoly [LawfulBEq R] (p : CPolynomial R) : p.toPoly.toImpl = p.trim := by - rw [← toPoly_trim] - exact toImpl_toPoly_of_canonical ⟨ p.trim, Trim.trim_twice p⟩ - -/-- evaluation stays the same after converting a mathlib `Polynomial` to a `CPolynomial` -/ -theorem eval_toImpl_eq_eval [LawfulBEq R] (x : R) (p : R[X]) : p.toImpl.eval x = p.eval x := by - rw [← toPoly_toImpl (p := p), toImpl_toPoly, ← toPoly_trim, eval_toPoly_eq_eval] - -/-- corollary: evaluation stays the same after trimming -/ -lemma eval_trim_eq_eval [LawfulBEq R] (x : R) (p : CPolynomial R) : p.trim.eval x = p.eval x := by - rw [← toImpl_toPoly, eval_toImpl_eq_eval, eval_toPoly_eq_eval] - -end ToPoly - -section Equiv - -open Trim - -/-- Reflexivity of the equivalence relation. -/ -@[simp] theorem equiv_refl (p : CPolynomial Q) : equiv p p := - by simp [equiv] - -/-- Symmetry of the equivalence relation. -/ -@[simp] theorem equiv_symm {p q : CPolynomial Q} : equiv p q → equiv q p := by - simp [equiv] - intro h i - exact Eq.symm (h i) - -/-- Transitivity of the equivalence relation. -/ -@[simp] theorem equiv_trans {p q r : CPolynomial Q} : Trim.equiv p q → equiv q r → equiv p r := by - simp_all [Trim.equiv] - -/-- The `CPolynomial.equiv` is indeed an equivalence relation. -/ -instance instEquivalenceEquiv : Equivalence (equiv (R := R)) where - refl := equiv_refl - symm := equiv_symm - trans := equiv_trans - -/-- The `Setoid` instance for `CPolynomial R` induced by `CPolynomial.equiv`. -/ -instance instSetoidCPolynomial : Setoid (CPolynomial R) where - r := equiv - iseqv := instEquivalenceEquiv - -/-- The quotient of `CPolynomial R` by `CPolynomial.equiv`. This will be changen to be equivalent to - `Polynomial R`. -/ -def QuotientCPolynomial (R : Type*) [Ring R] [BEq R] := Quotient (@instSetoidCPolynomial R _) - --- operations on `CPolynomial` descend to `QuotientCPolynomial` -namespace QuotientCPolynomial - -/- Aristotle failed to find a proof. -/ --- lemma mul_comm [LawfulBEq R] (a b : CPolynomial R) : --- a.mul b = b.mul a - -lemma mul_comm_equiv [LawfulBEq R] (a b : CPolynomial R) : - a.mul b ≈ b.mul a := by sorry - -#check Array.foldl_induction - -#check Polynomial R - -lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), - ∀ (q : CPolynomial R) (m l : ℕ), - l + m = n → - p.mul^[n] q = p.mul^[m] (p.mul^[l] q) := by - intro p n - induction n with - | zero => - intro q m l h_sizes - rw [Nat.add_eq_zero_iff] at h_sizes - obtain ⟨hl, hm⟩ := h_sizes - rw [hl, hm] - simp - | succ n₀ ih => - intro q m l h_sizes - cases l with - | zero => - simp at h_sizes - rw [h_sizes] - simp - | succ l₀ => - have h_sizes_simp : l₀ + m = n₀ := by linarith - clear h_sizes - simp - rw [ih (p.mul q) m l₀ h_sizes_simp] - -noncomputable section AristotleLemmas - -/- -Scalar multiplication by 0 is equivalent to the zero polynomial. --/ -lemma CompPoly.CPolynomial.smul_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CompPoly.CPolynomial R) : - CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.smul 0 p) 0 := by - -- By definition of scalar multiplication, multiplying by 0 results in the zero polynomial. - have h_smul_zero : ∀ (p : CPolynomial R), (smul 0 p).coeff = 0 := by - intro p; ext i; simp [CompPoly.CPolynomial.smul]; - cases p[i]? <;> simp +decide; - exact fun i => by simpa using congr_fun ( h_smul_zero p ) i; - -/- -Addition of polynomials respects equivalence. --/ -lemma CompPoly.CPolynomial.add_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (p1 p2 q1 q2 : CompPoly.CPolynomial R) - (hp : CompPoly.CPolynomial.Trim.equiv p1 p2) - (hq : CompPoly.CPolynomial.Trim.equiv q1 q2) : - CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.add p1 q1) (CompPoly.CPolynomial.add p2 q2) := by - -- By `add_equiv_raw`, `add p1 q1` is equivalent to `add_raw p1 q1`, and similarly for `p2, q2`. - have h_add_equiv_raw : ∀ p q : CompPoly.CPolynomial R, Trim.equiv (p.add q) (p.add_raw q) := by - exact?; - -- By `add_coeff?`, we have `(add_raw p1 q1).coeff i = p1.coeff i + q1.coeff i` and `(add_raw p2 q2).coeff i = p2.coeff i + q2.coeff i`. - have h_add_coeff : ∀ i, (p1.add_raw q1).coeff i = p1.coeff i + q1.coeff i ∧ (p2.add_raw q2).coeff i = p2.coeff i + q2.coeff i := by - exact fun i => ⟨ add_coeff? p1 q1 i, add_coeff? p2 q2 i ⟩; - simp_all +decide [ Trim.equiv ] - -/- -Multiplication by X^i respects equivalence. --/ -lemma CompPoly.CPolynomial.mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (i : ℕ) (p q : CompPoly.CPolynomial R) (h : CompPoly.CPolynomial.Trim.equiv p q) : - CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mulPowX i p) (CompPoly.CPolynomial.mulPowX i q) := by - unfold CompPoly.CPolynomial.Trim.equiv at *; - simp +zetaDelta at *; - intro j; by_cases hj : j < i <;> simp_all +decide [ CompPoly.CPolynomial.mulPowX ] ; - · unfold CompPoly.CPolynomial.mk; rw [ Array.getElem?_append, Array.getElem?_append ] ; aesop; - · convert h ( j - i ) using 1 <;> rw [ Array.getElem?_append ] <;> simp +decide [ hj ]; - · rw [ if_neg ( not_lt_of_ge hj ) ]; - · rw [ if_neg ( not_lt_of_ge hj ) ] - -/- -Adding a polynomial equivalent to zero acts as the identity. --/ -lemma CompPoly.CPolynomial.add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (p q : CompPoly.CPolynomial R) (hq : CompPoly.CPolynomial.Trim.equiv q 0) : - CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.add p q) p := by - intro x; - have := add_coeff? p q x; - have hq_zero : q.coeff x = 0 := by - exact hq x; - unfold CompPoly.CPolynomial.add; - rw [ Trim.coeff_eq_coeff ] ; aesop - -/- -Multiplying the zero polynomial by X^i results in a polynomial equivalent to zero. --/ -lemma CompPoly.CPolynomial.mulPowX_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (i : ℕ) : CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mulPowX i (0 : CompPoly.CPolynomial R)) 0 := by - unfold CompPoly.CPolynomial.Trim.equiv; - simp [CompPoly.CPolynomial.coeff]; - unfold CompPoly.CPolynomial.mulPowX; - grind - -/- -Definition of a single step in the polynomial multiplication algorithm. --/ -def CompPoly.CPolynomial.mul_step {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (q : CompPoly.CPolynomial R) (acc : CompPoly.CPolynomial R) (x : R × ℕ) : CompPoly.CPolynomial R := - acc.add ((CompPoly.CPolynomial.smul x.1 q).mulPowX x.2) - -/- -The multiplication step respects equivalence of the accumulator. --/ -lemma CompPoly.CPolynomial.mul_step_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (q : CompPoly.CPolynomial R) (acc1 acc2 : CompPoly.CPolynomial R) (x : R × ℕ) - (h : CompPoly.CPolynomial.Trim.equiv acc1 acc2) : - CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mul_step q acc1 x) (CompPoly.CPolynomial.mul_step q acc2 x) := by - apply_rules [ CompPoly.CPolynomial.add_equiv, CompPoly.CPolynomial.mulPowX_equiv, CompPoly.CPolynomial.smul_equiv ] - -/- -The multiplication step with a zero coefficient acts as the identity modulo equivalence. --/ -lemma CompPoly.CPolynomial.mul_step_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (q : CompPoly.CPolynomial R) (acc : CompPoly.CPolynomial R) (i : ℕ) : - CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mul_step q acc (0, i)) acc := by - -- By definition of `mul_step`, we have `mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i)`. - have h_mul_step : CompPoly.CPolynomial.mul_step q acc (0, i) = acc.add ((CompPoly.CPolynomial.smul 0 q).mulPowX i) := by - exact?; - -- By definition of `mulPowX`, we have `mulPowX i (smul 0 q) = smul 0 (mulPowX i q)`. - have h_mulPowX : CompPoly.CPolynomial.mulPowX i (CompPoly.CPolynomial.smul 0 q) = CompPoly.CPolynomial.smul 0 (CompPoly.CPolynomial.mulPowX i q) := by - unfold CompPoly.CPolynomial.mulPowX CompPoly.CPolynomial.smul; aesop; - rw [ h_mul_step, h_mulPowX ]; - exact add_zero_equiv _ _ ( smul_zero_equiv _ ) - -/- -Folding `mul_step` over a list of zero coefficients preserves equivalence. --/ -lemma CompPoly.CPolynomial.foldl_mul_step_zeros {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (q : CompPoly.CPolynomial R) (acc : CompPoly.CPolynomial R) (l : List (R × ℕ)) - (hl : ∀ x ∈ l, x.1 = 0) : - CompPoly.CPolynomial.Trim.equiv (l.foldl (CompPoly.CPolynomial.mul_step q) acc) acc := by - induction' l using List.reverseRecOn with x xs ih generalizing acc; - · exact fun _ => rfl; - · simp_all +decide [ List.foldl_append ]; - -- By the properties of the multiplication step and the induction hypothesis, we can conclude the proof. - have h_mul_step : CompPoly.CPolynomial.Trim.equiv (CompPoly.CPolynomial.mul_step q (List.foldl (CompPoly.CPolynomial.QuotientCPolynomial.CompPoly.CPolynomial.mul_step q) acc x) xs) (List.foldl (CompPoly.CPolynomial.QuotientCPolynomial.CompPoly.CPolynomial.mul_step q) acc x) := by - convert mul_step_zero q ( List.foldl ( CompPoly.CPolynomial.QuotientCPolynomial.CompPoly.CPolynomial.mul_step q ) acc x ) xs.2 using 1; - specialize hl _ _ ( Or.inr rfl ) ; aesop; - exact? - -/- -The `zipIdx` of a polynomial is the `zipIdx` of its trim followed by a list of zero coefficients. --/ -lemma CompPoly.CPolynomial.zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (p : CompPoly.CPolynomial R) : - ∃ l, p.zipIdx.toList = p.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by - -- Let `n` be `p.trim.size`. `p.trim` is the prefix of `p` of length `n`. - set n := p.trim.size with hn_def; - by_cases hn : n = 0; - · unfold n at hn; - -- Since `p.trim` is empty, `p` must be the zero polynomial. - have hp_zero : ∀ i (hi : i < p.size), p[i] = 0 := by - have := Trim.elim p; aesop; - use List.map (fun i => (0, i)) (List.range p.size); - simp +decide [ hp_zero ]; - refine' List.ext_get _ _ <;> aesop; - · -- Since `n` is not zero, `p.last_nonzero` is `some k` and `n = k + 1`. - obtain ⟨k, hk⟩ : ∃ k : Fin p.size, p.trim = p.extract 0 (k.val + 1) ∧ p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by - have := Trim.elim p; - aesop; - refine' ⟨ _, _, _ ⟩; - exact ( Array.zipIdx p ).toList.drop ( k + 1 ); - · rw [ hk.1 ]; - refine' List.ext_get _ _ <;> simp +decide [ List.get ]; - · rw [ min_eq_left ( by linarith [ Fin.is_lt k ] ), add_tsub_cancel_of_le ( by linarith [ Fin.is_lt k ] ) ]; - · intro n h₁ h₂; rw [ List.getElem_append ] ; simp +decide [ h₁, h₂ ] ; - grind; - · simp +decide [ List.mem_iff_get ]; - intro a; specialize hk; have := hk.2.2 ( k + 1 + a ) ; simp_all +decide [ Nat.add_assoc ] ; - -end AristotleLemmas - -lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : - a.mul b ≈ a.trim.mul b := by - have h_zipIdx_split : ∃ l, a.zipIdx.toList = a.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by - exact?; - obtain ⟨l, hl⟩ := h_zipIdx_split; - have h_foldl_split : ∃ acc, (a.mul b) = (l.foldl (CompPoly.CPolynomial.mul_step b) acc) ∧ (a.trim.mul b) = acc := by - -- By definition of `mul`, we can rewrite `a.mul b` using `mul_step` and the foldl operation. - have h_mul_def : a.mul b = (a.zipIdx.toList.foldl (CompPoly.CPolynomial.mul_step b) (CompPoly.CPolynomial.C 0)) := by - unfold CompPoly.CPolynomial.mul; - exact?; - have h_mul_def_trim : a.trim.mul b = (a.trim.zipIdx.toList.foldl (CompPoly.CPolynomial.mul_step b) (CompPoly.CPolynomial.C 0)) := by - unfold CompPoly.CPolynomial.mul; - exact?; - aesop; - obtain ⟨ acc, h₁, h₂ ⟩ := h_foldl_split; - exact h₁.symm ▸ h₂.symm ▸ CompPoly.CPolynomial.foldl_mul_step_zeros b acc l hl.2 - -lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : - equiv a₁ a₂ → a₁.mul b ≈ a₂.mul b := by - intro h - calc - a₁.mul b ≈ a₁.trim.mul b := mul_trim_equiv a₁ b - _ ≈ a₂.trim.mul b := by rw [eq_of_equiv h] - _ ≈ a₂.mul b := equiv_symm (mul_trim_equiv a₂ b) - --- Addition: add descends to `QuotientCPolynomial` -def add_descending (p q : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (add p q) - -lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : - equiv a₁ a₂ → equiv b₁ b₂ → add_descending a₁ b₁ = add_descending a₂ b₂ := by - intros heq_a heq_b - unfold add_descending - rw [Quotient.eq] - simp [instSetoidCPolynomial] - calc - add a₁ b₁ ≈ add_raw a₁ b₁ := add_equiv_raw a₁ b₁ - _ ≈ add_raw a₂ b₂ := by - intro i - rw [add_coeff? a₁ b₁ i, add_coeff? a₂ b₂ i, heq_a i, heq_b i] - _ ≈ add a₂ b₂ := equiv_symm (add_equiv_raw a₂ b₂) - -@[inline, specialize] -def add {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := - Quotient.lift₂ add_descending add_descends p q - --- Scalar multiplication: smul descends to `QuotientCPolynomial` -def smul_descending (r : R) (p : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (smul r p) - -lemma smul_descends [LawfulBEq R] (r : R) (p₁ p₂ : CPolynomial R) : - equiv p₁ p₂ → smul_descending r p₁ = smul_descending r p₂ := by - unfold equiv smul_descending - intro heq - rw [Quotient.eq] - simp [instSetoidCPolynomial] - intro i - rw [smul_equiv p₁, smul_equiv p₂] - rw [heq i] - -@[inline, specialize] -def smul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (r : R) (p : QuotientCPolynomial R) - : QuotientCPolynomial R := - Quotient.lift (smul_descending r) (smul_descends r) p - --- Scalar multiplication: nsmul_raw descends to `QuotientCPolynomial` -def nsmul_descending (n : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (nsmul n p) - -lemma nsmul_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : - equiv p₁ p₂ → nsmul_descending n p₁ = nsmul_descending n p₂ := by - unfold equiv - intro heq - unfold nsmul_descending - rw [Quotient.eq] - simp [instSetoidCPolynomial] - unfold nsmul equiv - intro i - repeat rw [nsmul_raw_equiv, coeff_eq_coeff] - rw [heq i] - -@[inline, specialize] -def nsmul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : QuotientCPolynomial R) - : QuotientCPolynomial R := - Quotient.lift (nsmul_descending n) (nsmul_descends n) p - --- Negation: neg descends to `QuotientCPolynomial` -def neg_descending (p : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (neg p) - -lemma neg_descends (a b : CPolynomial R) : equiv a b → neg_descending a = neg_descending b := by - unfold equiv neg_descending - intros heq - rw [Quotient.eq] - simp [instSetoidCPolynomial] - unfold equiv - intro i - rw [neg_coeff a i, neg_coeff b i, heq i] - -@[inline, specialize] -def neg {R : Type*} [Ring R] [BEq R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := - Quotient.lift neg_descending neg_descends p - --- Subtraction: sub descends to `QuotientCPolynomial` -def sub_descending (p q : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (sub p q) - -lemma sub_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : - equiv a₁ a₂ → equiv b₁ b₂ → sub_descending a₁ b₁ = sub_descending a₂ b₂ := by - unfold equiv sub_descending - intros heq_a heq_b - rw [Quotient.eq] - simp [instSetoidCPolynomial] - unfold sub equiv - calc - a₁.add b₁.neg ≈ a₁.add_raw b₁.neg := add_equiv_raw a₁ b₁.neg - _ ≈ a₂.add_raw b₂.neg := by - intro i - rw [add_coeff? a₁ b₁.neg i, add_coeff? a₂ b₂.neg i] - rw [neg_coeff b₁ i, neg_coeff b₂ i, heq_a i, heq_b i] - _ ≈ a₂.add b₂.neg := equiv_symm (add_equiv_raw a₂ b₂.neg) - -@[inline, specialize] -def sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := - Quotient.lift₂ sub_descending sub_descends p q - --- Multiplication by `X ^ i`: mulPowX descends to `QuotientCPolynomial` -def mulPowX_descending (i : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (mulPowX i p) - -lemma mulPowX_descends (i : ℕ) (p₁ p₂ : CPolynomial R) : - equiv p₁ p₂ → mulPowX_descending i p₁ = mulPowX_descending i p₂ := by - unfold equiv - intro heq - unfold mulPowX_descending - rw [Quotient.eq] - simp [instSetoidCPolynomial] - intro j - by_cases h : j ≥ i - . rw [mulPowX_equiv₁ p₁ i j h, mulPowX_equiv₁ p₂ i j h] - rw [heq] - . simp at h - rw [mulPowX_equiv₂ p₁ i j h, mulPowX_equiv₂ p₂ i j h] - -@[inline, specialize] -def mulPowX {R : Type*} [Ring R] [BEq R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := - Quotient.lift (mulPowX_descending i) (mulPowX_descends i) p - --- Multiplication of a `CPolynomial` by `X`, reduces to `mulPowX 1`. -@[inline, specialize] -def mulX (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 - --- Multiplication: mul descends to `QuotientPoly` -def mul_descending (p q : CPolynomial R) : QuotientCPolynomial R := - Quotient.mk _ (mul p q) - -lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : - equiv a₁ a₂ → equiv b₁ b₂ → mul_descending a₁ b₁ = mul_descending a₂ b₂ := by - unfold mul_descending - intros heq_a heq_b - rw [Quotient.eq] - simp [instSetoidCPolynomial] - calc - a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a - _ ≈ b₁.mul a₂ := mul_comm_equiv a₂ b₁ - _ ≈ b₂.mul a₂ := mul_equiv b₁ b₂ a₂ heq_b - _ ≈ a₂.mul b₂ := mul_comm_equiv b₂ a₂ - -@[inline, specialize] -def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := - Quotient.lift₂ mul_descending mul_descends p q - --- Exponentiation: pow descends to `QuotientCPolynomial` -def pow_descending (p : CPolynomial R) (n : ℕ) : QuotientCPolynomial R := - Quotient.mk _ (pow p n) - -lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : - equiv p₁ p₂ → pow_descending p₁ n = pow_descending p₂ n := by - intro heq - unfold pow_descending - rw [Quotient.eq] - simp [instSetoidCPolynomial] - unfold pow - have mul_pow_equiv : ∀ (p : CPolynomial R) (n : ℕ), - p.mul^[n + 1] (C 1) ≈ p.mul (p.mul^[n] (C 1)) := by - intro p n - rw [mul_pow_assoc p (n + 1) (C 1) 1 n] - . simp - simp - induction n with - | zero => simp - | succ n ih => - calc - p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_equiv p₁ n - _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := mul_comm_equiv p₁ (p₁.mul^[n] (C 1)) - _ ≈ (p₂.mul^[n] (C 1)).mul p₁ := mul_equiv _ _ p₁ ih - _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_comm_equiv (p₂.mul^[n] (C 1)) p₁ - _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq - _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_equiv p₂ n) - -@[inline, specialize] -def pow {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := - Quotient.lift (fun p => pow_descending p n) (pow_descends n) p - --- TODO div? - -end QuotientCPolynomial - -end Equiv - -namespace Lagrange - -end Lagrange - -end CPolynomial - -end CompPoly From abd0c55c0c8741b59e40601ad7157e7530ae9ed4 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 6 Jan 2026 11:52:12 +0000 Subject: [PATCH 06/11] feat: eliminate last sorrys, but avoided proving commutativity of multiplication after the quotient --- CompPoly/Univariate/Basic.lean | 38 +++++++++++++++++++++------------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 452f897..95c01a0 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -1133,9 +1133,9 @@ lemma zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] refine' List.ext_get _ _ <;> simp +decide [ List.get ]; · rw [ min_eq_left ( by linarith [ Fin.is_lt k ] ), add_tsub_cancel_of_le ( by linarith [ Fin.is_lt k ] ) ]; · intro n h₁ h₂; rw [ List.getElem_append ] ; simp +decide [ h₁, h₂ ] ; - grind; + grind · simp +decide [ List.mem_iff_get ]; - intro a; specialize hk; have := hk.2.2 ( k + 1 + a ) ; simp_all +decide [ Nat.add_assoc ] ; + intro a; specialize hk; have := hk.2.2 ( k + 1 + a ) ; simp_all +decide [ Nat.add_assoc ] lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : a.mul b ≈ a.trim.mul b := by @@ -1162,12 +1162,26 @@ lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : _ ≈ a₂.trim.mul b := by rw [eq_of_equiv h] _ ≈ a₂.mul b := equiv_symm (mul_trim_equiv a₂ b) --- TODO? --- lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial R) : --- b₁ ≈ b₂ → a.mul b₁ ≈ a.mul b₂ - -lemma mul_comm_equiv [LawfulBEq R] (a b : CPolynomial R) : - a.mul b ≈ b.mul a := by sorry +lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial R) : + b₁ ≈ b₂ → a.mul b₁ ≈ a.mul b₂ := by + -- By definition of multiplication, we can express `a.mul b₁` and `a.mul b₂` in terms of their sums of products of coefficients. + have h_mul_def : ∀ (a b : CompPoly.CPolynomial R), a.mul b = (a.zipIdx.foldl (fun acc ⟨a', i⟩ => acc.add ((smul a' b).mulPowX i)) (C 0)) := by + exact?; + intro h; + have h_foldl_equiv : ∀ (l : List (R × ℕ)) (acc : CompPoly.CPolynomial R), (List.foldl (fun acc (a', i) => acc.add ((smul a' b₁).mulPowX i)) acc l) ≈ (List.foldl (fun acc (a', i) => acc.add ((smul a' b₂).mulPowX i)) acc l) := by + intro l acc; + induction' l using List.reverseRecOn with l ih generalizing acc; + · rfl; + · simp +zetaDelta at *; + -- Apply the add_equiv lemma to the foldl results and the mulPowX terms. + apply add_equiv; + · exact?; + · -- Apply the lemma that multiplying by X^i preserves equivalence. + apply mulPowX_equiv; + exact fun i => by rw [ smul_equiv, smul_equiv ] ; exact congr_arg _ ( h i ) ; + convert h_foldl_equiv ( Array.toList ( Array.zipIdx a ) ) ( CompPoly.CPolynomial.C 0 ) using 1; + · grind + · grind end EquivalenceLemmas @@ -1310,9 +1324,7 @@ lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : simp [instSetoidCPolynomial] calc a₁.mul b₁ ≈ a₂.mul b₁ := mul_equiv a₁ a₂ b₁ heq_a - _ ≈ b₁.mul a₂ := mul_comm_equiv a₂ b₁ - _ ≈ b₂.mul a₂ := mul_equiv b₁ b₂ a₂ heq_b - _ ≈ a₂.mul b₂ := mul_comm_equiv b₂ a₂ + _ ≈ a₂.mul b₂ := mul_equiv₂ a₂ b₁ b₂ heq_b @[inline, specialize] def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := @@ -1340,9 +1352,7 @@ lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : | succ n ih => calc p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_equiv p₁ n - _ ≈ (p₁.mul^[n] (C 1)).mul p₁ := mul_comm_equiv p₁ (p₁.mul^[n] (C 1)) - _ ≈ (p₂.mul^[n] (C 1)).mul p₁ := mul_equiv _ _ p₁ ih - _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_comm_equiv (p₂.mul^[n] (C 1)) p₁ + _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_equiv₂ p₁ _ _ ih _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_equiv p₂ n) From ce5bc8fbe80097ae42ef37887c356e6211694ff4 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 6 Jan 2026 12:02:02 +0000 Subject: [PATCH 07/11] fix: remove extraneous files there by mistake --- CompPoly/.DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 CompPoly/.DS_Store diff --git a/CompPoly/.DS_Store b/CompPoly/.DS_Store deleted file mode 100644 index 8455f972ed6317f53df22d1225ba9246c4ada9d2..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeHKyK2Kg5Zp~%n7C2t@_xa8a0ulKjC%(hOd!Z$V%MttUHLT6J_r$V3Kwb2EbPwR z-p&b4q1B3rwx``nq!E!h+)yqSre^2n6MM>x0^zvhO^)(`_$BX?>e~t9zQ{&;@Xo*a z=k>AwJoNjx`!<PUgD#rGhvt(tClvLk Date: Tue, 6 Jan 2026 15:48:10 +0000 Subject: [PATCH 08/11] chore: clean up proofs, make them more robust to future changes, deal with linter warnings --- CompPoly/Univariate/Basic.lean | 175 +++++++++++++++++---------------- 1 file changed, 90 insertions(+), 85 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 95c01a0..e31cb99 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -575,11 +575,13 @@ theorem add_size {p q : CPolynomial Q} : (add_raw p q).size = max p.size q.size rw [zipWith_size matchSize_size_eq, matchSize_size] -- coeff on list concatenations +omit [BEq R] in lemma concat_coeff₁ (i : ℕ) : i < p.size → - (p ++ q).coeff i = p.coeff i := by simp ; grind + (p ++ q).coeff i = p.coeff i := by simp; grind +omit [BEq R] in lemma concat_coeff₂ (i : ℕ) : i ≥ p.size → - (p ++ q).coeff i = q.coeff (i - p.size) := by simp ; grind + (p ++ q).coeff i = q.coeff (i - p.size) := by simp; grind theorem add_coeff {p q : CPolynomial Q} {i : ℕ} (hi : i < (add_raw p q).size) : (add_raw p q)[i] = p.coeff i + q.coeff i @@ -615,6 +617,7 @@ def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), unfold mk rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] +omit [BEq R] in lemma mulPowX_equiv₁ : ∀ (i j : ℕ), j ≥ i → (mulPowX i p).coeff j = p.coeff (j - i) := by intro i j h @@ -626,6 +629,7 @@ lemma mulPowX_equiv₁ : ∀ (i j : ℕ), j ≥ i → simp exact h +omit [BEq R] in lemma mulPowX_equiv₂ : ∀ (i j : ℕ), j < i → (mulPowX i p).coeff j = 0 := by intro i j h @@ -1002,11 +1006,10 @@ Scalar multiplication by 0 is equivalent to the zero polynomial. -/ lemma smul_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (smul 0 p) ≈ 0 := by - -- By definition of scalar multiplication, multiplying by 0 results in the zero polynomial. have h_smul_zero : ∀ (p : CPolynomial R), (smul 0 p).coeff = 0 := by - intro p; ext i; simp [CPolynomial.smul]; - cases p[i]? <;> simp +decide; - exact fun i => by simpa using congr_fun ( h_smul_zero p ) i; + intro p; ext i; simp [smul] + cases p[i]? <;> simp + exact fun i => by simpa using congr_fun ( h_smul_zero p ) i /- Addition of polynomials respects equivalence. @@ -1015,26 +1018,26 @@ lemma add_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p1 p2 q1 q2 : CPolynomial R) (hp : equiv p1 p2) (hq : equiv q1 q2) : equiv (p1.add q1) (p2.add q2) := by - -- By `add_equiv_raw`, `add p1 q1` is equivalent to `add_raw p1 q1`, and similarly for `p2, q2`. have h_add_equiv_raw : ∀ p q : CPolynomial R, equiv (p.add q) (p.add_raw q) := by - exact? - -- By `add_coeff?`, we have `(add_raw p1 q1).coeff i = p1.coeff i + q1.coeff i` and `(add_raw p2 q2).coeff i = p2.coeff i + q2.coeff i`. - have h_add_coeff : ∀ i, (p1.add_raw q1).coeff i = p1.coeff i + q1.coeff i ∧ (p2.add_raw q2).coeff i = p2.coeff i + q2.coeff i := by + exact fun p q => add_equiv_raw p q + have h_add_coeff : ∀ i, + (p1.add_raw q1).coeff i = p1.coeff i + q1.coeff i ∧ (p2.add_raw q2).coeff i = p2.coeff i + q2.coeff i := by exact fun i => ⟨ add_coeff? p1 q1 i, add_coeff? p2 q2 i ⟩ - simp_all +decide [ equiv ] + simp_all [ equiv ] /- Multiplication by X^i respects equivalence. -/ lemma mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (i : ℕ) (p q : CPolynomial R) (h : equiv p q) : - equiv (CPolynomial.mulPowX i p) (CPolynomial.mulPowX i q) := by - unfold equiv at *; - simp +zetaDelta at *; - intro j; by_cases hj : j < i <;> simp_all +decide [ CPolynomial.mulPowX ] ; - · unfold CPolynomial.mk; rw [ Array.getElem?_append, Array.getElem?_append ] ; aesop; - · convert h ( j - i ) using 1 <;> rw [ Array.getElem?_append ] <;> simp +decide [ hj ]; - · rw [ if_neg ( not_lt_of_ge hj ) ]; + equiv (mulPowX i p) (mulPowX i q) := by + unfold equiv at * + simp +zetaDelta at * + intro j + by_cases hj : j < i <;> simp_all +decide [ mulPowX ] + · unfold mk; rw [ Array.getElem?_append, Array.getElem?_append ]; aesop + · convert h ( j - i ) using 1 <;> rw [ Array.getElem?_append ] <;> simp +decide [ hj ] + · rw [ if_neg ( not_lt_of_ge hj ) ] · rw [ if_neg ( not_lt_of_ge hj ) ] /- @@ -1042,22 +1045,23 @@ Adding a polynomial equivalent to zero acts as the identity. -/ lemma add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (hq : equiv q 0) : - equiv (CPolynomial.add p q) p := by - intro x; - have := add_coeff? p q x; + equiv (add p q) p := by + intro x + have := add_coeff? p q x have hq_zero : q.coeff x = 0 := by - exact hq x; - unfold CPolynomial.add; - rw [ Trim.coeff_eq_coeff ] ; aesop + exact hq x + unfold add + rw [ coeff_eq_coeff ] + aesop /- Multiplying the zero polynomial by X^i results in a polynomial equivalent to zero. -/ lemma mulPowX_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] - (i : ℕ) : equiv (CPolynomial.mulPowX i (0 : CPolynomial R)) 0 := by - unfold equiv; - simp [CPolynomial.coeff]; - unfold CPolynomial.mulPowX; + (i : ℕ) : equiv (mulPowX i (0 : CPolynomial R)) 0 := by + unfold equiv + simp [coeff] + unfold mulPowX grind /- @@ -1065,7 +1069,7 @@ Definition of a single step in the polynomial multiplication algorithm. -/ def mul_step {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (q : CPolynomial R) (acc : CPolynomial R) (x : R × ℕ) : CPolynomial R := - acc.add ((CPolynomial.smul x.1 q).mulPowX x.2) + acc.add ((smul x.1 q).mulPowX x.2) /- The multiplication step respects equivalence of the accumulator. @@ -1074,7 +1078,7 @@ lemma mul_step_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (q : CPolynomial R) (acc1 acc2 : CPolynomial R) (x : R × ℕ) (h : equiv acc1 acc2) : equiv (mul_step q acc1 x) (mul_step q acc2 x) := by - apply_rules [ add_equiv, mulPowX_equiv, CPolynomial.smul_equiv ] + apply_rules [ add_equiv, mulPowX_equiv, smul_equiv ] /- The multiplication step with a zero coefficient acts as the identity modulo equivalence. @@ -1082,13 +1086,10 @@ The multiplication step with a zero coefficient acts as the identity modulo equi lemma mul_step_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (q : CPolynomial R) (acc : CPolynomial R) (i : ℕ) : equiv (mul_step q acc (0, i)) acc := by - -- By definition of `mul_step`, we have `mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i)`. - have h_mul_step : mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i) := by - exact?; - -- By definition of `mulPowX`, we have `mulPowX i (smul 0 q) = smul 0 (mulPowX i q)`. - have h_mulPowX : CPolynomial.mulPowX i (CPolynomial.smul 0 q) = CPolynomial.smul 0 (CPolynomial.mulPowX i q) := by - unfold CPolynomial.mulPowX CPolynomial.smul; aesop; - rw [ h_mul_step, h_mulPowX ]; + have h_mul_step : mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i) := by exact rfl + have h_mulPowX : mulPowX i (smul 0 q) = smul 0 (mulPowX i q) := by + unfold mulPowX smul; aesop + rw [ h_mul_step, h_mulPowX ] exact add_zero_equiv _ _ ( smul_zero_equiv _ ) /- @@ -1098,14 +1099,15 @@ lemma foldl_mul_step_zeros {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (q : CPolynomial R) (acc : CPolynomial R) (l : List (R × ℕ)) (hl : ∀ x ∈ l, x.1 = 0) : equiv (l.foldl (mul_step q) acc) acc := by - induction' l using List.reverseRecOn with x xs ih generalizing acc; - · exact fun _ => rfl; - · simp_all +decide [ List.foldl_append ]; - -- By the properties of the multiplication step and the induction hypothesis, we can conclude the proof. + induction' l using List.reverseRecOn with x xs ih generalizing acc + · exact fun _ => rfl + · simp_all +decide [ List.foldl_append ] + -- use the multiplication step and the induction hypothesis have h_mul_step : equiv (mul_step q (List.foldl (mul_step q) acc x) xs) (List.foldl (mul_step q) acc x) := by - convert mul_step_zero q ( List.foldl ( mul_step q ) acc x ) xs.2 using 1; - specialize hl _ _ ( Or.inr rfl ) ; aesop; - exact? + convert mul_step_zero q ( List.foldl ( mul_step q ) acc x ) xs.2 using 1 + specialize hl _ _ ( Or.inr rfl ) + aesop + exact equiv_trans h_mul_step (ih acc) /- The `zipIdx` of a polynomial is the `zipIdx` of its trim followed by a list of zero coefficients. @@ -1114,44 +1116,44 @@ lemma zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : ∃ l, p.zipIdx.toList = p.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by -- Let `n` be `p.trim.size`. `p.trim` is the prefix of `p` of length `n`. - set n := p.trim.size with hn_def; - by_cases hn : n = 0; - · unfold n at hn; + set n := p.trim.size with hn_def + by_cases hn : n = 0 + · unfold n at hn -- Since `p.trim` is empty, `p` must be the zero polynomial. have hp_zero : ∀ i (hi : i < p.size), p[i] = 0 := by - have := Trim.elim p; aesop; - use List.map (fun i => (0, i)) (List.range p.size); - simp +decide [ hp_zero ]; - refine' List.ext_get _ _ <;> aesop; + have := Trim.elim p; aesop + use List.map (fun i => (0, i)) (List.range p.size) + simp + refine' List.ext_get _ _ <;> aesop · -- Since `n` is not zero, `p.last_nonzero` is `some k` and `n = k + 1`. obtain ⟨k, hk⟩ : ∃ k : Fin p.size, p.trim = p.extract 0 (k.val + 1) ∧ p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by - have := Trim.elim p; - aesop; - refine' ⟨ _, _, _ ⟩; - exact ( Array.zipIdx p ).toList.drop ( k + 1 ); - · rw [ hk.1 ]; - refine' List.ext_get _ _ <;> simp +decide [ List.get ]; - · rw [ min_eq_left ( by linarith [ Fin.is_lt k ] ), add_tsub_cancel_of_le ( by linarith [ Fin.is_lt k ] ) ]; - · intro n h₁ h₂; rw [ List.getElem_append ] ; simp +decide [ h₁, h₂ ] ; + have := Trim.elim p + aesop + refine' ⟨ _, _, _ ⟩ + exact ( Array.zipIdx p ).toList.drop ( k + 1 ) + · rw [ hk.1 ] + refine' List.ext_get _ _ <;> simp + · rw [ min_eq_left ( by linarith [ Fin.is_lt k ] ), add_tsub_cancel_of_le ( by linarith [ Fin.is_lt k ] ) ] + · intro n h₁ h₂; rw [ List.getElem_append ]; simp +decide [ h₁ ] grind - · simp +decide [ List.mem_iff_get ]; - intro a; specialize hk; have := hk.2.2 ( k + 1 + a ) ; simp_all +decide [ Nat.add_assoc ] + · simp +decide [ List.mem_iff_get ] + intro a; specialize hk; have := hk.2.2 ( k + 1 + a ); simp_all +decide [ Nat.add_assoc ] lemma mul_trim_equiv [LawfulBEq R] (a b : CPolynomial R) : a.mul b ≈ a.trim.mul b := by have h_zipIdx_split : ∃ l, a.zipIdx.toList = a.trim.zipIdx.toList ++ l ∧ ∀ x ∈ l, x.1 = 0 := by - exact?; - obtain ⟨l, hl⟩ := h_zipIdx_split; + exact zipIdx_trim_append a + obtain ⟨l, hl⟩ := h_zipIdx_split have h_foldl_split : ∃ acc, (a.mul b) = (l.foldl (mul_step b) acc) ∧ (a.trim.mul b) = acc := by -- By definition of `mul`, we can rewrite `a.mul b` using `mul_step` and the foldl operation. - have h_mul_def : a.mul b = (a.zipIdx.toList.foldl (mul_step b) (CPolynomial.C 0)) := by - unfold CPolynomial.mul; - exact?; - have h_mul_def_trim : a.trim.mul b = (a.trim.zipIdx.toList.foldl (mul_step b) (CPolynomial.C 0)) := by - unfold CPolynomial.mul; - exact?; - aesop; - obtain ⟨ acc, h₁, h₂ ⟩ := h_foldl_split; + have h_mul_def : a.mul b = (a.zipIdx.toList.foldl (mul_step b) (C 0)) := by + unfold mul + exact Eq.symm (Array.foldl_toList (mul_step b)) + have h_mul_def_trim : a.trim.mul b = (a.trim.zipIdx.toList.foldl (mul_step b) (C 0)) := by + unfold mul + exact Eq.symm (Array.foldl_toList (mul_step b)) + aesop + obtain ⟨ acc, h₁, h₂ ⟩ := h_foldl_split exact h₁.symm ▸ h₂.symm ▸ foldl_mul_step_zeros b acc l hl.2 lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : @@ -1164,22 +1166,25 @@ lemma mul_equiv [LawfulBEq R] (a₁ a₂ b : CPolynomial R) : lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial R) : b₁ ≈ b₂ → a.mul b₁ ≈ a.mul b₂ := by - -- By definition of multiplication, we can express `a.mul b₁` and `a.mul b₂` in terms of their sums of products of coefficients. - have h_mul_def : ∀ (a b : CompPoly.CPolynomial R), a.mul b = (a.zipIdx.foldl (fun acc ⟨a', i⟩ => acc.add ((smul a' b).mulPowX i)) (C 0)) := by - exact?; - intro h; - have h_foldl_equiv : ∀ (l : List (R × ℕ)) (acc : CompPoly.CPolynomial R), (List.foldl (fun acc (a', i) => acc.add ((smul a' b₁).mulPowX i)) acc l) ≈ (List.foldl (fun acc (a', i) => acc.add ((smul a' b₂).mulPowX i)) acc l) := by - intro l acc; - induction' l using List.reverseRecOn with l ih generalizing acc; - · rfl; - · simp +zetaDelta at *; + -- By definition of multiplication, we can express `a.mul b₁` and `a.mul b₂` in terms of + -- their sums of products of coefficients. + have h_mul_def : ∀ (a b : CompPoly.CPolynomial R), + a.mul b = (a.zipIdx.foldl (fun acc ⟨a', i⟩ => acc.add ((smul a' b).mulPowX i)) (C 0)) := by exact fun a b => rfl + intro h + have h_foldl_equiv : ∀ (l : List (R × ℕ)) (acc : CompPoly.CPolynomial R), + List.foldl (fun acc (a', i) => acc.add ((smul a' b₁).mulPowX i)) acc l ≈ + List.foldl (fun acc (a', i) => acc.add ((smul a' b₂).mulPowX i)) acc l := by + intro l acc + induction' l using List.reverseRecOn with l ih generalizing acc + · rfl + · simp +zetaDelta at * -- Apply the add_equiv lemma to the foldl results and the mulPowX terms. - apply add_equiv; - · exact?; + apply add_equiv + · expose_names; exact h_1 acc · -- Apply the lemma that multiplying by X^i preserves equivalence. - apply mulPowX_equiv; - exact fun i => by rw [ smul_equiv, smul_equiv ] ; exact congr_arg _ ( h i ) ; - convert h_foldl_equiv ( Array.toList ( Array.zipIdx a ) ) ( CompPoly.CPolynomial.C 0 ) using 1; + apply mulPowX_equiv + exact fun i => by rw [ smul_equiv, smul_equiv ]; exact congr_arg _ ( h i ) + convert h_foldl_equiv ( Array.toList ( Array.zipIdx a ) ) ( C 0 ) using 1 · grind · grind From 930f1f743e43375ffdb2801b8045adb7553d017a Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 6 Jan 2026 15:52:53 +0000 Subject: [PATCH 09/11] chore: more cleanup --- CompPoly/Univariate/Basic.lean | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index e31cb99..55dbe0e 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -635,12 +635,10 @@ lemma mulPowX_equiv₂ : ∀ (i j : ℕ), j < i → intro i j h unfold mulPowX mk rw [concat_coeff₁ (Array.replicate i 0) p j] - . simp - grind + . simp; grind have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp rw [← h_size i] - simp - exact h + simp; exact h omit [BEq R] in lemma neg_coeff : ∀ (p : CPolynomial R) (i : ℕ), p.neg.coeff i = - p.coeff i := by @@ -1032,7 +1030,6 @@ lemma mulPowX_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (i : ℕ) (p q : CPolynomial R) (h : equiv p q) : equiv (mulPowX i p) (mulPowX i q) := by unfold equiv at * - simp +zetaDelta at * intro j by_cases hj : j < i <;> simp_all +decide [ mulPowX ] · unfold mk; rw [ Array.getElem?_append, Array.getElem?_append ]; aesop @@ -1048,8 +1045,7 @@ lemma add_zero_equiv {R : Type*} [Ring R] [BEq R] [LawfulBEq R] equiv (add p q) p := by intro x have := add_coeff? p q x - have hq_zero : q.coeff x = 0 := by - exact hq x + have hq_zero : q.coeff x = 0 := by exact hq x unfold add rw [ coeff_eq_coeff ] aesop @@ -1087,8 +1083,7 @@ lemma mul_step_zero {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (q : CPolynomial R) (acc : CPolynomial R) (i : ℕ) : equiv (mul_step q acc (0, i)) acc := by have h_mul_step : mul_step q acc (0, i) = acc.add ((smul 0 q).mulPowX i) := by exact rfl - have h_mulPowX : mulPowX i (smul 0 q) = smul 0 (mulPowX i q) := by - unfold mulPowX smul; aesop + have h_mulPowX : mulPowX i (smul 0 q) = smul 0 (mulPowX i q) := by unfold mulPowX smul; aesop rw [ h_mul_step, h_mulPowX ] exact add_zero_equiv _ _ ( smul_zero_equiv _ ) @@ -1126,9 +1121,9 @@ lemma zipIdx_trim_append {R : Type*} [Ring R] [BEq R] [LawfulBEq R] simp refine' List.ext_get _ _ <;> aesop · -- Since `n` is not zero, `p.last_nonzero` is `some k` and `n = k + 1`. - obtain ⟨k, hk⟩ : ∃ k : Fin p.size, p.trim = p.extract 0 (k.val + 1) ∧ p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by - have := Trim.elim p - aesop + obtain ⟨k, hk⟩ : ∃ k : Fin p.size, + p.trim = p.extract 0 (k.val + 1) ∧ p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0) := by + have := Trim.elim p; aesop refine' ⟨ _, _, _ ⟩ exact ( Array.zipIdx p ).toList.drop ( k + 1 ) · rw [ hk.1 ] From d6db16a25519324c0b7548d56b6831f0cd2eca1e Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 7 Jan 2026 12:07:59 +0000 Subject: [PATCH 10/11] fix: some minor touch ups --- CompPoly/Univariate/Basic.lean | 38 ++++++++++++++-------------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index 55dbe0e..b7d6c9b 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -999,6 +999,10 @@ lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), simp rw [ih (p.mul q) m l₀ h_sizes_simp] +lemma mul_pow_succ (p q : CPolynomial R) (n : ℕ): + p.mul^[n + 1] q = p.mul (p.mul^[n] q) := by + rw [mul_pow_assoc p (n+1) q 1 n] <;> simp + /- Scalar multiplication by 0 is equivalent to the zero polynomial. -/ @@ -1170,8 +1174,7 @@ lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial R) : List.foldl (fun acc (a', i) => acc.add ((smul a' b₁).mulPowX i)) acc l ≈ List.foldl (fun acc (a', i) => acc.add ((smul a' b₂).mulPowX i)) acc l := by intro l acc - induction' l using List.reverseRecOn with l ih generalizing acc - · rfl + induction' l using List.reverseRecOn with l ih generalizing acc; rfl · simp +zetaDelta at * -- Apply the add_equiv lemma to the foldl results and the mulPowX terms. apply add_equiv @@ -1179,9 +1182,7 @@ lemma mul_equiv₂ [LawfulBEq R] (a b₁ b₂ : CPolynomial R) : · -- Apply the lemma that multiplying by X^i preserves equivalence. apply mulPowX_equiv exact fun i => by rw [ smul_equiv, smul_equiv ]; exact congr_arg _ ( h i ) - convert h_foldl_equiv ( Array.toList ( Array.zipIdx a ) ) ( C 0 ) using 1 - · grind - · grind + convert h_foldl_equiv ( Array.toList ( Array.zipIdx a ) ) ( C 0 ) using 1 <;> grind end EquivalenceLemmas @@ -1217,8 +1218,7 @@ lemma smul_descends [LawfulBEq R] (r : R) (p₁ p₂ : CPolynomial R) : rw [Quotient.eq] simp [instSetoidCPolynomial] intro i - rw [smul_equiv p₁, smul_equiv p₂] - rw [heq i] + rw [smul_equiv, smul_equiv, heq i] @[inline, specialize] def smul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (r : R) (p : QuotientCPolynomial R) @@ -1292,17 +1292,14 @@ def mulPowX_descending (i : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := lemma mulPowX_descends (i : ℕ) (p₁ p₂ : CPolynomial R) : equiv p₁ p₂ → mulPowX_descending i p₁ = mulPowX_descending i p₂ := by - unfold equiv + unfold equiv mulPowX_descending intro heq - unfold mulPowX_descending rw [Quotient.eq] simp [instSetoidCPolynomial] intro j - by_cases h : j ≥ i - . rw [mulPowX_equiv₁ p₁ i j h, mulPowX_equiv₁ p₂ i j h] - rw [heq] - . simp at h - rw [mulPowX_equiv₂ p₁ i j h, mulPowX_equiv₂ p₂ i j h] + by_cases h : j ≥ i <;> simp at h + . rw [mulPowX_equiv₁ p₁ i j h, mulPowX_equiv₁ p₂ i j h, heq] + . rw [mulPowX_equiv₂ p₁ i j h, mulPowX_equiv₂ p₂ i j h] @[inline, specialize] def mulPowX {R : Type*} [Ring R] [BEq R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := @@ -1327,7 +1324,7 @@ lemma mul_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial R) : _ ≈ a₂.mul b₂ := mul_equiv₂ a₂ b₁ b₂ heq_b @[inline, specialize] -def mul {R : Type} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := +def mul {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : QuotientCPolynomial R := Quotient.lift₂ mul_descending mul_descends p q -- Exponentiation: pow descends to `QuotientCPolynomial` @@ -1341,20 +1338,17 @@ lemma pow_descends [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial R) : rw [Quotient.eq] simp [instSetoidCPolynomial] unfold pow - have mul_pow_equiv : ∀ (p : CPolynomial R) (n : ℕ), + have mul_pow_succ_equiv (p : CPolynomial R) (n : ℕ): p.mul^[n + 1] (C 1) ≈ p.mul (p.mul^[n] (C 1)) := by - intro p n - rw [mul_pow_assoc p (n + 1) (C 1) 1 n] - . simp - simp + rw [mul_pow_succ] induction n with | zero => simp | succ n ih => calc - p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_equiv p₁ n + p₁.mul^[n + 1] (C 1) ≈ p₁.mul (p₁.mul^[n] (C 1)) := mul_pow_succ_equiv p₁ n _ ≈ p₁.mul (p₂.mul^[n] (C 1)) := mul_equiv₂ p₁ _ _ ih _ ≈ p₂.mul (p₂.mul^[n] (C 1)) := mul_equiv _ _ (p₂.mul^[n] (C 1)) heq - _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_equiv p₂ n) + _ ≈ p₂.mul^[n + 1] (C 1) := equiv_symm (mul_pow_succ_equiv p₂ n) @[inline, specialize] def pow {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : QuotientCPolynomial R) (n : ℕ) : QuotientCPolynomial R := From 8e82cc87fa45dadc0892e853aed8f8c6d4b8dd75 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Thu, 8 Jan 2026 10:33:31 +0000 Subject: [PATCH 11/11] fix: stylistic changes, proof simplification from review bot --- CompPoly/Univariate/Basic.lean | 96 +++++++++++++--------------------- 1 file changed, 36 insertions(+), 60 deletions(-) diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean index b7d6c9b..02ff039 100644 --- a/CompPoly/Univariate/Basic.lean +++ b/CompPoly/Univariate/Basic.lean @@ -603,13 +603,14 @@ lemma add_equiv_raw [LawfulBEq R] (p q : CPolynomial R) : Trim.equiv (p.add q) ( unfold Trim.equiv add exact Trim.coeff_eq_coeff (p.add_raw q) -def smul_equiv : ∀ (i : ℕ) (r : R), +omit [BEq R] in +lemma smul_equiv : ∀ (i : ℕ) (r : R), (smul r p).coeff i = r * (p.coeff i) := by intro i r unfold smul mk coeff rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] -def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), +lemma nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), (nsmul_raw n p).trim.coeff i = n * p.trim.coeff i := by intro n i unfold nsmul_raw @@ -617,28 +618,34 @@ def nsmul_raw_equiv [LawfulBEq R] : ∀ (n i : ℕ), unfold mk rcases (Nat.lt_or_ge i p.size) with hi | hi <;> simp [hi] -omit [BEq R] in -lemma mulPowX_equiv₁ : ∀ (i j : ℕ), j ≥ i → - (mulPowX i p).coeff j = p.coeff (j - i) := by - intro i j h - unfold mulPowX mk - rw [concat_coeff₂ (Array.replicate i 0) p j] - . simp - have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp - rw [← h_size i] - simp - exact h +lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), + ∀ (q : CPolynomial R) (m l : ℕ), + l + m = n → + p.mul^[n] q = p.mul^[m] (p.mul^[l] q) := by + intro p n + induction n with + | zero => + intro q m l h_sizes + rw [Nat.add_eq_zero_iff] at h_sizes + obtain ⟨hl, hm⟩ := h_sizes + rw [hl, hm] + simp + | succ n₀ ih => + intro q m l h_sizes + cases l with + | zero => + simp at h_sizes + rw [h_sizes] + simp + | succ l₀ => + have h_sizes_simp : l₀ + m = n₀ := by linarith + clear h_sizes + simp + rw [ih (p.mul q) m l₀ h_sizes_simp] -omit [BEq R] in -lemma mulPowX_equiv₂ : ∀ (i j : ℕ), j < i → - (mulPowX i p).coeff j = 0 := by - intro i j h - unfold mulPowX mk - rw [concat_coeff₁ (Array.replicate i 0) p j] - . simp; grind - have h_size : ∀ i : ℕ, (Array.replicate i 0).size = i := by simp - rw [← h_size i] - simp; exact h +lemma mul_pow_succ (p q : CPolynomial R) (n : ℕ): + p.mul^[n + 1] q = p.mul (p.mul^[n] q) := by + rw [mul_pow_assoc p (n+1) q 1 n] <;> simp omit [BEq R] in lemma neg_coeff : ∀ (p : CPolynomial R) (i : ℕ), p.neg.coeff i = - p.coeff i := by @@ -974,35 +981,6 @@ namespace QuotientCPolynomial section EquivalenceLemmas -lemma mul_pow_assoc : ∀ (p : CPolynomial R) (n : ℕ), - ∀ (q : CPolynomial R) (m l : ℕ), - l + m = n → - p.mul^[n] q = p.mul^[m] (p.mul^[l] q) := by - intro p n - induction n with - | zero => - intro q m l h_sizes - rw [Nat.add_eq_zero_iff] at h_sizes - obtain ⟨hl, hm⟩ := h_sizes - rw [hl, hm] - simp - | succ n₀ ih => - intro q m l h_sizes - cases l with - | zero => - simp at h_sizes - rw [h_sizes] - simp - | succ l₀ => - have h_sizes_simp : l₀ + m = n₀ := by linarith - clear h_sizes - simp - rw [ih (p.mul q) m l₀ h_sizes_simp] - -lemma mul_pow_succ (p q : CPolynomial R) (n : ℕ): - p.mul^[n + 1] q = p.mul (p.mul^[n] q) := by - rw [mul_pow_assoc p (n+1) q 1 n] <;> simp - /- Scalar multiplication by 0 is equivalent to the zero polynomial. -/ @@ -1290,24 +1268,22 @@ def sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) def mulPowX_descending (i : ℕ) (p : CPolynomial R) : QuotientCPolynomial R := Quotient.mk _ (mulPowX i p) -lemma mulPowX_descends (i : ℕ) (p₁ p₂ : CPolynomial R) : +lemma mulPowX_descends [LawfulBEq R] (i : ℕ) (p₁ p₂ : CPolynomial R) : equiv p₁ p₂ → mulPowX_descending i p₁ = mulPowX_descending i p₂ := by - unfold equiv mulPowX_descending + unfold mulPowX_descending intro heq rw [Quotient.eq] simp [instSetoidCPolynomial] - intro j - by_cases h : j ≥ i <;> simp at h - . rw [mulPowX_equiv₁ p₁ i j h, mulPowX_equiv₁ p₂ i j h, heq] - . rw [mulPowX_equiv₂ p₁ i j h, mulPowX_equiv₂ p₂ i j h] + apply mulPowX_equiv; exact heq @[inline, specialize] -def mulPowX {R : Type*} [Ring R] [BEq R] (i : ℕ) (p : QuotientCPolynomial R) : QuotientCPolynomial R := +def mulPowX {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (i : ℕ) (p : QuotientCPolynomial R) + : QuotientCPolynomial R := Quotient.lift (mulPowX_descending i) (mulPowX_descends i) p -- Multiplication of a `CPolynomial` by `X`, reduces to `mulPowX 1`. @[inline, specialize] -def mulX (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 +def mulX [LawfulBEq R] (p : QuotientCPolynomial R) : QuotientCPolynomial R := p.mulPowX 1 -- Multiplication: mul descends to `QuotientPoly` def mul_descending (p q : CPolynomial R) : QuotientCPolynomial R :=