mathlib style

Stream: general

[Damiano Testa]

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

-- halfway readable
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]

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

[Bryan Gin-ge Chen]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

Let me check!

[Kevin Buzzard]

It's immediate from this

[Damiano Testa]

actually yes!

polynomial.nat_degree_mul_le

[Damiano Testa]

(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]

And the nat_degree of a constant is zero I should think

[Kevin Buzzard]

And then you can abuse d+0 defeq to d

[Damiano Testa]

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]

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

Thanks for the suggestion, Kevin!

[Kevin Buzzard]

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]

calc proofs are very nice!

[Damiano Testa]

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