mathlib documentation

data.list.rotate

List rotation #

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

Main declarations #

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.lengthl.rotate' n = list.drop n l ++ list.take n 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_eq_drop_append_take {α : Type u} {l : list α} {n : } :
n l.lengthl.rotate n = list.drop n l ++ list.take n 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
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.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) :
(list.zip_with f l l').rotate n = list.zip_with f (l.rotate n) (l'.rotate n)
@[simp]
theorem list.zip_with_rotate_one {α : Type u} {β : Type u_1} (f : α → α → β) (x y : α) (l : list α) :
list.zip_with f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: list.zip_with f (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.rotate_injective {α : Type u} (n : ) :
function.injective (λ (l : list α), l.rotate n)
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)
theorem list.reverse_rotate {α : Type u} (l : list α) (n : ) :
theorem list.rotate_reverse {α : Type u} (l : list α) (n : ) :
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
theorem list.is_rotated.refl {α : Type u} (l : list α) :
l ~r l
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
@[simp]
theorem list.is_rotated.forall {α : Type u} (l : list α) (n : ) :
l.rotate n ~r l
theorem list.is_rotated.trans {α : Type u} {l l' l'' : list α} (h : l ~r l') (h' : l' ~r l'') :
l ~r l''
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 α} :
theorem list.is_rotated_concat {α : Type u} (hd : α) (tl : list α) :
(tl ++ [hd]) ~r (hd :: tl)
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 α} :
@[instance]
def list.setoid.r.decidable {α : Type u} [decidable_eq α] {l l' : list α} :
Equations