Zulip Chat Archive

Stream: new members

Topic: Golfing and medium-sized PRs to mathlib

view this post on Zulip 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

view this post on Zulip 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 = {} :=
  rw [mem_powerset_len, mem_singleton, card_eq_zero],
  refine λ h, h.2, λ h, _⟩,
  rw h,
  exact empty_subset s, rfl⟩,

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) :=

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 : α) :=
  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),

view this post on Zulip 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 :=
  intro hg,
  simp [nat.mem_antidiagonal] at *,
  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,

-- 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) :=
  rw coeff_mul,
  have h : range (n + 1) = image (λ (x :  × ), g x) (nat.antidiagonal n) :=
    { intro h,
      rw mem_image,
      use (a, n - a),
      { 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 },
  rw [h, sum_image (diag_inj n)],
  apply sum_congr, {refl},
  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),

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

view this post on Zulip 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:

view this post on Zulip 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,

view this post on Zulip Alex J. Best (Jan 09 2021 at 13:30):

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

view this post on Zulip 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.

view this post on Zulip 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: May 10 2021 at 18:22 UTC