Zulip Chat Archive

Stream: new members

Topic: polynomial: .to_fun vs .coeff


Damiano Testa (Sep 24 2020 at 11:30):

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 (Sep 24 2020 at 11:32):

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

Damiano Testa (Sep 24 2020 at 11:33):

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

Kevin Buzzard (Sep 24 2020 at 11:33):

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 (Sep 24 2020 at 11:33):

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

Damiano Testa (Sep 24 2020 at 11:34):

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

Damiano Testa (Sep 24 2020 at 11:35):

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 (Sep 24 2020 at 11:36):

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 (Sep 24 2020 at 12:23):

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 (Sep 24 2020 at 12:25):

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


Last updated: Dec 20 2023 at 11:08 UTC