Zulip Chat Archive

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

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!

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