# Theory Lucas_Theorem

(*
Title: Lucas_Theorem.thy
Author: Chelsea Edmonds, University of Cambridge
*)

theory Lucas_Theorem
imports Main
begin

notation fps_nth (infixl "$" 75) section ‹Extensions on Formal Power Series (FPS) Library› text ‹This section presents a few extensions on the Formal Power Series (FPS) library, described in \cite{Chaieb2011} › subsection ‹FPS Equivalence Relation › text ‹ This proof requires reasoning around the equivalence of coefficients mod some prime number. This section defines an equivalence relation on FPS using the pattern described by Paulson in \cite{paulsonDefiningFunctionsEquivalence2006}, as well as some basic lemmas for reasoning around how the equivalence holds after common operations are applied › definition "fpsmodrel p { (f, g). n. (f$ n) mod p = (g $n) mod p }" lemma fpsrel_iff [simp]: "(f, g) fpsmodrel p (n. (f$ n) mod p = (g $n) mod p)" by (simp add: fpsmodrel_def) lemma fps_equiv: "equiv UNIV (fpsmodrel p)" proof (rule equivI) show "refl (fpsmodrel p)" by (simp add: refl_on_def fpsmodrel_def) show "sym (fpsmodrel p)" by (simp add: sym_def fpsmodrel_def) show "trans (fpsmodrel p)" by (intro transI) (simp add: fpsmodrel_def) qed text ‹ Equivalence relation over multiplication › lemma fps_mult_equiv_coeff: fixes f g :: "('a :: {euclidean_ring_cancel}) fps" assumes "(f, g) fpsmodrel p" shows "(f*h)$n mod p = (g*h)$n mod p" proof - have "((f*h)$ n) mod p =(i=0..n. (f$i mod p * h$(n - i) mod p) mod p) mod p"
using mod_sum_eq mod_mult_left_eq
by (simp add: fps_mult_nth mod_sum_eq mod_mult_left_eq)
also have "... = (i=0..n. (g$i mod p * h$(n - i) mod p) mod p) mod p"
using assms by auto
also have "... = ((g*h) $n) mod p" by (simp add: mod_mult_left_eq mod_sum_eq fps_mult_nth) thus ?thesis by (simp add: calculation) qed lemma fps_mult_equiv: fixes f g :: "('a :: {euclidean_ring_cancel}) fps" assumes "(f, g) fpsmodrel p" shows "(f*h, g*h) fpsmodrel p" using fpsmodrel_def fps_mult_equiv_coeff assms by blast text ‹ Equivalence relation over power operator › lemma fps_power_equiv: fixes f g :: "('a :: {euclidean_ring_cancel}) fps" fixes x :: nat assumes "(f, g) fpsmodrel p" shows "(f^x, g^x) fpsmodrel p" using assms proof (induct x) case 0 thus ?case by (simp add: fpsmodrel_def) next case (Suc x) then have hyp: " n. f^x$ n mod p = g ^x $n mod p" using fpsrel_iff by blast thus ?case proof - have fact: "n h. (g * h)$ n mod p = (f * h) $n mod p" by (metis assms fps_mult_equiv_coeff) have "n h. (g ^ x * h)$ n mod p = (f ^ x * h) $n mod p" by (simp add: fps_mult_equiv_coeff hyp) then have "n h. (h * g ^ x)$ n mod p = (h * f ^ x) $n mod p" by (simp add: mult.commute) thus ?thesis using fact by force qed qed subsection ‹Binomial Coefficients › text ‹The @{term "fps_binomial"} definition in the formal power series uses the @{term "n gchoose k"} operator. It's defined as being of type @{typ "'a :: field_char_0 fps"}, however the equivalence relation requires a type @{typ 'a} that supports the modulo operator. The proof of the binomial theorem based on FPS coefficients below uses the choose operator and does not put bounds on the type of @{term "fps_X"}.› lemma binomial_coeffs_induct: fixes n k :: nat shows "(1 + fps_X)^n$ k = of_nat(n choose k)"
proof (induct n arbitrary: k)
case 0
thus ?case
by (metis binomial_eq_0_iff binomial_n_0 fps_nth_of_nat not_gr_zero of_nat_0 of_nat_1 power_0)
next
case h: (Suc n)
fix k
have start: "(1 + fps_X)^(n + 1) = (1 + fps_X) * (1 + fps_X)^n" by auto
show ?case
using One_nat_def Suc_eq_plus1 Suc_pred add.commute binomial_Suc_Suc binomial_n_0
fps_mult_fps_X_plus_1_nth h.hyps neq0_conv start by (smt of_nat_add)
qed

