Theory Periodicity_Lemma
theory Periodicity_Lemma
imports CoWBasic
begin
chapter "The Periodicity Lemma"
text‹The Periodicity Lemma says that if a sufficiently long word has two periods p and q,
then the period can be refined to @{term "gcd p q"}.
The consequence is equivalent to the fact that the corresponding periodic roots commute.
``Sufficiently long'' here means at least @{term "p + q - gcd p q"}.
It is also known as the Fine and Wilf theorem due to its authors \cite{ FineWilf}.›
text‹
If we relax the requirement to @{term "p + q"}, then the claim becomes easy, and it is proved in theory @{theory Combinatorics_Words.CoWBasic} as @{term two_pers_root}: @{thm[names_long] two_pers_root[no_vars]}.
›
theorem per_lemma_relaxed:
assumes "period w p" and "period w q" and "p + q ≤ ❙|w❙|"
shows "(take p w)⋅(take q w) = (take q w)⋅(take p w)"
using two_pers_root[OF
‹period w p›[unfolded period_def[of w p]]
‹period w q›[unfolded period_def[of w q]], unfolded
take_len[OF add_leD1[OF ‹p + q ≤ ❙|w❙|›]]
take_len[OF add_leD2[OF ‹p + q ≤ ❙|w❙|›]], OF ‹p + q ≤ ❙|w❙|›].
section ‹Main claim›
text‹We first formulate the claim of the Periodicity lemma in terms of commutation of two periodic roots.
For trivial reasons we can also drop the requirement that the roots are nonempty.
The proof is by induction which mimics the Euclidean algorithm. The step is given by the following lemma:
›
lemma per_lemma_step:
fixes u v' w' :: "'a list"
defines "w ≡ u ⋅ w'" and "v ≡ u ⋅ v'"
shows
per_lemma_step_pers: "w ≤p u ⋅ w ∧ w ≤p v ⋅ w ⟷ w' ≤p u ⋅ w' ∧ w' ≤p v' ⋅ w'"
proof
assume a1: "w' ≤p u ⋅ w' ∧ w' ≤p v' ⋅ w'"
show "w ≤p u ⋅ w ∧ w ≤p v ⋅ w"
unfolding w_def v_def
by (rule conjI, unfold pref_cancel_conv rassoc) (use a1 pref_prolong in blast)+
next
assume a2: "w ≤p u ⋅ w ∧ w ≤p v ⋅ w"
hence "w' ≤p u ⋅ w'" "w' ≤p v' ⋅ w"
unfolding w_def v_def
by force+
then show "w' ≤p u ⋅ w' ∧ w' ≤p v' ⋅ w'"
unfolding w_def
using pref_prod_pref by blast
qed
theorem per_lemma_comm:
assumes "w ≤p r ⋅ w" and "w ≤p s ⋅ w"
and len: "❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|"
shows "r ⋅ s = s ⋅ r"
using assms
proof (induction "❙|s❙| + ❙|s❙| + ❙|r❙|" arbitrary: w r s rule: less_induct)
case less
consider (empty) "s = ε" | (short) "❙|r❙| < ❙|s❙|" | (step) "s ≠ ε ∧ ❙|s❙| ≤ ❙|r❙|" by force
then show ?case
proof (cases)
case (empty)
thus "r ⋅ s = s ⋅ r"
by fastforce
next
case (short)
show "r ⋅ s = s ⋅ r"
proof (rule "less.hyps"[symmetric])
show "❙|r❙| + ❙|r❙| + ❙|s❙| < ❙|s❙| + ❙|s❙| + ❙|r❙|"
using short by simp
show "❙|s❙| + ❙|r❙| - (gcd ❙|s❙| ❙|r❙|) ≤ ❙|w❙|"
unfolding gcd.commute[of "❙|s❙|"] add.commute[of "❙|s❙|"] by fact
qed fact+
next
case (step)
hence "s ≠ ε" and "❙|s❙| ≤ ❙|r❙|"
by blast+
from le_add_diff[OF gcd_le2_nat[OF ‹s ≠ ε›[folded length_0_conv], of "❙|r❙|"], unfolded gcd.commute[of "❙|r❙|"], of "❙|r❙|"]
have "❙|r❙| ≤ ❙|w❙|"
using ‹❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|›[unfolded gcd.commute[of "❙|r❙|"] add.commute[of "❙|r❙|"]] order.trans by blast
hence "❙|s❙| ≤ ❙|w❙|"
using ‹❙|s❙| ≤ ❙|r❙|› order.trans by blast
from pref_prod_long[OF ‹w ≤p s ⋅ w› this]
have "s ≤p r"
using prefix_order.trans[OF _ ‹w ≤p r ⋅ w›] pref_prod_le ‹❙|s❙| ≤ ❙|r❙|›
by blast
hence r: "s ⋅ s¯⇧>r = r" and w': "s ⋅ s¯⇧>w = w"
using ‹s ≤p w› by simp_all
from per_lemma_step[of s "s¯⇧>w" "s¯⇧>r", unfolded w' r]
have new_pers: "s¯⇧>w ≤p s¯⇧>r ⋅ s¯⇧>w" "s¯⇧>w ≤p s ⋅ s¯⇧>w"
using ‹w ≤p s ⋅ w› ‹w ≤p r ⋅ w› unfolding w' by blast+
have ind_len: "❙|s¯⇧>r❙| + ❙|s❙| - (gcd ❙|s¯⇧>r❙| ❙|s❙|) ≤ ❙|s¯⇧>w❙|"
using ‹❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|›[folded lenarg[OF ‹s ⋅ s¯⇧>w = w›]]
unfolding pref_gcd_lq[OF ‹s ≤p r›, unfolded gcd.commute[of "❙|s❙|"]] lenmorph lq_short_len[OF ‹s ≤p r›, unfolded add.commute[of "❙|s❙|"]] by force
have "s ⋅ s¯⇧>r = s¯⇧>r ⋅ s"
using "less.hyps"[OF _ new_pers ind_len] ‹s ≤p r›
unfolding prefix_def
by force
thus "r ⋅ s = s ⋅ r"
using ‹s ≤p r› by (fastforce simp add: prefix_def)
qed
qed
text‹We can now prove the numeric version.›
theorem per_lemma: assumes "period w p" and "period w q" and len: "p + q - gcd p q ≤ ❙|w❙|"
shows "period w (gcd p q)"
proof-
have takep: "w ≤p (take p w) ⋅ w" and takeq: "w ≤p (take q w) ⋅ w"
using ‹period w p› ‹period w q› per_pref by blast+
have "p ≤ ❙|w❙|"
using per_lemma_len_le[OF len] per_not_zero[OF ‹period w q›].
have lenp: "❙|take p w❙| = p"
using gcd_le2_pos[OF per_not_zero[OF ‹period w q›], of p] len take_len
by auto
have lenq: "❙|take q w❙| = q"
using gcd_le1_pos[OF per_not_zero[OF ‹period w p›], of q] len take_len
by simp
obtain t k m where "take p w = t⇧@k" and "take q w = t⇧@m" and "t ≠ ε"
using commE[OF per_lemma_comm[OF takep takeq, unfolded lenp lenq, OF len]].
have "w <p t ⋅ w"
using per_root_drop_exp[OF ‹period w p›[unfolded period_def ‹take p w = t⇧@k›]].
with per_nemp[OF ‹period w q›]
have "period w ❙|t❙|"
by (rule periodI)
have "❙|t❙| dvd (gcd p q)"
using lenp[unfolded ‹take p w = t⇧@k›] lenq[unfolded ‹take q w = t⇧@m›] nemp_len[OF ‹t ≠ ε›]
unfolding lenmorph pow_len by force
from dvd_div_mult_self[OF this]
have "gcd p q div ❙|t❙| * ❙|t❙| = gcd p q".
have "gcd p q ≠ 0"
using ‹period w p› by auto
from this[folded dvd_div_eq_0_iff[OF ‹❙|t❙| dvd (gcd p q)›]]
show "period w (gcd p q)"
using per_mult[OF ‹period w ❙|t❙|›, of "gcd p q div ❙|t❙|", unfolded dvd_div_mult_self[OF ‹❙|t❙| dvd (gcd p q)›]] by blast
qed
section ‹Optimality of the bound by construction of the Fine and Wilf word.›
text‹‹FW_word› (where FW stands for Fine and Wilf) yields a word which shows the optimality of the bound in the Periodicity lemma.›
definition "fw_per k d ≡ [0..<d]⇧@k ⋅ [0..<(d-1)]"
definition "fw_base k d ≡ fw_per k d ⋅ [d] ⋅ fw_per k d"
fun FW_word :: "nat ⇒ nat ⇒ nat list" where
FW_word_def: "FW_word p q =
(if q < p then FW_word q p else
if p = 0 then ε else
if p dvd q then ε else
if gcd p q = q - p then fw_base (p div (gcd p q) -1) (gcd p q)
else (take p (FW_word p (q-p))) ⋅ FW_word p (q-p))"
lemma FW_sym: "FW_word p q = FW_word q p"
by (cases rule: linorder_cases[of p q]) simp+
lemma FW_dvd: assumes "p dvd q" shows "FW_word p q = ε"
proof (cases "q = 0", use FW_word_def[of p q] in force)
assume "q ≠ 0"
hence "¬ q < p"
using assms by auto
thus ?thesis
using FW_word_def ‹p dvd q› by auto
qed
lemma upt_minus_pref: "[i..< j-d] ≤p [i..< j]"
by (rule le_cases[of j d], force)
(use upt_add_eq_append[of i "j-d" d] in fastforce)
lemma fw_per_pref: "fw_per k d ≤p take d (fw_per k d) ⋅ (fw_per k d)"
proof-
consider "k = 0 ∨ d = 0" | "0 < k ∧ 0 < d"
by fastforce
thus ?thesis
proof(cases)
assume "k = 0 ∨ d = 0"
then show ?thesis
unfolding fw_per_def by fastforce
next
assume "0 < k ∧ 0 < d"
hence "0 < k" "0 < d"
by blast+
hence nemp: "[0..<d] ⇧@ k ≠ ε"
using emp_pow_pos_emp[OF _ ‹0 < k›, of "[0..<d]"]
unfolding upt_eq_Nil_conv[of 0 d] by blast
have t: "take d (fw_per k d) = [0..<d]"
unfolding fw_per_def pow_pos[OF ‹0 < k›]
butlast_append if_not_P[OF nemp] by auto
show ?thesis
unfolding t unfolding fw_per_def
unfolding lassoc pow_comm[symmetric]
unfolding rassoc pref_cancel_conv
using upt_minus_pref by simp
qed
qed
lemma fw_per_len: shows "❙|fw_per k d❙| = (k+1)*d - 1"
unfolding fw_per_def lenmorph pow_len
by (cases "d = 0") fastforce+
lemma fw_base_len: assumes "0 < d" shows "❙|fw_base k d❙| = (k+1)*d + (k+1)*d - 1"
unfolding fw_base_def lenmorph fw_per_len sing_len using assms by simp
lemma fw_base_per1: assumes "0 < d"
shows "period (fw_base k d) ((k+1)*d)"
proof-
have take: "take ((k+1)*d) (fw_base k d) = fw_per k d ⋅ [d]"
unfolding fw_base_def lassoc using fw_per_len ‹0 < d› by force
show "period (fw_base k d) ((k+1)*d)"
unfolding period_def take unfolding fw_base_def by force
qed
lemma fw_base_per2: assumes "0 < d"
shows "period (fw_base k d) ((k+1)*d + d)"
unfolding period_def
proof (rule per_rootI)
show "take ((k+1)*d + d) (fw_base k d) ≠ ε"
using ‹0 < d› unfolding fw_base_def by simp
have t1: "take ((k+1)*d) (fw_base k d) = fw_per k d ⋅ [d]"
unfolding fw_base_def lassoc using fw_per_len ‹0 < d› by force
have "❙|fw_per k d ⋅ [d]❙| = (k+1)*d"
using fw_per_len unfolding lenmorph sing_len using ‹0 < d› by simp
hence d: "drop ((k+1)*d) (fw_per k d ⋅ [d] ⋅ fw_per k d) = fw_per k d"
unfolding lassoc using drop_pref by metis
show "fw_base k d ≤p take (((k+1)*d) + d) (fw_base k d) ⋅ fw_base k d"
unfolding take_add t1 unfolding fw_base_def rassoc pref_cancel_conv d
using fw_per_pref pref_prolong triv_pref by meson
qed
lemma fw_base_not_per: assumes "0 < d" "0 < k"
shows "¬ period (fw_base k d) d" (is "¬ period ?w d")
proof
have u: "take d ?w = [0..< d]"
unfolding fw_base_def fw_per_def pow_pos[OF ‹0 < k›] by force
have suc: "[0..<d] = [0..<d-1]⋅[d-1]"
using ‹0 < d› upt_Suc_append[of 0 "d-1"] by fastforce
assume "period ?w d"
hence "?w ≤p [0..< d] ⋅ ?w"
unfolding period_def u[symmetric] by blast
hence "fw_per k d ⋅ [d] ≤p [0..< d] ⋅ fw_per k d ⋅ [d]"
unfolding fw_base_def lassoc
using pref_cancel_right by blast
hence " [0..<d-1] ⋅ [d] ≤p [0..<d] ⋅ [0..<d-1] ⋅ [d]"
unfolding u fw_per_def pow_pos[OF ‹0 < k›]
unfolding lassoc pow_comm[symmetric] by fastforce
from pref_prod_eq[OF this]
have eq: "[0..<d-1] ⋅ [d] = [0..<d]"
using ‹0 < d› by simp
thus False
using ‹0 < d› unfolding suc cancel by fastforce
qed
lemma per_mod: "period w n ⟹ i < ❙|w❙| ⟹ w!i = w!(i mod n)"
proof (induct i rule: less_induct)
case (less i)
then show ?case
proof (cases "i < n", unfold mod_less[of i n], blast)
assume "¬ i < n"
with per_not_zero[OF ‹period w n›]
have "i - n + n = i" "i - n < i" "i - n < ❙|w❙|" "(i - n) mod n = i mod n"
using ‹i < ❙|w❙|› mod_add_self2[of "i-n" n] by force+
from less.hyps[OF ‹i - n < i› ‹period w n› ‹i - n < ❙|w❙|›]
show "w ! i = w ! (i mod n)"
unfolding period_indeces[OF ‹period w n›, of "i-n", unfolded ‹i - n + n = i›, OF ‹i < ❙|w❙|›] ‹(i - n) mod n = i mod n›.
qed
qed
lemma fw_per_per: assumes "fw_per k d ≠ ε"
shows "period (fw_per k d) d"
unfolding period_def
proof (rule per_rootI[OF fw_per_pref])
show "take d (fw_per k d) ≠ ε"
using assms unfolding take_eq_Nil fw_per_def by fastforce
qed
lemma fw_per_nth: assumes "i < ❙|fw_per k d❙|"
shows "(fw_per k d)!i = i mod d"
proof (cases "k = 0")
assume "k = 0"
then show ?thesis
using assms unfolding fw_per_def by force
next
assume "k ≠ 0"
hence "0 < k"
by blast
have "fw_per k d ≠ ε"
using assms by fastforce
hence "0 < d"
unfolding fw_per_def by force
from per_mod[OF fw_per_per[OF ‹fw_per k d ≠ ε›] assms]
have mod: "fw_per k d ! i = fw_per k d ! (i mod d)".
show ?thesis
using assms nth_upt[of 0 "i mod d" d, unfolded add_0] mod_less_divisor[OF ‹0 < d›]
unfolding mod
unfolding fw_per_def pow_pos[OF ‹0 < k›] rassoc
using length_upt[of 0 d, unfolded diff_zero] unfolding nth_append by presburger
qed
lemma fw_base_nth: assumes "i < ❙|fw_base k d❙|"
shows "(fw_base k d)!i = (if i = ❙|fw_per k d❙| then d else i mod d)"
proof-
note formula = nth_append[of "fw_per k d ⋅ [d]" "fw_per k d" i, unfolded rassoc, folded fw_base_def]
show ?thesis
proof (rule linorder_cases[of i " ❙|fw_per k d❙|"])
assume "i = ❙|fw_per k d❙|"
hence "i < ❙|fw_per k d ⋅ [d]❙|"
by auto
show ?thesis
unfolding if_P[OF ‹i = ❙|fw_per k d❙|›] formula if_P[OF ‹i < ❙|fw_per k d ⋅ [d]❙|›]
unfolding ‹i = ❙|fw_per k d❙|› by simp
next
assume "i < ❙|fw_per k d❙|"
hence "i < ❙|fw_per k d ⋅ [d]❙|" "i ≠ ❙|fw_per k d❙|"
by auto
show ?thesis
unfolding formula if_not_P[OF ‹i ≠ ❙|fw_per k d❙|›] if_P[OF ‹i < ❙|fw_per k d ⋅ [d]❙|›]
using nth_append[of "fw_per k d" "[d]" i]
unfolding if_P[OF ‹i < ❙|fw_per k d❙|›] fw_per_nth[OF ‹i < ❙|fw_per k d❙|›].
next
assume "❙|fw_per k d❙| < i"
hence "¬ i < ❙|fw_per k d ⋅ [d]❙|" "i ≠ ❙|fw_per k d❙|" "❙|fw_per k d ⋅ [d]❙| ≤ i"
by auto
have diff_less: "i - ❙|fw_per k d ⋅ [d]❙| < ❙|fw_per k d❙|"
using diff_less_mono[OF assms ‹❙|fw_per k d ⋅ [d]❙| ≤ i›]
unfolding fw_base_def by force
have "d ≠ 0"
proof
assume "d = 0"
show False
using assms ‹❙|fw_per k d❙| < i› unfolding fw_base_def fw_per_def pow_len lenmorph
sing_len ‹d = 0› by force
qed
hence "(k + 1) * d - 1 + 1 = (k+1)*d"
by simp
have "(k+1)*d ≤ i"
using ‹❙|fw_per k d❙| < i› unfolding fw_per_len by force
show ?thesis
unfolding formula if_not_P[OF ‹i ≠ ❙|fw_per k d❙|›] if_not_P[OF ‹¬ i < ❙|fw_per k d ⋅ [d]❙|›]
fw_per_nth[OF diff_less]
unfolding lenmorph fw_per_len sing_len ‹(k + 1) * d - 1 + 1 = (k+1)*d›
using mod_mult_self3[of "k+1" d "i - (k + 1) * d"]
unfolding le_add_diff_inverse[OF ‹(k+1)*d ≤ i›] by force
qed
qed
lemma fw_base_match: assumes "i < ❙|fw_base k d❙|" "j < ❙|fw_base k d❙|" "i ≠ j" and
eq: "(fw_base k d)!i = (fw_base k d)!j"
shows "i mod d = j mod d" and "i ≠ ❙|fw_per k d❙|" and "j ≠ ❙|fw_per k d❙|"
proof (atomize (full), cases)
assume "d = 0"
hence "fw_base k d = [0]"
unfolding fw_base_def fw_per_def
by simp
have "i = j"
using assms(1-3) unfolding ‹fw_base k d = [0]› sing_len by blast
thus "i mod d = j mod d ∧ i ≠ ❙|fw_per k d❙| ∧ j ≠ ❙|fw_per k d❙|"
using ‹i ≠ j› by blast
next
assume "d ≠ 0"
hence "i mod d ≠ d" for i
using mod_less_divisor[of d i] by force
with eq[unfolded fw_base_nth[OF ‹i < ❙|fw_base k d❙|›] fw_base_nth[OF ‹j < ❙|fw_base k d❙|›]]
show "i mod d = j mod d ∧ i ≠ ❙|fw_per k d❙| ∧ j ≠ ❙|fw_per k d❙|"
using ‹i ≠ j› by metis
qed
lemma ext_per_sum: assumes "period w p" and "period w q" and "p ≤ ❙|w❙|"
shows "period ((take p w) ⋅ w) (p+q)"
proof-
have sum: "take (p + q) (take p w ⋅ w) = take p w ⋅ take q w"
unfolding take_add by (simp add: ‹p ≤ ❙|w❙|›)
show ?thesis
unfolding period_def sum rassoc
using pref_spref_prolong[OF self_pref spref_spref_prolong[OF assms(2,1)[unfolded period_def]]].
qed
lemma drop_per_diff: assumes "period w p" and "period w q" and "p < q" and "p < ❙|w❙|"
shows "period (drop p w) (q-p)"
proof-
have nemp: "take (q - p) (drop p w) ≠ ε"
using ‹p < ❙|w❙|› ‹p < q› by force
have t1: "take p w ⋅ drop p (take q w) = take q w"
unfolding drop_take take_add[symmetric] using ‹p < q› by simp
from per_lemma_step[of "take p w" "drop p w" "drop p (take q w)",
unfolded append_take_drop_id t1,
unfolded drop_take]
have "drop p w ≤p take (q - p) (drop p w) ⋅ drop p w"
using assms unfolding period_def using sprefD1 by blast
hence "drop p w <p take (q - p) (drop p w) ⋅ drop p w"
using nemp by blast
thus ?thesis
unfolding period_def.
qed
theorem fw_word: assumes "¬ p dvd q" "¬ q dvd p"
shows "❙|FW_word p q❙| = p + q - gcd p q - 1"
"period (FW_word p q) p" and "period (FW_word p q) q"
"¬ period (FW_word p q) (gcd p q)"
using assms
proof (atomize (full), induction "p + p + q" arbitrary: p q rule: less_induct)
case less
have "p ≠ 0"
using ‹¬ q dvd p› dvd_0_right[of q] by meson
hence "0 < p"
by simp
have "p ≠ q"
using ‹¬ p dvd q› by auto
then consider "q < p" | "p < q"
by linarith
then show ?case
proof (cases)
assume "q < p"
hence "q + q + p < p + p + q"
by simp
from "less.hyps"[OF this ‹¬ q dvd p› ‹¬ p dvd q›]
show ?case
unfolding FW_sym[of p q] gcd.commute[of p q] add.commute[of p q] by blast
next
assume "p < q"
hence "¬ q < p" "p + (q - p) = q" "p ≥ gcd p q" "q - p ≥ 1" "q -p ≠ 0"
using ‹p ≠ 0› ‹p < q› by auto
have "q - p ≥ gcd p q"
using ‹p < q› ‹p + (q - p) = q› ‹q -p ≠ 0› gcd_add2 gcd_le2_nat by metis
hence "q ≥ gcd p q + 1"
using ‹0 < p› ‹p + (q - p) = q› ‹p ≥ gcd p q› ‹q - p ≥ 1› by linarith
let ?w = "FW_word p q"
let ?d = "gcd p q"
let ?k = "p div gcd p q - 1"
let ?dw = "[0..<(gcd p q)]"
let ?pd = "p div (gcd p q)"
show ?thesis
proof (cases "?d = q - p")
assume "?d = q - p"
hence "p + ?d = q" "p + q - ?d = p + p" "0 < ?d" "?d ≠ q" "?d < q" "1 ≤ q - ?d"
using ‹p ≠ 0› ‹p < q› by auto
have "?d ≠ p"
using ‹¬ p dvd q› ‹gcd p q = q - p› gcd_unique_nat by metis
have kdp: "(?k + 1) * ?d = p"
by (metis ‹p ≠ 0› add.commute dvd_mult_div_cancel gcd_dvd1 less_one linordered_semidom_class.add_diff_inverse mult.commute mult_zero_right)
hence "0 < ?k"
using ‹?d ≠ p› add_0[of 1] mult_1 not_gr_zero by metis
let ?per = "fw_per ?k ?d"
have fw_base: "?w = fw_base ?k ?d"
unfolding FW_word_def[of p q] if_not_P[OF ‹¬ q < p›] if_not_P[OF ‹p ≠ 0›]
if_not_P[OF ‹p ≠ q›] if_P[OF ‹?d = q - p›] using less.prems(1) by argo
hence fw: "?w = ?per⋅[?d]⋅?per"
unfolding fw_base_def.
show "(❙|?w❙| = p + q - ?d - 1 ∧
period ?w p) ∧ period ?w q ∧
¬ period ?w ?d"
unfolding conj_assoc[symmetric]
proof (rule conjI)+
show "❙|?w❙| = p + q - ?d - 1"
unfolding fw_base fw_base_len[OF ‹0 < ?d›]
‹p + q - ?d = p + p› kdp..
show "period ?w p"
unfolding fw_base using fw_base_per1[OF ‹0 < ?d›, of ?k, unfolded kdp].
show "period ?w q"
unfolding fw_base using
fw_base_per2[OF ‹0 < ?d›, of ?k, unfolded kdp ‹p + gcd p q = q›].
show "¬ period ?w ?d"
using fw_base_not_per[OF ‹0 < ?d› ‹0 < ?k›] unfolding fw_base.
qed
next
assume "gcd p q ≠ q - p"
hence "q - p > gcd p q"
using ‹q - p ≥ gcd p q› by force
let ?w' = "FW_word p (q-p)"
have "gcd p (q-p) = ?d"
using gcd_add2[of p "q-p", unfolded le_add_diff_inverse[OF less_imp_le[OF ‹p < q›]], symmetric].
have fw: "?w = take p ?w' ⋅ ?w'"
using FW_word_def ‹p ≠ 0› ‹p ≠ q› ‹p < q› ‹gcd p q ≠ q - p›
‹¬ q < p› ‹¬ p dvd q› by meson
show "(❙|?w❙| = p + q - ?d - 1 ∧
period ?w p) ∧ period ?w q ∧
¬ period ?w ?d"
unfolding conj_assoc[symmetric]
proof (rule conjI)+
have divhyp1: "¬ p dvd q - p"
using ‹¬ p dvd q› ‹p < q› dvd_minus_self by auto
have divhyp2: "¬ q - p dvd p"
proof (rule notI)
assume "q - p dvd p"
have "q = p + (q - p)"
by (simp add: ‹p < q› less_or_eq_imp_le)
from gcd_add2[of p "q - p", folded this, unfolded gcd_nat.absorb2[of "q - p" p, OF ‹q - p dvd p›]]
show "False"
using ‹gcd p q ≠ q - p› by blast
qed
have lenhyp: "p + p + (q - p) < p + p + q"
using ‹p < q› ‹p ≠ 0› by linarith
have len_w': "❙|?w'❙| = p + (q - p) - ?d - 1" and "period ?w' p" and "period ?w' (q-p)" and
"¬ period ?w' (gcd p (q-p))"
using "less.hyps"[OF _ divhyp1 divhyp2] lenhyp
unfolding ‹gcd p (q-p) = ?d› by blast+
have "p ≤ ❙|?w'❙|"
unfolding len_w' using ‹q - p > gcd p q› by force
have "?w' ≠ ε"
using period_nemp[OF ‹period ?w' p›].
show "¬ period ?w ?d"
using ‹¬ period (FW_word p (q -p)) (gcd p (q-p))›
unfolding ‹gcd p (q-p) = ?d›
using period_fac[of "take p ?w'" "?w'" ε "?d", unfolded append_Nil2,
OF _ ‹?w' ≠ ε›, folded fw] by blast
show "❙|?w❙| = p + q - ?d - 1"
unfolding fw lenmorph len_w' take_len[OF ‹p ≤ ❙|?w'❙|›] ‹p + (q - p) = q›
using ‹q ≥ gcd p q + 1› by simp
show "period ?w p"
using fw ext_per_left[OF ‹period (FW_word p (q-p)) p› ‹p ≤ ❙|?w'❙|›]
by presburger
show "period ?w q"
using ext_per_sum[OF ‹period ?w' p› ‹period ?w' (q - p)› ‹p ≤ ❙|?w'❙|›, folded fw, unfolded ‹p + (q-p) = q›].
qed
qed
qed
qed
text‹Calculation examples›
section ‹Optimality of the Fine and Wilf word.›
text‹The ‹FW_word› is the most general word having the two desired properties. That is,
each equality of letters is forced by periods.›
lemma fw_base_mod_aux: assumes "(i :: nat) < p + p - 1" "i ≠ p - 1"
shows "i mod p < p - 1"
proof (cases p i rule: le_less_cases)
assume "p ≤ i"
have "i - p < p" "i - p < p - 1"
using diff_less_mono[OF ‹i < p + p - 1› ‹p ≤ i›] unfolding diff_cancel2 diff_diff_eq by simp_all
from le_mod_geq[OF ‹p ≤ i›]
have "i mod p = i - p"
unfolding mod_less[OF ‹i - p < p›].
thus ?thesis
using ‹i - p < p - 1› by argo
next
assume "i < p"
show ?thesis
unfolding mod_less[OF ‹i < p›]
using ‹i < p› ‹i ≠ p - 1› by linarith
qed
theorem fw_minimal: assumes "period w p" and "period w q" and "❙|w❙| = ❙|FW_word p q❙|" and
"i < ❙|w❙|" and "j < ❙|w❙|" and "(FW_word p q)!i = (FW_word p q)!j"
shows "w!i = w!j"
using assms
proof (induct "p + p + q" arbitrary: w i j p q rule: less_induct)
case less
have "FW_word p q ≠ ε"
using ‹j < ❙|w❙|› ‹❙|w❙| = ❙|FW_word p q❙|› emp_len[of "FW_word p q"] by linarith+
hence "¬ p dvd q" "0 < p"
using FW_dvd per_not_zero[OF less.prems(1)] by blast+
hence "1 < p"
using less_one nat_neq_iff one_dvd by metis
have "¬ q dvd p"
using FW_dvd ‹FW_word p q ≠ ε›[unfolded FW_sym[of p]] by blast
note fw_word[OF ‹¬ p dvd q› ‹¬ q dvd p›]
have w_len: "❙|w❙| = p + q - gcd p q - 1"
using fw_word(1)[OF ‹¬ p dvd q› ‹¬ q dvd p› ] unfolding ‹❙|w❙| = ❙|FW_word p q❙|›.
show "w ! i = w ! j"
proof (cases "i = j", blast)
assume "i ≠ j"
show "w ! i = w ! j"
proof (cases "q < p")
assume "q < p"
then show "w ! i = w ! j"
using less.hyps[OF _ less.prems(2,1) less.prems(3-6)[unfolded FW_sym[of p]]] by simp
next
assume "¬ q < p"
hence "p < q"
using ‹¬ p dvd q› linorder_neqE_nat by fastforce+
show "w ! i = w ! j"
proof (cases "gcd p q = q - p")
assume "gcd p q = q - p"
hence base: "FW_word p q = fw_base (p div (gcd p q) - 1) (gcd p q)"
using FW_word_def[of p q] ‹¬ q < p› ‹0 < p› ‹¬ p dvd q› by presburger
let ?d = "gcd p q"
let ?pref = "take (p-1) w"
let ?FW = "FW_word p q"
from ‹0 < p› dvd_div_eq_0_iff[OF gcd_nat.cobounded1, of p q]
have per_len: "❙|fw_per (p div ?d - 1) ?d❙| = p - 1"
unfolding fw_per_len
using dvd_mult_div_cancel[OF gcd_nat.cobounded1, of p q, unfolded mult.commute[of "?d"]] by force
have w_len': "❙|w❙| = p + p - 1"
unfolding w_len ‹?d = q - p› using ‹p < q› by auto
hence "p < ❙|w❙|" "p - 1 ≤ ❙|w❙|"
using ‹1 < p› by simp_all
have "i mod p mod ?d = i mod ?d"
using mod_mod_cancel[OF gcd_nat.cobounded1].
have ij_less: "i < ❙|?FW❙|" "j < ❙|?FW❙|"
using ‹i < ❙|w❙|› ‹j < ❙|w❙|› unfolding ‹❙|w❙| = ❙|?FW❙|› by force+
have "❙|?pref❙| = p - 1"
using ‹p - 1 ≤ ❙|w❙|› by simp
have mod_d_eq: "i mod ?d = j mod ?d" and not_max: "i ≠ p-1" "j ≠ p-1"
using fw_base_match[OF ij_less[unfolded base] ‹i ≠ j› ‹?FW ! i = ?FW ! j›[unfolded base]]
unfolding per_len by blast+
have "i mod p < p - 1" "j mod p < p - 1"
using fw_base_mod_aux ‹i < ❙|w❙|› ‹j < ❙|w❙|› not_max unfolding ‹❙|w❙| = p + p - 1› by blast+
have "period ?pref ?d"
proof-
have "drop p w = ?pref"
proof-
have "drop p w ≤p w"
using ‹period w p› unfolding per_shift by blast
moreover have "❙|drop p w❙| = p - 1"
using ‹❙|w❙| = p + p - 1› unfolding length_drop by force
ultimately show ?thesis
using pref_take_conv by metis
qed
show ?thesis
using drop_per_diff[OF ‹period w p› ‹period w q› ‹p < q› ‹p < ❙|w❙|›]
unfolding ‹drop p w = ?pref› ‹?d = q - p›.
qed
have mod_pref_reduce: "?pref ! (i mod p) = ?pref ! (i mod ?d)" "?pref ! (j mod p) = ?pref ! (j mod ?d)"
using per_mod[OF ‹period ?pref ?d›, unfolded ‹❙|?pref❙| = p - 1›, OF ‹i mod p < p-1›, unfolded mod_mod_cancel[OF gcd_nat.cobounded1]]
per_mod[OF ‹period ?pref ?d›, unfolded ‹❙|?pref❙| = p - 1›, OF ‹j mod p < p-1›, unfolded mod_mod_cancel[OF gcd_nat.cobounded1]].
have "?pref ! (i mod p) = ?pref ! (j mod p)"
unfolding mod_pref_reduce mod_d_eq..
thus "w ! i = w ! j"
unfolding nth_take[OF ‹i mod p < p-1›, of w] nth_take[OF ‹j mod p < p-1›, of w]
unfolding per_mod[OF ‹period w p› ‹i < ❙|w❙|›] per_mod[OF ‹period w p› ‹j < ❙|w❙|›].
next
assume "gcd p q ≠ q - p"
hence step: "FW_word p q = take p (FW_word p (q-p)) ⋅ FW_word p (q-p)"
unfolding FW_word_def[of p q] using ‹¬ q < p› ‹0 < p› ‹¬ p dvd q› by presburger
have "¬ p dvd (q-p)"
unfolding dvd_minus_self using ‹¬ q < p› ‹¬ p dvd q› by blast
have "¬ (q-p) dvd p"
using FW_dvd[of "q-p" p] FW_dvd[of "q-p" p, THEN Nil_take_Nil]
‹FW_word p q ≠ ε› unfolding step[unfolded FW_sym[of _ "q-p"]] by blast
have "gcd p (q - p) < (q - p)"
using ‹¬ q - p dvd p›[unfolded gcd_nat.absorb_iff2[of "q-p" p]]
nat_dvd_not_less[OF ‹p < q›[folded zero_less_diff[of q]], of "gcd p (q-p)"] by fastforce
hence "p ≤ ❙|FW_word p (q - p)❙|"
unfolding fw_word(1)[OF ‹¬ p dvd (q-p)› ‹¬ (q-p) dvd p›] by linarith
from drop_take_inv[OF this]
have fw': "FW_word p (q -p) = drop p (FW_word p q)"
using step by metis
have "p ≤ ❙|drop p w❙|"
using ‹p ≤ ❙|FW_word p (q - p)❙|› less.prems(3) unfolding fw' length_drop by argo
hence "p < ❙|w❙|"
using ‹0 < p› by fastforce
have "FW_word p (q - p) <p FW_word p q"
using ‹period (FW_word p q) p› unfolding per_shift fw'.
from sprefD1[OF this]
have "FW_word p (q - p) ! (i mod p) = FW_word p q ! (i mod p)" "FW_word p (q - p) ! (j mod p) = FW_word p q ! (j mod p)"
using pref_index[OF ‹FW_word p (q - p) ≤p FW_word p q›] less_le_trans[OF mod_less_divisor[OF ‹0 < p›] ‹p ≤ ❙|FW_word p (q-p)❙|›]
by blast+
with per_mod[OF ‹period (FW_word p q) p› ‹j < ❙|w❙|›[unfolded ‹❙|w❙| = ❙|FW_word p q❙|›]]
per_mod[OF ‹period (FW_word p q) p› ‹i < ❙|w❙|›[unfolded ‹❙|w❙| = ❙|FW_word p q❙|›]]
have reduce_fw: "FW_word p (q - p) ! (j mod p) = (FW_word p q) ! j" "FW_word p (q - p) ! (i mod p) = (FW_word p q) ! i"
by argo+
have "drop p w <p w"
using ‹period w p› unfolding per_shift.
from sprefD1[OF this]
have "drop p w ! (i mod p) = w ! (i mod p)" "drop p w ! (j mod p) = w ! (j mod p)"
using pref_index[OF ‹drop p w ≤p w›] less_le_trans[OF mod_less_divisor[OF ‹0 < p›] ‹p ≤ ❙|drop p w❙|›]
by blast+
with per_mod[OF ‹period w p› ‹j < ❙|w❙|›] per_mod[OF ‹period w p› ‹i < ❙|w❙|›]
have reduce_w: "w ! j = drop p w ! (j mod p)" "w ! i = drop p w ! (i mod p)"
by argo+
show "w ! i = w ! j"
unfolding reduce_w
proof(rule less.hyps[of p "q-p" "drop p w" "i mod p" "j mod p"])
show " p + p + (q - p) < p + p + q"
using ‹p < q› ‹0 < p› by linarith
show "period (drop p w) p"
using period_drop[OF ‹period w p› ‹p < ❙|w❙|›].
show "period (drop p w) (q - p)"
using drop_per_diff[OF ‹period w p› ‹period w q› ‹p < q› ‹p < ❙|w❙|›].
show "❙|drop p w❙| = ❙|FW_word p (q - p)❙|"
using fw' length_drop ‹❙|w❙| = ❙|FW_word p q❙|› by metis
show "i mod p < ❙|drop p w❙|" "j mod p < ❙|drop p w❙|"
using less_le_trans[OF mod_less_divisor[OF ‹0 < p›] ‹p ≤ ❙|drop p w❙|›] by blast+
show "FW_word p (q - p) ! (i mod p) = FW_word p (q - p) ! (j mod p)"
unfolding reduce_fw by fact
qed
qed
qed
qed
qed
theorem fw_minimal_set: assumes "period w p" and "period w q" and "❙|w❙| = ❙|FW_word p q❙|"
shows "card(set w) ≤ card(set (FW_word p q))"
proof-
let ?f = "λ n. (w ! (LEAST k.((FW_word p q)!k = n)))"
have map_f0: "?f ((FW_word p q)!i) = w!i" if "i < ❙|w❙|" for i
using fw_minimal[OF assms _ that LeastI[of "λ k.(FW_word p q ! k = FW_word p q ! i)", OF refl]]
Least_le[of "λ k.(FW_word p q ! k = FW_word p q ! i)", OF refl] that by linarith
have map_f: "map ?f (FW_word p q) = w"
by (rule nth_equalityI, unfold length_map, simp add: assms(3))
(use nth_map[of _ "FW_word p q" ?f] map_f0 assms(3) in presburger)
then have "set w = ?f ` (set (FW_word p q))"
using set_map[of ?f "FW_word p q"] by presburger
then show ?thesis
using card_image_le[of "set (FW_word p q)" ?f, OF finite_set] fw_minimal[OF assms] by presburger
qed
section "Other variants of the periodicity lemma"
text ‹Periodicity lemma is one of the most frequent tools in Combinatorics on words.
Here are some useful variants.›
text‹Note that the following lemmas are stronger versions of @{thm per_lemma_pref_suf fac_two_conjug_primroot fac_two_conjug_primroot fac_two_prim_conjug} that have a relaxed length assumption @{term "❙|p❙| + ❙|q❙| ≤ ❙|w❙|"} instead of @{term "❙|p❙| + ❙|q❙| - (gcd ❙|p❙| ❙|q❙|) ≤ ❙|w❙|"} (and which follow from the relaxed version of periodicity lemma @{thm two_pers}.›
lemma per_lemma_comm_pref:
assumes "u ≤p r⇧@k" "u ≤p s⇧@l"
and len: "❙|r❙| + ❙|s❙| - gcd (❙|r❙|) (❙|s❙|) ≤ ❙|u❙|"
shows "r ⋅ s = s ⋅ r"
using pref_pow_root[OF assms(2)] pref_pow_root[OF assms(1)] per_lemma_comm[OF _ _ len] by blast
lemma per_lemma_pref_suf_gcd: assumes "w <p p ⋅ w" and "w <s w ⋅ q" and
fw: "❙|p❙| + ❙|q❙| - (gcd ❙|p❙| ❙|q❙|) ≤ ❙|w❙|"
obtains r s k l m where "p = (r ⋅ s)⇧@k" and "q = (s ⋅ r)⇧@l" and "w = (r ⋅ s)⇧@m ⋅ r" and "primitive (r⋅s)"
proof-
let ?q = "(w ⋅ q)⇧<¯w"
have "w <p ?q ⋅ w"
using ssufD1[OF ‹w <s w ⋅ q›] rq_suf[symmetric, THEN per_rootI[OF prefI rq_ssuf_nemp[OF ‹w <s w ⋅ q›]]]
by argo
have "q ∼ ?q"
by (meson assms(2) conjugI1 conjug_sym rq_suf suffix_order.less_imp_le)
have nemps': "p ≠ ε" "?q ≠ ε"
using assms(1) ‹w <p ?q⋅w› by fastforce+
have "❙|p❙| + ❙|?q❙| - gcd (❙|p❙|) (❙|?q❙|) ≤ ❙|w❙|" using fw
unfolding conjug_len[OF ‹q ∼ ?q›].
from per_lemma_comm[OF sprefD1[OF ‹w <p p ⋅ w›] sprefD1[OF ‹w <p ?q⋅w›] this]
have "p ⋅ ?q = ?q ⋅ p".
then have "ρ p = ρ ?q" using comm_primroots[OF nemps'] by force
hence [symmetric]: "ρ q ∼ ρ p"
using conjug_primroot[OF ‹q ∼ (w ⋅ q)⇧<¯w›]
by argo
from conjug_primrootsE[OF this]
obtain r s k l where
"p = (r ⋅ s) ⇧@ k" and
"q = (s ⋅ r) ⇧@ l" and
"primitive (r ⋅ s)".
have "w ≤p (r⋅s)⋅w"
using assms per_root_drop_exp sprefD1 ‹p = (r ⋅ s) ⇧@ k›
by meson
have "w ≤s w⋅(s⋅r)"
using assms(2) per_root_drop_exp[reversed] ssufD1 ‹q = (s ⋅ r) ⇧@ l›
by meson
have "❙|r ⋅ s❙| ≤ ❙|w❙|"
using conjug_nemp_iff[OF ‹q ∼ ?q›] dual_order.trans length_0_conv nemps' per_lemma_len_le[OF fw] primroot_len_le[OF nemps'(1)]
unfolding primroot_unique[OF nemps'(1) ‹primitive (r ⋅ s)› ‹p = (r ⋅ s) ⇧@ k›]
by fastforce
from root_suf_conjug[OF ‹primitive (r ⋅ s)› ‹w ≤p (r⋅s)⋅w› ‹w ≤s w⋅(s⋅r)› this]
obtain m where "w = (r ⋅ s) ⇧@ m ⋅ r".
from that[OF ‹p = (r ⋅ s) ⇧@ k› ‹q = (s ⋅ r) ⇧@ l› this ‹primitive (r ⋅ s)›]
show ?thesis.
qed
lemma fac_two_conjug_primroot_gcd:
assumes facs: "w ≤f p⇧@k" "w ≤f q⇧@l" and nemps: "p ≠ ε" "q ≠ ε" and len: "❙|p❙| + ❙|q❙| - gcd (❙|p❙|) (❙|q❙|) ≤ ❙|w❙|"
obtains r s m where "ρ p ∼ r ⋅ s" and "ρ q ∼ r ⋅ s" and "w = (r ⋅ s)⇧@m ⋅ r" and "primitive (r⋅s)"
proof -
obtain p' where "w <p p'⋅w" "p ∼ p'" "p' ≠ ε"
using conjug_nemp_iff fac_pow_pref_conjug[OF facs(1)] nemps(1) per_rootI' by metis
obtain q' where "w <s w⋅q'" "q ∼ q'" "q' ≠ ε"
using fac_pow_pref_conjug[reversed, OF ‹w ≤f q⇧@l›] conjug_nemp_iff nemps(2) per_rootI'[reversed] by metis
from per_lemma_pref_suf_gcd[OF ‹w <p p'⋅w› ‹w <s w⋅q'›]
obtain r s k l m where
"p' = (r ⋅ s) ⇧@ k" and
"q' = (s ⋅ r) ⇧@ l" and
"w = (r ⋅ s) ⇧@ m ⋅ r" and
"primitive (r ⋅ s)"
using len[unfolded conjug_len[OF ‹p ∼ p'›] conjug_len[OF ‹q ∼ q'›]]
by metis
moreover have "ρ p' = r⋅s"
using ‹p' = (r ⋅ s) ⇧@ k› ‹primitive (r ⋅ s)› ‹p' ≠ ε› primroot_unique
by meson
hence "ρ p ∼ r⋅s"
using conjug_primroot[OF ‹p ∼ p'›]
by simp
moreover have "ρ q' = s⋅r"
using ‹q' = (s ⋅ r) ⇧@ l› ‹primitive (r ⋅ s)›[unfolded conjug_prim_iff'[of r]] ‹q' ≠ ε› primroot_unique
by meson
hence "ρ q ∼ s⋅r"
using conjug_primroot[OF ‹q ∼ q'›] by simp
hence "ρ q ∼ r⋅s"
using conjug_trans[OF _ conjugI']
by meson
ultimately show ?thesis
using that by blast
qed
corollary fac_two_conjug_primroot'_gcd:
assumes facs: "u ≤f r⇧@k" "u ≤f s⇧@l" and nemps: "r ≠ ε" "s ≠ ε" and len: "❙|r❙| + ❙|s❙| - gcd (❙|r❙|) (❙|s❙|) ≤ ❙|u❙|"
shows "ρ r ∼ ρ s"
using fac_two_conjug_primroot_gcd[OF assms] conjug_trans[OF _ conjug_sym[of "ρ s"]].
lemma fac_two_conjug_primroot''_gcd:
assumes facs: "u ≤f r⇧@k" "u ≤f s⇧@l" and "u ≠ ε" and len: "❙|r❙| + ❙|s❙| - gcd (❙|r❙|) (❙|s❙|) ≤ ❙|u❙|"
shows "ρ r ∼ ρ s"
proof -
have nemps: "r ≠ ε" "s ≠ ε" using facs ‹u ≠ ε› by force+
show "conjugate (ρ r) (ρ s)" using fac_two_conjug_primroot'_gcd[OF facs nemps len].
qed
lemma fac_two_prim_conjug_gcd:
assumes "w ≤f u⇧@n" "w ≤f v⇧@m" "primitive u" "primitive v" "❙|u❙| + ❙|v❙| - gcd (❙|u❙|) (❙|v❙|) ≤ ❙|w❙|"
shows "u ∼ v"
using fac_two_conjug_primroot'_gcd[OF assms(1-2) _ _ assms(5)] prim_nemp[OF ‹primitive u›] prim_nemp[OF ‹primitive v›]
unfolding prim_primroot[OF ‹primitive u›] prim_primroot[OF ‹primitive v›].
lemma two_pers_1:
assumes pu: "w ≤p u ⋅ w" and pv: "w ≤p v ⋅ w" and len: "❙|u❙| + ❙|v❙| - 1 ≤ ❙|w❙|"
shows "u ⋅ v = v ⋅ u"
proof (rule nemp_comm)
assume "u ≠ ε" "v ≠ ε"
hence "1 ≤ gcd ❙|u❙| ❙|v❙|"
using nemp_len by (simp add: Suc_leI)
thus ?thesis
using per_lemma_comm[OF pu pv] len by linarith
qed
end