Zulip Chat Archive

Stream: new members

Topic: My first project: help with coercion?


Hugo Labrande (Jul 31 2021 at 20:32):

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 (Jul 31 2021 at 20:38):

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

Hugo Labrande (Jul 31 2021 at 20:44):

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 (Jul 31 2021 at 20:48):

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

Adam Topaz (Jul 31 2021 at 20:48):

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

Adam Topaz (Jul 31 2021 at 20:49):

Can you post code in zulip using #backticks ?

Hugo Labrande (Jul 31 2021 at 20:52):

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 (Jul 31 2021 at 20:52):

Like this?

Adam Topaz (Jul 31 2021 at 21:24):

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.

Adam Topaz (Jul 31 2021 at 21:26):

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 (Jul 31 2021 at 21:33):

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

Kalle Kytölä (Jul 31 2021 at 21:34):

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 (Jul 31 2021 at 21:34):

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

Adam Topaz (Jul 31 2021 at 21:38):

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 (Jul 31 2021 at 22:36):

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!


Last updated: Dec 20 2023 at 11:08 UTC