## Stream: new members

### Topic: polynomial degree

#### Damiano Testa (Sep 08 2020 at 06:07):

Dear All,

more struggles... I am trying to prove something analogous to the code below, but I can't. Also in the specific example below, I am unable to find a proof of the fact that the nat_degree of a non-zero polynomial equals the maximum of the support. What am I doing wrong? How can I prove this? I always have problems accessing the xx-part of option xx.

Thank you!

import tactic
import data.polynomial.degree.basic

open polynomial

lemma defs {R : Type*} [semiring R] {f : polynomial R} {h : f.support.nonempty} : nat_degree f = f.support.max' h :=
begin
sorry,
end

#exit


#### Kevin Buzzard (Sep 08 2020 at 06:20):

Hey, you ask good questions now, and in a good way. You could ask this in #maths. The question seems not to be one about polynomials at all -- this looks like something which could/should be in the finsupp API, and there's a lot to get your head around with finsupps.

#### Kevin Buzzard (Sep 08 2020 at 06:21):

I would have thought that f \ne 0 was the canonical way to say that f was non-zero, rather than f.support.nonempty.

#### Johan Commelin (Sep 08 2020 at 06:23):

Kevin Buzzard said:

Hey, you ask good questions now, and in a good way. You could ask this in #maths. The question seems not to be one about polynomials at all -- this looks like something which could/should be in the finsupp API, and there's a lot to get your head around with finsupps.

Mwah... nat_degree is not really something about finsupps, is it?

#### Damiano Testa (Sep 08 2020 at 06:23):

Kevin Buzzard said:

Hey, you ask good questions now, and in a good way. You could ask this in #maths. The question seems not to be one about polynomials at all -- this looks like something which could/should be in the finsupp API, and there's a lot to get your head around with finsupps.

Thank you! I am glad that some progress can be detected from the outside!

To be honest, I try to avoid finsets as much as possible, since I do not really understand them. This is why I thought that this was an issue with polynomials. I am happy to see a solution using finsupp, though!

#### Kevin Buzzard (Sep 08 2020 at 06:23):

No but degree is, and degree equals nat_degree if f isn't zero

#### Damiano Testa (Sep 08 2020 at 06:24):

Kevin Buzzard said:

I would have thought that f \ne 0 was the canonical way to say that f was non-zero, rather than f.support.nonempty.

I am happy with either: I have a proof of the equivalence of f \neq 0 and f.support.nonempty!

#### Damiano Testa (Sep 08 2020 at 06:25):

Kevin Buzzard said:

No but degree is, and degree equals nat_degree if f isn't zero

Exactly! As much as I try to steer away from degree, nat_degreee is defined in terms of degree and that makes things very hard for me.

#### Kevin Buzzard (Sep 08 2020 at 06:25):

Right. The point I'm making is that if you want to state a bunch of lemmas and you switch between the two notions in the statements of the lemmas then you'll forever have to be rewriting the equivalence when you're trying to use your lemmas

#### Kevin Buzzard (Sep 08 2020 at 06:26):

I'm sorry the API isn't there, this shouldn't be too hard. Just sorry it and move on, and I'll fix it when I get to a computer?

#### Kevin Buzzard (Sep 08 2020 at 06:27):

You just need some result of the form finset.sup = finset.max which is surely there

#### Damiano Testa (Sep 08 2020 at 06:27):

Kevin Buzzard said:

I'm sorry the API isn't there, this shouldn't be too hard. Just sorry it and move on, and I'll fix it when I get to a computer?

Ok, thank you! I am curious to see how to fix it, since this might teach me how to deal with options!

#### Johan Commelin (Sep 08 2020 at 06:27):

lemma defs {f : polynomial R} (h : f.support.nonempty) :
f.nat_degree = f.support.max' h :=
begin
apply le_antisymm,
{ apply finset.le_max',
rw finsupp.mem_support_iff,
show f.leading_coeff ≠ 0,
rwa [finset.nonempty_iff_ne_empty, ne.def, finsupp.support_eq_empty] at h, },
{ apply polynomial.le_nat_degree_of_ne_zero,
have := finset.max'_mem _ h,
rwa finsupp.mem_support_iff at this, }
end


#### Kevin Buzzard (Sep 08 2020 at 06:27):

The idea is that users like us shouldn't have to worrying about this sort of thing at all

#### Damiano Testa (Sep 08 2020 at 06:27):

@Johan Commelin thanks! I'll use your code right now!

#### Kevin Buzzard (Sep 08 2020 at 06:27):

Because it should just all be there

#### Johan Commelin (Sep 08 2020 at 06:28):

Kevin, do we have a notion of degree for finsupps?

