refactor(data/polynomial): remove has_coe_to_fun, and @[reducible] on monomial (#3420)

I'm going to refactor in stages, trying to clean up some of the cruftier aspects of `data/polynomial/*`.

This PR:

1. removes the `has_coe_to_fun` on polynomial 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: kim-em

src/data/polynomial/basic.lean

@@ -43,18 +43,9 @@ instance : semimodule R (polynomial R) := add_monoid_algebra.semimodule
 instance subsingleton [subsingleton R] : subsingleton (polynomial R) :=
 ⟨λ _ _, ext (λ _, subsingleton.elim _ _)⟩
 
-/-- The coercion turning a `polynomial` into the function which reports the coefficient of a given
-monomial `X^n` -/
-def coeff_coe_to_fun : has_coe_to_fun (polynomial R) :=
-finsupp.has_coe_to_fun
-
-local attribute [instance] coeff_coe_to_fun
-
-
 @[simp] lemma support_zero : (0 : polynomial R).support = ∅ := rfl
 
 /-- `monomial s a` is the monomial `a * X^s` -/
-@[reducible]
 def monomial (n : ℕ) (a : R) : polynomial R := finsupp.single n a
 
 @[simp] lemma monomial_zero_right (n : ℕ) :
@@ -65,6 +56,11 @@ lemma monomial_add (n : ℕ) (r s : R) :
   monomial n (r + s) = monomial n r + monomial n s :=
 by simp [monomial]
 
+lemma monomial_mul_monomial (n m : ℕ) (r s : R) :
+  monomial n r * monomial m s = monomial (n + m) (r * s) :=
+by simp only [monomial, single_mul_single]
+
+
 /-- `X` is the polynomial variable (aka indeterminant). -/
 def X : polynomial R := monomial 1 1
 
@@ -89,17 +85,21 @@ by rw [mul_assoc, X_pow_mul, ←mul_assoc]
 /-- coeff p n is the coefficient of X^n in p -/
 def coeff (p : polynomial R) := p.to_fun
 
-lemma apply_eq_coeff : p n = coeff p n := rfl
-
-
 @[simp] lemma coeff_mk (s) (f) (h) : coeff (finsupp.mk s f h : polynomial R) = f := rfl
 
+lemma coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 :=
+by { dsimp [monomial, single, finsupp.single], congr, }
+
+/--
+This lemma is needed for occasions when we break through the abstraction from
+`polynomial` to `finsupp`; ideally it wouldn't be necessary at all.
+-/
 lemma coeff_single : coeff (single n a) m = if n = m then a else 0 :=
-by { dsimp [single, finsupp.single], congr, }
+coeff_monomial
 
 @[simp] lemma coeff_zero (n : ℕ) : coeff (0 : polynomial R) n = 0 := rfl
 
-@[simp] lemma coeff_one_zero : coeff (1 : polynomial R) 0 = 1 := coeff_single
+@[simp] lemma coeff_one_zero : coeff (1 : polynomial R) 0 = 1 := coeff_monomial
 
 
 instance [has_repr R] : has_repr (polynomial R) :=

src/data/polynomial/coeff.lean

@@ -31,7 +31,7 @@ section coeff
 
 @[simp, priority 990]
 lemma coeff_one (n : ℕ) : coeff (1 : polynomial R) n = if 0 = n then 1 else 0 :=
-coeff_single
+coeff_monomial
 
 @[simp]
 lemma coeff_add (p q : polynomial R) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n := rfl
@@ -64,7 +64,7 @@ have hite : ∀ a : ℕ × ℕ, ite (a.1 + a.2 = n) (coeff p (a.fst) * coeff q (
   (λ h, absurd (eq.refl (0 : R)) (by rwa if_neg h at ha)),
 calc coeff (p * q) n = ∑ a in p.support, ∑ b in q.support,
     ite (a + b = n) (coeff p a * coeff q b) 0 :
-  by simp only [mul_def, coeff_sum, coeff_single]; refl
+  by { simp only [mul_def, coeff_sum, coeff_single], refl }
 ... = ∑ v in p.support.product q.support, ite (v.1 + v.2 = n) (coeff p v.1 * coeff q v.2) 0 :
   by rw sum_product
 ... = ∑ x in nat.antidiagonal n, coeff p x.1 * coeff q x.2 :
@@ -92,8 +92,8 @@ by rw [← single_eq_C_mul_X]; simp [monomial, single, eq_comm, coeff]; congr
 @[simp] lemma coeff_C_mul (p : polynomial R) : coeff (C a * p) n = a * coeff p n :=
 begin
   conv in (a * _) { rw [← @sum_single _ _ _ p, coeff_sum] },
-  rw [mul_def, ←monomial_zero_left, sum_single_index],
-  { simp [coeff_single, finsupp.mul_sum, coeff_sum],
+  rw [mul_def, ←monomial_zero_left, monomial, sum_single_index],
+  { simp only [coeff_single, finsupp.mul_sum, coeff_sum],
     apply sum_congr rfl,
     assume i hi, by_cases i = n; simp [h] },
   { simp [finsupp.sum] }
@@ -104,15 +104,15 @@ end
 begin
   conv_rhs { rw [← @finsupp.sum_single _ _ _ p, coeff_sum] },
   rw [mul_def, ←monomial_zero_left], simp_rw [sum_single_index],
-  { simp [coeff_single, finsupp.sum_mul, coeff_sum],
+  { simp only [coeff_single, finsupp.sum_mul, coeff_sum],
     apply sum_congr rfl,
     assume i hi, by_cases i = n; simp [h], },
 end
 
 lemma monomial_one_eq_X_pow : ∀{n}, monomial n (1 : R) = X^n
 | 0     := rfl
 | (n+1) :=
-  calc monomial (n + 1) (1 : R) = monomial n 1 * X : by rw [X, single_mul_single, mul_one]
+  calc monomial (n + 1) (1 : R) = monomial n 1 * X : by rw [X, monomial_mul_monomial, mul_one]
     ... = X^n * X : by rw [monomial_one_eq_X_pow]
     ... = X^(n+1) : by simp only [pow_add, pow_one]
 

src/data/polynomial/degree/basic.lean

@@ -161,7 +161,7 @@ end
 by simp only [←C_eq_nat_cast, nat_degree_C]
 
 @[simp] lemma degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n :=
-by rw [← single_eq_C_mul_X, degree, support_single_ne_zero ha]; refl
+by rw [← single_eq_C_mul_X, degree, monomial, support_single_ne_zero ha]; refl
 
 lemma degree_monomial_le (n : ℕ) (a : R) : degree (C a * X ^ n) ≤ n :=
 if h : a = 0 then by rw [h, C_0, zero_mul]; exact bot_le else le_of_eq (degree_monomial n h)

src/data/polynomial/derivative.lean

@@ -49,8 +49,11 @@ end
 finsupp.sum_zero_index
 
 lemma derivative_monomial (a : R) (n : ℕ) : derivative (C a * X ^ n) = C (a * n) * X^(n - 1) :=
-by rw [← single_eq_C_mul_X, ← single_eq_C_mul_X, derivative, sum_single_index, single_eq_C_mul_X];
-  simp only [zero_mul, C_0]; refl
+begin
+  rw [← single_eq_C_mul_X, ← single_eq_C_mul_X, derivative, monomial,
+    sum_single_index, single_eq_C_mul_X],
+  simp only [zero_mul, C_0],
+end
 
 @[simp] lemma derivative_C {a : R} : derivative (C a) = 0 :=
 suffices derivative (C a * X^0) = C (a * 0:R) * X ^ 0,

src/data/polynomial/div.lean

@@ -30,6 +30,20 @@ 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}
 
+section
+/--
+The coercion turning a `polynomial` into the function which reports the coefficient of a given
+monomial `X^n`
+-/
+-- TODO we would like to completely remove this, but this requires fixing some proofs
+def coeff_coe_to_fun : has_coe_to_fun (polynomial R) :=
+finsupp.has_coe_to_fun
+
+local attribute [instance] coeff_coe_to_fun
+
+lemma apply_eq_coeff : p n = coeff p n := rfl
+end
+
 /-- `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 :=

src/data/polynomial/eval.lean

@@ -209,7 +209,8 @@ begin
   refine ext (λ n, _),
   rw [comp, eval₂],
   conv in (C _ * _) { rw ← single_eq_C_mul_X },
-  rw finsupp.sum_single
+  congr,
+  convert finsupp.sum_single _,
 end
 
 @[simp] lemma X_comp : X.comp p = p := eval₂_X _ _

src/data/polynomial/monomial.lean

@@ -61,16 +61,16 @@ end C
 
 section coeff
 
-@[simp] lemma coeff_X_one : coeff (X : polynomial R) 1 = 1 := coeff_single
+@[simp] lemma coeff_X_one : coeff (X : polynomial R) 1 = 1 := coeff_monomial
 
-@[simp] lemma coeff_X_zero : coeff (X : polynomial R) 0 = 0 := coeff_single
+@[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_single
+lemma coeff_X : coeff (X : polynomial R) n = if 1 = n then 1 else 0 := coeff_monomial
 
 lemma coeff_C : coeff (C a) n = ite (n = 0) a 0 :=
-by { convert coeff_single using 2, simp [eq_comm], }
+by { convert coeff_monomial using 2, simp [eq_comm], }
 
-@[simp] lemma coeff_C_zero : coeff (C a) 0 = a := coeff_single
+@[simp] lemma coeff_C_zero : coeff (C a) 0 = a := coeff_monomial
 
 theorem nonzero.of_polynomial_ne (h : p ≠ q) : nontrivial R :=
 ⟨⟨0, 1, λ h01 : 0 = 1, h $
@@ -79,7 +79,7 @@ theorem nonzero.of_polynomial_ne (h : p ≠ q) : nontrivial R :=
 lemma single_eq_C_mul_X : ∀{n}, monomial n a = C a * X^n
 | 0     := (mul_one _).symm
 | (n+1) :=
-  calc monomial (n + 1) a = monomial n a * X : by rw [X, single_mul_single, mul_one]
+  calc monomial (n + 1) a = monomial n a * X : by { rw [X, monomial_mul_monomial, mul_one], }
     ... = (C a * X^n) * X : by rw [single_eq_C_mul_X]
     ... = C a * X^(n+1) : by simp only [pow_add, mul_assoc, pow_one]
 

src/ring_theory/polynomial_algebra.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import ring_theory.tensor_product
 import ring_theory.matrix_algebra
-import data.polynomial.algebra_map
+import data.polynomial
 
 /-!
 # Algebra isomorphism between matrices of polynomials and polynomials of matrices
@@ -132,8 +132,10 @@ begin
   simp only [lift.tmul],
   dsimp [to_fun_bilinear, to_fun_linear_right, to_fun],
   ext k,
-  simp_rw [coeff_sum, coeff_single, finsupp.sum,
-    finset.sum_ite_eq', finsupp.mem_support_iff, ne.def, coeff_mul, finset_sum_coeff, coeff_single,
+  -- TODO This is a bit annoying: the polynomial API is breaking down.
+  have apply_eq_coeff : ∀ {p : ℕ →₀ R} {n : ℕ}, p n = coeff p n := by { intros, refl },
+  simp_rw [coeff_sum, coeff_monomial, finsupp.sum, finset.sum_ite_eq', finsupp.mem_support_iff,
+    ne.def, coeff_mul, finset_sum_coeff, coeff_monomial,
     finset.sum_ite_eq', finsupp.mem_support_iff, ne.def,
     mul_ite, mul_zero, ite_mul, zero_mul, apply_eq_coeff],
   simp_rw [ite_mul_zero_left (¬coeff p₁ _ = 0) (a₁ * (algebra_map R A) (coeff p₁ _))],
@@ -147,7 +149,7 @@ begin
   dsimp [to_fun_linear],
   simp only [lift.tmul],
   dsimp [to_fun_bilinear, to_fun_linear_right, to_fun],
-  rw [← C_1, ←monomial_zero_left, finsupp.sum_single_index],
+  rw [← C_1, ←monomial_zero_left, monomial, finsupp.sum_single_index],
   { simp, refl, },
   { simp, },
 end
@@ -208,6 +210,7 @@ begin
     rw [inv_fun, eval₂_monomial, alg_hom.coe_to_ring_hom, algebra.tensor_product.include_left_apply,
       algebra.tensor_product.tmul_pow, one_pow, algebra.tensor_product.tmul_mul_tmul,
       mul_one, one_mul, to_fun_alg_hom_apply_tmul, ←monomial_one_eq_X_pow],
+    dsimp [monomial],
     rw [finsupp.sum_single_index]; simp, }
 end
 
@@ -294,7 +297,7 @@ begin
   { intros p q hp hq, ext,
     simp [hp, hq, coeff_add, add_val, std_basis_matrix_add], },
   { intros k x,
-    simp only [mat_poly_equiv_coeff_apply_aux_1, coeff_single],
+    simp only [mat_poly_equiv_coeff_apply_aux_1, coeff_monomial],
     split_ifs; { funext, simp, }, }
 end