Physlib.Mathematics.List.InsertionSort

Let $r$ be a decidable binary relation on a type $\alpha$. For any element $i \in \alpha$ and any list $l$ of elements in $\alpha$, let $a = \text{insertionSortMinPos}(r, i, l)$ be the index of the leftmost minimal element of the list $i :: l$ (this is the index that corresponds to the first element of the list after it is sorted). Let $l_{drop} = \text{insertionSortDropMinPos}(r, i, l)$ be the list obtained by removing the element at index $a$ from $i :: l$. Then the index $a$ is strictly less than the length of $l_{drop}$ plus one, i.e., $a < \text{length}(l_{drop}) + 1$.

Let $\alpha$ be a type with a decidable binary relation $r$. For an element $i \in \alpha$ and a list $l$ over $\alpha$, let $a = \text{insertionSortMinPos}(r, i, l)$ be the index of the leftmost minimal element of the list $i :: l$. This definition returns $a$ as an element of the finite type $\text{Fin}(n + 1)$, where $n = \text{length}(\text{insertionSortDropMinPos}(r, i, l))$ is the length of the list $i :: l$ after the element at index $a$ has been removed.

Let $\alpha$ be a type equipped with a decidable binary relation $r$ that is both total and transitive. For any element $a \in \alpha$ and list $l$ of elements in $\alpha$, let $m = \text{insertionSortMin}(r, a, l)$ be the minimum element of the list $a :: l$ (the element that would appear at the head of the list after sorting). Let $l_{\text{rem}} = \text{insertionSortDropMinPos}(r, a, l)$ be the list $a :: l$ with that specific minimum element removed. Then, for any index $i$ of the list $l_{\text{rem}}$, the relation $r(m, l_{\text{rem}}[i])$ holds.

Let $\alpha$ be a type and $r$ be a decidable binary relation on $\alpha$. For any element $a \in \alpha$ and any list $l$ of elements in $\alpha$, let $\sigma$ denote the bijection `insertionSortEquiv` that maps the indices of the list $a :: l$ to the indices of the list sorted by insertion sort. Let $k$ be the index in $a :: l$ defined by `insertionSortMinPos(r, a, l)`. Then the equivalence $\sigma$ maps the index $k$ to the first position of the sorted list, i.e., $\sigma(k) = 0$.

Let $\alpha$ be a type equipped with a decidable binary relation $r$. For any element $a \in \alpha$ and list $l$ over $\alpha$, let $\sigma$ be the bijection (equivalence) between the indices of the list $a :: l$ and the indices of the sorted list $\text{insertionSort}(r, a :: l)$. Let $k_{\text{min}}$ be the index in the original list $a :: l$ that corresponds to the first element (index $0$) of the sorted list. For any index $k$ of the list $a :: l$, if $k \neq k_{\text{min}}$, then the index of the corresponding element in the sorted list is strictly greater than zero, i.e., $\sigma(k) > 0$.

Let $r$ be a decidable binary relation on a type $\alpha$. For any element $a \in \alpha$ and list $l$ over $\alpha$, let $k_{\text{min}} = \text{insertionSortMinPos}(r, a, l)$ be the index of the leftmost minimal element in the list $a :: l$ with respect to $r$, and let $x_{\text{min}} = \text{insertionSortMin}(r, a, l)$ be the value at that index. Let $L_{\text{drop}} = \text{insertionSortDropMinPos}(r, a, l)$ be the list formed by removing the element at index $k_{\text{min}}$ from $a :: l$. For any index $i$ of $L_{\text{drop}}$, if the corresponding index $k$ in the original list $a :: l$ (defined by $k = \text{succAbove}_{k_{\text{min}}}(i)$) satisfies $k < k_{\text{min}}$, then the relation $r$ does not hold for the pair $(L_{\text{drop}}[i], x_{\text{min}})$, i.e., $\neg r(L_{\text{drop}}[i], x_{\text{min}})$.

Let $\alpha$ be a type equipped with a decidable, total, and transitive relation $r$. For any list $l$ of elements in $\alpha$, applying the insertion sort algorithm with respect to $r$ twice is equivalent to applying it once: $$\text{insertionSort}_r (\text{insertionSort}_r l) = \text{insertionSort}_r l$$

