Formalizing Lucas' theorem

Stream: general

[Alexander Valentino]

Hi I'm a first-year mathematics undergraduate and I'd like to formalize Lucas' theorem (https://en.wikipedia.org/wiki/Lucas%27s_theorem), and I've completed everything but the inequality world in the natural number game, but I can't find how to define non-base 10 numbers, and easily be able to play around with the indices of products and sums. Where should I look to learn more about how to do such a thing? Is this a relevant thing to prove in Lean and try to get added to mathlib?

[Johan Commelin]

I think mathlib has docs#nat.digits which computes digits in some arbitrary base.

[Alexander Valentino]

Johan Commelin said:

I think mathlib has docs#nat.digits which computes digits in some arbitrary base.

Thank you, what about manipulating indicies? Or should I be asking this question elsewhere in the new members channel?

[Johan Commelin]

No, it's fine to ask it here

[Johan Commelin]

@Alexander Valentino What do you mean exactly with "manipulating indices"?

[Alexander Valentino]

Hi there, I'm wondering what would I need to grasp from starting with just having completed most of the natural number game to formalizing this theorem, copying the proof via generating functions from Wikipedia (https://en.wikipedia.org/wiki/Lucas%27s_theorem)?

[Alex J. Best]

It looks like the first half of the proof can be proved via docs#add_pow_char_pow_of_commute, other than that it would help to get a bit used to the material in https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html I guess.

[Yaël Dillies]

I remember seeing Lucas' theorem or something very close to it... Let me dig again.

[Bolton Bailey]

I have been working on this in #8820
Actually, this PR is Lucas' Primality theorem. Perhaps this is what Yaël was thinking of.

[Gareth Ma]

Hi, it's been two years, time to fix this :) I proved it here

[Gareth Ma]

I only proved the weaker version $\binom{n}{k} \equiv \binom{n \pmod{p}}{k \pmod{p}} \binom{n / p}{k / p} \pmod{p}$ but the full version can be done via induction. Can someone check if my formulation of lucas' is correct, or is there a better way to do it? Johan proposed .digits above but I'm not sure if it's the correct way

[Gareth Ma]

And I think sum_ite_iff_eqshould be in Mathlib so that it's more convenient to rewrite sums, but I don't know how to name it

[Gareth Ma]

Also the proof is quite slow and I don't know why. Here's profiler trace:

typeclass inference of CoeFun took 181ms
typeclass inference of CoeT took 201ms
typeclass inference of CoeT took 193ms
typeclass inference of CoeT took 184ms
typeclass inference of CoeFun took 164ms
typeclass inference of CoeT took 193ms
typeclass inference of CoeT took 191ms
typeclass inference of CoeT took 190ms
typeclass inference of CoeFun took 169ms
typeclass inference of CoeT took 197ms

[Yaël Dillies]

Your second lemma is just docs#ZMod.int_cast_eq_int_cast_iff

[Gareth Ma]

Yep, thanks

[Moritz Firsching]

your sum_ite_iff_eq can be golfed a little:

lemma sum_ite_iff_eq [DecidableEq α] [AddCommMonoid β]
    {p : α → Prop} [DecidablePred p]
    {f : α → β} {a : α} {s : Finset α}
    (h : ∀ x ∈ s, p x ↔ x = a) :
    (∑ x in s, if p x then f x else 0) = (if a ∈ s then f a else 0) :=
  (sum_ite_eq' s a f).symm ▸ sum_congr rfl (fun a => fun ha => if_congr (h a ha) rfl rfl)

[Gareth Ma]

@Moritz Firsching In that case, you can :curry: the function to fun a ha => too :) Thanks!

[Gareth Ma]

https://github.com/grhkm21/lean4/commit/0ec5a46d02a7d89e0e388e6c8ba856642e08304a
Here's the newest version. If someone wants to prove the full version please go ahead, as I will be travelling for the next few days :)
Though I can definitely do it when I come back

[Ruben Van de Velde]

Should this go into mathlib? :)

[Gareth Ma]

Yeah

[Gareth Ma]

But I think there are some other relevant theorems that’s provable

[Gareth Ma]

Maybe some generalisations - I remember one for mod p^2 for example, but it’s quite a lot more complicated

[Ruben Van de Velde]

Don't let the complete be the enemy of the good

[Gareth Ma]

Okay, I will start a draft PR first to force myself to progress :joy:

[Gareth Ma]

here we go. I will work on it afterwards, but PRs would be appreciated too :)