Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit da32780

Browse files
committed
chore(data/polynomial/*): create file data/polynomial/inductions and move around lemmas (#8563)
This PR is a precursor to #8463: it performs the move, without introducing lemmas and squeezes some `simp`s to make some proofs faster. I added add a doc-string to `lemma degree_pos_induction_on` with a reference to a lemma that will appear in #8463. The main reason why there are more added lines than removed ones is that the creation of a new file has a copyright statement, a module documentation and a few variable declarations.
1 parent b9e4c08 commit da32780

File tree

12 files changed

+228
-207
lines changed

12 files changed

+228
-207
lines changed

src/data/polynomial/degree/definitions.lean

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -656,6 +656,18 @@ begin
656656
refl
657657
end
658658

659+
lemma monomial_nat_degree_leading_coeff_eq_self (h : p.support.card ≤ 1) :
660+
monomial p.nat_degree p.leading_coeff = p :=
661+
begin
662+
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩,
663+
by_cases ha : a = 0;
664+
simp [ha]
665+
end
666+
667+
lemma C_mul_X_pow_eq_self (h : p.support.card ≤ 1) :
668+
C p.leading_coeff * X^p.nat_degree = p :=
669+
by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
670+
659671
lemma leading_coeff_pow' : leading_coeff p ^ n ≠ 0
660672
leading_coeff (p ^ n) = leading_coeff p ^ n :=
661673
nat.rec_on n (by simp) $

src/data/polynomial/degree/lemmas.lean

Lines changed: 0 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -49,27 +49,6 @@ else with_bot.coe_le_coe.1 $
4949
(le_nat_degree_of_ne_zero (mem_support_iff.1 hn))
5050
(nat.zero_le _))
5151

52-
lemma degree_map_eq_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
53-
(hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p :=
54-
le_antisymm (degree_map_le f _) $
55-
have hp0 : p ≠ 0, from λ hp0, by simpa [hp0, f.map_zero] using hf,
56-
begin
57-
rw [degree_eq_nat_degree hp0],
58-
refine le_degree_of_ne_zero _,
59-
rw [coeff_map], exact hf
60-
end
61-
62-
lemma nat_degree_map_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
63-
(hf : f (leading_coeff p) ≠ 0) : nat_degree (p.map f) = nat_degree p :=
64-
nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f hf)
65-
66-
lemma leading_coeff_map_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
67-
(hf : f (leading_coeff p) ≠ 0) : leading_coeff (p.map f) = f (leading_coeff p) :=
68-
begin
69-
unfold leading_coeff,
70-
rw [coeff_map, nat_degree_map_of_leading_coeff_ne_zero f hf],
71-
end
72-
7352
lemma degree_pos_of_root {p : polynomial R} (hp : p ≠ 0) (h : is_root p a) : 0 < degree p :=
7453
lt_of_not_ge $ λ hlt, begin
7554
have := eq_C_of_degree_le_zero hlt,
@@ -165,59 +144,6 @@ lemma degree_pos_of_eval₂_root {p : polynomial R} (hp : p ≠ 0) (f : R →+*
165144
0 < degree p :=
166145
nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_eval₂_root hp f hz inj)
167146

168-
section injective
169-
open function
170-
variables {f : R →+* S} (hf : injective f)
171-
include hf
172-
173-
lemma degree_map_eq_of_injective (p : polynomial R) : degree (p.map f) = degree p :=
174-
if h : p = 0 then by simp [h]
175-
else degree_map_eq_of_leading_coeff_ne_zero _
176-
(by rw [← f.map_zero]; exact mt hf.eq_iff.1
177-
(mt leading_coeff_eq_zero.1 h))
178-
179-
lemma degree_map' (p : polynomial R) :
180-
degree (p.map f) = degree p :=
181-
p.degree_map_eq_of_injective hf
182-
183-
lemma nat_degree_map' (p : polynomial R) :
184-
nat_degree (p.map f) = nat_degree p :=
185-
nat_degree_eq_of_degree_eq (degree_map' hf p)
186-
187-
lemma leading_coeff_map' (p : polynomial R) :
188-
leading_coeff (p.map f) = f (leading_coeff p) :=
189-
begin
190-
unfold leading_coeff,
191-
rw [coeff_map, nat_degree_map' hf p],
192-
end
193-
194-
lemma next_coeff_map (p : polynomial R) :
195-
(p.map f).next_coeff = f p.next_coeff :=
196-
begin
197-
unfold next_coeff,
198-
rw nat_degree_map' hf,
199-
split_ifs; simp
200-
end
201-
202-
end injective
203-
204-
section
205-
variable {f : polynomial R}
206-
207-
lemma monomial_nat_degree_leading_coeff_eq_self (h : f.support.card ≤ 1) :
208-
monomial f.nat_degree f.leading_coeff = f :=
209-
begin
210-
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩,
211-
by_cases ha : a = 0;
212-
simp [ha]
213-
end
214-
215-
lemma C_mul_X_pow_eq_self (h : f.support.card ≤ 1) :
216-
C f.leading_coeff * X^f.nat_degree = f :=
217-
by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
218-
219-
end
220-
221147
end degree
222148
end semiring
223149

src/data/polynomial/denoms_clearable.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Damiano Testa
55
-/
66
import data.polynomial.erase_lead
7+
import data.polynomial.eval
8+
79
/-!
810
# Denominators of evaluation of polynomials at ratios
911

src/data/polynomial/div.lean

Lines changed: 0 additions & 103 deletions
Original file line numberDiff line numberDiff line change
@@ -19,113 +19,10 @@ noncomputable theory
1919
open_locale classical big_operators
2020

2121
open finset
22-
2322
namespace polynomial
2423
universes u v w z
2524
variables {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}
2625

27-
section semiring
28-
variables [semiring R] {p q : polynomial R}
29-
30-
/-- `div_X p` return a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
31-
It can be used in a semiring where the usual division algorithm is not possible -/
32-
def div_X (p : polynomial R) : polynomial R :=
33-
∑ n in Ico 0 p.nat_degree, monomial n (p.coeff (n + 1))
34-
35-
@[simp] lemma coeff_div_X : (div_X p).coeff n = p.coeff (n+1) :=
36-
begin
37-
simp only [div_X, coeff_monomial, true_and, finset_sum_coeff, not_lt,
38-
Ico.mem, zero_le, finset.sum_ite_eq', ite_eq_left_iff],
39-
intro h,
40-
rw coeff_eq_zero_of_nat_degree_lt (nat.lt_succ_of_le h)
41-
end
42-
43-
lemma div_X_mul_X_add (p : polynomial R) : div_X p * X + C (p.coeff 0) = p :=
44-
ext $ by rintro ⟨_|_⟩; simp [coeff_C, nat.succ_ne_zero, coeff_mul_X]
45-
46-
@[simp] lemma div_X_C (a : R) : div_X (C a) = 0 :=
47-
ext $ λ n, by cases n; simp [div_X, coeff_C]; simp [coeff]
48-
49-
lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
50-
⟨λ h, by simpa [eq_comm, h] using div_X_mul_X_add p,
51-
λ h, by rw [h, div_X_C]⟩
52-
53-
lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
54-
ext $ by simp
55-
56-
lemma degree_div_X_lt (hp0 : p ≠ 0) : (div_X p).degree < p.degree :=
57-
by haveI := nontrivial.of_polynomial_ne hp0;
58-
calc (div_X p).degree < (div_X p * X + C (p.coeff 0)).degree :
59-
if h : degree p ≤ 0
60-
then begin
61-
have h' : C (p.coeff 0) ≠ 0, by rwa [← eq_C_of_degree_le_zero h],
62-
rw [eq_C_of_degree_le_zero h, div_X_C, degree_zero, zero_mul, zero_add],
63-
exact lt_of_le_of_ne bot_le (ne.symm (mt degree_eq_bot.1 $
64-
by simp [h'])),
65-
end
66-
else
67-
have hXp0 : div_X p ≠ 0,
68-
by simpa [div_X_eq_zero_iff, -not_le, degree_le_zero_iff] using h,
69-
have leading_coeff (div_X p) * leading_coeff X ≠ 0, by simpa,
70-
have degree (C (p.coeff 0)) < degree (div_X p * X),
71-
from calc degree (C (p.coeff 0)) ≤ 0 : degree_C_le
72-
... < 1 : dec_trivial
73-
... = degree (X : polynomial R) : degree_X.symm
74-
... ≤ degree (div_X p * X) :
75-
by rw [← zero_add (degree X), degree_mul' this];
76-
exact add_le_add
77-
(by rw [zero_le_degree_iff, ne.def, div_X_eq_zero_iff];
78-
exact λ h0, h (h0.symm ▸ degree_C_le))
79-
(le_refl _),
80-
by rw [degree_add_eq_left_of_degree_lt this];
81-
exact degree_lt_degree_mul_X hXp0
82-
... = p.degree : by rw div_X_mul_X_add
83-
84-
/-- An induction principle for polynomials, valued in Sort* instead of Prop. -/
85-
@[elab_as_eliminator] noncomputable def rec_on_horner
86-
{M : polynomial R → Sort*} : Π (p : polynomial R),
87-
M 0
88-
(Π p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a)) →
89-
(Π p, p ≠ 0 → M p → M (p * X)) →
90-
M p
91-
| p := λ M0 MC MX,
92-
if hp : p = 0 then eq.rec_on hp.symm M0
93-
else
94-
have wf : degree (div_X p) < degree p,
95-
from degree_div_X_lt hp,
96-
by rw [← div_X_mul_X_add p] at *;
97-
exact
98-
if hcp0 : coeff p 0 = 0
99-
then by rw [hcp0, C_0, add_zero];
100-
exact MX _ (λ h : div_X p = 0, by simpa [h, hcp0] using hp)
101-
(rec_on_horner _ M0 MC MX)
102-
else MC _ _ (coeff_mul_X_zero _) hcp0 (if hpX0 : div_X p = 0
103-
then show M (div_X p * X), by rw [hpX0, zero_mul]; exact M0
104-
else MX (div_X p) hpX0 (rec_on_horner _ M0 MC MX))
105-
using_well_founded {dec_tac := tactic.assumption}
106-
107-
@[elab_as_eliminator] lemma degree_pos_induction_on
108-
{P : polynomial R → Prop} (p : polynomial R) (h0 : 0 < degree p)
109-
(hC : ∀ {a}, a ≠ 0 → P (C a * X))
110-
(hX : ∀ {p}, 0 < degree p → P p → P (p * X))
111-
(hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
112-
rec_on_horner p
113-
(λ h, by rw degree_zero at h; exact absurd h dec_trivial)
114-
(λ p a _ _ ih h0,
115-
have 0 < degree p,
116-
from lt_of_not_ge (λ h, (not_lt_of_ge degree_C_le) $
117-
by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0),
118-
hadd this (ih this))
119-
(λ p _ ih h0',
120-
if h0 : 0 < degree p
121-
then hX h0 (ih h0)
122-
else by rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at *;
123-
exact hC (λ h : coeff p 0 = 0,
124-
by simpa [h, nat.not_lt_zero] using h0'))
125-
h0
126-
127-
end semiring
128-
12926
section comm_semiring
13027
variables [comm_semiring R]
13128

src/data/polynomial/erase_lead.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Damiano Testa
55
-/
6-
import data.polynomial.degree
76
import data.polynomial.degree.trailing_degree
7+
import data.polynomial.inductions
88

99
/-!
1010
# Erase the leading term of a univariate polynomial

src/data/polynomial/eval.lean

Lines changed: 43 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -389,8 +389,8 @@ eval₂_monomial _ _
389389
@[simp] lemma mul_X_comp : (p * X).comp r = p.comp r * r :=
390390
begin
391391
apply polynomial.induction_on' p,
392-
{ intros p q hp hq, simp [hp, hq, add_mul], },
393-
{ intros n b, simp [pow_succ', mul_assoc], }
392+
{ intros p q hp hq, simp only [hp, hq, add_mul, add_comp] },
393+
{ intros n b, simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp] }
394394
end
395395

396396
@[simp] lemma X_pow_comp {k : ℕ} : (X^k).comp p = p^k :=
@@ -529,14 +529,35 @@ nat_degree_le_nat_degree (degree_map_le f p)
529529
variables {f}
530530

531531
lemma map_monic_eq_zero_iff (hp : p.monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
532-
⟨ λ hfp x, calc f x = f x * f p.leading_coeff : by simp [hp]
533-
... = f x * (p.map f).coeff p.nat_degree : by { congr, apply (coeff_map _ _).symm }
534-
... = 0 : by simp [hfp],
535-
λ h, ext (λ n, by simp [h]) ⟩
532+
⟨ λ hfp x, calc f x = f x * f p.leading_coeff : by simp only [mul_one, hp.leading_coeff, f.map_one]
533+
... = f x * (p.map f).coeff p.nat_degree : congr_arg _ (coeff_map _ _).symm
534+
... = 0 : by simp only [hfp, mul_zero, coeff_zero],
535+
λ h, ext (λ n, by simp only [h, coeff_map, coeff_zero]) ⟩
536536

537537
lemma map_monic_ne_zero (hp : p.monic) [nontrivial S] : p.map f ≠ 0 :=
538538
λ h, f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)
539539

540+
lemma degree_map_eq_of_leading_coeff_ne_zero (f : R →+* S)
541+
(hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p :=
542+
le_antisymm (degree_map_le f _) $
543+
have hp0 : p ≠ 0, from leading_coeff_ne_zero.mp (λ hp0, hf (trans (congr_arg _ hp0) f.map_zero)),
544+
begin
545+
rw [degree_eq_nat_degree hp0],
546+
refine le_degree_of_ne_zero _,
547+
rw [coeff_map], exact hf
548+
end
549+
550+
lemma nat_degree_map_of_leading_coeff_ne_zero (f : R →+* S)
551+
(hf : f (leading_coeff p) ≠ 0) : nat_degree (p.map f) = nat_degree p :=
552+
nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f hf)
553+
554+
lemma leading_coeff_map_of_leading_coeff_ne_zero (f : R →+* S)
555+
(hf : f (leading_coeff p) ≠ 0) : leading_coeff (p.map f) = f (leading_coeff p) :=
556+
begin
557+
unfold leading_coeff,
558+
rw [coeff_map, nat_degree_map_of_leading_coeff_ne_zero f hf],
559+
end
560+
540561
variables (f)
541562

542563
@[simp] lemma map_ring_hom_id : map_ring_hom (ring_hom.id R) = ring_hom.id (polynomial R) :=
@@ -575,8 +596,9 @@ begin
575596
(nat_degree_map_le _ _).trans_lt (nat.lt_succ_self _),
576597
conv_lhs { rw [eval₂_eq_sum], },
577598
rw [sum_over_range' _ _ _ A],
578-
{ simp [coeff_map, eval₂_eq_sum, sum_over_range] },
579-
{ simp }
599+
{ simp only [coeff_map, eval₂_eq_sum, sum_over_range, forall_const, zero_mul, ring_hom.map_zero,
600+
function.comp_app, ring_hom.coe_comp] },
601+
{ simp only [forall_const, zero_mul, ring_hom.map_zero] }
580602
end
581603

582604
lemma eval_map (x : S) : (p.map f).eval x = p.eval₂ f x :=
@@ -588,9 +610,11 @@ lemma map_sum {ι : Type*} (g : ι → polynomial R) (s : finset ι) :
588610

589611
lemma map_comp (p q : polynomial R) : map f (p.comp q) = (map f p).comp (map f q) :=
590612
polynomial.induction_on p
591-
(by simp)
592-
(by simp {contextual := tt})
593-
(by simp [pow_succ', ← mul_assoc, polynomial.comp] {contextual := tt})
613+
(by simp only [map_C, forall_const, C_comp, eq_self_iff_true])
614+
(by simp only [map_add, add_comp, forall_const, implies_true_iff, eq_self_iff_true]
615+
{contextual := tt})
616+
(by simp only [pow_succ', ←mul_assoc, comp, forall_const, eval₂_mul_X, implies_true_iff,
617+
eq_self_iff_true, map_X, map_mul] {contextual := tt})
594618

595619
@[simp]
596620
lemma eval_zero_map (f : R →+* S) (p : polynomial R) :
@@ -602,17 +626,17 @@ lemma eval_one_map (f : R →+* S) (p : polynomial R) :
602626
(p.map f).eval 1 = f (p.eval 1) :=
603627
begin
604628
apply polynomial.induction_on' p,
605-
{ intros p q hp hq, simp [hp, hq], },
606-
{ intros n r, simp, }
629+
{ intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
630+
{ intros n r, simp only [one_pow, mul_one, eval_monomial, map_monomial] }
607631
end
608632

609633
@[simp]
610634
lemma eval_nat_cast_map (f : R →+* S) (p : polynomial R) (n : ℕ) :
611635
(p.map f).eval n = f (p.eval n) :=
612636
begin
613637
apply polynomial.induction_on' p,
614-
{ intros p q hp hq, simp [hp, hq], },
615-
{ intros n r, simp, }
638+
{ intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
639+
{ intros n r, simp only [f.map_nat_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
616640
end
617641

618642
@[simp]
@@ -621,8 +645,8 @@ lemma eval_int_cast_map {R S : Type*} [ring R] [ring S]
621645
(p.map f).eval i = f (p.eval i) :=
622646
begin
623647
apply polynomial.induction_on' p,
624-
{ intros p q hp hq, simp [hp, hq], },
625-
{ intros n r, simp, }
648+
{ intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
649+
{ intros n r, simp only [f.map_int_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
626650
end
627651

628652
end map
@@ -643,11 +667,9 @@ variables (f : R →+* S) (g : S →+* T) (p)
643667
lemma hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) :=
644668
begin
645669
apply polynomial.induction_on p; clear p,
646-
{ intros a, rw [eval₂_C, eval₂_C], refl, },
670+
{ simp only [forall_const, eq_self_iff_true, eval₂_C, ring_hom.coe_comp] },
647671
{ intros p q hp hq, simp only [hp, hq, eval₂_add, g.map_add] },
648-
{ intros n a ih,
649-
simp only [eval₂_mul, eval₂_C, eval₂_X_pow, g.map_mul, g.map_pow],
650-
refl, }
672+
{ intros n a ih, simpa only [eval₂_mul, eval₂_C, eval₂_X_pow, g.map_mul, g.map_pow] }
651673
end
652674

653675
end hom_eval₂
@@ -731,7 +753,6 @@ begin
731753
intros x,
732754
simp only [mem_support_iff],
733755
contrapose!,
734-
change p.coeff x = 0 → (map f p).coeff x = 0,
735756
rw coeff_map,
736757
intro hx,
737758
rw hx,

0 commit comments

Comments
 (0)