List.IsRotated.symm
theorem List.IsRotated.symm : ∀ {α : Type u} {l l' : List α}, l.IsRotated l' → l'.IsRotated l
This theorem states that the "isRotated" relation on lists is symmetric. In other words, for any given type `α` and any lists `l` and `l'` of this type, if `l` is a rotation of `l'`, then `l'` is also a rotation of `l`. Here, a list is said to be a rotation of another if it can be obtained by taking a contiguous part from the beginning and moving it to the end.
More concisely: If `l` is a rotation of `l'`, then `l'` is a rotation of `l` (for all lists `l` and `l` of the same type `α`).
|
List.rotate_nil
theorem List.rotate_nil : ∀ {α : Type u} (n : ℕ), [].rotate n = []
This theorem, `List.rotate_nil`, states that for any type `α` and any natural number `n`, rotating an empty list `[]` by `n` places results in the empty list `[]`. In other words, no matter how many positions you try to shift the elements of an empty list, the result will always be an empty list.
More concisely: For any type `α` and natural number `n`, the rotation of the empty list `[]` by `n` places is the empty list `[]`.
|
List.nthLe_rotate
theorem List.nthLe_rotate :
∀ {α : Type u} (l : List α) (n k : ℕ) (hk : k < (l.rotate n).length),
(l.rotate n).nthLe k hk = l.nthLe ((k + n) % l.length) ⋯
The theorem `List.nthLe_rotate` states that for any given type `α`, list `l` of type `α`, and natural numbers `n` and `k` such that `k` is less than the length of the list obtained by rotating `l` by `n`, the `k`-th element of the rotated list is the same as the `((k + n) % List.length l)`-th element of the original list `l`. In other words, if you rotate a list by `n` positions and then take the `k`-th element, it's the same as if you had taken the `((k + n) % List.length l)`-th element from the original list.
More concisely: For any list `l` of length `n` and natural numbers `k` and `n`, the `k`-th element of the rotated list `l` obtained by rotating `n` positions to the right is equal to the `((k + n) % n)`-th element of the original list `l`.
|
List.rotate_rotate
theorem List.rotate_rotate : ∀ {α : Type u} (l : List α) (n m : ℕ), (l.rotate n).rotate m = l.rotate (n + m)
The theorem `List.rotate_rotate` states that for any list `l` of elements of some type `α`, and for any two natural numbers `n` and `m`, rotating `l` by `n` places and then by `m` places is equivalent to rotating `l` by `n + m` places. In other words, the sequence of rotations is commutative; the order of applying the rotations doesn't change the final result.
More concisely: For any list `l` of length `n` and natural numbers `m` and `n`, rotating list `l` by `m` places and then by `n` places is equivalent to rotating it by `n + m` places.
|
List.length_rotate
theorem List.length_rotate : ∀ {α : Type u} (l : List α) (n : ℕ), (l.rotate n).length = l.length
This theorem states that for any list `l` of elements of some type `α` and any natural number `n`, the length of the list obtained by rotating `l` to the left by `n` positions is equal to the length of the original list `l`. In other words, performing a left rotation operation on a list doesn't change its length. This holds for any type `α` and any list `l` of that type.
More concisely: For any list `l` of length `n` and any natural number `n`, the length of the left rotated list `l.rotated n` is equal to `n`.
|
List.rotate_eq_rotate'
theorem List.rotate_eq_rotate' : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate n = l.rotate' n
This theorem states that for any list `l` of elements of an arbitrary type `α`, and for any natural number `n`, the function `List.rotate` applied to `l` and `n` returns the same result as the function `List.rotate'` applied to `l` and `n`. In other words, irrespective of the type of elements in the list and the number of times you wish to rotate the list, both `List.rotate` and `List.rotate'` yield the same output. This establishes the equivalence of `List.rotate` and `List.rotate'` for all lists and natural numbers.
More concisely: For any list `l` of type `α` and natural number `n`, `List.rotate l n` equals `List.rotate' l n`.
|
List.get_eq_get_rotate
theorem List.get_eq_get_rotate :
∀ {α : Type u} (l : List α) (n : ℕ) (k : Fin l.length),
l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩
This theorem, `List.get_eq_get_rotate`, is a version of `List.get_rotate` that is targeted towards expressing `List.get l` in terms of `List.get (List.rotate l n)` rather than the other way around. In simpler terms, it states that for any list `l` of a certain type `α`, and for any natural numbers `n` and `k` such that `k` is less than the length of `list`, retrieving the `k`-th element from the list `l` is equivalent to retrieving an element from the list obtained by rotating `l` by `n` places. The position of this element in the rotated list is calculated as `((l.length - n % l.length) + k) % l.length`. This theorem can be used in place of rewriting `List.get_rotate` from right to left.
More concisely: For any list `l` of length `n` and natural numbers `k` and `n`, `List.get l k = List.get (List.rotate l n) ((k % n) + (n % l.length))`, where `List.get` is the function that retrieves the element at the given position in a list.
|
List.rotate'_eq_drop_append_take
theorem List.rotate'_eq_drop_append_take :
∀ {α : Type u} {l : List α} {n : ℕ}, n ≤ l.length → l.rotate' n = List.drop n l ++ List.take n l
This theorem states that for any given list `l` of items of arbitrary type `α` and a non-negative integer `n` such that `n` is less than or equal to the length of the list `l`, rotating the list `l` `n` times is equivalent to removing the first `n` elements from the list `l` and appending them to the end of the list. This is expressed in Lean 4 with the `List.rotate'`, `List.drop` and `List.take` functions. In mathematical notation, we could express this as: for all lists `l` and all `n` such that `n ≤ |l|`, it holds that `rotate'(l, n) = drop(n, l) ++ take(n, l)`, where `|l|` represents the length of the list `l`, and `++` represents list concatenation.
More concisely: For any list `l` of length `|l|` and non-negative integer `n` with `n <= |l|`, list rotation `n` times (`rotate'(l, n)`) is equivalent to list prefix removal and suffix addition (`drop(n, l) ++ take(n, l)`).
|
List.IsRotated.perm
theorem List.IsRotated.perm : ∀ {α : Type u} {l l' : List α}, l.IsRotated l' → l.Perm l'
This theorem states that for any type `α` and any two lists `l` and `l'` of this type, if `l` is a rotation of `l'` (denoted `l ~r l'`), then `l` is a permutation of `l'` (denoted `List.Perm l l'`). In other words, if one list can be obtained by rotating another list, then the two lists contain the same elements, but possibly in a different order.
More concisely: If two lists `l` and `l'` of type `α` are rotations of each other, then they are permutations of each other.
|
List.IsRotated.mem_iff
theorem List.IsRotated.mem_iff : ∀ {α : Type u} {l l' : List α}, l.IsRotated l' → ∀ {a : α}, a ∈ l ↔ a ∈ l'
The theorem `List.IsRotated.mem_iff` states that for any type `α`, and any lists `l` and `l'` of that type, if `l` is a rotation of `l'`, then an element `a` of type `α` is a member of `l` if and only if `a` is a member of `l'`. In other words, a list and its rotation contain exactly the same elements.
More concisely: For any type `α` and lists `l` and `l'` of type `List α`, `l` is a rotation of `l'` if and only if they have the same elements.
|
List.rotate'_rotate'
theorem List.rotate'_rotate' : ∀ {α : Type u} (l : List α) (n m : ℕ), (l.rotate' n).rotate' m = l.rotate' (n + m) := by
sorry
This theorem states that for any list `l` of elements of an arbitrary type `α`, and any natural numbers `n` and `m`, rotating the list `l` by `n` places using `List.rotate'` function and then rotating the result by `m` places is equivalent to rotating the list `l` by `n + m` places in a single step. This property mirrors typical rotation behavior, where consecutive rotations can be summed up into a single rotation operation.
More concisely: For any list `l` of type `α` and natural numbers `n` and `m`, `List.rotate' l n >> List.rotate' _ m = List.rotate' l (n + m)`.
|
List.IsRotated.refl
theorem List.IsRotated.refl : ∀ {α : Type u} (l : List α), l.IsRotated l
This theorem, `List.IsRotated.refl`, states that for any list `l` of elements of an arbitrary type `α`, `l` is rotated version of itself. This is a reflexivity property of the rotation relation for lists: every list is trivially a rotation of itself.
More concisely: For any list `l` of type `α`, `l` is equivalent to any cyclic rotation of itself. (In Lean, this theorem is named `List.IsRotated.refl`.)
|
List.nthLe_rotate'
theorem List.nthLe_rotate' :
∀ {α : Type u} (l : List α) (n k : ℕ) (hk : k < l.length),
(l.rotate n).nthLe ((l.length - n % l.length + k) % l.length) ⋯ = l.nthLe k hk
This theorem, `List.nthLe_rotate'`, is a variant of the `List.nthLe_rotate` theorem useful for rewrites from right to left. It states that for a list `l` of a type `α`, and for any natural numbers `n` and `k` such that `k` is less than the length of `l`, the `k`-th element of the list obtained by rotating `l` `n` times is the same as the `k`-th element of `l`. The position in the rotated list is given by `((l.length - n % l.length + k) % l.length)`, which is a modular arithmetic expression ensuring the index stays within the list bounds.
More concisely: For any list `l` of length `n`, and natural numbers `k` and `m` such that `k` is less than `n`, the `k`-th element of `l` is equal to the `((k + m) % n)`-th element of the rotated list `l` obtained by shifting it `m` positions to the right.
|
List.rotate_mod
theorem List.rotate_mod : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate (n % l.length) = l.rotate n
The theorem `List.rotate_mod` states that for any list `l` of elements of any type `α` and any natural number `n`, rotating the list `l` by `n` modulo the length of `l` is equivalent to simply rotating the list `l` by `n`. In other words, the effect of rotating a list doesn't change if we replace the number of positions of rotation `n` with `n` modulo the length of the list.
More concisely: For any list `l` of length `n` and natural number `k`, rotating list `l` by `k` is equivalent to rotating it by `k mod n`.
|
List.Nodup.cyclicPermutations
theorem List.Nodup.cyclicPermutations : ∀ {α : Type u} {l : List α}, l.Nodup → l.cyclicPermutations.Nodup
This theorem states that for all lists `l` of any type `α`, if `l` has no duplicate elements (that is, `l` satisfies the `Nodup` property), then all cyclic permutations of `l` are distinct. A cyclic permutation is a rearrangement of elements such that each element moves to the position of the next one, with the last one moving to the first position. The output is itself a list of these cyclic permutations, and this theorem asserts that this list has no duplicate elements.
More concisely: If `α` is any type and `l` is a list of `α` with no duplicates, then the set of cyclic permutations of `l` is a subset of `α` without repetitions.
|
List.rotate_cons_succ
theorem List.rotate_cons_succ :
∀ {α : Type u} (l : List α) (a : α) (n : ℕ), (a :: l).rotate (n + 1) = (l ++ [a]).rotate n
This theorem states that for any list `l` of elements of type `α`, any element `a` of the same type, and any natural number `n`, rotating the list that results from prepending `a` to `l` by `n+1` is the same as rotating the list that results from appending `a` to `l` by `n`. In other words, the operation of rotating a list to the left by `n+1` positions after adding an element at the beginning is the same as rotating the extended list to the left by `n` positions after adding the same element at the end.
More concisely: For any list `l` of length `n` and any element `a` and natural number `n`, prepending `a` to `l` and rotating left by `n+1` is equivalent to appending `a` to `l` and rotating left by `n`.
|
List.rotate_zero
theorem List.rotate_zero : ∀ {α : Type u} (l : List α), l.rotate 0 = l
The theorem `List.rotate_zero` states that for all types `α` and any list `l` of type `α`, rotating the list `l` by 0 (i.e., not rotating it at all) will result in the original list `l`. This is equivalent to saying that the identity operation for list rotation is rotation by 0.
More concisely: For all types `α` and lists `l` of length `n` over `α`, `List.rotate l 0 = l`.
|
List.IsRotated.trans
theorem List.IsRotated.trans :
∀ {α : Type u} {l l' l'' : List α}, l.IsRotated l' → l'.IsRotated l'' → l.IsRotated l''
This theorem states that for any type `α`, and any three lists of type `α` named `l`, `l'`, and `l''`, if `l` is a rotation of `l'` and `l'` is a rotation of `l''`, then `l` is a rotation of `l''`. Here, a rotation is a transformation where we take an element from one end of the list and put it on the other end. The "~r" symbol is used to indicate a rotation relation between two lists.
More concisely: If `l` is a rotation of `l'` and `l'` is a rotation of `l''`, then `l` is a rotation of `l''` (in the context of lists `l`, `l'`, and `l''` of type `α`).
|
List.length_rotate'
theorem List.length_rotate' : ∀ {α : Type u} (l : List α) (n : ℕ), (l.rotate' n).length = l.length
The theorem `List.length_rotate'` states that for any type `α`, any list `l` of type `α`, and any natural number `n`, the length of the list obtained by rotating `l` `n` times (using the `rotate'` function) is equal to the length of the original list `l`. Essentially, it means that rotating a list does not change its length.
More concisely: For any type `α` and natural number `n`, the length of the list obtained by rotating a list `l` of type `α` by `n` positions is equal to the original list length.
|
List.IsRotated.nodup_iff
theorem List.IsRotated.nodup_iff : ∀ {α : Type u} {l l' : List α}, l.IsRotated l' → (l.Nodup ↔ l'.Nodup)
The theorem `List.IsRotated.nodup_iff` states that for any type `α` and any two lists `l` and `l'` of type `α`, if `l` is a rotation of `l'` (denoted as `l ~r l'`), then `l` has no duplicates if and only if `l'` has no duplicates. In other words, the property of having no duplicate elements is preserved under the operation of rotation.
More concisely: For any type `α` and lists `l` and `l'` of type `α`, `l` has no duplicates if and only if `l'` has no duplicates whenever `l` is a rotation of `l'`.
|
List.rotate'_zero
theorem List.rotate'_zero : ∀ {α : Type u} (l : List α), l.rotate' 0 = l
This theorem, `List.rotate'_zero`, states that for any list `l` of elements of an arbitrary type `α`, the `rotate'` operation applied to `l` with a rotation count of 0 results in the original list `l` itself. In other words, if you take any list and "rotate" it zero times (i.e., do nothing), you will end up with the original list.
More concisely: For any list `l` of type `α`, `rotate' l 0` equals `l`.
|
List.rotate_eq_drop_append_take_mod
theorem List.rotate_eq_drop_append_take_mod :
∀ {α : Type u} {l : List α} {n : ℕ}, l.rotate n = List.drop (n % l.length) l ++ List.take (n % l.length) l := by
sorry
The theorem `List.rotate_eq_drop_append_take_mod` states that for any list `l` of elements of an arbitrary type `α` and any natural number `n`, rotating `l` `n` times to the left is equivalent to removing the first `n` mod `List.length l` elements from `l` and appending them to the end of `l`. In other words, rotating a list is the same as slicing it at a particular index `(n mod List.length l)`, and then swapping the two halves.
More concisely: For any list `l` of length `n` and natural number `k`, rotating `l` `k` times to the left is equivalent to taking the sublist from index `(k mod n)` to the end of `l`, removing it, and then appending it to the beginning of the sublist from the start of `l` to index `(k mod n)`.
|
List.rotate'_cons_succ
theorem List.rotate'_cons_succ :
∀ {α : Type u} (l : List α) (a : α) (n : ℕ), (a :: l).rotate' n.succ = (l ++ [a]).rotate' n
The theorem `List.rotate'_cons_succ` states that for any list `l` of elements of an arbitrary type `α`, any element `a` of type `α`, and any natural number `n`, rotating the list obtained by prepending `a` to `l` by `n+1` places (using the `rotate'` function) is the same as first appending `a` to the end of `l` and then rotating the resultant list by `n` places. In other words, it's just as effective to rotate the list after moving the first element to the end as it is to rotate the list first and then move the element.
More concisely: For any list `l` of length `n+1` over type `α`, rotating `l` by `n+1` places using `rotate'` after appending an element `a` to the end is equivalent to first appending `a` to `l` and then rotating it by `n` places. In Lean notation: `(a :: l) ++ List.rotate l n = List.rotate (a :: l) (n + 1)`.
|