List rotation #

This file proves basic results about List.rotate, the list rotation.

Main declarations #

• List.IsRotated l₁ l₂: States that l₁ is a rotated version of l₂.
• List.cyclicPermutations l: The list of all cyclic permutants of l, up to the length of l.

Tags #

rotated, rotation, permutation, cycle

theorem List.rotate_mod {α : Type u} (l : List α) (n : ) :
l.rotate (n % l.length) = l.rotate n
@[simp]
theorem List.rotate_nil {α : Type u} (n : ) :
[].rotate n = []
@[simp]
theorem List.rotate_zero {α : Type u} (l : List α) :
l.rotate 0 = l
theorem List.rotate'_nil {α : Type u} (n : ) :
[].rotate' n = []
@[simp]
theorem List.rotate'_zero {α : Type u} (l : List α) :
l.rotate' 0 = l
theorem List.rotate'_cons_succ {α : Type u} (l : List α) (a : α) (n : ) :
(a :: l).rotate' n.succ = (l ++ [a]).rotate' n
@[simp]
theorem List.length_rotate' {α : Type u} (l : List α) (n : ) :
(l.rotate' n).length = l.length
theorem List.rotate'_eq_drop_append_take {α : Type u} {l : List α} {n : } :
n l.lengthl.rotate' n = ++
theorem List.rotate'_rotate' {α : Type u} (l : List α) (n : ) (m : ) :
(l.rotate' n).rotate' m = l.rotate' (n + m)
@[simp]
theorem List.rotate'_length {α : Type u} (l : List α) :
l.rotate' l.length = l
@[simp]
theorem List.rotate'_length_mul {α : Type u} (l : List α) (n : ) :
l.rotate' (l.length * n) = l
theorem List.rotate'_mod {α : Type u} (l : List α) (n : ) :
l.rotate' (n % l.length) = l.rotate' n
theorem List.rotate_eq_rotate' {α : Type u} (l : List α) (n : ) :
l.rotate n = l.rotate' n
theorem List.rotate_cons_succ {α : Type u} (l : List α) (a : α) (n : ) :
(a :: l).rotate (n + 1) = (l ++ [a]).rotate n
@[simp]
theorem List.mem_rotate {α : Type u} {l : List α} {a : α} {n : } :
a l.rotate n a l
@[simp]
theorem List.length_rotate {α : Type u} (l : List α) (n : ) :
(l.rotate n).length = l.length
@[simp]
theorem List.rotate_replicate {α : Type u} (a : α) (n : ) (k : ) :
().rotate k =
theorem List.rotate_eq_drop_append_take {α : Type u} {l : List α} {n : } :
n l.lengthl.rotate n = ++
theorem List.rotate_eq_drop_append_take_mod {α : Type u} {l : List α} {n : } :
l.rotate n = List.drop (n % l.length) l ++ List.take (n % l.length) l
@[simp]
theorem List.rotate_append_length_eq {α : Type u} (l : List α) (l' : List α) :
(l ++ l').rotate l.length = l' ++ l
theorem List.rotate_rotate {α : Type u} (l : List α) (n : ) (m : ) :
(l.rotate n).rotate m = l.rotate (n + m)
@[simp]
theorem List.rotate_length {α : Type u} (l : List α) :
l.rotate l.length = l
@[simp]
theorem List.rotate_length_mul {α : Type u} (l : List α) (n : ) :
l.rotate (l.length * n) = l
theorem List.rotate_perm {α : Type u} (l : List α) (n : ) :
(l.rotate n).Perm l
@[simp]
theorem List.nodup_rotate {α : Type u} {l : List α} {n : } :
(l.rotate n).Nodup l.Nodup
@[simp]
theorem List.rotate_eq_nil_iff {α : Type u} {l : List α} {n : } :
l.rotate n = [] l = []
@[simp]
theorem List.nil_eq_rotate_iff {α : Type u} {l : List α} {n : } :
[] = l.rotate n [] = l
@[simp]
theorem List.rotate_singleton {α : Type u} (x : α) (n : ) :
[x].rotate n = [x]
theorem List.zipWith_rotate_distrib {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List α) (l' : List β) (n : ) (h : l.length = l'.length) :
(List.zipWith f l l').rotate n = List.zipWith f (l.rotate n) (l'.rotate n)
theorem List.zipWith_rotate_one {α : Type u} {β : Type u_1} (f : ααβ) (x : α) (y : α) (l : List α) :
List.zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: List.zipWith f (y :: l) (l ++ [x])
theorem List.getElem?_rotate {α : Type u} {l : List α} {n : } {m : } (hml : m < l.length) :
(l.rotate n)[m]? = l[(m + n) % l.length]?
theorem List.getElem_rotate {α : Type u} (l : List α) (n : ) (k : ) (h : k < (l.rotate n).length) :
(l.rotate n)[k] = l[(k + n) % l.length]
theorem List.get?_rotate {α : Type u} {l : List α} {n : } {m : } (hml : m < l.length) :
(l.rotate n).get? m = l.get? ((m + n) % l.length)
theorem List.get_rotate {α : Type u} (l : List α) (n : ) (k : Fin (l.rotate n).length) :
(l.rotate n).get k = l.get (k + n) % l.length,
theorem List.head?_rotate {α : Type u} {l : List α} {n : } (h : n < l.length) :
(l.rotate n).head? = l[n]?
@[deprecated List.get_rotate]
theorem List.nthLe_rotate {α : Type u} (l : List α) (n : ) (k : ) (hk : k < (l.rotate n).length) :
(l.rotate n).nthLe k hk = l.nthLe ((k + n) % l.length)
theorem List.nthLe_rotate_one {α : Type u} (l : List α) (k : ) (hk : k < (l.rotate 1).length) :
(l.rotate 1).nthLe k hk = l.nthLe ((k + 1) % l.length)
theorem List.get_eq_get_rotate {α : Type u} (l : List α) (n : ) (k : Fin l.length) :
l.get k = (l.rotate n).get (l.length - n % l.length + k) % l.length,

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.

@[deprecated List.get_eq_get_rotate]
theorem List.nthLe_rotate' {α : Type u} (l : List α) (n : ) (k : ) (hk : k < l.length) :
(l.rotate n).nthLe ((l.length - n % l.length + k) % l.length) = l.nthLe k hk

A variant of List.nthLe_rotate useful for rewrites from right to left.

theorem List.rotate_eq_self_iff_eq_replicate {α : Type u} [hα : ] {l : List α} :
(∀ (n : ), l.rotate n = l) ∃ (a : α), l = List.replicate l.length a
theorem List.rotate_one_eq_self_iff_eq_replicate {α : Type u} [] {l : List α} :
l.rotate 1 = l ∃ (a : α), l = List.replicate l.length a
theorem List.rotate_injective {α : Type u} (n : ) :
Function.Injective fun (l : List α) => l.rotate n
@[simp]
theorem List.rotate_eq_rotate {α : Type u} {l : List α} {l' : List α} {n : } :
l.rotate n = l'.rotate n l = l'
theorem List.rotate_eq_iff {α : Type u} {l : List α} {l' : List α} {n : } :
l.rotate n = l' l = l'.rotate (l'.length - n % l'.length)
@[simp]
theorem List.rotate_eq_singleton_iff {α : Type u} {l : List α} {n : } {x : α} :
l.rotate n = [x] l = [x]
@[simp]
theorem List.singleton_eq_rotate_iff {α : Type u} {l : List α} {n : } {x : α} :
[x] = l.rotate n [x] = l
theorem List.reverse_rotate {α : Type u} (l : List α) (n : ) :
(l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)
theorem List.rotate_reverse {α : Type u} (l : List α) (n : ) :
l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse
theorem List.map_rotate {α : Type u} {β : Type u_1} (f : αβ) (l : List α) (n : ) :
List.map f (l.rotate n) = (List.map f l).rotate n
theorem List.Nodup.rotate_congr {α : Type u} {l : List α} (hl : l.Nodup) (hn : l []) (i : ) (j : ) (h : l.rotate i = l.rotate j) :
i % l.length = j % l.length
theorem List.Nodup.rotate_congr_iff {α : Type u} {l : List α} (hl : l.Nodup) {i : } {j : } :
l.rotate i = l.rotate j i % l.length = j % l.length l = []
theorem List.Nodup.rotate_eq_self_iff {α : Type u} {l : List α} (hl : l.Nodup) {n : } :
l.rotate n = l n % l.length = 0 l = []
def List.IsRotated {α : Type u} (l : List α) (l' : List α) :

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
• l ~r l' = ∃ (n : ), l.rotate n = l'
Instances For

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
theorem List.IsRotated.refl {α : Type u} (l : List α) :
l ~r l
theorem List.IsRotated.symm {α : Type u} {l : List α} {l' : List α} (h : l ~r l') :
l' ~r l
theorem List.isRotated_comm {α : Type u} {l : List α} {l' : List α} :
l ~r l' l' ~r l
@[simp]
theorem List.IsRotated.forall {α : Type u} (l : List α) (n : ) :
l.rotate n ~r l
theorem List.IsRotated.trans {α : Type u} {l : List α} {l' : List α} {l'' : List α} :
l ~r l'l' ~r l''l ~r l''
theorem List.IsRotated.eqv {α : Type u} :
Equivalence List.IsRotated
def List.IsRotated.setoid (α : Type u_1) :

The relation List.IsRotated l l' forms a Setoid of cycles.

Equations
• = { r := List.IsRotated, iseqv := }
Instances For
theorem List.IsRotated.perm {α : Type u} {l : List α} {l' : List α} (h : l ~r l') :
l.Perm l'
theorem List.IsRotated.nodup_iff {α : Type u} {l : List α} {l' : List α} (h : l ~r l') :
l.Nodup l'.Nodup
theorem List.IsRotated.mem_iff {α : Type u} {l : List α} {l' : List α} (h : l ~r l') {a : α} :
a l a l'
@[simp]
theorem List.isRotated_nil_iff {α : Type u} {l : List α} :
l ~r [] l = []
@[simp]
theorem List.isRotated_nil_iff' {α : Type u} {l : List α} :
[] ~r l [] = l
@[simp]
theorem List.isRotated_singleton_iff {α : Type u} {l : List α} {x : α} :
l ~r [x] l = [x]
@[simp]
theorem List.isRotated_singleton_iff' {α : Type u} {l : List α} {x : α} :
[x] ~r l [x] = l
theorem List.isRotated_concat {α : Type u} (hd : α) (tl : List α) :
(tl ++ [hd]) ~r (hd :: tl)
theorem List.isRotated_append {α : Type u} {l : List α} {l' : List α} :
(l ++ l') ~r (l' ++ l)
theorem List.IsRotated.reverse {α : Type u} {l : List α} {l' : List α} (h : l ~r l') :
l.reverse ~r l'.reverse
theorem List.isRotated_reverse_comm_iff {α : Type u} {l : List α} {l' : List α} :
l.reverse ~r l' l ~r l'.reverse
@[simp]
theorem List.isRotated_reverse_iff {α : Type u} {l : List α} {l' : List α} :
l.reverse ~r l'.reverse l ~r l'
theorem List.isRotated_iff_mod {α : Type u} {l : List α} {l' : List α} :
l ~r l' nl.length, l.rotate n = l'
theorem List.isRotated_iff_mem_map_range {α : Type u} {l : List α} {l' : List α} :
l ~r l' l' List.map l.rotate (List.range (l.length + 1))
theorem List.IsRotated.map {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ ~r l₂) (f : αβ) :
List.map f l₁ ~r List.map f l₂
def List.cyclicPermutations {α : Type u} :
List αList (List α)

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 nth 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
• x.cyclicPermutations = match x with | [] => [[]] | l@h:(head :: tail) => (List.zipWith (fun (x x_1 : List α) => x ++ x_1) l.tails l.inits).dropLast
Instances For
@[simp]
theorem List.cyclicPermutations_nil {α : Type u} :
[].cyclicPermutations = [[]]
theorem List.cyclicPermutations_cons {α : Type u} (x : α) (l : List α) :
(x :: l).cyclicPermutations = (List.zipWith (fun (x x_1 : List α) => x ++ x_1) (x :: l).tails (x :: l).inits).dropLast
theorem List.cyclicPermutations_of_ne_nil {α : Type u} (l : List α) (h : l []) :
l.cyclicPermutations = (List.zipWith (fun (x x_1 : List α) => x ++ x_1) l.tails l.inits).dropLast
theorem List.length_cyclicPermutations_cons {α : Type u} (x : α) (l : List α) :
(x :: l).cyclicPermutations.length = l.length + 1
@[simp]
theorem List.length_cyclicPermutations_of_ne_nil {α : Type u} (l : List α) (h : l []) :
l.cyclicPermutations.length = l.length
@[simp]
theorem List.cyclicPermutations_ne_nil {α : Type u} (l : List α) :
l.cyclicPermutations []
@[simp]
theorem List.getElem_cyclicPermutations {α : Type u} (l : List α) (n : ) (h : n < l.cyclicPermutations.length) :
l.cyclicPermutations[n] = l.rotate n
theorem List.get_cyclicPermutations {α : Type u} (l : List α) (n : Fin l.cyclicPermutations.length) :
l.cyclicPermutations.get n = l.rotate n
@[simp]
theorem List.head_cyclicPermutations {α : Type u} (l : List α) :
l.cyclicPermutations.head = l
@[simp]
theorem List.head?_cyclicPermutations {α : Type u} (l : List α) :
l.cyclicPermutations.head? = some l
theorem List.cyclicPermutations_injective {α : Type u} :
Function.Injective List.cyclicPermutations
@[simp]
theorem List.cyclicPermutations_inj {α : Type u} {l : List α} {l' : List α} :
l.cyclicPermutations = l'.cyclicPermutations l = l'
theorem List.length_mem_cyclicPermutations {α : Type u} {l' : List α} (l : List α) (h : l' l.cyclicPermutations) :
l'.length = l.length
theorem List.mem_cyclicPermutations_self {α : Type u} (l : List α) :
l l.cyclicPermutations
@[simp]
theorem List.cyclicPermutations_rotate {α : Type u} (l : List α) (k : ) :
(l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k
@[simp]
theorem List.mem_cyclicPermutations_iff {α : Type u} {l : List α} {l' : List α} :
l l'.cyclicPermutations l ~r l'
@[simp]
theorem List.cyclicPermutations_eq_nil_iff {α : Type u} {l : List α} :
l.cyclicPermutations = [[]] l = []
@[simp]
theorem List.cyclicPermutations_eq_singleton_iff {α : Type u} {l : List α} {x : α} :
l.cyclicPermutations = [[x]] l = [x]
theorem List.Nodup.cyclicPermutations {α : Type u} {l : List α} (hn : l.Nodup) :
l.cyclicPermutations.Nodup

If a l : List α is Nodup l, then all of its cyclic permutants are distinct.

theorem List.IsRotated.cyclicPermutations {α : Type u} {l : List α} {l' : List α} (h : l ~r l') :
l.cyclicPermutations ~r l'.cyclicPermutations
@[simp]
theorem List.isRotated_cyclicPermutations_iff {α : Type u} {l : List α} {l' : List α} :
l.cyclicPermutations ~r l'.cyclicPermutations l ~r l'
instance List.isRotatedDecidable {α : Type u} [] (l : List α) (l' : List α) :
Decidable (l ~r l')
Equations
instance List.instDecidableR_mathlib {α : Type u} [] {l : List α} {l' : List α} :
Equations
• List.instDecidableR_mathlib = l.isRotatedDecidable l'