refactor(data/polynomial/*): further refactors (#3435)

There's a lot further to go, but I need to do other things for a while so will PR what I have so far.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/polynomial/algebra_map.lean

@@ -14,9 +14,6 @@ We promote `eval₂` to an algebra hom in `aeval`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators

src/data/polynomial/basic.lean

@@ -16,8 +16,6 @@ In this file, we define `polynomial`, provide basic instances, and prove an `ext
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
 
 /-- `polynomial R` is the type of univariate polynomials over `R`.
 
@@ -101,17 +99,11 @@ coeff_monomial
 
 @[simp] lemma coeff_one_zero : coeff (1 : polynomial R) 0 = 1 := coeff_monomial
 
+@[simp] lemma coeff_X_one : coeff (X : polynomial R) 1 = 1 := coeff_monomial
 
-instance [has_repr R] : has_repr (polynomial R) :=
-⟨λ p, if p = 0 then "0"
-  else (p.support.sort (≤)).foldr
-    (λ n a, a ++ (if a = "" then "" else " + ") ++
-      if n = 0
-        then "C (" ++ repr (coeff p n) ++ ")"
-        else if n = 1
-          then if (coeff p n) = 1 then "X" else "C (" ++ repr (coeff p n) ++ ") * X"
-          else if (coeff p n) = 1 then "X ^ " ++ repr n
-            else "C (" ++ repr (coeff p n) ++ ") * X ^ " ++ repr n) ""⟩
+@[simp] lemma coeff_X_zero : coeff (X : polynomial R) 0 = 0 := coeff_monomial
+
+lemma coeff_X : coeff (X : polynomial R) n = if 1 = n then 1 else 0 := coeff_monomial
 
 theorem ext_iff {p q : polynomial R} : p = q ↔ ∀ n, coeff p n = coeff q n :=
 ⟨λ h n, h ▸ rfl, finsupp.ext⟩
@@ -126,7 +118,6 @@ by rw [←one_smul R p, ←h, zero_smul]
 
 end semiring
 
-
 section ring
 variables [ring R]
 
@@ -139,23 +130,38 @@ lemma coeff_sub (p q : polynomial R) (n : ℕ) : coeff (p - q) n = coeff p n - c
 
 end ring
 
-
-section comm_semiring
-variables [comm_semiring R]
-
-instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
-
-end comm_semiring
+instance [comm_semiring R] : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
+instance [comm_ring R] : comm_ring (polynomial R) := add_monoid_algebra.comm_ring
 
 section nonzero_semiring
 
-variables [semiring R] [nontrivial R] {p q : polynomial R}
+variables [semiring R] [nontrivial R]
 instance : nontrivial (polynomial R) :=
 begin
   refine nontrivial_of_ne 0 1 _, intro h,
   have := coeff_zero 0, revert this, rw h, simp,
 end
 
+lemma X_ne_zero : (X : polynomial R) ≠ 0 :=
+mt (congr_arg (λ p, coeff p 1)) (by simp)
+
 end nonzero_semiring
 
+section repr
+variables [semiring R]
+local attribute [instance, priority 100] classical.prop_decidable
+
+instance [has_repr R] : has_repr (polynomial R) :=
+⟨λ p, if p = 0 then "0"
+  else (p.support.sort (≤)).foldr
+    (λ n a, a ++ (if a = "" then "" else " + ") ++
+      if n = 0
+        then "C (" ++ repr (coeff p n) ++ ")"
+        else if n = 1
+          then if (coeff p n) = 1 then "X" else "C (" ++ repr (coeff p n) ++ ") * X"
+          else if (coeff p n) = 1 then "X ^ " ++ repr n
+            else "C (" ++ repr (coeff p n) ++ ") * X ^ " ++ repr n) ""⟩
+
+end repr
+
 end polynomial

src/data/polynomial/coeff.lean

@@ -15,7 +15,6 @@ The theorems include formulas for computing coefficients, such as
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
@@ -24,12 +23,10 @@ namespace polynomial
 universes u v
 variables {R : Type u} {S : Type v} {a b : R} {n m : ℕ}
 
-section semiring
 variables [semiring R] {p q r : polynomial R}
 
 section coeff
 
-@[simp, priority 990]
 lemma coeff_one (n : ℕ) : coeff (1 : polynomial R) n = if 0 = n then 1 else 0 :=
 coeff_monomial
 
@@ -42,11 +39,6 @@ lemma coeff_sum [semiring S] (n : ℕ) (f : ℕ → R → polynomial S) :
 @[simp] lemma coeff_smul (p : polynomial R) (r : R) (n : ℕ) :
 coeff (r • p) n = r * coeff p n := finsupp.smul_apply
 
--- TODO: bundle into a def instead of an instance?
-instance coeff.is_add_monoid_hom {n : ℕ} : is_add_monoid_hom (λ p : polynomial R, p.coeff n) :=
-{ map_add  := λ p q, coeff_add p q n,
-  map_zero := coeff_zero _ }
-
 variable (R)
 /-- The nth coefficient, as a linear map. -/
 def lcoeff (n : ℕ) : polynomial R →ₗ[R] R :=
@@ -81,9 +73,11 @@ end
 @[simp] lemma mul_coeff_zero (p q : polynomial R) : coeff (p * q) 0 = coeff p 0 * coeff q 0 :=
 by simp [coeff_mul]
 
-@[simp] lemma coeff_mul_X_zero (p : polynomial R) : coeff (p * X) 0 = 0 :=
-by rw [coeff_mul, nat.antidiagonal_zero];
-simp only [polynomial.coeff_X_zero, finset.sum_singleton, mul_zero]
+lemma coeff_mul_X_zero (p : polynomial R) : coeff (p * X) 0 = 0 :=
+by simp
+
+lemma coeff_X_mul_zero (p : polynomial R) : coeff (X * p) 0 = 0 :=
+by simp
 
 lemma coeff_C_mul_X (x : R) (k n : ℕ) :
   coeff (C x * X^k : polynomial R) n = if n = k then x else 0 :=
@@ -123,10 +117,15 @@ begin
     ... = a • X^n  : by rw monomial_one_eq_X_pow
 end
 
-@[simp] lemma coeff_X_pow (k n : ℕ) :
+lemma coeff_X_pow (k n : ℕ) :
   coeff (X^k : polynomial R) n = if n = k then 1 else 0 :=
 by rw [← monomial_one_eq_X_pow]; simp [monomial, single, eq_comm, coeff]; congr
 
+@[simp]
+lemma coeff_X_pow_self (n : ℕ) :
+  coeff (X^n : polynomial R) n = 1 :=
+by simp [coeff_X_pow]
+
 theorem coeff_mul_X_pow (p : polynomial R) (n d : ℕ) :
   coeff (p * polynomial.X ^ n) (d + n) = coeff p d :=
 begin
@@ -147,7 +146,4 @@ ext $ λ k, (coeff_mul_X_pow p n k).symm.trans $ ext_iff.1 H (k+n)
 
 end coeff
 
-end semiring
-
-
 end polynomial

src/data/polynomial/degree.lean

@@ -20,8 +20,6 @@ Some of the main results include
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
@@ -464,7 +462,7 @@ have h : leading_coeff (X : polynomial R) * leading_coeff (X ^ n) ≠ 0,
 by rw [pow_succ, degree_mul' h, degree_X, degree_X_pow, add_comm]; refl
 
 theorem not_is_unit_X : ¬ is_unit (X : polynomial R) :=
-λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← coeff_one_zero, ← hgf, coeff_mul_X_zero]
+λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by { rw [← coeff_one_zero, ← hgf], simp }
 
 end nonzero_semiring
 

src/data/polynomial/degree/basic.lean

@@ -15,13 +15,11 @@ The definitions include
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
 namespace polynomial
-universes u v --w x y z
+universes u v
 variables {R : Type u} {S : Type v} {a b : R} {n m : ℕ}
 
 section semiring

src/data/polynomial/derivative.lean

@@ -14,8 +14,6 @@ import data.polynomial.field_division
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 

src/data/polynomial/div.lean

@@ -18,8 +18,6 @@ We also define `root_multiplicity`.
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
--- local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
@@ -59,7 +57,7 @@ def div_X (p : polynomial R) : polynomial R :=
   mem_support_to_fun := λ n,
     suffices (∃ (a : ℕ), (¬coeff p a = 0 ∧ a > 0) ∧ a - 1 = n) ↔
       ¬coeff p (n + 1) = 0,
-    by simpa [finset.mem_def.symm, apply_eq_coeff],
+    by simpa [finset.mem_def.symm],
     ⟨λ ⟨a, ha⟩, by rw [← ha.2, nat.sub_add_cancel ha.1.2]; exact ha.1.1,
       λ h, ⟨n + 1, ⟨h, nat.succ_pos _⟩, nat.succ_sub_one _⟩⟩ }
 

src/data/polynomial/eval.lean

@@ -422,10 +422,8 @@ by rw [is_root.def, eval_sub, eval_X, eval_C, sub_eq_zero_iff_eq, eq_comm]
 
 end ring
 
-
 section comm_ring
 variables [comm_ring R] {p q : polynomial R}
-instance : comm_ring (polynomial R) := add_monoid_algebra.comm_ring
 
 instance eval₂.is_ring_hom {S} [comm_ring S]
   (f : R →+* S) {x : S} : is_ring_hom (eval₂ f x) :=

src/data/polynomial/field_division.lean

@@ -17,18 +17,13 @@ This file starts looking like the ring theory of $ R[X] $
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators
 
 namespace polynomial
 universes u v w y z
 variables {R : Type u} {S : Type v} {k : Type y} {A : Type z} {a b : R} {n : ℕ}
 
-
-
-
 section field
 variables [field R] {p q : polynomial R}
 

src/data/polynomial/identities.lean

@@ -12,9 +12,6 @@ The main def is `binom_expansion`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
@@ -24,12 +21,10 @@ universes u v w x y z
 variables {R : Type u} {S : Type v} {T : Type w} {ι : Type x} {k : Type y} {A : Type z}
   {a b : R} {m n : ℕ}
 
-
-
 section identities
 
 /- @TODO: pow_add_expansion and pow_sub_pow_factor are not specific to polynomials.
-  These belong somewhere else. But not in group_power because they depend on tactic.ring
+  These belong somewhere else. But not in group_power because they depend on tactic.ring_exp
 
 Maybe use data.nat.choose to prove it.
  -/

src/data/polynomial/induction.lean

@@ -12,9 +12,6 @@ The main results are `induction_on` and `as_sum`.
 -/
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
-
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
 
 open finsupp finset add_monoid_algebra
 open_locale big_operators
@@ -89,7 +86,7 @@ end coeff
 -- TODO find a home (this file)
 @[simp] lemma finset_sum_coeff (s : finset ι) (f : ι → polynomial R) (n : ℕ) :
   coeff (∑ b in s, f b) n = ∑ b in s, coeff (f b) n :=
-(s.sum_hom (λ q : polynomial R, q.coeff n)).symm
+(s.sum_hom (λ q : polynomial R, lcoeff R n q)).symm
 
 lemma as_sum (p : polynomial R) :
   p = ∑ i in range (p.nat_degree + 1), C (p.coeff i) * X^i :=

src/data/polynomial/monic.lean

@@ -1,14 +1,12 @@
-import data.polynomial.algebra_map
-import algebra.gcd_domain
-import tactic.omega
-import tactic.ring
-
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-
+import data.polynomial.algebra_map
+import algebra.gcd_domain
+import tactic.ring
+import tactic.omega
 
 /-!
 # Theory of monic polynomials
@@ -21,8 +19,6 @@ and then define `integral_normalization`, which relate arbitrary polynomials to
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
-local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
-
 open finsupp finset add_monoid_algebra
 open_locale big_operators