subsection ‹Freshman's Dream Lemma on FPS ›
text ‹ The Freshman's dream lemma modulo a prime number $p$ is a well known proof that $(1 + x^p) \equiv (1 + x)^p \mod p$›

text ‹ First prove that $\binom{p^n}{k} \equiv 0 \mod p$ for $k \ge 1$ and $k < p^n$. The eventual
proof only ended up requiring this with $n = 1$›

lemma pn_choose_k_modp_0:
fixes n k::nat
assumes "prime p"
"k  1  k  p^n - 1"
"n > 0"
shows "(p^n choose k) mod p = 0"
proof -
have inequality: "k  p^n" using assms (2) by arith
have choose_take_1: "((p^n - 1) choose ( k - 1))= fact (p^n - 1) div (fact (k - 1) * fact (p^n - k))"
using binomial_altdef_nat diff_le_mono inequality assms(2) by auto
have "k * (p^n choose k) = k * ((fact (p^n)) div (fact k * fact((p^n) - k)))"
using assms binomial_fact'[OF inequality] by auto
also have "... = k * fact (p^n) div (fact k * fact((p^n) - k))"
using binomial_fact_lemma div_mult_self_is_m fact_gt_zero inequality mult.assoc mult.commute
nat_0_less_mult_iff by smt
also have "... = k * fact (p^n) div (k * fact (k - 1) * fact((p^n) - k))"
by (metis assms(2) fact_nonzero fact_num_eq_if le0 le_antisym of_nat_id)
also have "... = fact (p^n) div (fact (k - 1) * fact((p^n) - k))"
using assms by auto
also have "... = ((p^n) * fact (p^n - 1)) div (fact (k - 1) * fact((p^n) - k))"
by (metis assms(2) fact_nonzero fact_num_eq_if inequality le0 le_antisym of_nat_id)
also have "... = (p^n) * (fact (p^n - 1) div (fact (k - 1) * fact((p^n) - k)))"
by (metis assms(2) calculation choose_take_1 neq0_conv not_one_le_zero times_binomial_minus1_eq)
finally have equality: "k * (p^n choose k) = p^n * ((p^n - 1) choose (k - 1))"
using assms(2) times_binomial_minus1_eq by auto
then have dvd_result: "p^n dvd (k * (p^n choose k))" by simp
have "¬ (p^n dvd k)"
using assms (2) binomial_n_0 diff_diff_cancel nat_dvd_not_less neq0_conv by auto
then have "p dvd (p^n choose k)"
using mult.commute prime_imp_prime_elem prime_power_dvd_multD assms dvd_result by metis
thus "?thesis" by simp
qed

text ‹ Applying the above lemma to the coefficients of $(1 + X)^p$, it is easy to show that all
coefficients other than the $0$th and $p$th will be $0$ ›

