List.eq_of_perm_of_sorted
theorem List.eq_of_perm_of_sorted :
∀ {α : Type uu} {r : α → α → Prop} [inst : IsAntisymm α r] {l₁ l₂ : List α},
l₁.Perm l₂ → List.Sorted r l₁ → List.Sorted r l₂ → l₁ = l₂
The theorem `List.eq_of_perm_of_sorted` states that for any type `α` and a binary relation `r` on `α` which is antisymmetric, given two lists `l₁` and `l₂` of elements of type `α`, if `l₁` is a permutation of `l₂` and both `l₁` and `l₂` are sorted with respect to the relation `r`, then `l₁` and `l₂` are equal. In other words, two sorted lists that are permutations of each other must be identical, given the sorting relation is antisymmetric. This theorem is important in scenarios where the order of elements matters, such as in sorting algorithms or computations related to order statistics.
More concisely: Given two sorted lists `l₁` and `l₂` of elements from a type `α` with an antisymmetric relation `r`, if `l₁` is a permutation of `l₂` with respect to `r`, then `l₁ = l₂`.
|
List.sorted_mergeSort
theorem List.sorted_mergeSort :
∀ {α : Type uu} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTotal α r] [inst_2 : IsTrans α r]
(l : List α), List.Sorted r (List.mergeSort r l)
The theorem `List.sorted_mergeSort` states that for all types `α` and for any relation `r` on `α` that is decidable, total, and transitive, if we have a list `l` of type `α`, then the list obtained by sorting `l` using the merge sort algorithm with respect to the relation `r` is sorted according to the same relation `r`. Here, being sorted is defined as the pairwise satisfaction of the relation `r` for all elements in the list.
More concisely: For any decidable, total, and transitive relation `r` on type `α`, the merge sort algorithm applied to a list `l` of `α` produces a sorted list according to `r`. That is, `∀x y in l, x r y ∧ mergeSort l r = l' ⟹ x r y' for all y' in l'`.
|
List.sorted_nil
theorem List.sorted_nil : ∀ {α : Type uu} {r : α → α → Prop}, List.Sorted r []
This theorem states that for any type `α` and any binary relation `r` on `α`, an empty list is `Sorted` with respect to `r`. In other words, an empty list is always sorted under any relation, since there are no elements to violate the sorting condition.
More concisely: For any type `α` and binary relation `r` on `α`, the empty list is a sorted list with respect to `r`.
|
List.sorted_lt_ofFn_iff
theorem List.sorted_lt_ofFn_iff :
∀ {n : ℕ} {α : Type uu} [inst : Preorder α] {f : Fin n → α},
List.Sorted (fun x x_1 => x < x_1) (List.ofFn f) ↔ StrictMono f
The theorem `List.sorted_lt_ofFn_iff` states that for any natural number `n`, any type `α` having a preorder structure, and any function `f` mapping from the finite ordered list of size `n` to `α`, the list generated by applying `f` to each element of the finite list is strictly sorted with respect to the less than (`<`) operator if and only if the function `f` is strictly monotone. In other words, a list constructed by applying a function to each element of a finite ordered list is strictly sorted if and only if the function increases for all consecutive elements in the list. Strict monotonicity of a function means that if `a` is less than `b`, then `f(a)` is less than `f(b)`.
More concisely: For any natural number `n` and type `α` with a preorder structure, a list `[a₁, ..., aₙ]` strictly sorted with respect to `<` by applying a function `f : List α -> α` if and only if `f` is strictly monotone.
|
List.monotone_iff_ofFn_sorted
theorem List.monotone_iff_ofFn_sorted :
∀ {n : ℕ} {α : Type uu} [inst : Preorder α] {f : Fin n → α},
Monotone f ↔ List.Sorted (fun x x_1 => x ≤ x_1) (List.ofFn f)
This theorem states that for any natural number `n`, any type `α` with a preorder, and any function `f` from `Fin n` to `α`, the function `f` is monotone if and only if the list obtained by applying `f` to each element in the finite sequence from `0` to `n-1` is sorted in non-decreasing order. In other words, a function `f` is increasing if and only if, when we apply `f` to each element in a finite sequence and create a list, that list is sorted from least to greatest. This list is created using the `List.ofFn` function in Lean 4, and being sorted is defined as any two elements in the list satisfying the `≤` relation according to their order in the list.
More concisely: For any natural number $n$, function $f$ from $Fin\, n$ to a preordered type $\alpha$, and sequence $(x\_i)_{i < n}$ in $Fin\, n$, the function $f$ is monotone if and only if the list $[f(x)\mid x \in Fin\, n]$ obtained from applying $f$ to each element in the sequence is sorted, i.e., $f(x\_i) \leq f(x\_j)$ for all $i < j < n$.
|
List.length_split_lt
theorem List.length_split_lt :
∀ {α : Type uu} {a b : α} {l l₁ l₂ : List α},
(a :: b :: l).split = (l₁, l₂) → l₁.length < (a :: b :: l).length ∧ l₂.length < (a :: b :: l).length
The theorem `List.length_split_lt` states that for any type `α` and any lists `l`, `l₁`, `l₂`, and elements `a`, `b` of type `α`, if the result of splitting the list `(a :: b :: l)` (which is a list starting with elements `a`, `b`, followed by the elements of `l`) is a pair of lists `(l₁, l₂)`, then the lengths of both `l₁` and `l₂` are strictly less than the length of the original list `(a :: b :: l)`. Essentially, this theorem ensures that the splitting operation does not result in a sublist that is longer than the original list.
More concisely: If `l = a :: b :: l` and `(l₁, l₂)` is the result of splitting `l`, then `length l₁ < length l` and `length l₂ < length l`.
|
List.perm_mergeSort
theorem List.perm_mergeSort :
∀ {α : Type uu} (r : α → α → Prop) [inst : DecidableRel r] (l : List α), (List.mergeSort r l).Perm l
The theorem `List.perm_mergeSort` states that for any type `α`, any decidable relation `r` on `α`, and any list `l` of elements of type `α`, the list obtained by performing a merge sort on `l` using the relation `r` is a permutation of `l`. In other words, merge sort rearranges the elements of the original list `l` without adding or removing elements.
More concisely: For any type `α` and decidable relation `r` on `α`, the merge sort function on a list `l` using relation `r` results in a permutation of `l`.
|
List.rel_of_sorted_cons
theorem List.rel_of_sorted_cons :
∀ {α : Type uu} {r : α → α → Prop} {a : α} {l : List α}, List.Sorted r (a :: l) → ∀ b ∈ l, r a b
This theorem states that for any type `α`, and any binary relation `r` on `α`, if we have a sorted list `l` under the relation `r` such that some element `a` is the first element of the list, then for any element `b` contained in `l`, the relation `r` holds between `a` and `b`. In other words, if a list is sorted according to a certain relation, the first element of the list will relate to all other elements in the list via this relation.
More concisely: If `α` is a type, `r` is a binary relation on `α`, and `l` is a list of `α` that is sorted under `r` with `a` as its first element, then `r(a, b)` holds for all `b` in `l`.
|
Monotone.ofFn_sorted
theorem Monotone.ofFn_sorted :
∀ {n : ℕ} {α : Type uu} [inst : Preorder α] {f : Fin n → α},
Monotone f → List.Sorted (fun x x_1 => x ≤ x_1) (List.ofFn f)
This theorem states that for any natural number `n` and any type `α` that has a defined preorder, if there exists a function `f` from finite `n` to `α` that is monotone (i.e., a function `f` such that if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`), then the list obtained from `f` using the `List.ofFn` function is sorted in non-decreasing order. In other words, for any two elements `x` and `x_1` in this list, `x` is less than or equal to `x_1`.
More concisely: For any natural number `n` and type `α` with a preorder, if `f:` Fin `n` `→` `α` is monotone, then `List.ofFn` `f` is a non-decreasing list.
|
List.orderedInsert_eq_take_drop
theorem List.orderedInsert_eq_take_drop :
∀ {α : Type uu} (r : α → α → Prop) [inst : DecidableRel r] (a : α) (l : List α),
List.orderedInsert r a l =
List.takeWhile (fun b => decide ¬r a b) l ++ a :: List.dropWhile (fun b => decide ¬r a b) l
The theorem `List.orderedInsert_eq_take_drop` proposes an alternative definition of the `orderedInsert` function using `takeWhile` and `dropWhile` functions in Lean 4. It states that for an arbitrary type `α`, a relation `r` on `α` which is decidable, and an element `a` of type `α` and a list `l` of type `α`, inserting `a` into `l` in order (`List.orderedInsert r a l`) is equivalent to taking the longest initial segment of `l` for which `a` does not have relation `r` with elements of `l` (`List.takeWhile (fun b => decide ¬r a b) l`), appending `a` to it, and finally appending the rest of the list starting at the first element that doesn't satisfy `r` with `a` (`List.dropWhile (fun b => decide ¬r a b) l`).
More concisely: For any decidable relation `r` on type `α`, `List.orderedInsert r a (List.takeWhile (λb, ¬r a b) l ++ [a] ++ List.dropWhile (λb, ¬r a b) l) = l` in Lean 4.
|
List.sorted_ofFn_iff
theorem List.sorted_ofFn_iff :
∀ {n : ℕ} {α : Type uu} {f : Fin n → α} {r : α → α → Prop},
List.Sorted r (List.ofFn f) ↔ ((fun x x_1 => x < x_1) ⇒ r) f f
This theorem, `List.sorted_ofFn_iff`, states that for any natural number `n`, any type `α`, any function `f` mapping from the finite set of `n` elements to `α`, and any relation `r` on `α`, the list generated by applying `f` to each element in the finite set is sorted according to the relation `r` if and only if `r` holds whenever `f` is applied to any pair of distinct elements in the finite set. In other words, if `r` is a relational property between two elements in the list, and `f` is a function that maps from each element in a finite list to the new list, then the list is sorted according to `r` if `r` is true for every pair of elements in the new list.
This theorem bridges the concept of a function preserving a property through its mapping and the sortedness of the resulting list.
More concisely: For any natural number `n`, type `α`, function `f` mapping a finite set of `n` elements to `α`, and relation `r` on `α`, `List.sorted (map f xs)` if and only if `r x y` for all distinct `x, y` in the finite set `xs`.
|
List.sorted_le_ofFn_iff
theorem List.sorted_le_ofFn_iff :
∀ {n : ℕ} {α : Type uu} [inst : Preorder α] {f : Fin n → α},
List.Sorted (fun x x_1 => x ≤ x_1) (List.ofFn f) ↔ Monotone f
This theorem states that for any natural number `n`, any type `α` with a preorder (which provides a `≤` relation), and any function `f` from `Fin n` (the set of natural numbers less than `n`) to `α`, the list generated by applying `f` to each element in `Fin n` (i.e., `List.ofFn f`) is sorted in non-decreasing order if and only if `f` is a monotone function. In other words, `f` preserves the `≤` relation if and only if the list created from `f` is sorted with respect to the `≤` relation.
More concisely: For any natural number `n`, any type `α` with a preorder, and any function `f: Fin n → α`, `List.ofFn f` is non-decreasing if and only if `f` is monotone.
|
List.Sorted.insertionSort_eq
theorem List.Sorted.insertionSort_eq :
∀ {α : Type uu} {r : α → α → Prop} [inst : DecidableRel r] {l : List α},
List.Sorted r l → List.insertionSort r l = l
This theorem states that for any list `l` of elements of an arbitrary type `α`, and any decidable relation `r` on `α`, if `l` is already sorted according to the relation `r` (that is, if `List.Sorted r l` holds), then applying the `insertionSort` function with the relation `r` to `l` will not change the list; symbolically, `List.insertionSort r l = l`. In other words, the insertion sort algorithm maintains the order of an already sorted list.
More concisely: If `l` is a list of elements from a type `α` that are already ordered according to a decidable relation `r`, then applying `List.insertionSort` with `r` to `l` results in the unchanged list, i.e., `List.insertionSort r l = l`.
|
List.sorted_insertionSort
theorem List.sorted_insertionSort :
∀ {α : Type uu} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTotal α r] [inst_2 : IsTrans α r]
(l : List α), List.Sorted r (List.insertionSort r l)
The theorem `List.sorted_insertionSort` states that for any type `α` and a relation `r` on `α` which is decidable, total, and transitive, the list `l` of type `α` when sorted using the `List.insertionSort` function with respect to `r`, results in a list that is sorted according to the relation `r`. This essentially means that the `List.insertionSort` function always produces a sorted list for any valid input, where the sorting order is defined by the relation `r`.
More concisely: For any decidable, total, and transitive relation `r` on type `α`, `List.insertionSort` guarantees a sorted list with respect to `r`.
|