## Stream: general

### Topic: mathlib style

#### Damiano Testa (Feb 13 2021 at 17:39):

Dear All,

I am planning to PR a few lemmas on polynomials. After yesterday's discussion in Liouville PR, I am wondering about preferred style. Below is an example: which form is preferred for the PR?

Note that in this case, the truth of the lemma is "trivial". My question applies to these kinds of lemmas. I am definitely not asking this question about proof with "mathematical content".

Thank you!

-- readable form
lemma nat_degree_mul_C_le (f : polynomial R) (a : R) :
(f * C a).nat_degree ≤ f.nat_degree :=
begin
refine (nat_degree_le_iff_coeff_eq_zero _).mpr (λ n hn, _),
refine (coeff_mul_C _ _ _).trans _,
refine mul_eq_zero_of_left _ _,
refine (nat_degree_le_iff_coeff_eq_zero (n - 1)).mp (nat.le_pred_of_lt hn) n _,
by_cases n0 : n = 0,
{ exact ((nat_degree f).not_lt_zero (hn.trans_le n0.le)).elim },
{ exact nat.pred_lt n0 }
end

lemma nat_degree_mul_C_le (f : polynomial R) (a : R) :
(f * C a).nat_degree ≤ f.nat_degree :=
begin
refine (nat_degree_le_iff_coeff_eq_zero f.nat_degree).mpr (λ n hn, (f.coeff_mul_C n a).trans _),
refine mul_eq_zero_of_left ((nat_degree_le_iff_coeff_eq_zero (n - 1)).mp (nat.le_pred_of_lt hn) n _) _,
by_cases n0 : n = 0,
{ exact ((nat_degree f).not_lt_zero (hn.trans_le n0.le)).elim },
{ exact nat.pred_lt n0 }
end

-- totally obscure
lemma nat_degree_mul_C_le (f : polynomial R) (a : R) :
(f * C a).nat_degree ≤ f.nat_degree :=
(nat_degree_le_iff_coeff_eq_zero (nat_degree f)).mpr (λ (n : ℕ) (hn : nat_degree f < n),
(coeff_mul_C f n a).trans  (mul_eq_zero_of_left  ((nat_degree_le_iff_coeff_eq_zero (n - 1)).mp (nat.le_pred_of_lt hn) n
(dite (n = 0) (λ (n0 : n = 0), ((nat_degree f).not_lt_zero (hn.trans_le n0.le)).elim)
(λ (n0 : ¬n = 0), nat.pred_lt n0)))   a))


#### Johan Commelin (Feb 13 2021 at 17:57):

My personal preference would be the middle version. I find the last version intimidating from a maintenance point of view

#### Bryan Gin-ge Chen (Feb 13 2021 at 17:58):

Is there any way to use calc for the initial inequality stuff?

#### Damiano Testa (Feb 13 2021 at 18:05):

Ok, I will aim for the halfway style.

As for calc, in this specific case, I think that there might not be enough "calc" stuff, but I will keep it in mind for similar lemmas that do have a succession of inequalities.

#### Damiano Testa (Feb 13 2021 at 18:06):

(I am a little intimidated by calc, hence my small resistance!)

#### Damiano Testa (Feb 13 2021 at 20:45):

I went for a style in-between the verbose and the halfway incomprehensible: PR #6224.

#### Kevin Buzzard (Feb 13 2021 at 20:51):

Do we have nat_degree(fg)<=nat_degree(f)+nat_degree(g)? It seems like this would be the most natural way to prove the above lemma

Let me check!

#### Kevin Buzzard (Feb 13 2021 at 20:53):

It's immediate from this

#### Damiano Testa (Feb 13 2021 at 20:54):

actually yes!

polynomial.nat_degree_mul_le

#### Damiano Testa (Feb 13 2021 at 20:55):

(My Lean is really slow right now, so I am having a little trouble actually checking that it works, but from the documentation it seems that it has the right assumptions!)

#### Kevin Buzzard (Feb 13 2021 at 20:55):

And the nat_degree of a constant is zero I should think

#### Kevin Buzzard (Feb 13 2021 at 20:55):

And then you can abuse d+0 defeq to d

#### Damiano Testa (Feb 13 2021 at 20:59):

Lean is now working again and this is a proof along your lines, Kevin:

lemma nat_degree_C_mul_le (a : R) (f : polynomial R) :
(C a * f).nat_degree ≤ f.nat_degree :=
nat_degree_mul_le.trans (add_le_iff_nonpos_left.mpr (le_zero_iff.mpr (nat_degree_C a)))


#### Damiano Testa (Feb 13 2021 at 21:10):

I made a git mess on my computer: I will push this proof tomorrow!

Thanks for the suggestion, Kevin!

#### Kevin Buzzard (Feb 13 2021 at 21:33):

Here's a calc proof for Bryan:

lemma nat_degree_mul_C_le (f : polynomial R) (a : R) :
(f * C a).nat_degree ≤ f.nat_degree :=
calc
(f * C a).nat_degree ≤ f.nat_degree + (C a).nat_degree : nat_degree_mul_le
... = f.nat_degree + 0 : by rw nat_degree_C a
... = f.nat_degree : add_zero _


#### Scott Morrison (Feb 13 2021 at 22:18):

calc proofs are very nice!

#### Damiano Testa (Feb 14 2021 at 04:38):

I pushed a version of the PR where all three proofs use calc mode!

Last updated: Dec 20 2023 at 11:08 UTC