chore(data/polynomial/*): create file data/polynomial/inductions an…

…d 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.

src/data/polynomial/degree/definitions.lean

@@ -656,6 +656,18 @@ begin
   refl
 end
 
+lemma monomial_nat_degree_leading_coeff_eq_self (h : p.support.card ≤ 1) :
+  monomial p.nat_degree p.leading_coeff = p :=
+begin
+  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩,
+  by_cases ha : a = 0;
+  simp [ha]
+end
+
+lemma C_mul_X_pow_eq_self (h : p.support.card ≤ 1) :
+  C p.leading_coeff * X^p.nat_degree = p :=
+by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
+
 lemma leading_coeff_pow' : leading_coeff p ^ n ≠ 0 →
   leading_coeff (p ^ n) = leading_coeff p ^ n :=
 nat.rec_on n (by simp) $

src/data/polynomial/degree/lemmas.lean

@@ -49,27 +49,6 @@ else with_bot.coe_le_coe.1 $
         (le_nat_degree_of_ne_zero (mem_support_iff.1 hn))
         (nat.zero_le _))
 
-lemma degree_map_eq_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
-  (hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p :=
-le_antisymm (degree_map_le f _) $
-  have hp0 : p ≠ 0, from λ hp0, by simpa [hp0, f.map_zero] using hf,
-  begin
-    rw [degree_eq_nat_degree hp0],
-    refine le_degree_of_ne_zero _,
-    rw [coeff_map], exact hf
-  end
-
-lemma nat_degree_map_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
-  (hf : f (leading_coeff p) ≠ 0) : nat_degree (p.map f) = nat_degree p :=
-nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f hf)
-
-lemma leading_coeff_map_of_leading_coeff_ne_zero [semiring S] (f : R →+* S)
-  (hf : f (leading_coeff p) ≠ 0) : leading_coeff (p.map f) = f (leading_coeff p) :=
-begin
-  unfold leading_coeff,
-  rw [coeff_map, nat_degree_map_of_leading_coeff_ne_zero f hf],
-end
-
 lemma degree_pos_of_root {p : polynomial R} (hp : p ≠ 0) (h : is_root p a) : 0 < degree p :=
 lt_of_not_ge $ λ hlt, begin
   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 →+*
   0 < degree p :=
 nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_eval₂_root hp f hz inj)
 
-section injective
-open function
-variables {f : R →+* S} (hf : injective f)
-include hf
-
-lemma degree_map_eq_of_injective (p : polynomial R) : degree (p.map f) = degree p :=
-if h : p = 0 then by simp [h]
-else degree_map_eq_of_leading_coeff_ne_zero _
-  (by rw [← f.map_zero]; exact mt hf.eq_iff.1
-    (mt leading_coeff_eq_zero.1 h))
-
-lemma degree_map' (p : polynomial R) :
-  degree (p.map f) = degree p :=
-p.degree_map_eq_of_injective hf
-
-lemma nat_degree_map' (p : polynomial R) :
-  nat_degree (p.map f) = nat_degree p :=
-nat_degree_eq_of_degree_eq (degree_map' hf p)
-
-lemma leading_coeff_map' (p : polynomial R) :
-  leading_coeff (p.map f) = f (leading_coeff p) :=
-begin
-  unfold leading_coeff,
-  rw [coeff_map, nat_degree_map' hf p],
-end
-
-lemma next_coeff_map (p : polynomial R) :
-  (p.map f).next_coeff = f p.next_coeff :=
-begin
-  unfold next_coeff,
-  rw nat_degree_map' hf,
-  split_ifs; simp
-end
-
-end injective
-
-section
-variable {f : polynomial R}
-
-lemma monomial_nat_degree_leading_coeff_eq_self (h : f.support.card ≤ 1) :
-  monomial f.nat_degree f.leading_coeff = f :=
-begin
-  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩,
-  by_cases ha : a = 0;
-  simp [ha]
-end
-
-lemma C_mul_X_pow_eq_self (h : f.support.card ≤ 1) :
-  C f.leading_coeff * X^f.nat_degree = f :=
-by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
-
-end
-
 end degree
 end semiring
 

src/data/polynomial/denoms_clearable.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import data.polynomial.erase_lead
+import data.polynomial.eval
+
 /-!
 # Denominators of evaluation of polynomials at ratios
 

src/data/polynomial/div.lean

@@ -19,113 +19,10 @@ noncomputable theory
 open_locale classical big_operators
 
 open finset
-
 namespace polynomial
 universes u v w z
 variables {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}
 
-section semiring
-variables [semiring R] {p q : polynomial R}
-
-/-- `div_X p` return a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
-  It can be used in a semiring where the usual division algorithm is not possible -/
-def div_X (p : polynomial R) : polynomial R :=
-∑ n in Ico 0 p.nat_degree, monomial n (p.coeff (n + 1))
-
-@[simp] lemma coeff_div_X : (div_X p).coeff n = p.coeff (n+1) :=
-begin
-  simp only [div_X, coeff_monomial, true_and, finset_sum_coeff, not_lt,
-    Ico.mem, zero_le, finset.sum_ite_eq', ite_eq_left_iff],
-  intro h,
-  rw coeff_eq_zero_of_nat_degree_lt (nat.lt_succ_of_le h)
-end
-
-lemma div_X_mul_X_add (p : polynomial R) : div_X p * X + C (p.coeff 0) = p :=
-ext $ by rintro ⟨_|_⟩; simp [coeff_C, nat.succ_ne_zero, coeff_mul_X]
-
-@[simp] lemma div_X_C (a : R) : div_X (C a) = 0 :=
-ext $ λ n, by cases n; simp [div_X, coeff_C]; simp [coeff]
-
-lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
-⟨λ h, by simpa [eq_comm, h] using div_X_mul_X_add p,
-  λ h, by rw [h, div_X_C]⟩
-
-lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
-ext $ by simp
-
-lemma degree_div_X_lt (hp0 : p ≠ 0) : (div_X p).degree < p.degree :=
-by haveI := nontrivial.of_polynomial_ne hp0;
-calc (div_X p).degree < (div_X p * X + C (p.coeff 0)).degree :
-  if h : degree p ≤ 0
-  then begin
-      have h' : C (p.coeff 0) ≠ 0, by rwa [← eq_C_of_degree_le_zero h],
-      rw [eq_C_of_degree_le_zero h, div_X_C, degree_zero, zero_mul, zero_add],
-      exact lt_of_le_of_ne bot_le (ne.symm (mt degree_eq_bot.1 $
-        by simp [h'])),
-    end
-  else
-    have hXp0 : div_X p ≠ 0,
-      by simpa [div_X_eq_zero_iff, -not_le, degree_le_zero_iff] using h,
-    have leading_coeff (div_X p) * leading_coeff X ≠ 0, by simpa,
-    have degree (C (p.coeff 0)) < degree (div_X p * X),
-      from calc degree (C (p.coeff 0)) ≤ 0 : degree_C_le
-         ... < 1 : dec_trivial
-         ... = degree (X : polynomial R) : degree_X.symm
-         ... ≤ degree (div_X p * X) :
-          by rw [← zero_add (degree X), degree_mul' this];
-            exact add_le_add
-              (by rw [zero_le_degree_iff, ne.def, div_X_eq_zero_iff];
-                exact λ h0, h (h0.symm ▸ degree_C_le))
-              (le_refl _),
-    by rw [degree_add_eq_left_of_degree_lt this];
-      exact degree_lt_degree_mul_X hXp0
-... = p.degree : by rw div_X_mul_X_add
-
-/-- An induction principle for polynomials, valued in Sort* instead of Prop. -/
-@[elab_as_eliminator] noncomputable def rec_on_horner
-  {M : polynomial R → Sort*} : Π (p : polynomial R),
-  M 0 →
-  (Π p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a)) →
-  (Π p, p ≠ 0 → M p → M (p * X)) →
-  M p
-| p := λ M0 MC MX,
-if hp : p = 0 then eq.rec_on hp.symm M0
-else
-have wf : degree (div_X p) < degree p,
-  from degree_div_X_lt hp,
-by rw [← div_X_mul_X_add p] at *;
-  exact
-  if hcp0 : coeff p 0 = 0
-  then by rw [hcp0, C_0, add_zero];
-    exact MX _ (λ h : div_X p = 0, by simpa [h, hcp0] using hp)
-      (rec_on_horner _ M0 MC MX)
-  else MC _ _ (coeff_mul_X_zero _) hcp0 (if hpX0 : div_X p = 0
-    then show M (div_X p * X), by rw [hpX0, zero_mul]; exact M0
-    else MX (div_X p) hpX0 (rec_on_horner _ M0 MC MX))
-using_well_founded {dec_tac := tactic.assumption}
-
-@[elab_as_eliminator] lemma degree_pos_induction_on
-  {P : polynomial R → Prop} (p : polynomial R) (h0 : 0 < degree p)
-  (hC : ∀ {a}, a ≠ 0 → P (C a * X))
-  (hX : ∀ {p}, 0 < degree p → P p → P (p * X))
-  (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
-rec_on_horner p
-  (λ h, by rw degree_zero at h; exact absurd h dec_trivial)
-  (λ p a _ _ ih h0,
-    have 0 < degree p,
-      from lt_of_not_ge (λ h, (not_lt_of_ge degree_C_le) $
-        by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0),
-    hadd this (ih this))
-  (λ p _ ih h0',
-    if h0 : 0 < degree p
-    then hX h0 (ih h0)
-    else by rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at *;
-      exact hC (λ h : coeff p 0 = 0,
-        by simpa [h, nat.not_lt_zero] using h0'))
-  h0
-
-end semiring
-
 section comm_semiring
 variables [comm_semiring R]
 

src/data/polynomial/erase_lead.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.polynomial.degree
 import data.polynomial.degree.trailing_degree
+import data.polynomial.inductions
 
 /-!
 # Erase the leading term of a univariate polynomial

src/data/polynomial/eval.lean

@@ -389,8 +389,8 @@ eval₂_monomial _ _
 @[simp] lemma mul_X_comp : (p * X).comp r = p.comp r * r :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq, add_mul], },
-  { intros n b, simp [pow_succ', mul_assoc], }
+  { intros p q hp hq, simp only [hp, hq, add_mul, add_comp] },
+  { intros n b, simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp] }
 end
 
 @[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)
 variables {f}
 
 lemma map_monic_eq_zero_iff (hp : p.monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
-⟨ λ hfp x, calc f x = f x * f p.leading_coeff : by simp [hp]
-                ... = f x * (p.map f).coeff p.nat_degree : by { congr, apply (coeff_map _ _).symm }
-                ... = 0 : by simp [hfp],
-  λ h, ext (λ n, by simp [h]) ⟩
+⟨ λ hfp x, calc f x = f x * f p.leading_coeff : by simp only [mul_one, hp.leading_coeff, f.map_one]
+                ... = f x * (p.map f).coeff p.nat_degree : congr_arg _ (coeff_map _ _).symm
+                ... = 0 : by simp only [hfp, mul_zero, coeff_zero],
+  λ h, ext (λ n, by simp only [h, coeff_map, coeff_zero]) ⟩
 
 lemma map_monic_ne_zero (hp : p.monic) [nontrivial S] : p.map f ≠ 0 :=
 λ h, f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)
 
+lemma degree_map_eq_of_leading_coeff_ne_zero (f : R →+* S)
+  (hf : f (leading_coeff p) ≠ 0) : degree (p.map f) = degree p :=
+le_antisymm (degree_map_le f _) $
+  have hp0 : p ≠ 0, from leading_coeff_ne_zero.mp (λ hp0, hf (trans (congr_arg _ hp0) f.map_zero)),
+  begin
+    rw [degree_eq_nat_degree hp0],
+    refine le_degree_of_ne_zero _,
+    rw [coeff_map], exact hf
+  end
+
+lemma nat_degree_map_of_leading_coeff_ne_zero (f : R →+* S)
+  (hf : f (leading_coeff p) ≠ 0) : nat_degree (p.map f) = nat_degree p :=
+nat_degree_eq_of_degree_eq (degree_map_eq_of_leading_coeff_ne_zero f hf)
+
+lemma leading_coeff_map_of_leading_coeff_ne_zero (f : R →+* S)
+  (hf : f (leading_coeff p) ≠ 0) : leading_coeff (p.map f) = f (leading_coeff p) :=
+begin
+  unfold leading_coeff,
+  rw [coeff_map, nat_degree_map_of_leading_coeff_ne_zero f hf],
+end
+
 variables (f)
 
 @[simp] lemma map_ring_hom_id : map_ring_hom (ring_hom.id R) = ring_hom.id (polynomial R) :=
@@ -575,8 +596,9 @@ begin
     (nat_degree_map_le _ _).trans_lt (nat.lt_succ_self _),
   conv_lhs { rw [eval₂_eq_sum], },
   rw [sum_over_range' _ _ _ A],
-  { simp [coeff_map, eval₂_eq_sum, sum_over_range] },
-  { simp }
+  { simp only [coeff_map, eval₂_eq_sum, sum_over_range, forall_const, zero_mul, ring_hom.map_zero,
+      function.comp_app, ring_hom.coe_comp] },
+  { simp only [forall_const, zero_mul, ring_hom.map_zero] }
 end
 
 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 ι) :
 
 lemma map_comp (p q : polynomial R) : map f (p.comp q) = (map f p).comp (map f q) :=
 polynomial.induction_on p
-  (by simp)
-  (by simp {contextual := tt})
-  (by simp [pow_succ', ← mul_assoc, polynomial.comp] {contextual := tt})
+  (by simp only [map_C, forall_const, C_comp, eq_self_iff_true])
+  (by simp only [map_add, add_comp, forall_const, implies_true_iff, eq_self_iff_true]
+        {contextual := tt})
+  (by simp only [pow_succ', ←mul_assoc, comp, forall_const, eval₂_mul_X, implies_true_iff,
+        eq_self_iff_true, map_X, map_mul] {contextual := tt})
 
 @[simp]
 lemma eval_zero_map (f : R →+* S) (p : polynomial R) :
@@ -602,17 +626,17 @@ lemma eval_one_map (f : R →+* S) (p : polynomial R) :
   (p.map f).eval 1 = f (p.eval 1) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq], },
-  { intros n r, simp, }
+  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros n r, simp only [one_pow, mul_one, eval_monomial, map_monomial] }
 end
 
 @[simp]
 lemma eval_nat_cast_map (f : R →+* S) (p : polynomial R) (n : ℕ) :
   (p.map f).eval n = f (p.eval n) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq], },
-  { intros n r, simp, }
+  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros n r, simp only [f.map_nat_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
 end
 
 @[simp]
@@ -621,8 +645,8 @@ lemma eval_int_cast_map {R S : Type*} [ring R] [ring S]
   (p.map f).eval i = f (p.eval i) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp [hp, hq], },
-  { intros n r, simp, }
+  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros n r, simp only [f.map_int_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
 end
 
 end map
@@ -643,11 +667,9 @@ variables (f : R →+* S) (g : S →+* T) (p)
 lemma hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) :=
 begin
   apply polynomial.induction_on p; clear p,
-  { intros a, rw [eval₂_C, eval₂_C], refl, },
+  { simp only [forall_const, eq_self_iff_true, eval₂_C, ring_hom.coe_comp] },
   { intros p q hp hq, simp only [hp, hq, eval₂_add, g.map_add] },
-  { intros n a ih,
-    simp only [eval₂_mul, eval₂_C, eval₂_X_pow, g.map_mul, g.map_pow],
-    refl, }
+  { intros n a ih, simpa only [eval₂_mul, eval₂_C, eval₂_X_pow, g.map_mul, g.map_pow] }
 end
 
 end hom_eval₂
@@ -731,7 +753,6 @@ begin
   intros x,
   simp only [mem_support_iff],
   contrapose!,
-  change p.coeff x = 0 → (map f p).coeff x = 0,
   rw coeff_map,
   intro hx,
   rw hx,