data.list.rotate

# List rotation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main declarations #

• is_rotated l₁ l₂: States that l₁ is a rotated version of l₂.
• cyclic_permutations 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 : ) :
@[simp]
theorem list.rotate_zero {α : Type u} (l : list α) :
l.rotate 0 = l
@[simp]
theorem list.rotate'_nil {α : Type u} (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 : ) :
theorem list.rotate'_eq_drop_append_take {α : Type u} {l : list α} {n : } :
n l.length l.rotate' n = 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 α) :
@[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.succ = (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 : ) :
theorem list.rotate_replicate {α : Type u} (a : α) (n k : ) :
a).rotate k =
theorem list.rotate_eq_drop_append_take {α : Type u} {l : list α} {n : } :
n l.length l.rotate n = l ++ l
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 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 α) :
@[simp]
theorem list.rotate_length_mul {α : Type u} (l : list α) (n : ) :
l.rotate (l.length * n) = l
theorem list.prod_rotate_eq_one_of_prod_eq_one {α : Type u} [group α] {l : list α} (hl : l.prod = 1) (n : ) :
(l.rotate n).prod = 1
theorem list.rotate_perm {α : Type u} (l : list α) (n : ) :
l.rotate n ~ l
@[simp]
theorem list.nodup_rotate {α : Type u} {l : list α} {n : } :
@[simp]
theorem list.rotate_eq_nil_iff {α : Type u} {l : list α} {n : } :
@[simp]
theorem list.nil_eq_rotate_iff {α : Type u} {l : list α} {n : } :
@[simp]
theorem list.rotate_singleton {α : Type u} (x : α) (n : ) :
[x].rotate n = [x]
theorem list.zip_with_rotate_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (l : list α) (l' : list β) (n : ) (h : l.length = l'.length) :
l l').rotate n = (l.rotate n) (l'.rotate n)
@[simp]
theorem list.zip_with_rotate_one {α : Type u} {β : Type u_1} (f : α α β) (x y : α) (l : list α) :
(x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: (y :: l) (l ++ [x])
theorem list.nth_le_rotate_one {α : Type u} (l : list α) (k : ) (hk : k < (l.rotate 1).length) :
(l.rotate 1).nth_le k hk = l.nth_le ((k + 1) % l.length) _
theorem list.nth_le_rotate {α : Type u} (l : list α) (n k : ) (hk : k < (l.rotate n).length) :
(l.rotate n).nth_le k hk = l.nth_le ((k + n) % l.length) _
theorem list.nth_le_rotate' {α : Type u} (l : list α) (n k : ) (hk : k < l.length) :
(l.rotate n).nth_le ((l.length - n % l.length + k) % l.length) _ = l.nth_le k hk

A variant of nth_le_rotate useful for rewrites.

theorem list.nth_rotate {α : Type u} {l : list α} {n m : } (hml : m < l.length) :
(l.rotate n).nth m = l.nth ((m + n) % l.length)
theorem list.head'_rotate {α : Type u} {l : list α} {n : } (h : n < l.length) :
theorem list.rotate_eq_self_iff_eq_replicate {α : Type u} [hα : nonempty α] {l : list α} :
( (n : ), l.rotate n = l) (a : α), l =
theorem list.rotate_one_eq_self_iff_eq_replicate {α : Type u} [nonempty α] {l : list α} :
l.rotate 1 = l (a : α), l =
theorem list.rotate_injective {α : Type u} (n : ) :
function.injective (λ (l : list α), l.rotate n)
@[simp]
theorem list.rotate_eq_rotate {α : Type u} {l l' : list α} {n : } :
l.rotate n = l'.rotate n l = l'
theorem list.rotate_eq_iff {α : Type u} {l 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 : ) :
theorem list.rotate_reverse {α : Type u} (l : list α) (n : ) :
theorem list.map_rotate {α : Type u} {β : Type u_1} (f : α β) (l : list α) (n : ) :
(l.rotate n) = (list.map f l).rotate n
theorem list.nodup.rotate_eq_self_iff {α : Type u} {l : list α} (hl : l.nodup) {n : } :
l.rotate n = l n % l.length = 0
theorem list.nodup.rotate_congr {α : Type u} {l : list α} (hl : l.nodup) (hn : l list.nil) (i j : ) (h : l.rotate i = l.rotate j) :
i % l.length = j % l.length
def list.is_rotated {α : Type u} (l l' : list α) :
Prop

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

The relation list.is_rotated l l' forms a setoid of cycles.

Equations
theorem list.is_rotated.perm {α : Type u} {l l' : list α} (h : l ~r l') :
l ~ l'
theorem list.is_rotated.nodup_iff {α : Type u} {l l' : list α} (h : l ~r l') :
theorem list.is_rotated.mem_iff {α : Type u} {l l' : list α} (h : l ~r l') {a : α} :
a l a l'
@[simp]
theorem list.is_rotated_nil_iff {α : Type u} {l : list α} :
@[simp]
theorem list.is_rotated_nil_iff' {α : Type u} {l : list α} :
@[simp]
theorem list.is_rotated_singleton_iff {α : Type u} {l : list α} {x : α} :
l ~r [x] l = [x]
@[simp]
theorem list.is_rotated_singleton_iff' {α : Type u} {l : list α} {x : α} :
[x] ~r l [x] = l
theorem list.is_rotated_concat {α : Type u} (hd : α) (tl : list α) :
(tl ++ [hd]) ~r (hd :: tl)
theorem list.is_rotated_append {α : Type u} {l l' : list α} :
(l ++ l') ~r (l' ++ l)
theorem list.is_rotated.reverse {α : Type u} {l l' : list α} (h : l ~r l') :
theorem list.is_rotated_reverse_comm_iff {α : Type u} {l l' : list α} :
l.reverse ~r l' l ~r l'.reverse
@[simp]
theorem list.is_rotated_reverse_iff {α : Type u} {l l' : list α} :
l.reverse ~r l'.reverse l ~r l'
theorem list.is_rotated_iff_mod {α : Type u} {l l' : list α} :
l ~r l' (n : ) (H : n l.length), l.rotate n = l'
theorem list.is_rotated_iff_mem_map_range {α : Type u} {l l' : list α} :
l ~r l' l' (list.range (l.length + 1))
theorem list.is_rotated.map {α : Type u} {β : Type u_1} {l₁ l₂ : list α} (h : l₁ ~r l₂) (f : α β) :
l₁ ~r l₂
def list.cyclic_permutations {α : Type u} :
list α list (list α)

List of all cyclic permutations of l. The cyclic_permutations of a nonempty list l will always contain list.length l elements. This implies that under certain conditions, there are duplicates in list.cyclic_permutations l. The nth entry is equal to l.rotate n, proven in list.nth_le_cyclic_permutations. The proof that every cyclic permutant of l is in the list is list.mem_cyclic_permutations_iff.

 cyclic_permutations [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
@[simp]
theorem list.cyclic_permutations_nil {α : Type u} :
theorem list.cyclic_permutations_cons {α : Type u} (x : α) (l : list α) :
theorem list.cyclic_permutations_of_ne_nil {α : Type u} (l : list α) (h : l list.nil) :
theorem list.length_cyclic_permutations_cons {α : Type u} (x : α) (l : list α) :
@[simp]
theorem list.length_cyclic_permutations_of_ne_nil {α : Type u} (l : list α) (h : l list.nil) :
@[simp]
theorem list.nth_le_cyclic_permutations {α : Type u} (l : list α) (n : ) (hn : n < l.cyclic_permutations.length) :
hn = l.rotate n
theorem list.mem_cyclic_permutations_self {α : Type u} (l : list α) :
theorem list.length_mem_cyclic_permutations {α : Type u} {l' : list α} (l : list α) (h : l' l.cyclic_permutations) :
@[simp]
theorem list.mem_cyclic_permutations_iff {α : Type u} {l l' : list α} :
l ~r l'
@[simp]
theorem list.cyclic_permutations_eq_nil_iff {α : Type u} {l : list α} :
@[simp]
theorem list.cyclic_permutations_eq_singleton_iff {α : Type u} {l : list α} {x : α} :
l = [x]
theorem list.nodup.cyclic_permutations {α : Type u} {l : list α} (hn : l.nodup) :

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

@[simp]
theorem list.cyclic_permutations_rotate {α : Type u} (l : list α) (k : ) :
theorem list.is_rotated.cyclic_permutations {α : Type u} {l l' : list α} (h : l ~r l') :
@[simp]
theorem list.is_rotated_cyclic_permutations_iff {α : Type u} {l l' : list α} :
l ~r l'
@[protected, instance]
def list.is_rotated_decidable {α : Type u} [decidable_eq α] (l l' : list α) :
decidable (l ~r l')
Equations
@[protected, instance]
def list.setoid.r.decidable {α : Type u} [decidable_eq α] {l l' : list α} :
Equations