Mathlib.Data.List.Rotate

List.rotate_mod theorem

(l : List α) (n : ℕ) : l.rotate (n % l.length) = l.rotate n

Full source

theorem rotate_mod (l : List α) (n : ℕ) : l.rotate (n % l.length) = l.rotate n := by simp [rotate]

List Rotation Invariance under Modulo Length: $l.\text{rotate}(n \bmod |l|) = l.\text{rotate}(n)$

Informal description

For any list $l$ of type $\alpha$ and any natural number $n$, rotating $l$ by $n \bmod \text{length}(l)$ positions is equal to rotating $l$ by $n$ positions. That is, $l.\text{rotate}(n \bmod |l|) = l.\text{rotate}(n)$.

List.rotate_nil theorem

(n : ℕ) : ([] : List α).rotate n = []

Full source

@[simp]
theorem rotate_nil (n : ℕ) : ([] : List α).rotate n = [] := by simp [rotate]

Rotation of Empty List is Empty

Informal description

For any natural number $n$, rotating the empty list by $n$ positions results in the empty list.

List.rotate_zero theorem

(l : List α) : l.rotate 0 = l

Full source

@[simp]
theorem rotate_zero (l : List α) : l.rotate 0 = l := by simp [rotate]

Rotation by Zero Preserves List

Informal description

For any list $l$ of elements of type $\alpha$, rotating $l$ by $0$ positions leaves the list unchanged, i.e., $l.\mathrm{rotate}(0) = l$.

List.rotate'_nil theorem

(n : ℕ) : ([] : List α).rotate' n = []

Full source

theorem rotate'_nil (n : ℕ) : ([] : List α).rotate' n = [] := by simp

Rotation of Empty List is Empty

Informal description

For any natural number $n$, rotating the empty list by $n$ positions results in the empty list, i.e., $\text{rotate}'_n([]) = []$.

List.rotate'_zero theorem

(l : List α) : l.rotate' 0 = l

Full source

@[simp]
theorem rotate'_zero (l : List α) : l.rotate' 0 = l := by cases l <;> rfl

Rotation by Zero Preserves List

Informal description

For any list $l$ of elements of type $\alpha$, rotating $l$ by $0$ positions leaves the list unchanged, i.e., $l.\mathrm{rotate}'\,0 = l$.

List.rotate'_cons_succ theorem

(l : List α) (a : α) (n : ℕ) : (a :: l : List α).rotate' n.succ = (l ++ [a]).rotate' n

Full source

