# 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

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 : ℕ) :
[].rotate n = []
source
@[simp]
theorem List.rotate_zero {α : Type u} (l : List α) :
l.rotate 0 = l
source
theorem List.rotate'_nil {α : Type u} (n : ℕ) :
[].rotate' n = []
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 = drop n l ++ 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
@[simp]
theorem List.rotate_cons_succ {α : Type u} (l : List α) (a : α) (n : ℕ) :
(a :: l).rotate (n + 1) = (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
@[simp]
theorem List.rotate_replicate {α : Type u} (a : α) (n k : ℕ) :
(replicate n a).rotate k = replicate n a
source
theorem List.rotate_eq_drop_append_take {α : Type u} {l : List α} {n : ℕ} :
n ≤ l.length → l.rotate n = drop n l ++ take n l
source
theorem List.rotate_eq_drop_append_take_mod {α : Type u} {l : List α} {n : ℕ} :
l.rotate n = drop (n % l.length) l ++ 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.rotate_perm {α : Type u} (l : List α) (n : ℕ) :
(l.rotate n).Perm 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 = [] ↔ l = []
source
theorem List.nil_eq_rotate_iff {α : Type u} {l : List α} {n : ℕ} :
[] = l.rotate n ↔ [] = l
source
@[simp]
theorem List.rotate_singleton {α : Type u} (x : α) (n : ℕ) :
[x].rotate n = [x]
source
theorem List.zipWith_rotate_distrib {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : List α) (l' : List β) (n : ℕ) (h : l.length = l'.length) :
(zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)
source
theorem List.zipWith_rotate_one {α : Type u} {β : Type u_1} (f : α → α → β) (x y : α) (l : List α) :
zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x])
source
theorem List.getElem?_rotate {α : Type u} {l : List α} {n m : ℕ} (hml : m < l.length) :
(l.rotate n)[m]? = l[(m + n) % l.length]?
source
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]
source
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, ⋯⟩
source
theorem List.head?_rotate {α : Type u} {l : List α} {n : ℕ} (h : n < l.length) :
(l.rotate n).head? = l[n]?
source
theorem List.get_rotate_one {α : Type u} (l : List α) (k : Fin (l.rotate 1).length) :
(l.rotate 1).get k = l.get ⟨(↑k + 1) % l.length, ⋯⟩
source
theorem List.getElem_eq_getElem_rotate {α : Type u} (l : List α) (n k : ℕ) (hk : k < l.length) :
l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]

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.

source
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.

source
theorem List.rotate_eq_self_iff_eq_replicate {α : Type u} [hα : Nonempty α] {l : List α} :
(∀ (n : ℕ), l.rotate n = l) ↔ ∃ (a : α), l = 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 = replicate l.length a
source
theorem List.rotate_injective {α : Type u} (n : ℕ) :
Function.Injective fun (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 : ℕ) :
map f (l.rotate n) = (map f l).rotate n
source
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
source
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 = []
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 = []
source
def List.IsRotated {α : Type u} (l l' : List α) :
Prop

`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

source
def List.«term_~r_» :
Lean.TrailingParserDescr

`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

- List.«term_~r_» = Lean.ParserDescr.trailingNode `List.«term_~r_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~r ") (Lean.ParserDescr.cat `term 50))

Instances For

