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 : ℕ) : List.rotate l (n % List.length l) = List.rotate l n

@[simp]

theorem List.rotate_nil {α : Type u} (n : ℕ) : List.rotate [] n = []

@[simp]

theorem List.rotate_zero {α : Type u} (l : List α) : List.rotate l 0 = l

theorem List.rotate'_nil {α : Type u} (n : ℕ) : List.rotate' [] n = []

@[simp]

theorem List.rotate'_zero {α : Type u} (l : List α) : List.rotate' l 0 = l

theorem List.rotate'_cons_succ {α : Type u} (l : List α) (a : α) (n : ℕ) : List.rotate' (a :: l) (Nat.succ n) = List.rotate' (l ++ [a]) n

@[simp]

theorem List.length_rotate' {α : Type u} (l : List α) (n : ℕ) : List.length (List.rotate' l n) = List.length l

theorem List.rotate'_eq_drop_append_take {α : Type u} {l : List α} {n : ℕ} : n ≤ List.length l → List.rotate' l n = List.drop n l ++ List.take n l

theorem List.rotate'_rotate' {α : Type u} (l : List α) (n : ℕ) (m : ℕ) : List.rotate' (List.rotate' l n) m = List.rotate' l (n + m)

@[simp]

theorem List.rotate'_length {α : Type u} (l : List α) : List.rotate' l (List.length l) = l

@[simp]

theorem List.rotate'_length_mul {α : Type u} (l : List α) (n : ℕ) : List.rotate' l (List.length l * n) = l

theorem List.rotate'_mod {α : Type u} (l : List α) (n : ℕ) : List.rotate' l (n % List.length l) = List.rotate' l n

theorem List.rotate_eq_rotate' {α : Type u} (l : List α) (n : ℕ) : List.rotate l n = List.rotate' l n

theorem List.rotate_cons_succ {α : Type u} (l : List α) (a : α) (n : ℕ) : List.rotate (a :: l) (Nat.succ n) = List.rotate (l ++ [a]) n

@[simp]

theorem List.mem_rotate {α : Type u} {l : List α} {a : α} {n : ℕ} : a ∈ List.rotate l n ↔ a ∈ l

@[simp]

theorem List.length_rotate {α : Type u} (l : List α) (n : ℕ) : List.length (List.rotate l n) = List.length l

@[simp]

theorem List.rotate_replicate {α : Type u} (a : α) (n : ℕ) (k : ℕ) : List.rotate (List.replicate n a) k = List.replicate n a

theorem List.rotate_eq_drop_append_take {α : Type u} {l : List α} {n : ℕ} : n ≤ List.length l → List.rotate l n = List.drop n l ++ List.take n l

theorem List.rotate_eq_drop_append_take_mod {α : Type u} {l : List α} {n : ℕ} : List.rotate l n = List.drop (n % List.length l) l ++ List.take (n % List.length l) l

@[simp]

theorem List.rotate_append_length_eq {α : Type u} (l : List α) (l' : List α) : List.rotate (l ++ l') (List.length l) = l' ++ l

theorem List.rotate_rotate {α : Type u} (l : List α) (n : ℕ) (m : ℕ) : List.rotate (List.rotate l n) m = List.rotate l (n + m)

@[simp]

theorem List.rotate_length {α : Type u} (l : List α) : List.rotate l (List.length l) = l

@[simp]

theorem List.rotate_length_mul {α : Type u} (l : List α) (n : ℕ) : List.rotate l (List.length l * n) = l

theorem List.rotate_perm {α : Type u} (l : List α) (n : ℕ) : List.Perm (List.rotate l n) l

@[simp]

theorem List.nodup_rotate {α : Type u} {l : List α} {n : ℕ} : List.Nodup (List.rotate l n) ↔ List.Nodup l

@[simp]

theorem List.rotate_eq_nil_iff {α : Type u} {l : List α} {n : ℕ} : List.rotate l n = [] ↔ l = []

@[simp]

theorem List.nil_eq_rotate_iff {α : Type u} {l : List α} {n : ℕ} : [] = List.rotate l n ↔ [] = l

@[simp]

theorem List.rotate_singleton {α : Type u} (x : α) (n : ℕ) : List.rotate [x] n = [x]

theorem List.zipWith_rotate_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l : List α) (l' : List β) (n : ℕ) (h : List.length l = List.length l') : List.rotate (List.zipWith f l l') n = List.zipWith f (List.rotate l n) (List.rotate l' n)

theorem List.zipWith_rotate_one {α : Type u} {β : Type u_1} (f : α → α → β) (x : α) (y : α) (l : List α) : List.zipWith f (x :: y :: l) (List.rotate (x :: y :: l) 1) = f x y :: List.zipWith f (y :: l) (l ++ [x])

