Documentation

Mathlib.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 : ) :
@[simp]
theorem List.rotate_nil {α : Type u} (n : ) :
List.rotate [] n = []
@[simp]
theorem List.rotate_zero {α : Type u} (l : List α) :
theorem List.rotate'_nil {α : Type u} (n : ) :
List.rotate' [] n = []
@[simp]
theorem List.rotate'_zero {α : Type u} (l : List α) :
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 : ) :
theorem List.rotate'_rotate' {α : Type u} (l : List α) (n : ) (m : ) :
@[simp]
theorem List.rotate'_length {α : Type u} (l : List α) :
@[simp]
theorem List.rotate'_length_mul {α : Type u} (l : List α) (n : ) :
theorem List.rotate'_mod {α : Type u} (l : List α) (n : ) :
theorem List.rotate_eq_rotate' {α : Type u} (l : List α) (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 : } :
@[simp]
theorem List.length_rotate {α : Type u} (l : List α) (n : ) :
@[simp]
theorem List.rotate_replicate {α : Type u} (a : α) (n : ) (k : ) :
theorem List.rotate_eq_drop_append_take {α : Type u} {l : List α} {n : } :
@[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 : ) :
@[simp]
theorem List.rotate_length {α : Type u} (l : List α) :
@[simp]
theorem List.rotate_length_mul {α : Type u} (l : List α) (n : ) :
theorem List.prod_rotate_eq_one_of_prod_eq_one {α : Type u} [Group α] {l : List α} :
List.prod l = 1∀ (n : ), List.prod (List.rotate l n) = 1
theorem List.rotate_perm {α : Type u} (l : List α) (n : ) :
@[simp]
theorem List.nodup_rotate {α : Type u} {l : List α} {n : } :
@[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') :
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) :
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) :
@[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) :

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 : } :
@[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.map_rotate {α : Type u} {β : Type u_1} (f : αβ) (l : List α) (n : ) :
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 = []
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) :
def List.IsRotated {α : Type u} (l : List α) (l' : List α) :

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
Instances For

    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
    Instances For
      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 : ) :
      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) :

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

      Equations
      Instances For
        theorem List.IsRotated.perm {α : Type u} {l : List α} {l' : List α} (h : l ~r l') :
        theorem List.IsRotated.nodup_iff {α : Type u} {l : List α} {l' : List α} (h : l ~r 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') :
        theorem List.isRotated_reverse_comm_iff {α : Type u} {l : List α} {l' : List α} :
        @[simp]
        theorem List.isRotated_reverse_iff {α : Type u} {l : List α} {l' : List α} :
        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 α} :
        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.nthLe_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
        Instances For
          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 []) :
          @[simp]
          theorem List.mem_cyclicPermutations_iff {α : Type u} {l : List α} {l' : List α} :
          @[simp]
          @[simp]
          theorem List.cyclicPermutations_eq_singleton_iff {α : Type u} {l : List α} {x : α} :

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

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