theorem rotate'_cons_succ (l : List α) (a : α) (n : ℕ) :
    (a :: l : List α).rotate' n.succ = (l ++ [a]).rotate' n := by simp [rotate']

Recursive rotation of a cons list: $(a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n$

Informal description

For any list `l` of type `α`, element `a : α`, and natural number `n`, rotating the list `a :: l` by `n + 1` positions is equal to rotating the list `l ++ [a]` by `n` positions. In other words, $(a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n$.

List.length_rotate' theorem

: ∀ (l : List α) (n : ℕ), (l.rotate' n).length = l.length

Full source

@[simp]
theorem length_rotate' : ∀ (l : List α) (n : ℕ), (l.rotate' n).length = l.length
  | [], _ => by simp
  | _ :: _, 0 => rfl
  | a :: l, n + 1 => by rw [List.rotate', length_rotate' (l ++ [a]) n]; simp

Length Preservation under List Rotation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the length of the list obtained by rotating $l$ by $n$ positions is equal to the length of $l$, i.e., $\text{length}(l.\text{rotate}'\, n) = \text{length}(l)$.

List.rotate'_eq_drop_append_take theorem

: ∀ {l : List α} {n : ℕ}, n ≤ l.length → l.rotate' n = l.drop n ++ l.take n

Full source

theorem rotate'_eq_drop_append_take :
    ∀ {l : List α} {n : ℕ}, n ≤ l.length → l.rotate' n = l.drop n ++ l.take n
  | [], n, h => by simp [drop_append_of_le_length h]
  | l, 0, h => by simp [take_append_of_le_length h]
  | a :: l, n + 1, h => by
    have hnl : n ≤ l.length := le_of_succ_le_succ h
    have hnl' : n ≤ (l ++ [a]).length := by
      rw [length_append, length_cons, List.length]; exact le_of_succ_le h
    rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take,
        drop_append_of_le_length hnl, take_append_of_le_length hnl]; simp

List Rotation as Drop-Take Concatenation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ such that $n \leq \text{length}(l)$, rotating $l$ by $n$ positions is equal to concatenating the list obtained by dropping the first $n$ elements of $l$ with the list obtained by taking the first $n$ elements of $l$, i.e., $l.\text{rotate}'\, n = \text{drop}\, n\, l +\!\!+ \text{take}\, n\, l$.

List.rotate'_rotate' theorem

: ∀ (l : List α) (n m : ℕ), (l.rotate' n).rotate' m = l.rotate' (n + m)

Full source

theorem rotate'_rotate' : ∀ (l : List α) (n m : ℕ), (l.rotate' n).rotate' m = l.rotate' (n + m)
  | a :: l, 0, m => by simp
  | [], n, m => by simp
  | a :: l, n + 1, m => by
    rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]

Composition of List Rotations: $(l.\text{rotate}'\, n).\text{rotate}'\, m = l.\text{rotate}'\, (n + m)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural numbers $n$ and $m$, rotating $l$ by $n$ positions and then rotating the result by $m$ positions is equivalent to rotating $l$ by $n + m$ positions, i.e., $(l.\text{rotate}'\, n).\text{rotate}'\, m = l.\text{rotate}'\, (n + m)$.

List.rotate'_length theorem

(l : List α) : rotate' l l.length = l

Full source

@[simp]
theorem rotate'_length (l : List α) : rotate' l l.length = l := by
  rw [rotate'_eq_drop_append_take le_rfl]; simp

Rotation by List Length Preserves List

Informal description

For any list $l$ of elements of type $\alpha$, rotating $l$ by its length leaves the list unchanged, i.e., $l.\text{rotate}'\, \text{length}(l) = l$.

List.rotate'_length_mul theorem

(l : List α) : ∀ n : ℕ, l.rotate' (l.length * n) = l

Full source

@[simp]
theorem rotate'_length_mul (l : List α) : ∀ n : ℕ, l.rotate' (l.length * n) = l
  | 0 => by simp
  | n + 1 =>
    calc
      l.rotate' (l.length * (n + 1)) =
          (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length := by
        simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']
      _ = l := by rw [rotate'_length, rotate'_length_mul l n]

Rotation by Multiple of List Length Preserves List

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, rotating $l$ by $n$ times its length leaves the list unchanged, i.e., $l.\text{rotate}'\, (|l| \cdot n) = l$, where $|l|$ denotes the length of $l$.

List.rotate'_mod theorem

(l : List α) (n : ℕ) : l.rotate' (n % l.length) = l.rotate' n

Full source

theorem rotate'_mod (l : List α) (n : ℕ) : l.rotate' (n % l.length) = l.rotate' n :=
  calc
    l.rotate' (n % l.length) =
        (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) :=
      by rw [rotate'_length_mul]
    _ = l.rotate' n := by rw [rotate'_rotate', length_rotate', Nat.mod_add_div]

Rotation by Modulo List Length Equals Rotation by Original Index

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, rotating $l$ by $n$ modulo the length of $l$ is equivalent to rotating $l$ by $n$, i.e., $l.\text{rotate}'\, (n \bmod |l|) = l.\text{rotate}'\, n$, where $|l|$ denotes the length of $l$.

List.rotate_eq_rotate' theorem

(l : List α) (n : ℕ) : l.rotate n = l.rotate' n

Full source

theorem rotate_eq_rotate' (l : List α) (n : ℕ) : l.rotate n = l.rotate' n :=
  if h : l.length = 0 then by simp_all [length_eq_zero_iff]
  else by
    rw [← rotate'_mod,
        rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
    simp [rotate]

Equivalence of List Rotation Functions: $\text{rotate}\, n = \text{rotate}'\, n$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the rotation of $l$ by $n$ positions using the `rotate` function is equal to the rotation using the `rotate'` function, i.e., $l.\text{rotate}\, n = l.\text{rotate}'\, n$.

List.rotate_cons_succ theorem

(l : List α) (a : α) (n : ℕ) : (a :: l : List α).rotate (n + 1) = (l ++ [a]).rotate n

Full source

@[simp] theorem rotate_cons_succ (l : List α) (a : α) (n : ℕ) :
    (a :: l : List α).rotate (n + 1) = (l ++ [a]).rotate n := by
  rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]

Recursive rotation of a cons list: $(a :: l).\text{rotate}\, (n + 1) = (l ++ [a]).\text{rotate}\, n$

Informal description

For any list $l$ of elements of type $\alpha$, any element $a \in \alpha$, and any natural number $n$, rotating the list $a :: l$ by $n + 1$ positions is equal to rotating the list $l ++ [a]$ by $n$ positions, i.e., $(a :: l).\text{rotate}\, (n + 1) = (l ++ [a]).\text{rotate}\, n$.

List.mem_rotate theorem

: ∀ {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate n ↔ a ∈ l

Full source

@[simp]
theorem mem_rotate : ∀ {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate na ∈ l.rotate n ↔ a ∈ l
  | [], _, n => by simp
  | a :: l, _, 0 => by simp
  | a :: l, _, n + 1 => by simp [rotate_cons_succ, mem_rotate, or_comm]

Membership Preservation under List Rotation: $a \in l.\mathrm{rotate}\,n \leftrightarrow a \in l$

Informal description

For any list $l$ of elements of type $\alpha$, any element $a \in \alpha$, and any natural number $n$, the element $a$ is in the rotated list $l.\mathrm{rotate}\,n$ if and only if $a$ is in the original list $l$. In other words, $a \in l.\mathrm{rotate}\,n \leftrightarrow a \in l$.

List.length_rotate theorem

(l : List α) (n : ℕ) : (l.rotate n).length = l.length

Full source

@[simp]
theorem length_rotate (l : List α) (n : ℕ) : (l.rotate n).length = l.length := by
  rw [rotate_eq_rotate', length_rotate']

Length Preservation under List Rotation: $\text{length}(l.\text{rotate}\, n) = \text{length}(l)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the length of the list obtained by rotating $l$ by $n$ positions is equal to the length of $l$, i.e., $\text{length}(l.\text{rotate}\, n) = \text{length}(l)$.

List.rotate_replicate theorem

(a : α) (n : ℕ) (k : ℕ) : (replicate n a).rotate k = replicate n a

Full source

@[simp]
theorem rotate_replicate (a : α) (n : ℕ) (k : ℕ) : (replicate n a).rotate k = replicate n a :=
  eq_replicate_iff.2 ⟨by rw [length_rotate, length_replicate], fun b hb =>
    eq_of_mem_replicate <| mem_rotate.1 hb⟩

Rotation Invariance of Replicated Lists: $\mathrm{replicate}\,n\,a.\mathrm{rotate}\,k = \mathrm{replicate}\,n\,a$

Informal description

For any element $a$ of type $\alpha$ and natural numbers $n$ and $k$, rotating a list consisting of $n$ copies of $a$ by $k$ positions yields the same list, i.e., $\mathrm{replicate}\,n\,a.\mathrm{rotate}\,k = \mathrm{replicate}\,n\,a$.

List.rotate_eq_drop_append_take theorem

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

Full source

theorem rotate_eq_drop_append_take {l : List α} {n : ℕ} :
    n ≤ l.length → l.rotate n = l.drop n ++ l.take n := by
  rw [rotate_eq_rotate']; exact rotate'_eq_drop_append_take

List Rotation as Drop-Take Concatenation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ such that $n \leq \text{length}(l)$, rotating $l$ by $n$ positions is equal to concatenating the list obtained by dropping the first $n$ elements of $l$ with the list obtained by taking the first $n$ elements of $l$, i.e., $l.\text{rotate}\, n = \text{drop}\, n\, l +\!\!+ \text{take}\, n\, l$.

List.rotate_eq_drop_append_take_mod theorem

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

Full source

theorem rotate_eq_drop_append_take_mod {l : List α} {n : ℕ} :
    l.rotate n = l.drop (n % l.length) ++ l.take (n % l.length) := by
  rcases l.length.zero_le.eq_or_lt with hl | hl
  · simp [eq_nil_of_length_eq_zero hl.symm]
  rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

List Rotation Formula via Modulo Length Drop-Take Concatenation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, rotating $l$ by $n$ positions is equal to concatenating the list obtained by dropping the first $n \bmod \text{length}(l)$ elements of $l$ with the list obtained by taking the first $n \bmod \text{length}(l)$ elements of $l$, i.e., $l.\text{rotate}\, n = \text{drop}\, (n \bmod |l|)\, l +\!\!+ \text{take}\, (n \bmod |l|)\, l$.

List.rotate_append_length_eq theorem

(l l' : List α) : (l ++ l').rotate l.length = l' ++ l

Full source

@[simp]
theorem rotate_append_length_eq (l l' : List α) : (l ++ l').rotate l.length = l' ++ l := by
  rw [rotate_eq_rotate']
  induction l generalizing l'
  · simp
  · simp_all [rotate']

Rotation of Concatenated List by First List's Length

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, rotating the concatenated list $l \mathbin{+\!\!+} l'$ by the length of $l$ results in the list $l' \mathbin{+\!\!+} l$.

List.rotate_rotate theorem

(l : List α) (n m : ℕ) : (l.rotate n).rotate m = l.rotate (n + m)

Full source

theorem rotate_rotate (l : List α) (n m : ℕ) : (l.rotate n).rotate m = l.rotate (n + m) := by
  rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']

Composition of List Rotations: $(l.\text{rotate}\, n).\text{rotate}\, m = l.\text{rotate}\, (n + m)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural numbers $n$ and $m$, rotating $l$ by $n$ positions and then rotating the result by $m$ positions is equivalent to rotating $l$ by $n + m$ positions, i.e., $(l.\text{rotate}\, n).\text{rotate}\, m = l.\text{rotate}\, (n + m)$.

List.rotate_length theorem

(l : List α) : rotate l l.length = l

Full source

@[simp]
theorem rotate_length (l : List α) : rotate l l.length = l := by
  rw [rotate_eq_rotate', rotate'_length]

Rotation by List Length Preserves List

Informal description

For any list $l$ of elements of type $\alpha$, rotating $l$ by its length leaves the list unchanged, i.e., $l.\text{rotate}\, \text{length}(l) = l$.

List.rotate_length_mul theorem

(l : List α) (n : ℕ) : l.rotate (l.length * n) = l

Full source

@[simp]
theorem rotate_length_mul (l : List α) (n : ℕ) : l.rotate (l.length * n) = l := by
  rw [rotate_eq_rotate', rotate'_length_mul]

Rotation by Multiple of List Length Preserves List

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, rotating $l$ by $n$ times its length leaves the list unchanged, i.e., $l.\text{rotate}\, (|l| \cdot n) = l$, where $|l|$ denotes the length of $l$.

List.rotate_perm theorem

(l : List α) (n : ℕ) : l.rotate n ~ l

Full source

theorem rotate_perm (l : List α) (n : ℕ) : l.rotate n ~ l := by
  rw [rotate_eq_rotate']
  induction' n with n hn generalizing l
  · simp
  · rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

Rotation Preserves List Permutation: $l.\mathrm{rotate}\,n \sim l$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the rotation of $l$ by $n$ positions is a permutation of $l$, i.e., $l.\mathrm{rotate}\,n \sim l$.

List.nodup_rotate theorem

{l : List α} {n : ℕ} : Nodup (l.rotate n) ↔ Nodup l

Full source

@[simp]
theorem nodup_rotate {l : List α} {n : ℕ} : NodupNodup (l.rotate n) ↔ Nodup l :=
  (rotate_perm l n).nodup_iff

Rotation Preserves Distinctness: $\mathrm{Nodup}(l.\mathrm{rotate}\,n) \leftrightarrow \mathrm{Nodup}\,l$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the rotated list $l.\mathrm{rotate}\,n$ has no duplicate elements if and only if the original list $l$ has no duplicate elements.

List.rotate_eq_nil_iff theorem

{l : List α} {n : ℕ} : l.rotate n = [] ↔ l = []

Full source

@[simp]
theorem rotate_eq_nil_iff {l : List α} {n : ℕ} : l.rotate n = [] ↔ l = [] := by
  induction' n with n hn generalizing l
  · simp
  · rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [rotate_cons_succ, hn]

Rotation Yields Empty List iff Original List is Empty

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the rotation of $l$ by $n$ positions is the empty list if and only if $l$ itself is the empty list, i.e., $l.\mathrm{rotate}\,n = [] \leftrightarrow l = []$.

List.nil_eq_rotate_iff theorem

{l : List α} {n : ℕ} : [] = l.rotate n ↔ [] = l

Full source

theorem nil_eq_rotate_iff {l : List α} {n : ℕ} : [][] = l.rotate n ↔ [] = l := by
  rw [eq_comm, rotate_eq_nil_iff, eq_comm]

Empty List Equals Rotation iff Original List is Empty

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the empty list equals the rotation of $l$ by $n$ positions if and only if the empty list equals $l$, i.e., $[] = l.\mathrm{rotate}\,n \leftrightarrow [] = l$.

List.rotate_singleton theorem

(x : α) (n : ℕ) : [x].rotate n = [x]

Full source

@[simp]
theorem rotate_singleton (x : α) (n : ℕ) : [x].rotate n = [x] :=
  rotate_replicate x 1 n

Rotation Invariance of Singleton Lists: $[x].\mathrm{rotate}\,n = [x]$

Informal description

For any element $x$ of type $\alpha$ and any natural number $n$, rotating the singleton list $[x]$ by $n$ positions yields the same list $[x]$, i.e., $[x].\mathrm{rotate}\,n = [x]$.

List.zipWith_rotate_distrib theorem

 {β γ : Type*} (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)

Full source

theorem zipWith_rotate_distrib {β γ : Type*} (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) := by
  rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod,
    rotate_eq_drop_append_take_mod, h, zipWith_append, ← drop_zipWith, ←
    take_zipWith, List.length_zipWith, h, min_self]
  rw [length_drop, length_drop, h]

Rotation Distributes Over ZipWith: $(\text{zipWith}\, f\, l\, l').\text{rotate}\, n = \text{zipWith}\, f\, (l.\text{rotate}\, n)\, (l'.\text{rotate}\, n)$

Informal description

For any types $\alpha, \beta, \gamma$, function $f : \alpha \to \beta \to \gamma$, lists $l : \text{List } \alpha$ and $l' : \text{List } \beta$, and natural number $n$, if $l$ and $l'$ have the same length, then rotating the list obtained by applying $\text{zipWith}\, f$ to $l$ and $l'$ by $n$ positions is equal to applying $\text{zipWith}\, f$ to the rotations of $l$ and $l'$ by $n$ positions. In symbols: $$(\text{zipWith}\, f\, l\, l').\text{rotate}\, n = \text{zipWith}\, f\, (l.\text{rotate}\, n)\, (l'.\text{rotate}\, n)$$

List.zipWith_rotate_one theorem

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

Full source

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

ZipWith-Rotation Identity for Single Rotation: $\text{zipWith}\, f\, (x :: y :: l)\, (L.\text{rotate}\, 1) = f(x, y) :: \text{zipWith}\, f\, (y :: l)\, (l ++ [x])$ where $L = x :: y :: l$

Informal description

For any function $f : \alpha \to \alpha \to \beta$, elements $x, y \in \alpha$, and list $l \in \text{List } \alpha$, the zipWith operation of $f$ applied to the list $x :: y :: l$ and its rotation by 1 position is equal to the list starting with $f(x, y)$ followed by the zipWith operation of $f$ applied to $y :: l$ and $l ++ [x]$. In symbols: $$\text{zipWith}\, f\, (x :: y :: l)\, ((x :: y :: l).\text{rotate}\, 1) = f(x, y) :: \text{zipWith}\, f\, (y :: l)\, (l ++ [x])$$

List.getElem?_rotate theorem

{l : List α} {n m : ℕ} (hml : m < l.length) : (l.rotate n)[m]? = l[(m + n) % l.length]?

Full source

theorem getElem?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) :
    (l.rotate n)[m]? = l[(m + n) % l.length]? := by
  rw [rotate_eq_drop_append_take_mod]
  rcases lt_or_le m (l.drop (n % l.length)).length with hm | hm
  · rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]
    rw [length_drop, Nat.lt_sub_iff_add_lt] at hm
    rw [mod_eq_of_lt hm, Nat.add_comm]
  · have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
    rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
    · congr 1
      rw [length_drop] at hm
      have hm' := Nat.sub_le_iff_le_add'.1 hm
      have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
      omega
    · rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

Element Access in Rotated List via Modulo Indexing

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $n$ and $m$ such that $m < |l|$, the $m$-th element (if it exists) of the list obtained by rotating $l$ by $n$ positions is equal to the $(m + n) \bmod |l|$-th element of the original list $l$.

List.getElem_rotate theorem

 (l : List α) (n : ℕ) (k : Nat) (h : k < (l.rotate n).length) :
  (l.rotate n)[k] = l[(k + n) % l.length]'(mod_lt _ (length_rotate l n ▸ k.zero_le.trans_lt h))

Full source

theorem getElem_rotate (l : List α) (n : ℕ) (k : Nat) (h : k < (l.rotate n).length) :
    (l.rotate n)[k] =
      l[(k + n) % l.length]'(mod_lt _ (length_rotate l n ▸ k.zero_le.trans_lt h)) := by
  rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]
  exact h.trans_eq (length_rotate _ _)

Element Access in Rotated List via Modulo Indexing: $(l.\text{rotate}\, n)[k] = l[(k + n) \bmod |l|]$

Informal description

For any list $l$ of elements of type $\alpha$, natural numbers $n$ and $k$, and a proof $h$ that $k$ is less than the length of the rotated list $l.\text{rotate}\, n$, the $k$-th element of the rotated list is equal to the $(k + n) \bmod |l|$-th element of the original list $l$. In symbols: $$(l.\text{rotate}\, n)[k] = l[(k + n) \bmod |l|]$$

List.get?_rotate theorem

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

Full source

@[deprecated getElem?_rotate (since := "2025-02-14")]
theorem get?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) :
    (l.rotate n).get? m = l.get? ((m + n) % l.length) := by
  simp only [get?_eq_getElem?, length_rotate, hml, getElem?_eq_getElem, getElem_rotate]
  rw [← getElem?_eq_getElem]

Element Access in Rotated List via Modulo Indexing: $(l.\text{rotate}\, n)[m]? = l[(m + n) \bmod |l|]?$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $n$ and $m$ such that $m < |l|$, the $m$-th element (if it exists) of the list obtained by rotating $l$ by $n$ positions is equal to the $(m + n) \bmod |l|$-th element of the original list $l$. In symbols: $$(l.\text{rotate}\, n)[m]? = l[(m + n) \bmod |l|]?$$

List.get_rotate theorem

 (l : List α) (n : ℕ) (k : Fin (l.rotate n).length) :
  (l.rotate n).get k = l.get ⟨(k + n) % l.length, mod_lt _ (length_rotate l n ▸ k.pos)⟩

Full source

theorem get_rotate (l : List α) (n : ℕ) (k : Fin (l.rotate n).length) :
    (l.rotate n).get k = l.get ⟨(k + n) % l.length, mod_lt _ (length_rotate l n ▸ k.pos)⟩ := by
  simp [getElem_rotate]

Element Access in Rotated List via Modulo Indexing: $(l.\text{rotate}\, n)[k] = l[(k + n) \bmod |l|]$

Informal description

For any list $l$ of elements of type $\alpha$, natural number $n$, and index $k$ (with proof that $k$ is within bounds of the rotated list), the $k$-th element of the list rotated by $n$ positions equals the element at position $(k + n) \bmod |l|$ in the original list $l$. In symbols: $$(l.\text{rotate}\, n)[k] = l[(k + n) \bmod |l|]$$

List.head?_rotate theorem

{l : List α} {n : ℕ} (h : n < l.length) : head? (l.rotate n) = l[n]?

Full source

theorem head?_rotate {l : List α} {n : ℕ} (h : n < l.length) : head? (l.rotate n) = l[n]? := by
  rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]

Head of Rotated List Equals nth Element of Original List

Informal description

For any list $l$ of elements of type $\alpha$ and a natural number $n$ such that $n < |l|$, the head element (if it exists) of the list obtained by rotating $l$ by $n$ positions is equal to the $n$-th element of the original list $l$.

List.get_rotate_one theorem

 (l : List α) (k : Fin (l.rotate 1).length) :
  (l.rotate 1).get k = l.get ⟨(k + 1) % l.length, mod_lt _ (length_rotate l 1 ▸ k.pos)⟩

Full source

theorem get_rotate_one (l : List α) (k : Fin (l.rotate 1).length) :
    (l.rotate 1).get k = l.get ⟨(k + 1) % l.length, mod_lt _ (length_rotate l 1 ▸ k.pos)⟩ :=
  get_rotate l 1 k

Element Access in List Rotated by One Position: $(l.\text{rotate}\, 1)[k] = l[(k + 1) \bmod |l|]$

Informal description

For any list $l$ of elements of type $\alpha$ and index $k$ (with proof that $k$ is within bounds of the rotated list), the $k$-th element of the list rotated by one position equals the element at position $(k + 1) \bmod |l|$ in the original list $l$. In symbols: $$(l.\text{rotate}\, 1)[k] = l[(k + 1) \bmod |l|]$$

List.getElem_eq_getElem_rotate theorem

 (l : List α) (n : ℕ) (k : Nat) (hk : k < l.length) :
  l[k] =
    ((l.rotate
        n)[(l.length - n % l.length + k) %
        l.length]'((Nat.mod_lt _ (k.zero_le.trans_lt hk)).trans_eq (length_rotate _ _).symm))

Full source

/-- 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. -/
theorem getElem_eq_getElem_rotate (l : List α) (n : ℕ) (k : Nat) (hk : k < l.length) :
    l[k] = ((l.rotate n)[(l.length - n % l.length + k) % l.length]'
      ((Nat.mod_lt _ (k.zero_le.trans_lt hk)).trans_eq (length_rotate _ _).symm)) := by
  rw [getElem_rotate]
  refine congr_arg l.get (Fin.eq_of_val_eq ?_)
  simp only [mod_add_mod]
  rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
  exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]

Element Access in Original List via Rotated List: $l[k] = (l.\text{rotate}\, n)[(|l| - n \bmod |l| + k) \bmod |l|]$

Informal description

For any list $l$ of elements of type $\alpha$, natural numbers $n$ and $k$ with $k < |l|$, the $k$-th element of $l$ is equal to the element at position $(|l| - n \bmod |l| + k) \bmod |l|$ in the list obtained by rotating $l$ by $n$ positions. In symbols: $$l[k] = (l.\text{rotate}\, n)\left[(|l| - n \bmod |l| + k) \bmod |l|\right]$$

List.get_eq_get_rotate theorem

 (l : List α) (n : ℕ) (k : Fin l.length) :
  l.get k =
    (l.rotate n).get
      ⟨(l.length - n % l.length + k) % l.length,
        (Nat.mod_lt _ (k.1.zero_le.trans_lt k.2)).trans_eq (length_rotate _ _).symm⟩

Full source

/-- 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. -/
theorem get_eq_get_rotate (l : List α) (n : ℕ) (k : Fin l.length) :
    l.get k = (l.rotate n).get ⟨(l.length - n % l.length + k) % l.length,
      (Nat.mod_lt _ (k.1.zero_le.trans_lt k.2)).trans_eq (length_rotate _ _).symm⟩ := by
  rw [get_rotate]
  refine congr_arg l.get (Fin.eq_of_val_eq ?_)
  simp only [mod_add_mod]
  rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
  exacts [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]

Element Access in Original List via Rotated List: $l[k] = (l.\text{rotate}\, n)[(|l| - n \bmod |l| + k) \bmod |l|]$

Informal description

For any list $l$ of elements of type $\alpha$, natural number $n$, and index $k$ (with proof that $k$ is within bounds of $l$), the $k$-th element of $l$ is equal to the element at position $(|l| - n \bmod |l| + k) \bmod |l|$ in the list obtained by rotating $l$ by $n$ positions. In symbols: $$l[k] = (l.\text{rotate}\, n)\left[(|l| - n \bmod |l| + k) \bmod |l|\right]$$

List.rotate_eq_self_iff_eq_replicate theorem

[hα : Nonempty α] : ∀ {l : List α}, (∀ n, l.rotate n = l) ↔ ∃ a, l = replicate l.length a

Full source

theorem rotate_eq_self_iff_eq_replicate [hα : Nonempty α] :
    ∀ {l : List α}, (∀ n, l.rotate n = l) ↔ ∃ a, l = replicate l.length a
  | [] => by simp
  | a :: l => ⟨fun h => ⟨a, ext_getElem length_replicate.symm fun n h₁ h₂ => by
      rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]⟩,
    fun ⟨b, hb⟩ n => by rw [hb, rotate_replicate]⟩

Rotation Invariance Characterizes Replicated Lists: $(\forall n, l.\mathrm{rotate}\,n = l) \leftrightarrow \exists a, l = \mathrm{replicate}\,|l|\,a$

Informal description

For any nonempty type $\alpha$ and list $l$ of elements of type $\alpha$, the following are equivalent: 1. For all natural numbers $n$, rotating $l$ by $n$ positions yields $l$ itself (i.e., $l.\mathrm{rotate}\, n = l$ for all $n$). 2. There exists an element $a : \alpha$ such that $l$ is a list consisting of $|l|$ copies of $a$ (i.e., $l = \mathrm{replicate}\,|l|\,a$).

List.rotate_one_eq_self_iff_eq_replicate theorem

[Nonempty α] {l : List α} : l.rotate 1 = l ↔ ∃ a : α, l = List.replicate l.length a

Full source

theorem rotate_one_eq_self_iff_eq_replicate [Nonempty α] {l : List α} :
    l.rotate 1 = l ↔ ∃ a : α, l = List.replicate l.length a :=
  ⟨fun h =>
    rotate_eq_self_iff_eq_replicate.mp fun n =>
      Nat.rec l.rotate_zero (fun n hn => by rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]) n,
    fun h => rotate_eq_self_iff_eq_replicate.mpr h 1⟩

Single Rotation Invariance Characterizes Replicated Lists: $l.\text{rotate}\,1 = l \leftrightarrow \exists a, l = \text{replicate}\,|l|\,a$

Informal description

For a nonempty type $\alpha$ and a list $l$ of elements of type $\alpha$, rotating $l$ by one position leaves it unchanged if and only if $l$ consists of repeated copies of a single element $a$, i.e., $l = \text{replicate}\,|l|\,a$.

List.rotate_injective theorem

(n : ℕ) : Function.Injective fun l : List α => l.rotate n

Full source

theorem rotate_injective (n : ℕ) : Function.Injective fun l : List α => l.rotate n := by
  rintro l l' (h : l.rotate n = l'.rotate n)
  have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
  rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h
  obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
  rw [← take_append_drop _ l, ht, hd, take_append_drop]

Injectivity of List Rotation by $n$ Positions

Informal description

For any natural number $n$, the function that rotates a list $l$ by $n$ positions is injective. That is, if $l_1$ and $l_2$ are lists such that $l_1.\text{rotate}\, n = l_2.\text{rotate}\, n$, then $l_1 = l_2$.

List.rotate_eq_rotate theorem

{l l' : List α} {n : ℕ} : l.rotate n = l'.rotate n ↔ l = l'

Full source

@[simp]
theorem rotate_eq_rotate {l l' : List α} {n : ℕ} : l.rotate n = l'.rotate n ↔ l = l' :=
  (rotate_injective n).eq_iff

Rotation Equality Criterion for Lists: $l.\text{rotate}\, n = l'.\text{rotate}\, n \leftrightarrow l = l'$

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$ and any natural number $n$, the rotation of $l$ by $n$ positions is equal to the rotation of $l'$ by $n$ positions if and only if $l$ is equal to $l'$. In other words, $l.\text{rotate}\, n = l'.\text{rotate}\, n \leftrightarrow l = l'$.

List.rotate_eq_iff theorem

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

Full source

theorem rotate_eq_iff {l l' : List α} {n : ℕ} :
    l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length) := by
  rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
  rcases l'.length.zero_le.eq_or_lt with hl | hl
  · rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
  · rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
    · simp [← hn]
    · rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
      exact (Nat.mod_lt _ hl).le

Characterization of List Rotation Equality: $l.\mathrm{rotate}(n) = l' \leftrightarrow l = l'.\mathrm{rotate}(|l'| - (n \bmod |l'|))$

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$ and any natural number $n$, the rotation of $l$ by $n$ positions equals $l'$ if and only if $l$ equals the rotation of $l'$ by $|l'| - (n \bmod |l'|)$ positions. That is, $$ l.\mathrm{rotate}(n) = l' \leftrightarrow l = l'.\mathrm{rotate}(|l'| - (n \bmod |l'|)). $$

List.rotate_eq_singleton_iff theorem

{l : List α} {n : ℕ} {x : α} : l.rotate n = [x] ↔ l = [x]

Full source

@[simp]
theorem rotate_eq_singleton_iff {l : List α} {n : ℕ} {x : α} : l.rotate n = [x] ↔ l = [x] := by
  rw [rotate_eq_iff, rotate_singleton]

Rotation Yields Singleton iff Original is Singleton: $l.\mathrm{rotate}(n) = [x] \leftrightarrow l = [x]$

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $n$, and any element $x \in \alpha$, the rotation of $l$ by $n$ positions equals the singleton list $[x]$ if and only if $l$ itself is the singleton list $[x]$. That is, $$ l.\mathrm{rotate}(n) = [x] \leftrightarrow l = [x]. $$

List.singleton_eq_rotate_iff theorem

{l : List α} {n : ℕ} {x : α} : [x] = l.rotate n ↔ [x] = l

Full source

@[simp]
theorem singleton_eq_rotate_iff {l : List α} {n : ℕ} {x : α} : [x][x] = l.rotate n ↔ [x] = l := by
  rw [eq_comm, rotate_eq_singleton_iff, eq_comm]

Singleton-Rotation Equivalence: $[x] = l.\mathrm{rotate}(n) \leftrightarrow [x] = l$

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $n$, and any element $x \in \alpha$, the singleton list $[x]$ equals the rotation of $l$ by $n$ positions if and only if $[x]$ equals $l$ itself. That is, $$ [x] = l.\mathrm{rotate}(n) \leftrightarrow [x] = l. $$

List.reverse_rotate theorem

(l : List α) (n : ℕ) : (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)

Full source

theorem reverse_rotate (l : List α) (n : ℕ) :
    (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length) := by
  rw [← length_reverse, ← rotate_eq_iff]
  induction' n with n hn generalizing l
  · simp
  · rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp

Reverse-Rotate Identity: $(l.\mathrm{rotate}\, n)^{\mathrm{rev}} = l^{\mathrm{rev}}.\mathrm{rotate}\, (|l| - n \bmod |l|)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the reverse of the list rotated by $n$ positions is equal to the reverse of $l$ rotated by $|l| - (n \bmod |l|)$ positions, i.e., $$(l.\mathrm{rotate}\, n)^{\mathrm{rev}} = l^{\mathrm{rev}}.\mathrm{rotate}\, (|l| - (n \bmod |l|)).$$

List.rotate_reverse theorem

(l : List α) (n : ℕ) : l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Full source

theorem rotate_reverse (l : List α) (n : ℕ) :
    l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse := by
  rw [← reverse_reverse l]
  simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
    length_reverse]
  rw [← length_reverse]
  let k := n % l.reverse.length
  rcases hk' : k with - | k'
  · simp_all! [k, length_reverse, ← rotate_rotate]
  · rcases l with - | ⟨x, l⟩
    · simp
    · rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
      · exact Nat.sub_le _ _
      · exact Nat.sub_lt (by simp) (by simp_all! [k])

Rotate-Reverse Identity: $l^{\mathrm{rev}}.\mathrm{rotate}\, n = (l.\mathrm{rotate}\, (|l| - n \bmod |l|))^{\mathrm{rev}}$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, rotating the reverse of $l$ by $n$ positions is equal to the reverse of rotating $l$ by $|l| - (n \bmod |l|)$ positions, i.e., $$l^{\mathrm{rev}}.\mathrm{rotate}\, n = (l.\mathrm{rotate}\, (|l| - n \bmod |l|))^{\mathrm{rev}}.$$

List.map_rotate theorem

{β : Type*} (f : α → β) (l : List α) (n : ℕ) : map f (l.rotate n) = (map f l).rotate n

Full source

theorem map_rotate {β : Type*} (f : α → β) (l : List α) (n : ℕ) :
    map f (l.rotate n) = (map f l).rotate n := by
  induction' n with n hn IH generalizing l
  · simp
  · rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [hn]

Map Commutes with Rotation: $f(l.\mathrm{rotate}(n)) = (f(l)).\mathrm{rotate}(n)$

Informal description

For any function $f : \alpha \to \beta$, any list $l$ of elements of type $\alpha$, and any natural number $n$, the map of the rotated list $l.\mathrm{rotate}(n)$ under $f$ is equal to the rotation by $n$ of the map of $l$ under $f$, i.e., $f(l.\mathrm{rotate}(n)) = (f(l)).\mathrm{rotate}(n)$.

List.Nodup.rotate_congr theorem

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

Full source

theorem Nodup.rotate_congr {l : List α} (hl : l.Nodup) (hn : l ≠ []) (i j : ℕ)
    (h : l.rotate i = l.rotate j) : i % l.length = j % l.length := by
  rw [← rotate_mod l i, ← rotate_mod l j] at h
  simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj,
    hl.getElem_inj_iff, Fin.ext_iff] using congr_arg head? h

Rotation Congruence for Nodup Lists: $l.\mathrm{rotate}(i) = l.\mathrm{rotate}(j) \Rightarrow i \bmod |l| = j \bmod |l|$

Informal description

For any list $l$ of elements of type $\alpha$ that has no duplicates (i.e., $l$ is `Nodup`), if $l$ is non-empty and the rotations of $l$ by $i$ and $j$ positions are equal (i.e., $l.\mathrm{rotate}(i) = l.\mathrm{rotate}(j)$), then $i \bmod |l| = j \bmod |l|$.

List.Nodup.rotate_congr_iff theorem

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

Full source

theorem Nodup.rotate_congr_iff {l : List α} (hl : l.Nodup) {i j : ℕ} :
    l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = [] := by
  rcases eq_or_ne l [] with rfl | hn
  · simp
  · simp only [hn, or_false]
    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
    rw [← rotate_mod, h, rotate_mod]

Rotation Congruence Criterion for Nodup Lists: $l.\mathrm{rotate}(i) = l.\mathrm{rotate}(j) \leftrightarrow (i \equiv j \bmod |l| \lor l = [])$

Informal description

For any list $l$ of elements of type $\alpha$ with no duplicates (i.e., $l$ is `Nodup`), and for any natural numbers $i$ and $j$, the rotations of $l$ by $i$ and $j$ positions are equal if and only if either $i \bmod |l| = j \bmod |l|$ or $l$ is the empty list. That is, $l.\mathrm{rotate}(i) = l.\mathrm{rotate}(j) \leftrightarrow (i \bmod |l| = j \bmod |l| \lor l = [])$.

List.Nodup.rotate_eq_self_iff theorem

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

Full source

theorem Nodup.rotate_eq_self_iff {l : List α} (hl : l.Nodup) {n : ℕ} :
    l.rotate n = l ↔ n % l.length = 0 ∨ l = [] := by
  rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]

Rotation Identity Criterion for Nodup Lists: $l.\mathrm{rotate}(n) = l \leftrightarrow (n \equiv 0 \bmod |l| \lor l = [])$

Informal description

For any list $l$ of elements of type $\alpha$ with no duplicates (i.e., $l$ is `Nodup`), and for any natural number $n$, the rotation of $l$ by $n$ positions equals $l$ if and only if either $n$ is congruent to $0$ modulo the length of $l$ or $l$ is the empty list. That is, $l.\mathrm{rotate}(n) = l \leftrightarrow (n \bmod |l| = 0 \lor l = [])$.

List.IsRotated definition

: Prop

Full source

/-- `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'`. -/
def IsRotated : Prop :=
  ∃ n, l.rotate n = l'

List rotation equivalence

Informal description

Two lists $l_1$ and $l_2$ are said to be rotated versions of each other, denoted $l_1 \sim_r l_2$, if there exists a natural number $n$ such that rotating $l_1$ by $n$ positions yields $l_2$. In other words, $l_1 \sim_r l_2$ if $\exists n, \text{rotate}(l_1, n) = l_2$.

List.term_~r_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc List.IsRotated]
-- This matches the precedence of the infix `~` for `List.Perm`, and of other relation infixes
infixr:50 " ~r " => IsRotated

List rotation

Informal description

The operation `rotate` applied to a list `l` and a natural number `n` returns the list obtained by rotating `l` by `n` positions to the left. Specifically, the first `n` elements are moved to the end of the list. If `n` is greater than the length of `l`, the rotation wraps around using modulo arithmetic.

List.IsRotated.refl theorem

(l : List α) : l ~r l

Full source

@[refl]
theorem IsRotated.refl (l : List α) : l ~r l :=
  ⟨0, by simp⟩

Reflexivity of List Rotation

Informal description

For any list $l$ of elements of type $\alpha$, $l$ is a rotated version of itself, i.e., $l \sim_r l$.

List.IsRotated.symm theorem

(h : l ~r l') : l' ~r l

Full source

@[symm]
theorem IsRotated.symm (h : l ~r l') : l' ~r l := by
  obtain ⟨n, rfl⟩ := h
  rcases l with - | ⟨hd, tl⟩
  · exists 0
  · use (hd :: tl).length * n - n
    rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
    exact Nat.le_mul_of_pos_left _ (by simp)

Symmetry of List Rotation Relation

Informal description

If a list $l$ is a rotated version of another list $l'$, then $l'$ is also a rotated version of $l$. In other words, the rotation relation is symmetric: $l \sim_r l'$ implies $l' \sim_r l$.

List.isRotated_comm theorem

: l ~r l' ↔ l' ~r l

Full source

theorem isRotated_comm : l ~r l'l ~r l' ↔ l' ~r l :=
  ⟨IsRotated.symm, IsRotated.symm⟩

Symmetry of List Rotation Relation: $l \sim_r l' \leftrightarrow l' \sim_r l$

Informal description

For any two lists $l$ and $l'$, $l$ is a rotated version of $l'$ if and only if $l'$ is a rotated version of $l$. In other words, the rotation relation is symmetric: $l \sim_r l' \leftrightarrow l' \sim_r l$.

List.IsRotated.forall theorem

(l : List α) (n : ℕ) : l.rotate n ~r l

Full source

@[simp]
protected theorem IsRotated.forall (l : List α) (n : ℕ) : l.rotate n ~r l :=
  IsRotated.symm ⟨n, rfl⟩

Rotation Preserves List Equivalence: $l.\text{rotate}(n) \sim_r l$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$, the rotated version of $l$ by $n$ positions is a rotated version of $l$ itself. In other words, $l.\text{rotate}(n) \sim_r l$ for all $n \in \mathbb{N}$.

List.IsRotated.trans theorem

: ∀ {l l' l'' : List α}, l ~r l' → l' ~r l'' → l ~r l''

Full source

@[trans]
theorem IsRotated.trans : ∀ {l l' l'' : List α}, l ~r l' → l' ~r l'' → l ~r l''
  | _, _, _, ⟨n, rfl⟩, ⟨m, rfl⟩ => ⟨n + m, by rw [rotate_rotate]⟩

Transitivity of List Rotation: $l \sim_r l' \land l' \sim_r l'' \implies l \sim_r l''$

Informal description

For any lists $l$, $l'$, and $l''$ of elements of type $\alpha$, if $l$ is a rotated version of $l'$ and $l'$ is a rotated version of $l''$, then $l$ is a rotated version of $l''$. In other words, the relation "is a rotated version of" is transitive.

List.IsRotated.eqv theorem

: Equivalence (@IsRotated α)

Full source

theorem IsRotated.eqv : Equivalence (@IsRotated α) :=
  Equivalence.mk IsRotated.refl IsRotated.symm IsRotated.trans

Equivalence of List Rotation Relation

Informal description

The relation `IsRotated` on lists of type $\alpha$ is an equivalence relation, meaning it is reflexive, symmetric, and transitive. Specifically: 1. (Reflexivity) For any list $l$, $l \sim_r l$. 2. (Symmetry) For any lists $l$ and $l'$, if $l \sim_r l'$, then $l' \sim_r l$. 3. (Transitivity) For any lists $l$, $l'$, and $l''$, if $l \sim_r l'$ and $l' \sim_r l''$, then $l \sim_r l''$.

List.IsRotated.setoid definition

(α : Type*) : Setoid (List α)

Full source

/-- The relation `List.IsRotated l l'` forms a `Setoid` of cycles. -/
def IsRotated.setoid (α : Type*) : Setoid (List α) where
  r := IsRotated
  iseqv := IsRotated.eqv

Setoid of list rotation equivalence

Informal description

The setoid (set with an equivalence relation) on lists of type $\alpha$ where the equivalence relation is defined by list rotation. Two lists $l_1$ and $l_2$ are equivalent if one can be obtained from the other by rotation, i.e., there exists an $n$ such that $\text{rotate}(l_1, n) = l_2$.

List.IsRotated.perm theorem

(h : l ~r l') : l ~ l'

Full source

theorem IsRotated.perm (h : l ~r l') : l ~ l' :=
  Exists.elim h fun _ hl => hl ▸ (rotate_perm _ _).symm

Rotation Implies Permutation: $l \sim_r l' \Rightarrow l \sim l'$

Informal description

If two lists $l$ and $l'$ are rotated versions of each other (i.e., $l \sim_r l'$), then they are permutations of each other (i.e., $l \sim l'$).

List.IsRotated.nodup_iff theorem

(h : l ~r l') : Nodup l ↔ Nodup l'

Full source

theorem IsRotated.nodup_iff (h : l ~r l') : NodupNodup l ↔ Nodup l' :=
  h.perm.nodup_iff

Preservation of No-Duplicates Property under List Rotation: $l \sim_r l' \Rightarrow (\text{Nodup}(l) \leftrightarrow \text{Nodup}(l'))$

Informal description

For two lists $l$ and $l'$ that are rotated versions of each other (i.e., $l \sim_r l'$), the property of having no duplicate elements is equivalent for both lists. That is, $l$ has no duplicates if and only if $l'$ has no duplicates.

List.IsRotated.mem_iff theorem

(h : l ~r l') {a : α} : a ∈ l ↔ a ∈ l'

Full source

theorem IsRotated.mem_iff (h : l ~r l') {a : α} : a ∈ la ∈ l ↔ a ∈ l' :=
  h.perm.mem_iff

Membership Preservation under List Rotation: $a \in l \leftrightarrow a \in l'$ when $l \sim_r l'$

Informal description

For any two lists $l$ and $l'$ that are rotated versions of each other (i.e., $l \sim_r l'$), and for any element $a$, $a$ is a member of $l$ if and only if $a$ is a member of $l'$.

List.isRotated_nil_iff theorem

: l ~r [] ↔ l = []

Full source

@[simp]
theorem isRotated_nil_iff : l ~r []l ~r [] ↔ l = [] :=
  ⟨fun ⟨n, hn⟩ => by simpa using hn, fun h => h ▸ by rfl⟩

Rotation of List to Empty List iff List is Empty

Informal description

A list $l$ is a rotated version of the empty list if and only if $l$ is itself the empty list, i.e., $l \sim_r [] \leftrightarrow l = []$.

List.isRotated_nil_iff' theorem

: [] ~r l ↔ [] = l

Full source

@[simp]
theorem isRotated_nil_iff' : [][] ~r l[] ~r l ↔ [] = l := by
  rw [isRotated_comm, isRotated_nil_iff, eq_comm]

Empty List Rotation Equivalence: $[] \sim_r l \leftrightarrow [] = l$

Informal description

The empty list is a rotated version of a list $l$ if and only if $l$ is itself the empty list, i.e., $[] \sim_r l \leftrightarrow [] = l$.

List.isRotated_singleton_iff theorem

{x : α} : l ~r [x] ↔ l = [x]

Full source

@[simp]
theorem isRotated_singleton_iff {x : α} : l ~r [x]l ~r [x] ↔ l = [x] :=
  ⟨fun ⟨n, hn⟩ => by simpa using hn, fun h => h ▸ by rfl⟩

Singleton List Rotation Equivalence

Informal description

For any list $l$ and element $x$ of type $\alpha$, $l$ is a rotated version of the singleton list $[x]$ if and only if $l$ is equal to $[x]$, i.e., $l \sim_r [x] \leftrightarrow l = [x]$.

List.isRotated_singleton_iff' theorem

{x : α} : [x] ~r l ↔ [x] = l

Full source

@[simp]
theorem isRotated_singleton_iff' {x : α} : [x][x] ~r l[x] ~r l ↔ [x] = l := by
  rw [isRotated_comm, isRotated_singleton_iff, eq_comm]

Singleton List Rotation Equivalence (Reversed)

Informal description

For any element $x$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the singleton list $[x]$ is a rotated version of $l$ if and only if $l$ is equal to $[x]$, i.e., $[x] \sim_r l \leftrightarrow [x] = l$.

List.isRotated_concat theorem

(hd : α) (tl : List α) : (tl ++ [hd]) ~r (hd :: tl)

Full source

theorem isRotated_concat (hd : α) (tl : List α) : (tl ++ [hd]) ~r (hd :: tl) :=
  IsRotated.symm ⟨1, by simp⟩

Rotation equivalence between concatenated tail and cons list: $(tl \mathbin{+\!\!+} [hd]) \sim_r (hd :: tl)$

Informal description

For any element $hd$ of type $\alpha$ and any list $tl$ of elements of type $\alpha$, the concatenated list $tl \mathbin{+\!\!+} [hd]$ is a rotated version of the list $hd :: tl$, i.e., $(tl \mathbin{+\!\!+} [hd]) \sim_r (hd :: tl)$.

List.isRotated_append theorem

: (l ++ l') ~r (l' ++ l)

Full source

theorem isRotated_append : (l ++ l') ~r (l' ++ l) :=
  ⟨l.length, by simp⟩

Rotation Equivalence of Concatenated Lists: $(l \mathbin{+\!\!+} l') \sim_r (l' \mathbin{+\!\!+} l)$

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the concatenated list $l \mathbin{+\!\!+} l'$ is a rotated version of $l' \mathbin{+\!\!+} l$, denoted as $(l \mathbin{+\!\!+} l') \sim_r (l' \mathbin{+\!\!+} l)$.

List.IsRotated.reverse theorem

(h : l ~r l') : l.reverse ~r l'.reverse

Full source

theorem IsRotated.reverse (h : l ~r l') : l.reverse ~r l'.reverse := by
  obtain ⟨n, rfl⟩ := h
  exact ⟨_, (reverse_rotate _ _).symm⟩

Rotation Equivalence Preserved Under Reversal

Informal description

For any two lists $l$ and $l'$ such that $l$ is a rotated version of $l'$, their reverses $l^{\mathrm{rev}}$ and $l'^{\mathrm{rev}}$ are also rotated versions of each other. In other words, if $l \sim_r l'$, then $l^{\mathrm{rev}} \sim_r l'^{\mathrm{rev}}$.

List.isRotated_reverse_comm_iff theorem

: l.reverse ~r l' ↔ l ~r l'.reverse

Full source

theorem isRotated_reverse_comm_iff : l.reverse ~r l'l.reverse ~r l' ↔ l ~r l'.reverse := by
  constructor <;>
    · intro h
      simpa using h.reverse

Rotation Equivalence Between Reversed Lists: $l^{\mathrm{rev}} \sim_r l' \leftrightarrow l \sim_r l'^{\mathrm{rev}}$

Informal description

For any two lists $l$ and $l'$, the reverse of $l$ is a rotated version of $l'$ if and only if $l$ is a rotated version of the reverse of $l'$. In other words, $l^{\mathrm{rev}} \sim_r l' \leftrightarrow l \sim_r l'^{\mathrm{rev}}$, where $\sim_r$ denotes the rotation equivalence relation and $^{\mathrm{rev}}$ denotes list reversal.

List.isRotated_reverse_iff theorem

: l.reverse ~r l'.reverse ↔ l ~r l'

Full source

@[simp]
theorem isRotated_reverse_iff : l.reverse ~r l'.reversel.reverse ~r l'.reverse ↔ l ~r l' := by
  simp [isRotated_reverse_comm_iff]

Rotation Equivalence Preserved Under List Reversal

Informal description

For any two lists $l$ and $l'$, the reverse of $l$ is a rotation of the reverse of $l'$ if and only if $l$ is a rotation of $l'$. In other words, $l^{\mathrm{rev}} \sim_r l'^{\mathrm{rev}} \leftrightarrow l \sim_r l'$, where $\sim_r$ denotes the rotation equivalence relation and $^{\mathrm{rev}}$ denotes list reversal.

List.isRotated_iff_mod theorem

: l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l'

Full source

theorem isRotated_iff_mod : l ~r l'l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l' := by
  refine ⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
  obtain ⟨n, rfl⟩ := h
  rcases l with - | ⟨hd, tl⟩
  · simp
  · refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
    refine (Nat.mod_lt _ ?_).le
    simp

Characterization of List Rotation via Bounded Rotation Index

Informal description

Two lists $l$ and $l'$ are rotated versions of each other if and only if there exists a natural number $n$ such that $n \leq \text{length}(l)$ and rotating $l$ by $n$ positions yields $l'$. In other words, $l \sim_r l'$ if and only if $\exists n \leq |l|, \text{rotate}(l, n) = l'$.

List.isRotated_iff_mem_map_range theorem

: l ~r l' ↔ l' ∈ (List.range (l.length + 1)).map l.rotate

Full source

theorem isRotated_iff_mem_map_range : l ~r l'l ~r l' ↔ l' ∈ (List.range (l.length + 1)).map l.rotate := by
  simp_rw [mem_map, mem_range, isRotated_iff_mod]
  exact
    ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩,
      fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩

Characterization of List Rotation via Range Mapping

Informal description

Two lists $l$ and $l'$ are rotated versions of each other if and only if $l'$ appears in the list obtained by applying the rotation operation to $l$ for all natural numbers from $0$ to the length of $l$ (inclusive). In other words, $l \sim_r l'$ if and only if $l'$ is in the set $\{\text{rotate}(l, n) \mid n \in \{0, \ldots, \text{length}(l)\}\}$.

List.IsRotated.map theorem

{β : Type*} {l₁ l₂ : List α} (h : l₁ ~r l₂) (f : α → β) : map f l₁ ~r map f l₂

Full source

theorem IsRotated.map {β : Type*} {l₁ l₂ : List α} (h : l₁ ~r l₂) (f : α → β) :
    mapmap f l₁ ~r map f l₂ := by
  obtain ⟨n, rfl⟩ := h
  rw [map_rotate]
  use n

Rotation Equivalence Preserved Under Mapping: $l_1 \sim_r l_2 \Rightarrow f(l_1) \sim_r f(l_2)$

Informal description

For any function $f : \alpha \to \beta$ and any two lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a rotated version of $l_2$, then the mapped lists $f(l_1)$ and $f(l_2)$ are also rotated versions of each other. In other words, if $l_1 \sim_r l_2$, then $f(l_1) \sim_r f(l_2)$.

List.IsRotated.cons_getLast_dropLast theorem

(L : List α) (hL : L ≠ []) : L.getLast hL :: L.dropLast ~r L

Full source

theorem IsRotated.cons_getLast_dropLast
    (L : List α) (hL : L ≠ []) : L.getLast hL :: L.dropLastL.getLast hL :: L.dropLast ~r L := by
  induction L using List.reverseRecOn with
  | nil => simp at hL
  | append_singleton a L _ =>
    simp only [getLast_append, dropLast_concat]
    apply IsRotated.symm
    apply isRotated_concat

Rotation equivalence between $\text{last}(L) :: \text{dropLast}(L)$ and $L$

Informal description

For any nonempty list $L$ of type $\alpha$, the list obtained by prepending the last element of $L$ to the list formed by dropping the last element of $L$ is a rotated version of $L$ itself. In other words, if $L \neq []$, then $\text{last}(L) :: \text{dropLast}(L) \sim_r L$.

List.IsRotated.dropLast_tail theorem

{α} {L : List α} (hL : L ≠ []) (hL' : L.head hL = L.getLast hL) : L.dropLast ~r L.tail

Full source

theorem IsRotated.dropLast_tail {α}
    {L : List α} (hL : L ≠ []) (hL' : L.head hL = L.getLast hL) : L.dropLast ~r L.tail :=
  match L with
  | [] => by simp
  | [_] => by simp
  | a :: b :: L => by
    simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'
    simp [hL', IsRotated.cons_getLast_dropLast]

Rotation equivalence between dropLast and tail of a list with matching head and last elements

Informal description

For any nonempty list $L$ of type $\alpha$ such that the head of $L$ equals its last element, the list obtained by dropping the last element of $L$ is a rotated version of the tail of $L$. In other words, if $L \neq []$ and $\text{head}(L) = \text{last}(L)$, then $\text{dropLast}(L) \sim_r \text{tail}(L)$.

List.cyclicPermutations definition

: List α → List (List α)

Full source

/-- 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]] -/
def cyclicPermutations : List α → List (List α)
  | [] => [[]]
  | l@(_ :: _) => dropLast (zipWith (· ++ ·) (tails l) (inits l))

List of cyclic permutations

Informal description

For a given list `l`, the function `cyclicPermutations` returns a list of all cyclic permutations of `l`. Each cyclic permutation is obtained by rotating the list `l` by some number of positions. The number of distinct cyclic permutations is equal to the length of `l`. For example, the cyclic permutations of `[1, 2, 3, 2, 4]` are: \[ [[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]] \]

List.cyclicPermutations_nil theorem

: cyclicPermutations ([] : List α) = [[]]

Full source

@[simp]
theorem cyclicPermutations_nil : cyclicPermutations ([] : List α) = [[]] :=
  rfl

Cyclic Permutations of Empty List

Informal description

The list of cyclic permutations of the empty list is the singleton list containing the empty list, i.e., $\text{cyclicPermutations}([]) = [[]]$.

List.cyclicPermutations_cons theorem

(x : α) (l : List α) : cyclicPermutations (x :: l) = dropLast (zipWith (· ++ ·) (tails (x :: l)) (inits (x :: l)))

Full source

theorem cyclicPermutations_cons (x : α) (l : List α) :
    cyclicPermutations (x :: l) = dropLast (zipWith (· ++ ·) (tails (x :: l)) (inits (x :: l))) :=
  rfl

Cyclic Permutations of Cons List via Zipping Tails and Inits

Informal description

For any element $x$ and list $l$, the cyclic permutations of the list $x :: l$ are obtained by dropping the last element of the list formed by zipping together the tails and inits of $x :: l$ with concatenation. That is: \[ \text{cyclicPermutations}(x :: l) = \text{dropLast}\left(\text{zipWith}\, (\cdot{+}\!\!{+}\cdot)\, (\text{tails}\, (x :: l))\, (\text{inits}\, (x :: l))\right) \]

List.cyclicPermutations_of_ne_nil theorem

(l : List α) (h : l ≠ []) : cyclicPermutations l = dropLast (zipWith (· ++ ·) (tails l) (inits l))

Full source

theorem cyclicPermutations_of_ne_nil (l : List α) (h : l ≠ []) :
    cyclicPermutations l = dropLast (zipWith (· ++ ·) (tails l) (inits l)) := by
  obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h
  exact cyclicPermutations_cons _ _

Construction of Cyclic Permutations for Non-Empty Lists via Tails and Inits

Informal description

For any non-empty list $l$, the list of cyclic permutations of $l$ is obtained by dropping the last element of the list formed by zipping together the tails and inits of $l$ with concatenation. That is: \[ \text{cyclicPermutations}(l) = \text{dropLast}\left(\text{zipWith}\, (\cdot{+}\!\!{+}\cdot)\, (\text{tails}\, l)\, (\text{inits}\, l)\right) \]

List.length_cyclicPermutations_cons theorem

(x : α) (l : List α) : length (cyclicPermutations (x :: l)) = length l + 1

Full source

theorem length_cyclicPermutations_cons (x : α) (l : List α) :
    length (cyclicPermutations (x :: l)) = length l + 1 := by simp [cyclicPermutations_cons]

Length of Cyclic Permutations for Cons List

Informal description

For any element $x$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the length of the list of cyclic permutations of $x :: l$ is equal to the length of $l$ plus one, i.e., \[ |\text{cyclicPermutations}(x :: l)| = |l| + 1. \]

List.length_cyclicPermutations_of_ne_nil theorem

(l : List α) (h : l ≠ []) : length (cyclicPermutations l) = length l

Full source

@[simp]
theorem length_cyclicPermutations_of_ne_nil (l : List α) (h : l ≠ []) :
    length (cyclicPermutations l) = length l := by simp [cyclicPermutations_of_ne_nil _ h]

Length of Cyclic Permutations Equals Length of List

Informal description

For any non-empty list $l$, the number of cyclic permutations of $l$ is equal to the length of $l$, i.e., $|\text{cyclicPermutations}(l)| = |l|$.

List.cyclicPermutations_ne_nil theorem

: ∀ l : List α, cyclicPermutations l ≠ []

Full source

@[simp]
theorem cyclicPermutations_ne_nil : ∀ l : List α, cyclicPermutationscyclicPermutations l ≠ []
  | a::l, h => by simpa using congr_arg length h

Non-emptiness of Cyclic Permutations List

Informal description

For any list $l$ of elements of type $\alpha$, the list of cyclic permutations of $l$ is non-empty.

List.getElem_cyclicPermutations theorem

(l : List α) (n : Nat) (h : n < length (cyclicPermutations l)) : (cyclicPermutations l)[n] = l.rotate n

Full source

@[simp]
theorem getElem_cyclicPermutations (l : List α) (n : Nat) (h : n < length (cyclicPermutations l)) :
    (cyclicPermutations l)[n] = l.rotate n := by
  cases l with
  | nil => simp
  | cons a l =>
    simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]
    rw [rotate_eq_drop_append_take (by simpa using h.le)]

Indexed Cyclic Permutation Equals Rotation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ such that $n < |\text{cyclicPermutations}(l)|$, the $n$-th element of the list of cyclic permutations of $l$ is equal to $l$ rotated by $n$ positions, i.e., $\text{cyclicPermutations}(l)[n] = l.\text{rotate}\, n$.

List.get_cyclicPermutations theorem

(l : List α) (n : Fin (length (cyclicPermutations l))) : (cyclicPermutations l).get n = l.rotate n

Full source

theorem get_cyclicPermutations (l : List α) (n : Fin (length (cyclicPermutations l))) :
    (cyclicPermutations l).get n = l.rotate n := by
  simp

Cyclic Permutation Element Equals Rotation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ such that $n$ is less than the length of the list of cyclic permutations of $l$, the $n$-th element of the cyclic permutations list is equal to $l$ rotated by $n$ positions, i.e., $\text{cyclicPermutations}(l)[n] = \text{rotate}(l, n)$.

List.head_cyclicPermutations theorem

(l : List α) : (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l

Full source

@[simp]
theorem head_cyclicPermutations (l : List α) :
    (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l := by
  have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)
  rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]

First Cyclic Permutation is Original List

Informal description

For any list $l$ of elements of type $\alpha$, the first element of the list of cyclic permutations of $l$ is equal to $l$ itself, i.e., $\text{head}(\text{cyclicPermutations}(l)) = l$.

List.head?_cyclicPermutations theorem

(l : List α) : (cyclicPermutations l).head? = l

Full source

@[simp]
theorem head?_cyclicPermutations (l : List α) : (cyclicPermutations l).head? = l := by
  rw [head?_eq_head, head_cyclicPermutations]

First Cyclic Permutation is Original List (Optional Head Version)

Informal description

For any list $l$ of elements of type $\alpha$, the first element of the list of cyclic permutations of $l$ (when viewed as an optional value) is equal to $l$ itself, i.e., $\text{head?}(\text{cyclicPermutations}(l)) = l$.

List.cyclicPermutations_injective theorem

: Function.Injective (@cyclicPermutations α)

Full source

theorem cyclicPermutations_injective : Function.Injective (@cyclicPermutations α) := fun l l' h ↦ by
  simpa using congr_arg head? h

Injectivity of Cyclic Permutations Function

Informal description

The function that maps a list to its list of cyclic permutations is injective. That is, for any two lists $l$ and $l'$ of elements of type $\alpha$, if their cyclic permutations are equal, then the original lists are equal: $\text{cyclicPermutations}(l) = \text{cyclicPermutations}(l')$ implies $l = l'$.

List.cyclicPermutations_inj theorem

{l l' : List α} : cyclicPermutations l = cyclicPermutations l' ↔ l = l'

Full source

@[simp]
theorem cyclicPermutations_inj {l l' : List α} :
    cyclicPermutationscyclicPermutations l = cyclicPermutations l' ↔ l = l' :=
  cyclicPermutations_injective.eq_iff

Equality of Cyclic Permutation Lists Implies List Equality

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the list of cyclic permutations of $l$ is equal to the list of cyclic permutations of $l'$ if and only if $l = l'$.

List.length_mem_cyclicPermutations theorem

(l : List α) (h : l' ∈ cyclicPermutations l) : length l' = length l

Full source

theorem length_mem_cyclicPermutations (l : List α) (h : l' ∈ cyclicPermutations l) :
    length l' = length l := by
  obtain ⟨k, hk, rfl⟩ := get_of_mem h
  simp

Length Preservation in Cyclic Permutations: $|l'| = |l|$

Informal description

For any list $l$ of elements of type $\alpha$ and any list $l'$ in the set of cyclic permutations of $l$, the length of $l'$ is equal to the length of $l$, i.e., $|l'| = |l|$.

List.mem_cyclicPermutations_self theorem

(l : List α) : l ∈ cyclicPermutations l

Full source

theorem mem_cyclicPermutations_self (l : List α) : l ∈ cyclicPermutations l := by
  simpa using head_mem (cyclicPermutations_ne_nil l)

Self-Membership in Cyclic Permutations: $l \in \text{cyclicPermutations}(l)$

Informal description

For any list $l$ of elements of type $\alpha$, the list $l$ is an element of its own cyclic permutations, i.e., $l \in \text{cyclicPermutations}(l)$.

List.cyclicPermutations_rotate theorem

(l : List α) (k : ℕ) : (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Full source

@[simp]
theorem cyclicPermutations_rotate (l : List α) (k : ℕ) :
    (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k := by
  have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) := by
    cases l
    · simp
    · rw [length_cyclicPermutations_of_ne_nil] <;> simp
  refine ext_get this fun n hn hn' => ?_
  rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
  cases l <;> simp

Rotation Commutes with Cyclic Permutations: $\text{cyclicPermutations}(l.\text{rotate}\, k) = \text{cyclicPermutations}(l).\text{rotate}\, k$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $k$, the cyclic permutations of the list obtained by rotating $l$ by $k$ positions are equal to the cyclic permutations of $l$ rotated by $k$ positions. That is, \[ \text{cyclicPermutations}(l.\text{rotate}\, k) = \text{cyclicPermutations}(l).\text{rotate}\, k. \]

List.mem_cyclicPermutations_iff theorem

: l ∈ cyclicPermutations l' ↔ l ~r l'

Full source

@[simp]
theorem mem_cyclicPermutations_iff : l ∈ cyclicPermutations l'l ∈ cyclicPermutations l' ↔ l ~r l' := by
  constructor
  · simp_rw [mem_iff_get, get_cyclicPermutations]
    rintro ⟨k, rfl⟩
    exact .forall _ _
  · rintro ⟨k, rfl⟩
    rw [cyclicPermutations_rotate, mem_rotate]
    apply mem_cyclicPermutations_self

Membership in Cyclic Permutations Characterizes Rotation Equivalence: $l \in \text{cyclicPermutations}(l') \leftrightarrow l \sim_r l'$

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the list $l$ is an element of the cyclic permutations of $l'$ if and only if $l$ is a rotated version of $l'$. In other words, \[ l \in \text{cyclicPermutations}(l') \leftrightarrow l \sim_r l'. \]

List.cyclicPermutations_eq_nil_iff theorem

{l : List α} : cyclicPermutations l = [[]] ↔ l = []

Full source

@[simp]
theorem cyclicPermutations_eq_nil_iff {l : List α} : cyclicPermutationscyclicPermutations l = [[]] ↔ l = [] :=
  cyclicPermutations_injective.eq_iff' rfl

Cyclic Permutations of Empty List Characterization

Informal description

For any list $l$ of elements of type $\alpha$, the list of cyclic permutations of $l$ equals the singleton list containing the empty list if and only if $l$ itself is the empty list. That is, \[ \text{cyclicPermutations}(l) = [[]] \leftrightarrow l = []. \]

List.cyclicPermutations_eq_singleton_iff theorem

{l : List α} {x : α} : cyclicPermutations l = [[x]] ↔ l = [x]

Full source

@[simp]
theorem cyclicPermutations_eq_singleton_iff {l : List α} {x : α} :
    cyclicPermutationscyclicPermutations l = [[x]] ↔ l = [x] :=
  cyclicPermutations_injective.eq_iff' rfl

Cyclic Permutations of Singleton List

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x : \alpha$, the list of cyclic permutations of $l$ is equal to the singleton list containing $[x]$ if and only if $l$ is equal to the singleton list $[x]$. In other words, $\text{cyclicPermutations}(l) = [[x]] \leftrightarrow l = [x]$.

List.Nodup.cyclicPermutations theorem

{l : List α} (hn : Nodup l) : Nodup (cyclicPermutations l)

Full source

/-- If a `l : List α` is `Nodup l`, then all of its cyclic permutants are distinct. -/
protected theorem Nodup.cyclicPermutations {l : List α} (hn : Nodup l) :
    Nodup (cyclicPermutations l) := by
  rcases eq_or_ne l [] with rfl | hl
  · simp
  · rw [nodup_iff_injective_get]
    rintro ⟨i, hi⟩ ⟨j, hj⟩ h
    simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj
    simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h

Distinctness of Cyclic Permutations for Lists Without Duplicates

Informal description

For any list $l$ of elements of type $\alpha$ with no duplicates, the list of all cyclic permutations of $l$ also has no duplicates. That is, if $l$ is `Nodup`, then $\text{cyclicPermutations}(l)$ is `Nodup`.

List.IsRotated.cyclicPermutations theorem

{l l' : List α} (h : l ~r l') : l.cyclicPermutations ~r l'.cyclicPermutations

Full source

protected theorem IsRotated.cyclicPermutations {l l' : List α} (h : l ~r l') :
    l.cyclicPermutations ~r l'.cyclicPermutations := by
  obtain ⟨k, rfl⟩ := h
  exact ⟨k, by simp⟩

Rotation of Lists Preserves Cyclic Permutations

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ is a rotated version of $l'$ (denoted $l \sim_r l'$), then the list of cyclic permutations of $l$ is a rotated version of the list of cyclic permutations of $l'$. That is, \[ l \sim_r l' \implies \text{cyclicPermutations}(l) \sim_r \text{cyclicPermutations}(l'). \]

List.isRotated_cyclicPermutations_iff theorem

{l l' : List α} : l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'

Full source

@[simp]
theorem isRotated_cyclicPermutations_iff {l l' : List α} :
    l.cyclicPermutations ~r l'.cyclicPermutationsl.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l' := by
  simp only [IsRotated, ← cyclicPermutations_rotate, cyclicPermutations_inj]

Equivalence of List Rotation and Cyclic Permutation Rotation

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the cyclic permutations of $l$ are rotated versions of the cyclic permutations of $l'$ if and only if $l$ itself is a rotated version of $l'$. In other words: \[ \text{cyclicPermutations}(l) \sim_r \text{cyclicPermutations}(l') \leftrightarrow l \sim_r l' \]

List.isRotatedDecidable instance

(l l' : List α) : Decidable (l ~r l')

Full source

instance isRotatedDecidable (l l' : List α) : Decidable (l ~r l') :=
  decidable_of_iff' _ isRotated_iff_mem_map_range

Decidability of List Rotation Equivalence

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the property of being rotated versions of each other (denoted $l \sim_r l'$) is decidable.

List.instDecidableR_mathlib instance

{l l' : List α} : Decidable (IsRotated.setoid α l l')

Full source

instance {l l' : List α} : Decidable (IsRotated.setoid α l l') :=
  List.isRotatedDecidable _ _

Decidability of List Rotation Equivalence

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the property of being equivalent under list rotation (denoted by the setoid relation $\sim_r$) is decidable.

Mathlib.Data.List.Rotate

Main declarations

Tags