golfing challenge

Stream: maths

[Johan Commelin]

This shouldn't be so hard/long/slow...

import ring_theory.polynomial

namespace polynomial

/-- The formal derivative of polynomials, as additive homomorphism. -/
noncomputable def derivative_hom (R : Type*) [comm_semiring R] : polynomial R →+ polynomial R :=
{ to_fun := derivative,
  map_zero' := derivative_zero,
  map_add' := λ p q, derivative_add }

@[simp] lemma derivative_neg {R : Type*} [comm_ring R] (f : polynomial R) :
  derivative (-f) = -derivative f :=
(derivative_hom R).map_neg f

@[simp] lemma derivative_sub {R : Type*} [comm_ring R] (f g : polynomial R) :
  derivative (f - g) = derivative f - derivative g :=
(derivative_hom R).map_sub f g

lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {R : Type*} [field R]
  (f : polynomial R) (r : R) (hf : f.is_root r) (hf' : f.derivative.eval r ≠ 0) :
  ideal.is_coprime (X - C r : polynomial R) (f /ₘ (X - C r)) :=
begin
  rw ← mul_div_by_monic_eq_iff_is_root at hf,
  rw ← hf at hf',
  simp only [eval_C, eval_X, add_zero, derivative_X, derivative_mul, one_mul, zero_mul,
    eval_sub, sub_zero, ne.def, derivative_sub, eval_add, eval_mul, derivative_C, sub_self] at hf',
  apply is_coprime_of_dvd,
  { push_neg, left, assume eqz,
    apply_fun polynomial.degree at eqz,
    rw polynomial.degree_X_sub_C at eqz,
    exact option.no_confusion eqz },
  { rintros a h1 h2 ⟨b, hab⟩ H,
    have : irreducible (X - C r),
    { apply polynomial.irreducible_of_degree_eq_one, exact polynomial.degree_X_sub_C _ },
    rcases (this.is_unit_or_is_unit hab) with ha|⟨b,rfl⟩,
    { exact h1 ha },
    apply hf',
    show is_root _ _,
    rw ← dvd_iff_is_root,
    refine dvd_trans ⟨↑b⁻¹, _⟩ H,
    rw [hab, units.mul_inv_cancel_right] }
end

end polynomial

[Alex J. Best]

Probably this can be golfed more, but heres a slightly different proof (I think?)

lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {R : Type*} [field R]
  (f : polynomial R) (r : R) (hf : f.is_root r) (hf' : f.derivative.eval r ≠ 0) :
  ideal.is_coprime (X - C r : polynomial R) (f /ₘ (X - C r)) :=
begin
  have aa : (X - C r) * (f /ₘ (X - C r)) = f - (f %ₘ (X - C r))  := begin
    rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', mod_by_monic_eq_sub_mul_div],
    exact monic_X_sub_C r,
  end,
  apply_fun derivative at aa,
  simp only [derivative_X, derivative_mul, one_mul, sub_zero, derivative_sub, mod_by_monic_X_sub_C_eq_C_eval, derivative_C] at aa,
  refine or.resolve_left (dvd_or_coprime (X - C r) (f /ₘ (X - C r)) (irreducible_of_degree_eq_one (polynomial.degree_X_sub_C r))) _,
  intro,
  apply hf',
  have : (X - C r) ∣ derivative f := aa ▸ (dvd_add a (dvd.intro (derivative (f /ₘ (X - C r))) rfl)),
  rw [← dvd_iff_mod_by_monic_eq_zero (monic_X_sub_C _), mod_by_monic_X_sub_C_eq_C_eval] at this,
  apply_fun coeff at this,
  convert congr_fun this 0,
  rw [coeff_C_zero],
end

[Johan Commelin]

Thanks... it's certainly shorter than what I had.

[Johan Commelin]

Feel free to turn this into a kata.

import data.nat.choose

-- Generalise this to arbitrary property that is respected by addition/multiplication:
-- example applications: sum_pos, sum_neg, ... others?
lemma dvd_sum {α : Type*} {R : Type*} [comm_ring R]
  (s : finset α) (f : α → R) (b : R) (H : ∀ a ∈ s, b ∣ f a) :
  b ∣ s.sum f :=
begin
  let t := s,
  replace H : ∀ a ∈ t, b ∣ f a := H,
  have hs : s ⊆ t := finset.subset.refl s,
  revert hs,
  classical,
  apply finset.induction_on s, {simp},
  intros a s' ha IH hs',
  rw finset.insert_subset at hs',
  cases hs' with has hs',
  simp [*, dvd_add]
end

lemma coe_nat_dvd {α : Type*} [comm_ring α] (m n : ℕ) (h : m ∣ n) :
  (m : α) ∣ n :=
by { rcases h with ⟨k, rfl⟩, refine ⟨k, by norm_cast⟩ }

lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ℕ) [hp : fact p.prime]
  (a b : R) (h : (p : R) ∣ a - b) (k : ℕ) :
  (p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
begin
  induction k with k ih, { simpa using h }, clear h,
  simp only [nat.succ_eq_add_one],
  rcases ih with ⟨c, hc⟩,
  rw sub_eq_iff_eq_add' at hc,
  replace hc := congr_arg (λ x, x^p) hc,
  dsimp only at hc,
  rw [← pow_mul, add_pow, finset.sum_range_succ, nat.choose_self, nat.cast_one, mul_one,
    nat.sub_self, pow_zero, mul_one] at hc,
  conv { congr, skip, rw [nat.pow_succ] },
  simp only [nat.pow_eq_pow] at hc,
  rw [hc, pow_mul, add_sub_cancel'], clear hc a,
  apply dvd_sum,
  intros i hi,
  rw finset.mem_range at hi,
  rw mul_pow,
  conv { congr, skip, congr, congr, skip, rw mul_comm },
  repeat { rw mul_assoc, apply dvd_mul_of_dvd_right }, clear c b,
  norm_cast,
  apply coe_nat_dvd,
  by_cases H : i = 0,
  { subst H,
    suffices : p ^ (k + 1 + 1) ∣ (p ^ (k + 1)) ^ p, by simpa,
    rw ← nat.pow_mul,
    apply nat.pow_dvd_pow,
    refine le_trans (add_le_add_left' $ le_add_left $ le_refl _ : k + 1 + 1 ≤ k + 1 + (k + 1)) _,
    refine le_trans (le_of_eq _) (nat.mul_le_mul_left (k+1) $ (hp.two_le : 2 ≤ p)),
    rw mul_two },
  have i_pos := nat.pos_of_ne_zero H, clear H,
  rw nat.pow_succ,
  apply mul_dvd_mul,
  { generalize H : (p^(k+1)) = b,
    have := nat.sub_pos_of_lt hi,
    conv {congr, rw ← nat.pow_one b},
    apply nat.pow_dvd_pow,
    exact this },
  exact nat.prime.dvd_choose i_pos hi ‹_›
end

[Johan Commelin]

Currently it takes so long on my machine that I'm worried codewars wouldn't accept it.

[Reid Barton]

Johan Commelin said:

Feel free to turn this into a kata mathlib PR.

[Johan Commelin]

Only after it's fast enough to be a kata

[Chris Hughes]

The generalization of the first theorem is is_add_submonoid.sum_mem. Whether that's a good way to state it I don't know.

[Johan Commelin]

But it might be a good way to prove it.

[Johan Commelin]

On the other hand, the other suggestions don't really follow from sum_mem, I guess. Things like sum_pos and sum_neg

[Johan Commelin]

Well, they do, but I don't think the relevant submonoids have been set up.

[Chris Hughes]

sum_pos and sum_neg actually need is_add_subsemigroup.sum_mem_of_ne_empty which doesn't exist.

[Johan Commelin]

sum_nonpos and sum_nonneg...

[Kenny Lau]

import data.nat.choose algebra.geom_sum ring_theory.ideals

-- Generalise this to arbitrary property that is respected by addition/multiplication:
-- example applications: sum_pos, sum_neg, ... others?
lemma dvd_sum {α : Type*} {R : Type*} [comm_ring R]
  (s : finset α) (f : α → R) (b : R) (H : ∀ a ∈ s, b ∣ f a) :
  b ∣ s.sum f :=
begin
  classical, revert H,
  apply finset.induction_on s,
  { intros, exact dvd_zero b, },
  intros a s has ih H,
  rw finset.forall_mem_insert at H,
  rw finset.sum_insert has,
  exact dvd_add H.1 (ih H.2)
end

lemma coe_nat_dvd {α : Type*} [comm_ring α] (m n : ℕ) (h : m ∣ n) :
  (m : α) ∣ n :=
by { rcases h with ⟨k, rfl⟩, refine ⟨k, by norm_cast⟩ }

instance {α : Type*} [comm_ring α] (I : ideal α) : is_ring_hom (ideal.quotient.mk I) :=
(ideal.quotient.mk_hom I).is_ring_hom

lemma mk_eq_mk_hom {α : Type*} [comm_ring α] (I : ideal α) (x : α) :
  ideal.quotient.mk I x = ideal.quotient.mk_hom I x :=
rfl

theorem ring_hom.map_geom_series₂ {α β : Type*} [comm_ring α] [comm_ring β] (x y : α) (n : ℕ)
  (f : α →+* β) : f (geom_series₂ x y n) = geom_series₂ (f x) (f y) n :=
by { rw [geom_series₂_def, geom_series₂_def, ← finset.sum_hom _ f],
    simp_rw [f.map_mul, f.map_pow] }

theorem geom_series₂_self {α : Type*} [comm_ring α] (x : α) (n : ℕ) :
  geom_series₂ x x n = n * x ^ (n-1) :=
calc  (finset.range n).sum (λ i, x ^ i * x ^ (n - 1 - i))
    = (finset.range n).sum (λ i, x ^ (i + (n - 1 - i))) : by simp_rw [← pow_add]
... = (finset.range n).sum (λ i, x ^ (n - 1)) : finset.sum_congr rfl
  (λ i hi, congr_arg _ $ nat.add_sub_cancel' $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
... = add_monoid.smul (finset.range n).card (x ^ (n - 1)) : finset.sum_const _
... = n * x ^ (n - 1) : by rw [finset.card_range, add_monoid.smul_eq_mul]


lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ℕ) [hp : fact p.prime]
  (a b : R) (h : (p : R) ∣ a - b) (k : ℕ) :
  (p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
begin
  induction k with k ih,
  { rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
  rw [nat.pow_succ, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ],
  refine mul_dvd_mul _ ih,
  rw [← ideal.mem_span_singleton, ← ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
  rw [← ideal.mem_span_singleton, ← ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom,
      ring_hom.map_geom_series₂, ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self,
      ← ring_hom.map_pow, ← ring_hom.map_pow, ← add_monoid.smul_eq_mul],
  erw [← (ideal.quotient.mk_hom (ideal.span ({p} : set R))).to_add_monoid_hom.map_smul,
      ideal.quotient.eq_zero_iff_mem],
  rw add_monoid.smul_eq_mul,
  exact ideal.mul_mem_right _ (ideal.mem_span_singleton.2 $ dvd_refl (p : R))
end

[Kenny Lau]

@Johan Commelin the trick is to use geom_series\2 and quotient ring

[Johan Commelin]

@Kenny Lau Sounds good. Thanks! Wanna make a PR?

[Kenny Lau]

go ahead

[Johan Commelin]

@Kenny Lau Golfed further:

lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ℕ) [hp : fact p.prime]
  (a b : R) (h : (p : R) ∣ a - b) (k : ℕ) :
  (p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
begin
  induction k with k ih,
  { rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
  rw [nat.pow_succ, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ],
  refine mul_dvd_mul _ ih,
  have : (p : R) ∈ ideal.span ({p} : set R), { rw ideal.mem_span_singleton },
  rw [← ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom, ring_hom.map_nat_cast] at this,
  rw [← ideal.mem_span_singleton, ← ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
  rw [← ideal.mem_span_singleton, ← ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom,
      ring_hom.map_geom_series₂, ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self,
      this, zero_mul],
end

[Kenny Lau]

@Johan Commelin aha, you applied the quotient philosophy even more

[Kevin Buzzard]

Wow, from a monster it's now at de Bruijn index 1!

[Johan Commelin]

#2640

[Johan Commelin]

Unexpected side effect: the proof doesn't use that p is prime (-;

[Johan Commelin]

Maybe not so unexpected after all. But that hypothesis certainly existed in my mental copy of this lemma (-;

[Johan Commelin]

Linters are good.

[Kenny Lau]

wow that's unexpected

[Mario Carneiro]

it's probably because you called the variable p

[Johan Commelin]

It's called n now (-;

[Reid Barton]

I sort of think it should still be called p

[Reid Barton]

I had no idea this was true for p not prime and I would certainly expect to see p in the theorem statement

[Johan Commelin]

Oops... I didn't update the theorem name...

[Johan Commelin]

@Reid Barton You can prove the special case, if you want :grinning_face_with_smiling_eyes:

[Reid Barton]

I don't need the special case, I just want the theorem statement to read as expected, with the prime p hypothesis mysteriously absent.

[Johan Commelin]

Sure, was only joking

[Kevin Buzzard]

Yeah I like that style, it's kind of an in joke

[Kevin Buzzard]

For 2 you can beat this result, 2^(k+2) divides the 2^kth power if k>=1.

[Johan Commelin]

And does this get used somewhere?

[Kevin Buzzard]

And the pair (1,5) show that this is tight for all k>=1

[Kevin Buzzard]

Analogous to the pair (1,p+1) showing its tight for odd primes

[Johan Commelin]

You mean for arbitrary p ≥ 3?

[Johan Commelin]

For p = 1 you can do even better than for p = 2!!!

[Kevin Buzzard]

Yes you can use it to demonstrate that 1+p resp 5 have large multiplicative orders mod p^n, and determine their order precisely

[Johan Commelin]

And is this fact about 5 used somewhere?

[Kevin Buzzard]

This gives you the structure theorem for the units of Z/p^nZ and then by CRT the structure of the units in Z/NZ

[Johan Commelin]

Aah, I see

[Kevin Buzzard]

Yes it tells you that the units in Z/32 have an element of order 8 and with that and the elements +-17 you know the structure of the group modulo the structure theorem

[Kevin Buzzard]

Which you can probably prove by hand here

[Johan Commelin]

dec_trivial?

[Johan Commelin]

Lol, just kidding

[Kevin Buzzard]

If only

[Johan Commelin]

But were you aware that this lemma doesn't need the primality assumption?

[Kevin Buzzard]

It's come_on_lean you need

[Kevin Buzzard]

No I didn't know

[Johan Commelin]

Would that give you a speed up for the structure theorem?

[Kevin Buzzard]

But everything I said needed it

[Johan Commelin]

Ok, I see

[Johan Commelin]

Well, we can make those tightness bounds into an issue for later

[David Wärn]

I think this is made more precise by the "Lifting the Exponent lemma", i.e. "$v_p(a^n - b^n) = v_p(a-b) + v_p(n)$ for p odd prime with p dividing $a-b$ but not a or b"

[Johan Commelin]

But that needs the primality assumption...

[David Wärn]

Probably one direction does, yes

[David Wärn]

Or maybe both... Not sure