Golfing and medium-sized PRs to mathlib

Stream: new members

[Hanting Zhang]

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]

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
-- use polynomial.leading_coeff_prod

lemma linear_poly_coeff_zero (a : α) : coeff (X + C a) 0 = a :=
by rw [coeff_add, coeff_X_zero, zero_add, coeff_C_zero]

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]

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,
  rw add_left_cancel 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]

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

[Alex J. Best]

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]

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

[Adam Topaz]

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

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