My first project: help with coercion?

Stream: new members

[Hugo Labrande]

Hello everyone, I recently found out about Lean and did some tutorials, and I really like the idea of contributing to mathlib (I'm a former math teacher, and the idea of being able to dive back in sounds appealing :D )
For my first little project, I wanted to prove that the degree of the nth Chebyshev polynomial was n (super easy, inductive proof). My proof is rather complicated and I'll no doubt make it more efficient later ("suggest" has been rather unhelpful, unfortunately), but I'm stuck on the last few things, which are a bit silly and both have to do with coercion (I think? they both involve the ↑):

• proving that "r1.degree = ↑(r1.nat_degree)"
• proving that the degree of 2X is 1 : I want to use "nat_degree_C_mul_X", but it fails to unify (2 * X).nat_degree = 1 with (⇑C ?m_3 * X).nat_degree = 1
  Could anyone tell me what I'm missing, and how to get around these? I'd appreciate it very much :) Thank you!

[Eric Wieser]

Welcome! Would you be able to produce a #mwe with the goals you're stuck on?

[Hugo Labrande]

Sure! I'll try to isolate these. (I can also post my 70-line proof with my 3 sorrys, if needed) Thank you!

[Hugo Labrande]

Here, I spun these into two lemmas, each with one of the problems. Thanks :) mwe.lean

[Adam Topaz]

A #mwe would indeed be helpful, but I think docs#polynomial.degree_eq_nat_degree would help for the first issue

[Adam Topaz]

Can you post code in zulip using #backticks ?

[Hugo Labrande]

import data.polynomial.degree
import ring_theory.polynomial.chebyshev
import analysis.complex.basic

noncomputable theory
namespace polynomial.chebyshev
open polynomial

lemma problem_1 : ∀ n, (T ℂ n).nat_degree = n :=
begin
  let r1 : polynomial ℂ := 2*X,
  have m1 : r1 = 2*X := by refl,
  have d1 : r1.nat_degree = 1 := by begin
      rw m1,
      /- issue here -/
      apply nat_degree_C_mul_X,
  end,
  have l1 : r1.leading_coeff ≠ 0 := by begin
      apply coeff_ne_zero_of_eq_degree,
      /- how to proceed?-/
    end,
end

[Hugo Labrande]

Like this?

[Adam Topaz]

I've cleaned up your code a bit, and added a few hints. The last sorry should be doable, but once you finish it off, I suggest trying to shorten the proof a bit.

import data.polynomial.degree
import ring_theory.polynomial.chebyshev
import analysis.complex.basic

noncomputable theory
namespace polynomial.chebyshev
open polynomial

lemma problem_1 : ∀ n, (T ℂ n).nat_degree = n :=
begin
  set r1 : polynomial ℂ := 2*X with m1,
  have d1 : r1.nat_degree = 1,
  {  rw m1,
    have : (2 : polynomial ℂ) = polynomial.C 2, by simp,
    rw this,
    apply nat_degree_C_mul_X,
    exact two_ne_zero' },
  have l1 : r1.leading_coeff ≠ 0,
  { apply coeff_ne_zero_of_eq_degree,
    apply degree_eq_nat_degree,
    simp only [ne.def, mul_eq_zero, not_or_distrib],
    refine ⟨_, X_ne_zero⟩,
    sorry },
  sorry,
end

end polynomial.chebyshev

[Adam Topaz]

One thing that's a bit confusing here is that when you wrote let r1 : polynomial ℂ := 2*X,, lean considers the 2 as an element of polynomial \C. Whenever you have a ring A, lean lets you write 2 : A. But it's a theorem that this agrees with polynomial.C 2 in this case, and lean needs some hints to be able to see this.

[Eric Wieser]

Is (2 : ℂ) • X easier or harder to work with than 2*X?

[Kalle Kytölä]

As far as I can tell, the shorter syntax

set r1 : polynomial ℂ := 2*X with m1,

has identical effect as your first two lines:

let r1 : polynomial ℂ := 2*X,
have m1 : r1 = 2*X := by refl,

I think it is convenient to use set ... with instead of let most of the time. (Actually are there any benefits to let? It is a bit unfortunate that let is common in written math, but not so convenient in Lean.)

Regarding the actual question... It is possible to use e.g. docs#polynomial.nat_degree_monomial together with docs#polynomial.monomial_eq_C_mul_X , but I'm almost sure that Adam's answer is better (in particular explains why the latter lemma was needed).

[Adam Topaz]

My inclination would be to say that \smul would be easier in this case, but I haven't tried.

[Adam Topaz]

Also, it seems that we're missing some instances:

import data.polynomial.degree
import ring_theory.polynomial.chebyshev
import analysis.complex.basic

example : char_zero ℂ := by apply_instance
example : char_zero (polynomial ℂ) := by apply_instance -- fails

[Hugo Labrande]

Thank you so much everybody! I'm going to take a look at all that. I also appreciate the hints to shorten proofs; I was wondering how you used "let" definitions as propositions (for rewriting for instance) so that really helps!