lemma fps_middle_coeffs:
assumes "prime p"
"n  0  n  p"
shows "((1 + fps_X :: int fps) ^p) $n mod p = 0 mod p" proof - let ?f = "(1 + fps_X :: int fps)^p" have " n. n > 0 n < p (p choose n) mod p = 0" using pn_choose_k_modp_0 by (metis (no_types, lifting) add_le_imp_le_diff assms(1) diff_diff_cancel diff_is_0_eq' discrete le_add_diff_inverse le_numeral_extra(4) power_one_right zero_le_one zero_less_one) then have middle_0: " n. n > 0 n < p (?f$ n) mod p = 0"
using binomial_coeffs_induct by (metis of_nat_0 zmod_int)
have " n. n > p  ?f $n mod p = 0" using binomial_eq_0_iff binomial_coeffs_induct mod_0 by (metis of_nat_eq_0_iff) thus ?thesis using middle_0 assms(2) nat_neq_iff by auto qed text ‹It follows that$(1+ X)^p$is equivalent to$(1 + X^p)$under our equivalence relation, as required to prove the freshmans dream lemma. › lemma fps_freshmans_dream: assumes "prime p" shows "(((1 + fps_X :: int fps ) ^p), (1 + (fps_X)^(p))) fpsmodrel p" proof - let ?f = "(1 + fps_X :: int fps)^p" let ?g = "(1 + (fps_X :: int fps)^p)" have all_f_coeffs: " n. n 0 n p ?f$ n mod p = 0 mod p"
using fps_middle_coeffs assms by blast
have "?g $0 = 1" using assms by auto then have "?g$ 0 mod p = 1 mod p"
using int_ops(2) zmod_int assms by presburger
then have "?g $p mod p = 1 mod p" using assms by auto then have " n . ?f$ n mod p = ?g $n mod p" using all_f_coeffs by (simp add: binomial_coeffs_induct) thus ?thesis using fpsrel_iff by blast qed section ‹Lucas's Theorem Proof› text ‹A formalisation of Lucas's theorem based on a generating function proof using the existing formal power series (FPS) Isabelle library› subsection ‹Reasoning about Coefficients Helpers› text ‹A generating function proof of Lucas's theorem relies on direct comparison between coefficients of FPS which requires a number of helper lemmas to prove formally. In particular it compares the coefficients of$(1 + X)^n \mod p$to$(1 + X^p)^N * (1 + X) ^rn \mod p$, where$N = n / p$, and$rn = n \mod p$. This section proves that the$k$th coefficient of$(1 + X^p)^N * (1 + X) ^rn = (N choose K) * (rn choose rk)$› text ‹Applying the @{term "fps_compose"} operator enables reasoning about the coefficients of$(1 + X^p)^n$using the existing binomial theorem proof with$X^p$instead of$X$.› lemma fps_binomial_p_compose: assumes "p 0" shows "(1 + (fps_X:: ('a :: {idom} fps))^p)^n = ((1 + fps_X)^n) oo (fps_X^p)" proof - have "(1::'a fps) + fps_X ^ p = 1 + fps_X oo fps_X ^ p" by (simp add: assms fps_compose_add_distrib) then show ?thesis by (simp add: assms fps_compose_power) qed text ‹ Next the proof determines the value of the$k$th coefficient of$(1 + X^p)^N$. › lemma fps_X_pow_binomial_coeffs: assumes "prime p" shows "(1 + (fps_X ::int fps)^p)^N$k = (if p dvd k then (N choose (k div p)) else 0)"
proof -
let ?fx = "(fps_X :: int fps)"
have "(1 + ?fx^p)^N $k = (((1 + ?fx)^N) oo (?fx^p))$k"
by (metis assms fps_binomial_p_compose not_prime_0)
also have "... = (i=0..k.((1 + ?fx)^N)$i * ((?fx^p)^i$k))"
finally have coeffs: "(1 + ?fx^p)^N $k = (i=0..k. (N choose i) * ((?fx^(p*i))$k))"
using binomial_coeffs_induct sum.cong by (metis (no_types, lifting) power_mult)
thus ?thesis
proof (cases "p dvd k")
case False ― ‹$p$ does not divide $k$ implies the $k$th term has a coefficient of 0›
have " i. ¬(p dvd k)  (?fx^(p*i)) $k = 0" by auto thus ?thesis using coeffs by (simp add: False) next case True ― ‹$p$divides$k$implies the$k$th term has a non-zero coefficient› have contained: "k div p {0.. k}" by simp have " i. i k div p (?fx^(p*i))$ k = 0" using assms by auto
then have notdivpis0: " i  ({0 .. k} - {k div p}). (?fx^(p*i)) $k = 0" by simp have "(1 + ?fx^p)^N$ k = (N choose (k div p)) * (?fx^(p * (k div p))) $k + (i({0..k} -{k div p}). (N choose i) * ((?fx^(p*i))$k))"
using contained coeffs sum.remove by (metis (no_types, lifting) finite_atLeastAtMost)
thus ?thesis using notdivpis0 True by simp
qed
qed

text ‹ The final helper lemma proves the $k$th coefficient is equivalent to $\binom{?N}{?K}*\binom{?rn}{?rk}$ as required.›
lemma fps_div_rep_coeffs:
assumes "prime p"
shows "((1 + (fps_X::int fps)^p)^(n div p) * (1 + fps_X)^(n mod p)) $k = ((n div p) choose (k div p)) * ((n mod p) choose (k mod p))" (is "((1 + (fps_X::int fps)^p)^?N * (1 + fps_X)^?rn)$ k = (?N choose ?K) * (?rn choose ?rk)")
proof -
― ‹Initial facts with results around representation and 0 valued terms›
let ?fx = "fps_X :: int fps"
have krep: "k - ?rk = ?K*p"
have rk_in_range: "?rk  {0..k}" by simp
have " i  p. (?rn choose i) = 0"
using binomial_eq_0_iff
by (metis assms(1) leD le_less_trans linorder_cases mod_le_divisor mod_less_divisor prime_gt_0_nat)
then have ptok0: " i  {p..k}. ((?rn choose i) * (1 + ?fx^p)^?N $(k - i)) = 0" by simp then have notrkis0: "i {0.. k}. i ?rk (?rn choose i) * (1 + ?fx^p)^?N$ (k - i) = 0"
proof (cases "k < p")
case True ― ‹When $k < p$, it presents a side case with regards to range of reasoning›
then have k_value: "k = ?rk" by simp
then have " i < k. ¬ (p dvd (k - i))"
using True by (metis diff_diff_cancel diff_is_0_eq dvd_imp_mod_0 less_imp_diff_less less_irrefl_nat mod_less)
then show ?thesis using fps_X_pow_binomial_coeffs assms(1) k_value by simp
next
case False
then have " i < p. i  ?rk  ¬(p dvd (k - i))"
using mod_nat_eqI by auto
then have " i  {0..<p}. i  ?rk  (1 + ?fx^p)^?N $(k - i) = 0" using assms fps_X_pow_binomial_coeffs by simp then show ?thesis using ptok0 by auto qed ― ‹Main body of the proof, using helper facts above› have "((1 + fps_X^p)^?N * (1 + fps_X)^?rn)$ k = (((1 + fps_X)^?rn) * (1 + fps_X^p)^?N) $k" by (metis (no_types, hide_lams) distrib_left distrib_right fps_mult_fps_X_commute fps_one_mult(1) fps_one_mult(2) power_commuting_commutes) also have "... = (i=0..k.(of_nat(?rn choose i)) * ((1 + (fps_X)^p)^?N$ (k - i)))"
also have "... =  ((?rn choose ?rk) * (1 + ?fx^p)^?N $(k - ?rk)) + (i({0..k} - {?rk}). (?rn choose i) * (1 + ?fx^p)^?N$ (k - i))"
using rk_in_range sum.remove by (metis (no_types, lifting) finite_atLeastAtMost)
finally have "((1 + ?fx^p)^?N * (1 + ?fx)^?rn) $k = ((?rn choose ?rk) * (1 + ?fx^p)^?N$ (k - ?rk))"
using notrkis0 by simp
thus ?thesis using fps_X_pow_binomial_coeffs assms krep by auto
qed

(* Lucas theorem proof *)
subsection ‹Lucas Theorem Proof›

text ‹ The proof of Lucas's theorem combines a generating function approach, based off \cite{Fine} with induction.
For formalisation purposes, it was easier to first prove a well known corollary of the main theorem (also
often presented as an alternative statement for Lucas's theorem), which can itself be used to backwards
prove the the original statement by induction.
This approach was adapted from P. Cameron's lecture notes on combinatorics \cite{petercameronNotesCombinatorics2007} ›

subsubsection ‹ Proof of the Corollary ›
text ‹ This step makes use of the coefficient equivalence arguments proved in the previous sections ›
corollary lucas_corollary:
fixes n k :: nat
assumes "prime p"
shows "(n choose k) mod p = (((n div p) choose (k div p)) * ((n mod p) choose (k mod p))) mod p"
(is "(n choose k) mod p = ((?N choose ?K) * (?rn choose ?rk)) mod p")
proof -
let ?fx = "fps_X :: int fps"
have n_rep: "n = ?N * p  + ?rn"
by simp
have k_rep: "k =?K * p + ?rk" by simp
have rhs_coeffs: "((1 + ?fx^p)^(?N) * (1 + ?fx)^(?rn)) $k = (?N choose ?K) * (?rn choose ?rk)" using assms fps_div_rep_coeffs k_rep n_rep by blast ― ‹Application of coefficient reasoning› have "((((1 + ?fx)^p)^(?N) * (1 + ?fx)^(?rn)), ((1 + ?fx^p)^(?N) * (1 + ?fx)^(?rn))) fpsmodrel p" using fps_freshmans_dream assms fps_mult_equiv fps_power_equiv by blast ― ‹Application of equivalence facts and freshmans dream lemma› then have modrel2: "((1 + ?fx)^n, ((1 + ?fx^p)^(?N) * (1 + ?fx)^(?rn))) fpsmodrel p" by (metis (mono_tags, hide_lams) mult_div_mod_eq power_add power_mult) thus ?thesis using fpsrel_iff binomial_coeffs_induct rhs_coeffs by (metis of_nat_eq_iff zmod_int) qed subsubsection ‹ Proof of the Theorem › text ‹The theorem statement requires a formalised way of referring to the base$p$representation of a number. We use a definition that specifies the$i$th digit of the base$p$representation. This definition is originally from the Hilbert's 10th Problem Formalisation project \cite{bayerDPRMTheoremIsabelle2019} which this work contributes to.› definition nth_digit_general :: "nat nat nat nat" where "nth_digit_general num i base = (num div (base ^ i)) mod base" text ‹Applying induction on$d$, where$d$is the highest power required in either$n$or$k$'s base$p\$
representation, @{thm lucas_corollary} can be used to prove the original theorem.›

theorem lucas_theorem:
fixes n k d::nat
assumes "n < p ^ (Suc d)"
assumes "k < p ^ (Suc d)"
assumes "prime p"
shows "(n choose k) mod p = (id. ((nth_digit_general n i p) choose (nth_digit_general k i p))) mod p"
using assms
proof (induct d arbitrary: n k)
case 0
thus ?case using nth_digit_general_def assms by simp
next
case (Suc d)
― ‹Representation Variables›
let ?N = "n div p"
let ?K = "k div p"
let ?nr = "n mod p"
let ?kr = "k mod p"
― ‹Required assumption facts›
have Mlessthan: "?N < p ^ (Suc d)"
using less_mult_imp_div_less power_Suc2 assms(3) prime_ge_2_nat Suc.prems(1) by metis
have Nlessthan: "?K < p ^ (Suc d)"
using less_mult_imp_div_less power_Suc2 prime_ge_2_nat Suc.prems(2) assms(3) by metis
have shift_bounds_fact: "(i=(Suc 0)..(Suc (d )). ((nth_digit_general n i p) choose (nth_digit_general k i p))) =
(i=0..(d).  (nth_digit_general n (Suc i) p) choose (nth_digit_general k (Suc i) p))"
using prod.shift_bounds_cl_Suc_ivl by blast ― ‹Product manipulation helper fact›
have "(n choose k ) mod p = ((?N choose ?K) * (?nr choose ?kr)) mod p"
using lucas_corollary assms(3) by blast ― ‹Application of corollary›
also have "...= ((id. ((nth_digit_general ?N i p) choose (nth_digit_general ?K i p))) * (?nr choose ?kr)) mod p"
using Mlessthan Nlessthan Suc.hyps mod_mult_cong assms(3) by blast ― ‹Using Inductive Hypothesis›
― ‹Product manipulation steps›
also have "... = ((i=0..(d). (nth_digit_general n (Suc i) p) choose (nth_digit_general k (Suc i) p)) * (?nr choose ?kr)) mod p"
using  atMost_atLeast0 nth_digit_general_def div_mult2_eq by auto
also have "... = ((i=1..(d+1). (nth_digit_general n i p) choose (nth_digit_general k i p)) *
((nth_digit_general n 0 p) choose (nth_digit_general k 0 p))) mod p"
using nth_digit_general_def shift_bounds_fact by simp
finally have "(n choose k ) mod p = ((i=0..(d+1). (nth_digit_general n i p) choose (nth_digit_general k i p))) mod p"
using One_nat_def atMost_atLeast0 mult.commute prod.atLeast1_atMost_eq prod.atMost_shift
by (smt Suc_eq_plus1 shift_bounds_fact)
thus ?case
using Suc_eq_plus1 atMost_atLeast0 by presburger
qed

end