#### Damiano Testa (Sep 08 2020 at 06:28):

Ok, I am slowly understanding the difference between things that I should worry about and things that I should not!

#### Johan Commelin (Sep 08 2020 at 06:28):

I'm not really aware of it

#### Kevin Buzzard (Sep 08 2020 at 06:28):

But actually the reason we discover holes in the library like this is because people are actually using the library

#### Kevin Buzzard (Sep 08 2020 at 06:29):

I was filling in holes in the with_bot library yesterday.

#### Kevin Buzzard (Sep 08 2020 at 06:30):

Degree is just defined to be some max

Or some sup

#### Damiano Testa (Sep 08 2020 at 06:32):

Yes, and to work with at_infty I was trying to work with with_top and trailing_degrees, but it got ugly...

#### Kevin Buzzard (Sep 08 2020 at 06:50):

One should imagine the API you want and then find it or complain that it's not there :-)

#### Mario Carneiro (Sep 08 2020 at 07:27):

:point_up: This. It is actually really valuable to spec out the API when you find it missing. This is the hard part of library building - the proofs are usually all trival

#### Mario Carneiro (Sep 08 2020 at 07:29):

Especially, once you find an individual proof going not as smoothly as you would hope, rather than making a huge proof anyway you should step back and ask yourself what theorem you would like to have found in the library, and write its statement precisely. Then PR it

#### Damiano Testa (Sep 08 2020 at 07:31):

Mario Carneiro said:

Especially, once you find an individual proof going not as smoothly as you would hope, rather than making a huge proof anyway you should step back and ask yourself what theorem you would like to have found in the library, and write its statement precisely. Then PR it

Ok, so one thing that would be very valuable for me, at the moment, would be to have all the statements about degree, nat_degree, leading_coeff,... (in data.polynomial.degree.basic) available also for trailing_degree, nat_trailing_degree, trailing_coeff,...

write them down

#### Damiano Testa (Sep 08 2020 at 07:32):

I have started this, and got quite a bit into it, but could not reprove everything

#### Mario Carneiro (Sep 08 2020 at 07:32):

don't worry about that

just statements

#### Damiano Testa (Sep 08 2020 at 07:32):

ok, writing them down (and almost proving them) was a simple matter of using the right sed. with a couple of exceptions!

#### Mario Carneiro (Sep 08 2020 at 07:32):

if you post them here people can probably prove them in a few minutes and then bam you've got a PR

#### Damiano Testa (Sep 08 2020 at 07:33):

ok, I will get to it!

#### Mario Carneiro (Sep 08 2020 at 07:33):

the important part is to identify those pain points and what statements would avoid them

#### Damiano Testa (Sep 08 2020 at 09:01):

Ok, I have converted the statements in data.polynomial.degree.basic to their upside down. The proofs that just went through with mechanical twitching are not commented. The proofs that do not work are commented. Should I simply make a gist and post the link here?

#### Damiano Testa (Sep 08 2020 at 09:02):

I am not necessarily interested in all these lemmas. What I do care about is that the trailing coefficient of a product of polynomials is the product of the trailing coefficients (at least when the product of the trailing coefficients is non-zero).

#### Johan Commelin (Sep 08 2020 at 09:03):

Even better than a gist, would be to push it to a branch of mathlib

#### Johan Commelin (Sep 08 2020 at 09:04):

Do you already have write access to mathlib branches on github?

#### Damiano Testa (Sep 08 2020 at 09:05):

I am not sure: besides being new to Lean, I am also new to github...

#### Damiano Testa (Sep 08 2020 at 09:05):

I feel like I am constantly wasting everybody's time with my not being able to do basic stuf...

#### Johan Commelin (Sep 08 2020 at 09:06):

https://github.com/leanprover-community/mathlib/invitations

I accepted!

#### Damiano Testa (Sep 08 2020 at 09:06):

(I assume that this was what I was supposed to do! Ahaha)

#### Johan Commelin (Sep 08 2020 at 09:07):

So, did you write those lemmas in a file inside mathlib?

#### Damiano Testa (Sep 08 2020 at 09:07):

I wrote them inside a project that I created. Does that count?

Hmm, not really

No worries

Ok

#### Damiano Testa (Sep 08 2020 at 09:08):

I can copy the file elsewhere, of course

#### Kevin Buzzard (Sep 08 2020 at 09:08):

Damiano Testa said:

I feel like I am constantly wasting everybody's time with my not being able to do basic stuf...

For me this was a really important part of the learning process. I bombarded Mario with questions about all 1st year undergrad material (algebra, analysis, ...) and MSc level algebra