theorem List.get?_rotate {α : Type u} {l : List α} {n : ℕ} {m : ℕ} (hml : m < List.length l) : List.get? (List.rotate l n) m = List.get? l ((m + n) % List.length l)

theorem List.get_rotate {α : Type u} (l : List α) (n : ℕ) (k : Fin (List.length (List.rotate l n))) : List.get (List.rotate l n) k = List.get l { val := (↑k + n) % List.length l, isLt := ⋯ }

theorem List.head?_rotate {α : Type u} {l : List α} {n : ℕ} (h : n < List.length l) : List.head? (List.rotate l n) = List.get? l n

@[deprecated List.get_rotate]

theorem List.nthLe_rotate {α : Type u} (l : List α) (n : ℕ) (k : ℕ) (hk : k < List.length (List.rotate l n)) : List.nthLe (List.rotate l n) k hk = List.nthLe l ((k + n) % List.length l) ⋯

theorem List.nthLe_rotate_one {α : Type u} (l : List α) (k : ℕ) (hk : k < List.length (List.rotate l 1)) : List.nthLe (List.rotate l 1) k hk = List.nthLe l ((k + 1) % List.length l) ⋯

theorem List.get_eq_get_rotate {α : Type u} (l : List α) (n : ℕ) (k : Fin (List.length l)) : List.get l k = List.get (List.rotate l n) { val := (List.length l - n % List.length l + ↑k) % List.length l, isLt := ⋯ }

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 < List.length l) : List.nthLe (List.rotate l n) ((List.length l - n % List.length l + k) % List.length l) ⋯ = List.nthLe l 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α : Nonempty α] {l : List α} : (∀ (n : ℕ), List.rotate l n = l) ↔ ∃ (a : α), l = List.replicate (List.length l) a

theorem List.rotate_one_eq_self_iff_eq_replicate {α : Type u} [Nonempty α] {l : List α} : List.rotate l 1 = l ↔ ∃ (a : α), l = List.replicate (List.length l) a

theorem List.rotate_injective {α : Type u} (n : ℕ) : Function.Injective fun (l : List α) => List.rotate l n

@[simp]

theorem List.rotate_eq_rotate {α : Type u} {l : List α} {l' : List α} {n : ℕ} : List.rotate l n = List.rotate l' n ↔ l = l'

theorem List.rotate_eq_iff {α : Type u} {l : List α} {l' : List α} {n : ℕ} : List.rotate l n = l' ↔ l = List.rotate l' (List.length l' - n % List.length l')

@[simp]

theorem List.rotate_eq_singleton_iff {α : Type u} {l : List α} {n : ℕ} {x : α} : List.rotate l n = [x] ↔ l = [x]

@[simp]

theorem List.singleton_eq_rotate_iff {α : Type u} {l : List α} {n : ℕ} {x : α} : [x] = List.rotate l n ↔ [x] = l

theorem List.reverse_rotate {α : Type u} (l : List α) (n : ℕ) : List.reverse (List.rotate l n) = List.rotate (List.reverse l) (List.length l - n % List.length l)

theorem List.rotate_reverse {α : Type u} (l : List α) (n : ℕ) : List.rotate (List.reverse l) n = List.reverse (List.rotate l (List.length l - n % List.length l))

theorem List.map_rotate {α : Type u} {β : Type u_1} (f : α → β) (l : List α) (n : ℕ) : List.map f (List.rotate l n) = List.rotate (List.map f l) n

theorem List.Nodup.rotate_congr {α : Type u} {l : List α} (hl : List.Nodup l) (hn : l ≠ []) (i : ℕ) (j : ℕ) (h : List.rotate l i = List.rotate l j) : i % List.length l = j % List.length l

theorem List.Nodup.rotate_congr_iff {α : Type u} {l : List α} (hl : List.Nodup l) {i : ℕ} {j : ℕ} : List.rotate l i = List.rotate l j ↔ i % List.length l = j % List.length l ∨ l = []

theorem List.Nodup.rotate_eq_self_iff {α : Type u} {l : List α} (hl : List.Nodup l) {n : ℕ} : List.rotate l n = l ↔ n % List.length l = 0 ∨ l = []

def List.IsRotated {α : Type u} (l : List α) (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 : ℕ), List.rotate l n = l'

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_ 1000 1001 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~r ") (Lean.ParserDescr.cat `term 1000))

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 : ℕ) : List.rotate l 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) : Setoid (List α)

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

Equations

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

theorem List.IsRotated.perm {α : Type u} {l : List α} {l' : List α} (h : l ~r l') : List.Perm l l'

theorem List.IsRotated.nodup_iff {α : Type u} {l : List α} {l' : List α} (h : l ~r l') : List.Nodup l ↔ List.Nodup l'

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') : List.reverse l ~r List.reverse l'

