Proposed contribution: periodicity lemma (and more)

Stream: mathlib4

[Stepan Holub]

Hello,

I have done some work in Lean on periods of lists. I have a pretty large library about related stuff in Isabelle, but have no contribution in mathlib so far.

I do not think the period of List is defined in mathlib at the moment, and I propose a definition using self-overlap as follows:

def hasPeriod (w : List α) (p : ℕ) : Prop := w <+: (take p w ++ w) ∧ w ≠ [] ∧ p ≠ 0

I have a proof that this is equivalent to the other natural definiton:

lemma hasPeriod_iff_getElem? (p : ℕ) (w : List α): (hasPeriod w p) ↔ w ≠ [] ∧ p ≠ 0 ∧ (∀ i < w.length - p, w[i]? = w[i+p]?)

One of the first nontrivial results about periods of lists is the Periodicity Lemma, also known as the "Fine and Wilf Theorem". I have a proof of it. The claim reads as follows:

theorem periodicity_lemma{α : Type u} [DecidableEq α] (w : List α) (p q : ℕ)
    (per_p: hasPeriod w p) (per_q: hasPeriod w q)
    (len : p + q - p.gcd q ≤ w.length) :
    hasPeriod w (p.gcd q)

The module with Periodicity Lemma starting with the definition has about 200 lines.

I also have a much larger module which generalizes the periodicity lemma to a Finset of periods, including generation of the most "free" word with given periods, and proofs of its optimality.

Is anything of this suitable for mathlib?

P.S.: All this is part of a prepared publication about multiperiodic words, and their formalization in both Isabelle and Lean.

[Jakub Nowak]

Do you need w ≠ [] in the definition? Won't most results still be true without that assumption?

[Stepan Holub]

There is a trade off. Both options would work somehow. The basic idea is that w should be a proper prefix of take p w ++ w

[Alex Meiburg]

I would push for dropping that, and p ≠ 0! Both of your other facts (hasPeriod_iff_getElem? and periodicity_lemma) work without it

[Alex Meiburg]

You'll get other nice things, like that hasPeriod is monotonic under taking prefixes / suffixes

[Stepan Holub]

A crucial part of thinking about periods is the "periodic root" which is the r for which w <+: r ++ w. For example, w is a prefix of the infinite word r^\omega. The case r = [] is pathologic in many respects, for example, it has no primitve root. That said, the property w <+: r ++ w with no further condition is also useful, but it is so simple to state that it is not necessary to give it a special name. On the contrary, omitting the nonemptyness from the definition of hasPeriod would create the necessity to often deal with the empty case seperately. In the proposed way, the assumption hasPeriod w p naturaly eliminates unwanted trivial cases.

[Alex Meiburg]

Okay, that could be! It just wasn't how it looked based on your results -- but, if you say so.

I think the Fine and Wilf theorem would be mathlib suitable, and a cool thing to include! You should make a PR with the code you have, and then probably people can start pointing at how to clean it up in one way or another to get it suitable to merge. If it's a large PR (a subjective measure, but if it's substantially modifying several files), then the PR might need to be split up, and people can give pointers there too.

[Stepan Holub]

After further reflection, I have removed the nonemptiness from the definition as you suggested. It is probably overall more convenient to deal with the empty case separately. Thanls.

[Stepan Holub]

...and the PR is made