#### Johan Commelin (Sep 08 2020 at 09:08):

In that case, just save the file, commit, and push it to your project

#### Johan Commelin (Sep 08 2020 at 09:08):

Are you hosting the project on github?

#### Damiano Testa (Sep 08 2020 at 09:10):

Johan Commelin said:

Are you hosting the project on github?

I like to think that I am, but I am worried to moving it to github, since I fear that I might copy the empty project in github to my computer, instead of uploading the files on my computer to github...

#### Johan Commelin (Sep 08 2020 at 09:10):

This might be an interesting video to watch, if you have some spare minutes.

#### Damiano Testa (Sep 08 2020 at 09:10):

I push the github button on VSC every once in a while, though

#### Damiano Testa (Sep 08 2020 at 09:11):

Johan Commelin said:

This might be an interesting video to watch, if you have some spare minutes.

I will watch later, thanks!

#### Damiano Testa (Sep 08 2020 at 09:17):

While I watch the video and digest it, here is the gist

#### Damiano Testa (Sep 08 2020 at 09:17):

(there may be mistakes in some of the statements, since reversing all the le signs is not as easy to do!)

#### Damiano Testa (Sep 08 2020 at 09:40):

I am watching the video and I have added and committed a file.

#### Damiano Testa (Sep 08 2020 at 11:43):

Still continuing with problems involving degrees, minima and infima: do you know how to prove the lemma below? Thanks!

import tactic
import data.polynomial.degree.basic

open polynomial

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} : f.support.min' fne ∈ f.support.min :=
begin
sorry,
end


#### Damiano Testa (Sep 08 2020 at 11:44):

(If you prefer to have {fne : f ≠ 0} as a hypothesis, go ahead!)

#### Shing Tak Lam (Sep 08 2020 at 11:50):

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} :
f.support.min' fne ∈ f.support.min :=
by rw [option.mem_def, finset.min', option.some_get]


#### Mario Carneiro (Sep 08 2020 at 11:50):

The statement doesn't have anything to do with support

#### Mario Carneiro (Sep 08 2020 at 11:51):

it's a good idea to generalize away as many details of the original context while retaining the essence of the statement, in this case yielding a statement about finsets

#### Damiano Testa (Sep 08 2020 at 11:52):

Mario Carneiro said:

it's a good idea to generalize away as many details of the original context while retaining the essence of the statement, in this case yielding a statement about finsets

I normally try to do that, but in this case, I was unable to formulate f.support.min' fne without the fne : f.support.nonempty assumption...

#### Damiano Testa (Sep 08 2020 at 11:53):

Shing Tak Lam said:

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} :
f.support.min' fne ∈ f.support.min :=
by rw [option.mem_def, finset.min', option.some_get]


Thanks! I do not understand the proof, but Lean does!

#### Mario Carneiro (Sep 08 2020 at 11:53):

you can change the type to s.nonempty

#### Mario Carneiro (Sep 08 2020 at 11:54):

you can look at the type of finset.min' to see what things are needed to state it

#### Damiano Testa (Sep 08 2020 at 11:54):

Mario Carneiro said:

you can change the type to s.nonempty

Ah, I see what you are saying! I should have made f.support the subject!

#### Mario Carneiro (Sep 08 2020 at 11:55):

another thing to notice about shing tak lam's proof is that the lemmas are also not polynomial specific, which suggests that some "trivial generalization" is at play

#### Shing Tak Lam (Sep 08 2020 at 11:56):

Here's the proof for any finset (with some comments), and using it in your lemma

import tactic
import data.polynomial.degree.basic

open polynomial

lemma finset.min'_mem_min {α : Type} [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
s.min' hs ∈ s.min :=
begin
-- Unfold the definition of ∈ for options
rw option.mem_def,
-- Unfold the definition of min'
rw finset.min',
-- some (option.get ↥(s.min.is_some)) is just s.min
rw option.some_get,
end

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} :
f.support.min' fne ∈ f.support.min :=
finset.min'_mem_min _


#### Damiano Testa (Sep 08 2020 at 11:57):

Ok, since this is a step in a proof about degrees of polynomials, and, in my mind, finsets are not what I think when I am thinking about polynomials, I overlooked that I should have formulated it with finsets.

#### Damiano Testa (Sep 08 2020 at 11:58):

Shing Tak Lam said:

Here's the proof for any finset (with some comments), and using it in your lemma

Very useful: thank you!

#### Bryan Gin-ge Chen (Sep 10 2020 at 18:39):

Damiano Testa said:

I am watching the video and I have added and committed a file.

For future reference, the corresponding PR is #4069.

Last updated: May 14 2021 at 12:18 UTC