theorem List.isRotated_reverse_comm_iff {α : Type u} {l : List α} {l' : List α} : List.reverse l ~r l' ↔ l ~r List.reverse l'

@[simp]

theorem List.isRotated_reverse_iff {α : Type u} {l : List α} {l' : List α} : List.reverse l ~r List.reverse l' ↔ l ~r l'

theorem List.isRotated_iff_mod {α : Type u} {l : List α} {l' : List α} : l ~r l' ↔ ∃ n ≤ List.length l, List.rotate l n = l'

theorem List.isRotated_iff_mem_map_range {α : Type u} {l : List α} {l' : List α} : l ~r l' ↔ l' ∈ List.map (List.rotate l) (List.range (List.length l + 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

• List.cyclicPermutations x = match x with | [] => [[]] | l@h:(head :: tail) => List.dropLast (List.zipWith (fun (x x_1 : List α) => x ++ x_1) (List.tails l) (List.inits l))

@[simp]

theorem List.cyclicPermutations_nil {α : Type u} : List.cyclicPermutations [] = [[]]

theorem List.cyclicPermutations_cons {α : Type u} (x : α) (l : List α) : List.cyclicPermutations (x :: l) = List.dropLast (List.zipWith (fun (x x_1 : List α) => x ++ x_1) (List.tails (x :: l)) (List.inits (x :: l)))

theorem List.cyclicPermutations_of_ne_nil {α : Type u} (l : List α) (h : l ≠ []) : List.cyclicPermutations l = List.dropLast (List.zipWith (fun (x x_1 : List α) => x ++ x_1) (List.tails l) (List.inits l))

theorem List.length_cyclicPermutations_cons {α : Type u} (x : α) (l : List α) : List.length (List.cyclicPermutations (x :: l)) = List.length l + 1

@[simp]

theorem List.length_cyclicPermutations_of_ne_nil {α : Type u} (l : List α) (h : l ≠ []) : List.length (List.cyclicPermutations l) = List.length l

@[simp]

theorem List.cyclicPermutations_ne_nil {α : Type u} (l : List α) : List.cyclicPermutations l ≠ []

@[simp]

theorem List.get_cyclicPermutations {α : Type u} (l : List α) (n : Fin (List.length (List.cyclicPermutations l))) : List.get (List.cyclicPermutations l) n = List.rotate l ↑n

@[simp]

theorem List.head_cyclicPermutations {α : Type u} (l : List α) : List.head (List.cyclicPermutations l) ⋯ = l

@[simp]

theorem List.head?_cyclicPermutations {α : Type u} (l : List α) : List.head? (List.cyclicPermutations l) = some l

theorem List.cyclicPermutations_injective {α : Type u} : Function.Injective List.cyclicPermutations

@[simp]

theorem List.cyclicPermutations_inj {α : Type u} {l : List α} {l' : List α} : List.cyclicPermutations l = List.cyclicPermutations l' ↔ l = l'

theorem List.length_mem_cyclicPermutations {α : Type u} {l' : List α} (l : List α) (h : l' ∈ List.cyclicPermutations l) : List.length l' = List.length l

theorem List.mem_cyclicPermutations_self {α : Type u} (l : List α) : l ∈ List.cyclicPermutations l

@[simp]

theorem List.cyclicPermutations_rotate {α : Type u} (l : List α) (k : ℕ) : List.cyclicPermutations (List.rotate l k) = List.rotate (List.cyclicPermutations l) k

@[simp]

theorem List.mem_cyclicPermutations_iff {α : Type u} {l : List α} {l' : List α} : l ∈ List.cyclicPermutations l' ↔ l ~r l'

@[simp]

theorem List.cyclicPermutations_eq_nil_iff {α : Type u} {l : List α} : List.cyclicPermutations l = [[]] ↔ l = []

@[simp]

theorem List.cyclicPermutations_eq_singleton_iff {α : Type u} {l : List α} {x : α} : List.cyclicPermutations l = [[x]] ↔ l = [x]

theorem List.Nodup.cyclicPermutations {α : Type u} {l : List α} (hn : List.Nodup l) : List.Nodup (List.cyclicPermutations l)

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') : List.cyclicPermutations l ~r List.cyclicPermutations l'

@[simp]

theorem List.isRotated_cyclicPermutations_iff {α : Type u} {l : List α} {l' : List α} : List.cyclicPermutations l ~r List.cyclicPermutations l' ↔ l ~r l'

instance List.isRotatedDecidable {α : Type u} [DecidableEq α] (l : List α) (l' : List α) : Decidable (l ~r l')

Equations

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

instance List.instDecidableRListSetoid {α : Type u} [DecidableEq α] {l : List α} {l' : List α} : Decidable (Setoid.r l l')

Equations

• List.instDecidableRListSetoid = List.isRotatedDecidable l l'