Zulip Chat Archive

Stream: general

Topic: golf challenge

Kenny Lau (Jan 29 2019 at 09:15):

import data.equiv.basic data.polynomial linear_algebra.multivariate_polynomial

universes u v w

namespace mv_polynomial

variables (α : Type u) (β : Type v) [comm_ring α] [decidable_eq α] [decidable_eq β]

def option_ring_equiv_aux11 : α → polynomial (mv_polynomial β α) :=
polynomial.C ∘ C

instance option_ring_equiv_aux12 : ring (polynomial (mv_polynomial β α)) :=
@comm_ring.to_ring _ $ polynomial.comm_ring

instance option_ring_equiv_aux13 : is_ring_hom (polynomial.C : mv_polynomial β α → polynomial (mv_polynomial β α)) :=
by apply polynomial.C.is_ring_hom

instance option_ring_equiv_aux14 : is_ring_hom (option_ring_equiv_aux11 α β) :=
is_ring_hom.comp _ _

instance option_ring_equiv_aux15 : is_semiring_hom (option_ring_equiv_aux11 α β) :=
is_ring_hom.is_semiring_hom _

def option_ring_equiv_aux1 : mv_polynomial (option β) α → polynomial (mv_polynomial β α) :=
eval₂ (option_ring_equiv_aux11 α β) (λ x, option.rec_on x polynomial.X (polynomial.C ∘ X))

def option_ring_equiv_aux21 : mv_polynomial β α → mv_polynomial (option β) α :=
eval₂ C (X ∘ some)

instance option_ring_equiv_aux22 : is_ring_hom (option_ring_equiv_aux21 α β) :=
by convert eval₂.is_ring_hom _ _; apply_instance

instance option_ring_equiv_aux23 : is_semiring_hom (option_ring_equiv_aux21 α β) :=
is_ring_hom.is_semiring_hom _

def option_ring_equiv_aux2 : polynomial (mv_polynomial β α) → mv_polynomial (option β) α :=
polynomial.eval₂ (option_ring_equiv_aux21 α β) (X none)

variables {α β}
set_option class.instance_max_depth 5
theorem option_ring_equiv_aux3 (f : mv_polynomial (option β) α) : option_ring_equiv_aux2 α β (option_ring_equiv_aux1 α β f) = f :=
induction_on f
  (λ r, calc option_ring_equiv_aux2 α β (option_ring_equiv_aux1 α β (C r))
           = option_ring_equiv_aux2 α β (option_ring_equiv_aux11 α β r) : by congr' 1; convert eval₂_C _ _ _; convert mv_polynomial.option_ring_equiv_aux15 α β
       ... = option_ring_equiv_aux21 α β (C r) : by convert polynomial.eval₂_C _ _; apply_instance
       ... = C r : by convert eval₂_C _ _ _; apply_instance)
  sorry
  sorry

end mv_polynomial

Kenny Lau (Jan 29 2019 at 09:15):

challenge: shorten this code, but keep the compiling time low

Kenny Lau (Jan 29 2019 at 09:16):

(yes, the set_option class.instance_max_depth 5 line is there to keep the compiling time low)

Kenny Lau (Jan 29 2019 at 09:16):

@Johannes Hölzl

Kenny Lau (Jan 29 2019 at 12:31):

@Chris Hughes

Johannes Hölzl (Jan 30 2019 at 15:18):

@Kenny Lau I think we have a problem either with the ring homomorphisms, or some of the mv_polynomial instances... I changed the proof to mv_polynomial (β ⊕ γ) α ≃r mv_polynomial β (mv_polynomial γ α), allowing also the symmetric variant.

Kenny Lau (Jan 30 2019 at 15:19):

are you planning to put this into mathlib? I'm about to prove the same theorem

Johannes Hölzl (Jan 30 2019 at 15:20):

its already in master

Johannes Hölzl (Jan 30 2019 at 15:20):

https://github.com/leanprover/mathlib/commit/f7b9d6b43e478661eb87fef36c75e8e4ffc08499

Kenny Lau (Jan 30 2019 at 15:20):

oh nice!

Johan Commelin (Jan 30 2019 at 15:23):

Aah, using rename we might be able to slightly cleanup the mv_polynomial adjunction that I PR'd a while ago.

Kenny Lau (Jul 02 2020 at 08:59):

import data.polynomial

universes u

open polynomial
open_locale classical

