List rotation #
This file proves basic results about List.rotate
, the list rotation.
Main declarations #
List.IsRotated l₁ l₂
: States thatl₁
is a rotated version ofl₂
.List.cyclicPermutations l
: The list of all cyclic permutants ofl
, up to the length ofl
.
Tags #
rotated, rotation, permutation, cycle
A version of List.getElem_rotate
that represents l[k]
in terms of
(List.rotate l n)[⋯]
, not vice versa. Can be used instead of rewriting List.getElem_rotate
from right to left.
A version of List.get_rotate
that represents List.get l
in terms of
List.get (List.rotate l n)
, not vice versa. Can be used instead of rewriting List.get_rotate
from right to left.
IsRotated l₁ l₂
or l₁ ~r l₂
asserts that l₁
and l₂
are cyclic permutations
of each other. This is defined by claiming that ∃ n, l.rotate n = l'
.
Equations
Instances For
List of all cyclic permutations of l
.
The cyclicPermutations
of a nonempty list l
will always contain List.length l
elements.
This implies that under certain conditions, there are duplicates in List.cyclicPermutations l
.
The n
th entry is equal to l.rotate n
, proven in List.get_cyclicPermutations
.
The proof that every cyclic permutant of l
is in the list is List.mem_cyclicPermutations_iff
.
cyclicPermutations [1, 2, 3, 2, 4] =
[[1, 2, 3, 2, 4], [2, 3, 2, 4, 1], [3, 2, 4, 1, 2],
[2, 4, 1, 2, 3], [4, 1, 2, 3, 2]]
Equations
Instances For
If a l : List α
is Nodup l
, then all of its cyclic permutants are distinct.