polynomial: .to_fun vs .coeff

Stream: new members

[Damiano Testa]

Dear All,

another question with a complete, yet annoying, proof. Lean likes to use .to_fun to refer to the coefficients of a polynomial, but whenever it does, I need to insert a have statement to convert .to_fun to .coeff (with proof refl), since most of the functionality that I know uses .coeff instead of .to_fun. In the example below, you can see this happening at the have line. Can I avoid the have statement?

Thank you very much!

import tactic
import data.polynomial.degree.basic

open finset polynomial

lemma support_monomial {R : Type*} [semiring R] {n : ℕ} : (X ^ n : polynomial R).support ⊆ singleton n :=
begin
  intros a a_1,
  rw mem_singleton,
  rw (X ^ n).3 at a_1,
  have : (X ^ n).to_fun a = (X ^ n).coeff a,
    refl,
  rw this at a_1,
  rw coeff_X_pow n a at a_1,
  finish,
end

[Kevin Buzzard]

Things like rw (X^n).3 are not an official part of the API, which is why you're seeing to_fun.

[Damiano Testa]

Ok, in this case, possibly. I have also seen it happen after simp, though

[Kevin Buzzard]

lemma support_monomial {R : Type*} [semiring R] {n : ℕ} :
  (X ^ n : polynomial R).support ⊆ singleton n :=
begin
  intros a ha,
  rw mem_singleton,
  rw mem_support_iff_coeff_ne_zero at ha,
  rw coeff_X_pow n a at ha,
  finish,
end

[Kevin Buzzard]

If it happens after simp then there might be a missing (or bad) simp lemma.

[Damiano Testa]

@Kevin Buzzard Thank you for the working example! This is what I was hoping for!

[Damiano Testa]

Kevin Buzzard said:

If it happens after simp then there might be a missing (or bad) simp lemma.

Should it happen again with simp, I may report it as well

[Kevin Buzzard]

The trick with these things is to try and keep everything (hypotheses, goals) in the "standard form" (because this is what simp and rw like to see).

[Scott Morrison]

Essentially: anytime you see .to_fun, it's a reflection that the API for polynomials is imperfect. We should aim to get out of this situation! The fact that polynomial is actually defined in terms of finsupp should be sealed away as early as practically possible. PRs that improve on this are very welcome. :-)

[Damiano Testa]

Very well: I will take a close look at whether I produce .to_fun myself, or whether it is produced by simp/Lean!