lemma nat_degree_le_nat_degree {R : Type u} [semiring R] {f g : polynomial R}
  (hfg : f.degree ≤ g.degree) : f.nat_degree ≤ g.nat_degree :=
begin
  by_cases hf : f = 0, { rw [hf, nat_degree_zero], exact zero_le _ },
  by_cases hg : g = 0, { rw [hg, degree_zero, le_bot_iff, degree_eq_bot] at hfg, cc },
  rwa [degree_eq_nat_degree hf, degree_eq_nat_degree hg, with_bot.coe_le_coe] at hfg
end

theorem nat_degree_div_by_monic {R : Type u} [comm_ring R] (f : polynomial R) {g : polynomial R}
  (hg : g.monic) : nat_degree (f /ₘ g) = nat_degree f - nat_degree g :=
begin
  by_cases h01 : (0 : R) = 1,
  { haveI := subsingleton_of_zero_eq_one h01,
    rw [subsingleton.elim (f /ₘ g) 0, subsingleton.elim f 0, subsingleton.elim g 0,
        nat_degree_zero] },
  haveI : nonzero R := ⟨h01⟩,
  by_cases hfg : f /ₘ g = 0,
  { rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg hg.ne_zero at hfg,
    rw nat.sub_eq_zero_of_le (nat_degree_le_nat_degree $ le_of_lt hfg) },
  have hgf := hfg, rw div_by_monic_eq_zero_iff hg hg.ne_zero at hgf, push_neg at hgf,
  have := degree_add_div_by_monic hg hgf,
  have hf : f ≠ 0, { intro hf, apply hfg, rw [hf, zero_div_by_monic] },
  rw [degree_eq_nat_degree hf, degree_eq_nat_degree hg.ne_zero, degree_eq_nat_degree hfg,
      ← with_bot.coe_add, with_bot.coe_eq_coe] at this,
  rw [← this, nat.add_sub_cancel_left]
end

Kenny Lau (Jul 10 2020 at 11:39):

import data.mv_polynomial
import linear_algebra.determinant

universes u v

variables (n : Type u) [fintype n] [decidable_eq n]

noncomputable def det_poly : mv_polynomial (n × n) ℤ :=
matrix.det $ λ i j : n, mv_polynomial.X (i, j)

variables {n} {R : Type v} [comm_ring R] (M : matrix n n R)

theorem eval_det_poly : (det_poly n).eval₂ coe (λ p, M p.1 p.2) = M.det :=
sorry

Kenny Lau (Jul 10 2020 at 11:40):

golf challenge

Reid Barton (Jul 10 2020 at 11:41):

https://github.com/rwbarton/swan/blob/lean-3.4.2/src/for_mathlib/determinant.lean

Kenny Lau (Jul 10 2020 at 11:41):

lol

Reid Barton (Jul 10 2020 at 11:43):

It might use simp lemmas that weren't in mathlib at the time

Kenny Lau (Jul 10 2020 at 12:01):

my solution:

import data.mv_polynomial
import linear_algebra.determinant

universes u v

variables (n : Type u) [fintype n] [decidable_eq n]

noncomputable def det_poly : mv_polynomial (n × n) ℤ :=
matrix.det $ λ i j : n, mv_polynomial.X (i, j)

variables {n} {R : Type v} [comm_ring R] (M : matrix n n R)

namespace mv_polynomial

theorem eval₂_int_cast {α β σ : Type*} [comm_ring α] [comm_ring β]
  (f : α → β) (g : σ → β) [is_ring_hom f] (n : ℤ) :
  (n : mv_polynomial σ α).eval₂ f g = n :=
int.induction_on n (eval₂_zero f g)
  (λ i ih, by rw [int.cast_add, int.cast_add, int.cast_one, int.cast_one, eval₂_add, ih, eval₂_one])
  (λ i ih, by rw [int.cast_sub, int.cast_sub, int.cast_one, int.cast_one, eval₂_sub, ih, eval₂_one])

end mv_polynomial

open mv_polynomial

theorem eval_det_poly : (det_poly n).eval₂ coe (λ p, M p.1 p.2) = M.det :=
begin
  unfold det_poly matrix.det,
  haveI : is_semiring_hom (coe : ℤ → R) := ⟨int.cast_zero, int.cast_one, int.cast_add, int.cast_mul⟩,
  haveI : is_ring_hom (coe : ℤ → R) := is_ring_hom.of_semiring _,
  simp_rw [eval₂_sum, eval₂_mul, eval₂_int_cast, eval₂_prod, eval₂_X]
end