mathlib3 documentation

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 #

Tags #

rotated, rotation, permutation, cycle

source
theorem list.rotate_mod {α : Type u} (l : list α) (n : ℕ) :
l.rotate (n % l.length) = l.rotate n
source
@[simp]
theorem list.rotate_nil {α : Type u} (n : ℕ) :
list.nil.rotate n = list.nil
source
@[simp]
theorem list.rotate_zero {α : Type u} (l : list α) :
l.rotate 0 = l
source
@[simp]
theorem list.rotate'_nil {α : Type u} (n : ℕ) :
list.nil.rotate' n = list.nil
source
@[simp]
theorem list.rotate'_zero {α : Type u} (l : list α) :
l.rotate' 0 = l
source
theorem list.rotate'_cons_succ {α : Type u} (l : list α) (a : α) (n : ℕ) :
(a :: l).rotate' n.succ = (l ++ [a]).rotate' n
source
@[simp]
theorem list.length_rotate' {α : Type u} (l : list α) (n : ℕ) :
(l.rotate' n).length = l.length
source
theorem list.rotate'_eq_drop_append_take {α : Type u} {l : list α} {n : ℕ} :
n ≤ l.length → l.rotate' n = list.drop n l ++ list.take n l
source
theorem list.rotate'_rotate' {α : Type u} (l : list α) (n m : ℕ) :
(l.rotate' n).rotate' m = l.rotate' (n + m)
source
@[simp]
theorem list.rotate'_length {α : Type u} (l : list α) :
l.rotate' l.length = l
source
@[simp]
theorem list.rotate'_length_mul {α : Type u} (l : list α) (n : ℕ) :
l.rotate' (l.length * n) = l
source
theorem list.rotate'_mod {α : Type u} (l : list α) (n : ℕ) :
l.rotate' (n % l.length) = l.rotate' n
source
theorem list.rotate_eq_rotate' {α : Type u} (l : list α) (n : ℕ) :
l.rotate n = l.rotate' n
source
theorem list.rotate_cons_succ {α : Type u} (l : list α) (a : α) (n : ℕ) :
(a :: l).rotate n.succ = (l ++ [a]).rotate n
source
@[simp]
theorem list.mem_rotate {α : Type u} {l : list α} {a : α} {n : ℕ} :
a ∈ l.rotate n ↔ a ∈ l
source
@[simp]
theorem list.length_rotate {α : Type u} (l : list α) (n : ℕ) :
(l.rotate n).length = l.length
source
theorem list.rotate_replicate {α : Type u} (a : α) (n k : ℕ) :
(list.replicate n a).rotate k = list.replicate n a
source
theorem list.rotate_eq_drop_append_take {α : Type u} {l : list α} {n : ℕ} :
n ≤ l.length → l.rotate n = list.drop n l ++ list.take n l
source
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
source
@[simp]
theorem list.rotate_append_length_eq {α : Type u} (l l' : list α) :
(l ++ l').rotate l.length = l' ++ l
source
theorem list.rotate_rotate {α : Type u} (l : list α) (n m : ℕ) :
(l.rotate n).rotate m = l.rotate (n + m)
source
@[simp]
theorem list.rotate_length {α : Type u} (l : list α) :
l.rotate l.length = l
source
@[simp]
theorem list.rotate_length_mul {α : Type u} (l : list α) (n : ℕ) :
l.rotate (l.length * n) = l
source
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
source
theorem list.rotate_perm {α : Type u} (l : list α) (n : ℕ) :
l.rotate n ~ l
source
@[simp]
theorem list.nodup_rotate {α : Type u} {l : list α} {n : ℕ} :
(l.rotate n).nodup ↔ l.nodup
source
@[simp]
theorem list.rotate_eq_nil_iff {α : Type u} {l : list α} {n : ℕ} :
l.rotate n = list.nil ↔ l = list.nil
source
@[simp]
theorem list.nil_eq_rotate_iff {α : Type u} {l : list α} {n : ℕ} :
list.nil = l.rotate n ↔ list.nil = l
source
@[simp]
theorem list.rotate_singleton {α : Type u} (x : α) (n : ℕ) :
[x].rotate n = [x]
source
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)
source
@[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])
source
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) _
source
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) _
source
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.