Let $r$ be a total and transitive binary relation on a type $\alpha$. For any elements $a, b \in \alpha$ and any list $l$ of elements in $\alpha$, if the relation $r(a, b)$ does not hold, then the result of performing an ordered insertion of $b$ then $a$ into $l$ is equal to the result of performing an ordered insertion of $a$ then $b$. That is, $$\text{orderedInsert}(r, a, \text{orderedInsert}(r, b, l)) = \text{orderedInsert}(r, b, \text{orderedInsert}(r, a, l))$$ where $\text{orderedInsert}$ is the operation that inserts an element into a list at the first position that maintains the ordering according to $r$.

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. For any element $a \in \alpha$ and any lists $l_1, l_2$ of elements in $\alpha$, applying insertion sort to the concatenation of (the ordered insertion of $a$ into $l_1$) and $l_2$ yields the same result as applying insertion sort to the concatenation of (the list formed by prepending $a$ to $l_1$) and $l_2$. That is, $$\text{insertionSort}_r (\text{orderedInsert}(r, a, l_1) ++ l_2) = \text{insertionSort}_r ((a :: l_1) ++ l_2)$$ where $\text{orderedInsert}(r, a, l_1)$ is the operation that inserts $a$ into $l_1$ at the first position maintaining the order according to $r$, $a :: l_1$ denotes the list with $a$ prepended to $l_1$, and $++$ denotes list concatenation.

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. For any two lists $l_1$ and $l_2$ of elements in $\alpha$, applying insertion sort to the concatenation of the sorted version of $l_1$ and the list $l_2$ yields the same result as applying insertion sort to the concatenation of the original $l_1$ and $l_2$. That is, $$\text{insertionSort}_r (\text{insertionSort}_r(l_1) ++ l_2) = \text{insertionSort}_r (l_1 ++ l_2)$$ where $\text{insertionSort}_r$ denotes the insertion sort algorithm with respect to the relation $r$, and $++$ denotes list concatenation.

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. For any three lists $l_1, l_2$, and $l_3$ of elements in $\alpha$, applying insertion sort to the concatenation of $l_1$, the sorted version of $l_2$, and $l_3$ yields the same result as applying insertion sort to the concatenation of the original lists $l_1, l_2$, and $l_3$. That is, $$\text{insertionSort}_r (l_1 ++ \text{insertionSort}_r(l_2) ++ l_3) = \text{insertionSort}_r (l_1 ++ l_2 ++ l_3)$$ where $\text{insertionSort}_r$ denotes the insertion sort algorithm with respect to the relation $r$, and $++$ denotes list concatenation.

For any type $\alpha$, a decidable binary relation $r$ on $\alpha$, an element $a \in \alpha$, and a list $l$ of elements in $\alpha$, the length of the list resulting from the ordered insertion of $a$ into $l$ with respect to $r$ is equal to the length of the list formed by prepending $a$ to $l$ (i.e., $\text{length}(a :: l)$ or $\text{length}(l) + 1$).

Let $\alpha$ be a type with a decidable, total, and transitive relation $r$. Given two elements $a, b \in \alpha$ such that the relation $r(a, b)$ does not hold, for any list $l$ over $\alpha$, the length of the prefix of the list obtained by performing an ordered insertion of $b$ into $l$ (denoted $\text{orderedInsert}(r, b, l)$) consisting of elements $c$ for which $r(a, c)$ is false, is equal to the length of the corresponding prefix in $l$ plus one. That is, $$\text{length}(\text{takeWhile } (\lambda c. \neg r(a, c)) (\text{orderedInsert } r \text{ } b \text{ } l)) = \text{length}(\text{takeWhile } (\lambda c. \neg r(a, c)) \text{ } l) + 1$$ where $\text{takeWhile}$ is the function that returns the longest prefix of a list satisfying a given predicate.

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. For any two elements $a, b \in \alpha$ such that the relation $r(a, b)$ does not hold, and for any list $l$ over $\alpha$, the length of the longest prefix of the list obtained by performing an ordered insertion of $a$ into $l$ (denoted $\text{orderedInsert}(r, a, l)$) consisting of elements $c$ for which $r(b, c)$ is false, is equal to the length of the corresponding prefix in the original list $l$. That is, $$\text{length}(\text{takeWhile } (\lambda c. \neg r(b, c)) (\text{orderedInsert } r \text{ } a \text{ } l)) = \text{length}(\text{takeWhile } (\lambda c. \neg r(b, c)) \text{ } l)$$ where $\text{takeWhile}$ is the function that returns the longest prefix of a list satisfying a given predicate.

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. Let $a, b \in \alpha$ be elements such that the relation $r(a, b)$ does not hold. For any list $l$ and any natural number $n$ such that $n+2$ is a valid index for the list $a :: b :: l$, let $\phi_L$ denote the bijection `insertionSortEquiv` which maps the indices of a list $L$ to the indices of its sorted version $\text{insertionSort}(r, L)$. Then it holds that: $$\phi_{a :: b :: l}(n+2) = \phi_{b :: a :: l}(n+2)$$ This theorem states that for elements originally located in the tail $l$ of a list, their final position in the sorted list is independent of the initial order of the head elements $a$ and $b$, provided that $a$ and $b$ are the same pair and their relative sorted order is fixed (by $\neg r(a, b)$).

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. For any elements $a, a_2 \in \alpha$ and lists $l_1, l_2$ of elements in $\alpha$, let $\phi_L$ denote the bijection `insertionSortEquiv` which maps the indices of a list $L$ to the indices of its sorted version $\text{insertionSort}(r, L)$. Then, the final position (index) in the sorted list for the element $a_2$ is the same whether $a$ is prepended to $l_1$ or inserted into $l_1$ using an ordered insertion. That is: $$\phi_{\text{orderedInsert}(r, a, l_1) \mathbin{+\!+} (a_2 :: l_2)}(|l_1| + 1) = \phi_{(a :: l_1) \mathbin{+\!+} (a_2 :: l_2)}(|l_1| + 1)$$ where $|l_1|$ is the length of list $l_1$, and the index $|l_1| + 1$ refers to the position of element $a_2$ in both concatenated lists.