source
theorem List.IsRotated.refl {α : Type u} (l : List α) :
l ~r l
source
theorem List.IsRotated.symm {α : Type u} {l l' : List α} (h : l ~r l') :
l' ~r l
source
theorem List.isRotated_comm {α : Type u} {l l' : List α} :
l ~r l' ↔ l' ~r l
source
@[simp]
theorem List.IsRotated.forall {α : Type u} (l : List α) (n : ℕ) :
l.rotate n ~r l
source
theorem List.IsRotated.trans {α : Type u} {l l' l'' : List α} :
l ~r l' → l' ~r l'' → l ~r l''
source
theorem List.IsRotated.eqv {α : Type u} :
Equivalence IsRotated
source
def List.IsRotated.setoid (α : Type u_1) :
Setoid (List α)

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

Equations

- List.IsRotated.setoid α = { r := List.IsRotated, iseqv := ⋯ }

Instances For

source
theorem List.IsRotated.perm {α : Type u} {l l' : List α} (h : l ~r l') :
l.Perm l'
source
theorem List.IsRotated.nodup_iff {α : Type u} {l l' : List α} (h : l ~r l') :
l.Nodup ↔ l'.Nodup
source
theorem List.IsRotated.mem_iff {α : Type u} {l l' : List α} (h : l ~r l') {a : α} :
a ∈ l ↔ a ∈ l'
source
@[simp]
theorem List.isRotated_nil_iff {α : Type u} {l : List α} :
l ~r [] ↔ l = []
source
@[simp]
theorem List.isRotated_nil_iff' {α : Type u} {l : List α} :
[] ~r l ↔ [] = l
source
@[simp]
theorem List.isRotated_singleton_iff {α : Type u} {l : List α} {x : α} :
l ~r [x] ↔ l = [x]
source
@[simp]
theorem List.isRotated_singleton_iff' {α : Type u} {l : List α} {x : α} :
[x] ~r l ↔ [x] = l
source
theorem List.isRotated_concat {α : Type u} (hd : α) (tl : List α) :
tl ++ [hd] ~r hd :: tl
source
theorem List.isRotated_append {α : Type u} {l l' : List α} :
l ++ l' ~r l' ++ l
source
theorem List.IsRotated.reverse {α : Type u} {l l' : List α} (h : l ~r l') :
l.reverse ~r l'.reverse
source
theorem List.isRotated_reverse_comm_iff {α : Type u} {l l' : List α} :
l.reverse ~r l' ↔ l ~r l'.reverse
source
@[simp]
theorem List.isRotated_reverse_iff {α : Type u} {l l' : List α} :
l.reverse ~r l'.reverse ↔ l ~r l'
source
theorem List.isRotated_iff_mod {α : Type u} {l l' : List α} :
l ~r l' ↔ ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'
source
theorem List.isRotated_iff_mem_map_range {α : Type u} {l l' : List α} :
l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))
source
theorem List.IsRotated.map {α : Type u} {β : Type u_1} {l₁ l₂ : List α} (h : l₁ ~r l₂) (f : α → β) :
List.map f l₁ ~r List.map f l₂
source
theorem List.IsRotated.cons_getLast_dropLast {α : Type u} (L : List α) (hL : L ≠ []) :
L.getLast hL :: L.dropLast ~r L
source
theorem List.IsRotated.dropLast_tail {α : Type u_1} {L : List α} (hL : L ≠ []) (hL' : L.head hL = L.getLast hL) :
L.dropLast ~r L.tail
source
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 `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

- [].cyclicPermutations = [[]]
- (head :: tail).cyclicPermutations = (List.zipWith (fun (x1 x2 : List α) => x1 ++ x2) (head :: tail).tails (head :: tail).inits).dropLast

Instances For

source
@[simp]
theorem List.cyclicPermutations_nil {α : Type u} :
[].cyclicPermutations = [[]]
source
theorem List.cyclicPermutations_cons {α : Type u} (x : α) (l : List α) :
(x :: l).cyclicPermutations = (zipWith (fun (x1 x2 : List α) => x1 ++ x2) (x :: l).tails (x :: l).inits).dropLast
source
theorem List.cyclicPermutations_of_ne_nil {α : Type u} (l : List α) (h : l ≠ []) :
l.cyclicPermutations = (zipWith (fun (x1 x2 : List α) => x1 ++ x2) l.tails l.inits).dropLast
source
theorem List.length_cyclicPermutations_cons {α : Type u} (x : α) (l : List α) :
(x :: l).cyclicPermutations.length = l.length + 1
source
@[simp]
theorem List.length_cyclicPermutations_of_ne_nil {α : Type u} (l : List α) (h : l ≠ []) :
l.cyclicPermutations.length = l.length
source
@[simp]
theorem List.cyclicPermutations_ne_nil {α : Type u} (l : List α) :
l.cyclicPermutations ≠ []
source
@[simp]
theorem List.getElem_cyclicPermutations {α : Type u} (l : List α) (n : ℕ) (h : n < l.cyclicPermutations.length) :
l.cyclicPermutations[n] = l.rotate n
source
theorem List.get_cyclicPermutations {α : Type u} (l : List α) (n : Fin l.cyclicPermutations.length) :
l.cyclicPermutations.get n = l.rotate ↑n
source
@[simp]
theorem List.head_cyclicPermutations {α : Type u} (l : List α) :
l.cyclicPermutations.head ⋯ = l
source
@[simp]
theorem List.head?_cyclicPermutations {α : Type u} (l : List α) :
l.cyclicPermutations.head? = some l
source
theorem List.cyclicPermutations_injective {α : Type u} :
Function.Injective cyclicPermutations
source
@[simp]
theorem List.cyclicPermutations_inj {α : Type u} {l l' : List α} :
l.cyclicPermutations = l'.cyclicPermutations ↔ l = l'
source
theorem List.length_mem_cyclicPermutations {α : Type u} {l' : List α} (l : List α) (h : l' ∈ l.cyclicPermutations) :
l'.length = l.length
source
theorem List.mem_cyclicPermutations_self {α : Type u} (l : List α) :
l ∈ l.cyclicPermutations
source
@[simp]
theorem List.cyclicPermutations_rotate {α : Type u} (l : List α) (k : ℕ) :
(l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k
source
@[simp]
theorem List.mem_cyclicPermutations_iff {α : Type u} {l l' : List α} :
l ∈ l'.cyclicPermutations ↔ l ~r l'
source
@[simp]
theorem List.cyclicPermutations_eq_nil_iff {α : Type u} {l : List α} :
l.cyclicPermutations = [[]] ↔ l = []
source
@[simp]
theorem List.cyclicPermutations_eq_singleton_iff {α : Type u} {l : List α} {x : α} :
l.cyclicPermutations = [[x]] ↔ l = [x]
source
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.

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

- l.isRotatedDecidable l' = decidable_of_iff' (l' ∈ List.map l.rotate (List.range (l.length + 1))) ⋯

source
instance List.instDecidableR_mathlib {α : Type u} [DecidableEq α] {l l' : List α} :
Decidable ((IsRotated.setoid α) l l')
Equations

- List.instDecidableR_mathlib = l.isRotatedDecidable l'