source
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)
source
theorem list.head'_rotate {α : Type u} {l : list α} {n : ℕ} (h : n < l.length) :
(l.rotate n).head' = l.nth n
source
theorem list.rotate_eq_self_iff_eq_replicate {α : Type u} [hα : nonempty α] {l : list α} :
(∀ (n : ℕ), l.rotate n = l) ↔ ∃ (a : α), l = list.replicate l.length a
source
theorem list.rotate_one_eq_self_iff_eq_replicate {α : Type u} [nonempty α] {l : list α} :
l.rotate 1 = l ↔ ∃ (a : α), l = list.replicate l.length a
source
theorem list.rotate_injective {α : Type u} (n : ℕ) :
function.injective (λ (l : list α), l.rotate n)
source
@[simp]
theorem list.rotate_eq_rotate {α : Type u} {l l' : list α} {n : ℕ} :
l.rotate n = l'.rotate n ↔ l = l'
source
theorem list.rotate_eq_iff {α : Type u} {l l' : list α} {n : ℕ} :
l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)
source
@[simp]
theorem list.rotate_eq_singleton_iff {α : Type u} {l : list α} {n : ℕ} {x : α} :
l.rotate n = [x] ↔ l = [x]
source
@[simp]
theorem list.singleton_eq_rotate_iff {α : Type u} {l : list α} {n : ℕ} {x : α} :
[x] = l.rotate n ↔ [x] = l
source
theorem list.reverse_rotate {α : Type u} (l : list α) (n : ℕ) :
(l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)
source
theorem list.rotate_reverse {α : Type u} (l : list α) (n : ℕ) :
l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse
source
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
source
theorem list.nodup.rotate_eq_self_iff {α : Type u} {l : list α} (hl : l.nodup) {n : ℕ} :
l.rotate n = l ↔ n % l.length = 0 ∨ l = list.nil
source
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
source
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
source
@[refl]
theorem list.is_rotated.refl {α : Type u} (l : list α) :
l ~r l
source
@[symm]
theorem list.is_rotated.symm {α : Type u} {l l' : list α} (h : l ~r l') :
l' ~r l
source
theorem list.is_rotated_comm {α : Type u} {l l' : list α} :
l ~r l' ↔ l' ~r l
source
@[protected, simp]
theorem list.is_rotated.forall {α : Type u} (l : list α) (n : ℕ) :
l.rotate n ~r l
source
@[trans]
theorem list.is_rotated.trans {α : Type u} {l l' l'' : list α} :
l ~r l' → l' ~r l'' → l ~r l''
source
theorem list.is_rotated.eqv {α : Type u} :
equivalence list.is_rotated
source
def list.is_rotated.setoid (α : Type u_1) :
setoid (list α)

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

Equations
source
theorem list.is_rotated.perm {α : Type u} {l l' : list α} (h : l ~r l') :
l ~ l'
source
theorem list.is_rotated.nodup_iff {α : Type u} {l l' : list α} (h : l ~r l') :
l.nodup ↔ l'.nodup
source
theorem list.is_rotated.mem_iff {α : Type u} {l l' : list α} (h : l ~r l') {a : α} :
a ∈ l ↔ a ∈ l'
source
@[simp]
theorem list.is_rotated_nil_iff {α : Type u} {l : list α} :
l ~r list.nil ↔ l = list.nil
source
@[simp]
theorem list.is_rotated_nil_iff' {α : Type u} {l : list α} :
list.nil ~r l ↔ list.nil = l
source
@[simp]
theorem list.is_rotated_singleton_iff {α : Type u} {l : list α} {x : α} :
l ~r [x] ↔ l = [x]
source
@[simp]
theorem list.is_rotated_singleton_iff' {α : Type u} {l : list α} {x : α} :
[x] ~r l ↔ [x] = l
source
theorem list.is_rotated_concat {α : Type u} (hd : α) (tl : list α) :
(tl ++ [hd]) ~r (hd :: tl)
source
theorem list.is_rotated_append {α : Type u} {l l' : list α} :
(l ++ l') ~r (l' ++ l)
source
theorem list.is_rotated.reverse {α : Type u} {l l' : list α} (h : l ~r l') :
l.reverse ~r l'.reverse
source
theorem list.is_rotated_reverse_comm_iff {α : Type u} {l l' : list α} :
l.reverse ~r l' ↔ l ~r l'.reverse
source
@[simp]
theorem list.is_rotated_reverse_iff {α : Type u} {l l' : list α} :
l.reverse ~r l'.reverse ↔ l ~r l'
source
theorem list.is_rotated_iff_mod {α : Type u} {l l' : list α} :
l ~r l' ↔ ∃ (n : ℕ) (H : n ≤ l.length), l.rotate n = l'
source
theorem list.is_rotated_iff_mem_map_range {α : Type u} {l l' : list α} :
l ~r l' ↔ l' ∈ list.map l.rotate (list.range (l.length + 1))
source
theorem list.is_rotated.map {α : Type u} {β : Type u_1} {l₁ l₂ : list α} (h : l₁ ~r l₂) (f : α → β) :
list.map f l₁ ~r list.map f l₂
source
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
source
@[simp]
theorem list.cyclic_permutations_nil {α : Type u} :
list.nil.cyclic_permutations = [list.nil]
source
theorem list.cyclic_permutations_cons {α : Type u} (x : α) (l : list α) :
(x :: l).cyclic_permutations = (list.zip_with has_append.append (x :: l).tails (x :: l).inits).init
source
theorem list.cyclic_permutations_of_ne_nil {α : Type u} (l : list α) (h : l ≠ list.nil) :
l.cyclic_permutations = (list.zip_with has_append.append l.tails l.inits).init
source
theorem list.length_cyclic_permutations_cons {α : Type u} (x : α) (l : list α) :
(x :: l).cyclic_permutations.length = l.length + 1
source
@[simp]
theorem list.length_cyclic_permutations_of_ne_nil {α : Type u} (l : list α) (h : l ≠ list.nil) :
l.cyclic_permutations.length = l.length
source
@[simp]
theorem list.nth_le_cyclic_permutations {α : Type u} (l : list α) (n : ℕ) (hn : n < l.cyclic_permutations.length) :
l.cyclic_permutations.nth_le n hn = l.rotate n
source
theorem list.mem_cyclic_permutations_self {α : Type u} (l : list α) :
l ∈ l.cyclic_permutations
source
theorem list.length_mem_cyclic_permutations {α : Type u} {l' : list α} (l : list α) (h : l' ∈ l.cyclic_permutations) :
l'.length = l.length
source
@[simp]
theorem list.mem_cyclic_permutations_iff {α : Type u} {l l' : list α} :
l ∈ l'.cyclic_permutations ↔ l ~r l'
source
@[simp]
theorem list.cyclic_permutations_eq_nil_iff {α : Type u} {l : list α} :
l.cyclic_permutations = [list.nil] ↔ l = list.nil
source
@[simp]
theorem list.cyclic_permutations_eq_singleton_iff {α : Type u} {l : list α} {x : α} :
l.cyclic_permutations = [[x]] ↔ l = [x]
source
theorem list.nodup.cyclic_permutations {α : Type u} {l : list α} (hn : l.nodup) :
l.cyclic_permutations.nodup

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

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