## Stream: new members

### Topic: Golfing and medium-sized PRs to mathlib

#### Hanting Zhang (Jan 09 2021 at 01:53):

Y'ello again. I've just finished proving a version of Vieta's formulas. The file, however, messy, verbose, and needs a lot of golfing. I've spent some time trying to tidy things up, but I don't think I can simplify anything more on my own. If anyone is willing to look through my proof and give me some pointers on improvement I would be very grateful for any input. vietas.txt

#### Damiano Testa (Jan 09 2021 at 05:08):

Below is a first attempt at shortening. Note that I simply scanned the file from the top down, instead of trying to figure out where each of the pieces would fit.

-- in polynomial.
theorem coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [semiring R] (h : n ≠ 0) : (C a).coeff n = 0 :=
by rw [coeff_C, if_neg h]

namespace finset
variables {α : Type u} (s : finset α)

@[simp] lemma powerset_len_zero (s : finset α) : powerset_len 0 s = {∅} :=
begin
ext,
rw [mem_powerset_len, mem_singleton, card_eq_zero],
refine ⟨λ h, h.2, λ h, _⟩,
rw h,
exact ⟨empty_subset s, rfl⟩,
end

end finset
namespace vieta

variables {α : Type u} [integral_domain α]
variables {n : ℕ} {r : ℕ → α} {f : polynomial α}

lemma coeff_prod (n : ℕ) (p q : polynomial α) : coeff (p * q) n = ∑ i in range (n + 1), coeff p i * coeff q (n - i) :=
begin
sorry
end

example (n : ℕ) : ∏ i in range n, 1 = 1 := prod_const_one

lemma linear_poly_coeff_zero (a : α) : coeff (X + C a) 0 = a :=

lemma linear_poly_coeff_one (a : α) : coeff (X + C a) 1 = (1 : α) :=
by rw [coeff_add, coeff_X_one, add_right_eq_self, coeff_C, if_neg (@one_ne_zero ℕ _ _)]

lemma linear_poly_coeff_ge_two (a : α) (h : 2 ≤ n) : coeff (X + C a) n = (0 : α) :=
begin
rw [coeff_add, coeff_C_ne_zero, add_zero, coeff_X, if_neg (ne_of_lt (nat.succ_le_iff.mp h))],
exact ne_of_gt (lt_of_lt_of_le zero_lt_two h),
end


#### Hanting Zhang (Jan 09 2021 at 05:50):

Thanks! I've put the shortened proofs in. I guess it would be better to just ask for specific stuff directly.

import tactic
import ring_theory.polynomial.basic
import algebra.polynomial.big_operators

universes u v w
open_locale big_operators

open finset polynomial

variables {α : Type u} [integral_domain α]

def g : ℕ × ℕ → ℕ := λ x, x.fst

lemma diag_inj (n : ℕ) (x : ℕ × ℕ) (hx : x ∈ nat.antidiagonal n) (y : ℕ × ℕ) (hy : y ∈ nat.antidiagonal n) : g x = g y → x = y :=
begin
intro hg,
simp [nat.mem_antidiagonal] at *,
ext,
exact hg,
replace hg : x.fst = y.fst := by exact hg, -- x.fst and g x are defeq, but Lean refuses to rewrite?
rw [← hx, hg] at hy,
end

-- The nth coefficient of p * q is the sum over coefficients i, j of p, q respectively, where i + j = n.
lemma coeff_prod (n : ℕ) (p q : polynomial α) : coeff (p * q) n = ∑ i in range (n + 1), coeff p i * coeff q (n - i) :=
begin
rw coeff_mul,
symmetry,
have h : range (n + 1) = image (λ (x : ℕ × ℕ), g x) (nat.antidiagonal n) :=
begin
ext,
split,
{ intro h,
rw mem_image,
use (a, n - a),
split,
{ simp only [nat.mem_antidiagonal],
exact nat.add_sub_cancel' (mem_range_succ_iff.mp h) },
{ refl } },
{ intro h,
rcases (mem_image.mp h) with ⟨x, hx, hxx⟩,
replace hxx : x.fst = a := by exact hxx, -- these are defeq, but Lean again refuses to rewrite so I have to do this replace.
rw [nat.mem_antidiagonal, hxx] at hx,
rw mem_range_succ_iff,
linarith },
end,
rw [h, sum_image (diag_inj n)],
apply sum_congr, {refl},
intros,
simp only, -- this one is weird, this only tidies the expressions, but if I remove it rw doesn't work.
rw nat.mem_antidiagonal at H,
rw ← nat.sub_eq_of_eq_add (eq.symm H),
refl,
end


I'm mostly confused about the defeq replace lines. Using erw doesn't work either. Any feedback would be appreciated!

#### Alex J. Best (Jan 09 2021 at 13:20):

The file extension for lean files is .lean, you should use that instead of .txt :smile:

#### Alex J. Best (Jan 09 2021 at 13:29):

Waht do you mean lean refuses to rewrite? For the second one

      dsimp [g] at hxx,


works fine, the idiom for changing to something defeq by hand is tactic#change though, eg.

      change x.fst = a at hxx,


#### Alex J. Best (Jan 09 2021 at 13:30):

Oh you mean the line rw [hg] would fail without what you did.

#### Adam Topaz (Jan 09 2021 at 14:07):

@Hanting Zhang the way most of us share lean code is using GitHub gists or by pushing to a non-master branch of mathlib.

#### Hanting Zhang (Jan 10 2021 at 03:41):

Ah, thanks for the info. Like this? https://github.com/leanprover-community/mathlib/compare/master...vietas

Last updated: Dec 20 2023 at 11:08 UTC