Let $\alpha$ be a type equipped with a decidable, total, and transitive binary relation $r$. For any element $a \in \alpha$ and any two lists $l_1, l_2$ of elements in $\alpha$, let $\phi_L$ denote the bijection `insertionSortEquiv` which maps the indices of a list $L$ to the indices of its sorted version $\text{insertionSort}(r, L)$. Then, the final position (index) in the sorted list for the element $a$ is the same whether the prefix $l_1$ is sorted prior to the global sort or not. That is: $$\phi_{\text{insertionSort}(r, l_1) \mathbin{+\!+} (a :: l_2)}(|l_1|) = \phi_{l_1 \mathbin{+\!+} (a :: l_2)}(|l_1|)$$ where $|l_1|$ is the length of the list $l_1$, and the index $|l_1|$ refers to the position of element $a$ in both concatenated lists.

Let $\alpha$ be a type, $r$ be a transitive and decidable binary relation on $\alpha$, and $p$ be a decidable predicate on $\alpha$. If an element $a \in \alpha$ satisfies the predicate $p$, then for any list $l$ that is pairwise ordered by $r$, filtering the result of an ordered insertion of $a$ into $l$ is equal to performing an ordered insertion of $a$ into the filtered version of $l$: $$\text{filter } p (\text{orderedInsert } r \ a \ l) = \text{orderedInsert } r \ a (\text{filter } p \ l)$$ Here, `orderedInsert` denotes the operation of inserting an element into a list while maintaining the order defined by $r$, and `filter` denotes the selection of elements in a list that satisfy the predicate $p$.

Let $\alpha$ be a type with a decidable binary relation $r$. For any element $a \in \alpha$ and any decidable predicate $p$ such that $p(a)$ is false, and for any list $l$ of elements in $\alpha$, the result of filtering the list after performing an ordered insertion of $a$ into $l$ is the same as filtering the original list $l$. That is, $$\text{filter } p (\text{orderedInsert } r \ a \ l) = \text{filter } p \ l$$

Let $\alpha$ be a type, $r$ be a decidable, total, and transitive binary relation on $\alpha$, and $p$ be a decidable predicate on $\alpha$. For any list $l$ of elements in $\alpha$, performing an insertion sort on the list filtered by $p$ yields the same result as filtering the list after it has been sorted using insertion sort. That is, $$\text{insertionSort}(r, \text{filter}(p, l)) = \text{filter}(p, \text{insertionSort}(r, l))$$

Let $r$ be a transitive binary relation on a type $\alpha$. For any element $a \in \alpha$ and any list $l$ of elements in $\alpha$ that is pairwise related by $r$ (i.e., for any elements $x, y$ in $l$, if $x$ appears before $y$, then $r(x, y)$ holds), the operation of taking elements from the beginning of $l$ while $\neg r(a, c)$ holds is equivalent to filtering the entire list $l$ for elements satisfying $\neg r(a, c)$. That is, $\text{takeWhile}(\lambda c. \neg r(a, c), l) = \text{filter}(\lambda c. \neg r(a, c), l)$.

Let $r$ be a transitive and decidable binary relation on a type $\alpha$. For any element $a \in \alpha$ and any list $l$ that is pairwise related by $r$ (i.e., $l$ is sorted with respect to $r$), the list obtained by dropping elements from the beginning of $l$ that do not satisfy $r(a, c)$ is equal to the list obtained by filtering $l$ to keep only those elements $c$ such that $r(a, c)$ holds.

Let $r$ be a transitive binary relation on a type $\alpha$. For any list $l$ of elements in $\alpha$ that is pairwise related by $r$ (meaning for any elements $x$ and $y$ in $l$ such that $x$ appears before $y$, the relation $r(x, y)$ holds), and for any element $a \in \alpha$, the sublist of $l$ containing elements $c$ for which $r(a, c)$ holds is equal to the concatenation of: 1. The sublist of elements $c \in l$ satisfying both $r(a, c)$ and $r(c, a)$. 2. The sublist of elements $c \in l$ satisfying $r(a, c)$ but not $r(c, a)$. In mathematical notation, this is expressed as: $$\text{filter}(\lambda c. r(a, c), l) = \text{filter}(\lambda c. r(a, c) \wedge r(c, a), l) ++ \text{filter}(\lambda c. r(a, c) \wedge \neg r(c, a), l)$$ where $\text{filter}(P, l)$ is the sublist of elements in $l$ satisfying property $P$, and $++$ denotes the concatenation of two lists.

Let $r$ be a decidable, total, and transitive binary relation on a type $\alpha$. For any element $a \in \alpha$ and any list $l$ of elements in $\alpha$, the sublist of elements $c$ that are equivalent to $a$ under $r$ (satisfying $r(a, c) \wedge r(c, a)$) is the same whether it is extracted from the original list $l$ or from the list obtained after performing an insertion sort on $l$ with respect to $r$. In mathematical notation: $$\text{filter}(\lambda c. r(a, c) \wedge r(c, a), \text{insertionSort } r \ l) = \text{filter}(\lambda c. r(a, c) \wedge r(c, a), l)$$ where $\text{insertionSort } r \ l$ denotes the list $l$ sorted by the insertion sort algorithm according to the relation $r$.

Let $r$ be a decidable, total, and transitive binary relation on a type $\alpha$. Let $a \in \alpha$ be an element, and let $l_1, l,$ and $l_2$ be lists of elements in $\alpha$. Suppose that every element $b$ in the list $l$ is equivalent to $a$ with respect to $r$ (i.e., $r(a, b) \wedge r(b, a)$ holds for all $b \in l$). Then the insertion sort of the concatenation $l_1 ++ l ++ l_2$ with respect to $r$ is equal to the concatenation of the following five parts: 1. The prefix of $\text{insertionSort}(r, l_1 ++ l_2)$ consisting of elements $c$ such that $\neg r(a, c)$. 2. The sublist of $l_1$ consisting of elements $c$ such that $r(a, c) \wedge r(c, a)$. 3. The list $l$ itself. 4. The sublist of $l_2$ consisting of elements $c$ such that $r(a, c) \wedge r(c, a)$. 5. The sublist of $\text{insertionSort}(r, l_1 ++ l_2)$ consisting of elements $c$ such that $r(a, c) \wedge \neg r(c, a)$. In mathematical notation: $$\begin{aligned} \text{insertionSort}(r, l_1 ++ l ++ l_2) = \text{ } & \text{takeWhile}(\lambda c. \neg r(a, c), \text{insertionSort}(r, l_1 ++ l_2)) \ ++ \\ & \text{filter}(\lambda c. r(a, c) \wedge r(c, a), l_1) \ ++ \\ & l \ ++ \\ & \text{filter}(\lambda c. r(a, c) \wedge r(c, a), l_2) \ ++ \\ & \text{filter}(\lambda c. r(a, c) \wedge \neg r(c, a), \text{insertionSort}(r, l_1 ++ l_2)) \end{aligned}$$

Let $r$ be a decidable, total, and transitive binary relation on a type $\alpha$. For any element $a \in \alpha$ and any two lists $l_1, l_2$ of elements in $\alpha$, the insertion sort of the concatenation $l_1 ++ l_2$ with respect to $r$ can be decomposed into the concatenation of the following four parts: 1. The prefix of $\text{insertionSort}(r, l_1 ++ l_2)$ consisting of elements $c$ such that $\neg r(a, c)$. 2. The sublist of $l_1$ consisting of elements $c$ equivalent to $a$ (satisfying $r(a, c) \wedge r(c, a)$). 3. The sublist of $l_2$ consisting of elements $c$ equivalent to $a$ (satisfying $r(a, c) \wedge r(c, a)$). 4. The sublist of $\text{insertionSort}(r, l_1 ++ l_2)$ consisting of elements $c$ such that $r(a, c) \wedge \neg r(c, a)$. In mathematical notation: $$\begin{aligned} \text{insertionSort}(r, l_1 ++ l_2) = \text{ } & \text{takeWhile}(\lambda c. \neg r(a, c), \text{insertionSort}(r, l_1 ++ l_2)) \ ++ \\ & \text{filter}(\lambda c. r(a, c) \wedge r(c, a), l_1) \ ++ \\ & \text{filter}(\lambda c. r(a, c) \wedge r(c, a), l_2) \ ++ \\ & \text{filter}(\lambda c. r(a, c) \wedge \neg r(c, a), \text{insertionSort}(r, l_1 ++ l_2)) \end{aligned}$$