Physlib.Mathematics.List

Let $I$ be a type and $P$ be a decidable predicate on $I$. Let $l$ be a list of elements of type $I$. Suppose that the predicate $P$ is downward-closed with respect to the indices of $l$; that is, for any indices $0 \le j < k < \text{length}(l)$, if the element at index $k$ satisfies $P$, then the element at index $j$ must also satisfy $P$. Then, for any index $i \in \mathbb{N}$, it holds that $$\text{takeWhile}(P, \text{eraseIdx}(l, i)) = \text{eraseIdx}(\text{takeWhile}(P, l), i)$$ where $\text{eraseIdx}(l, i)$ denotes the list $l$ with the element at index $i$ removed, and $\text{takeWhile}(P, l)$ is the longest prefix of $l$ consisting only of elements that satisfy $P$.

Let $I$ be a type and $P$ be a decidable predicate on $I$. Let $l$ be a list of elements of type $I$ and $i$ be a natural number representing an index. Suppose that for any indices $j$ and $k$ of the list $l$, if $j < k$ and the element at index $k$ satisfies $P$, then the element at index $j$ also satisfies $P$. Then, the result of removing the prefix of elements satisfying $P$ from the list $l$ after erasing the element at index $i$ is given by: $$\text{dropWhile } P (\text{eraseIdx } l \, i) = \begin{cases} \text{eraseIdx } (\text{dropWhile } P \, l) (i - \text{length}(\text{takeWhile } P \, l)) & \text{if } \text{length}(\text{takeWhile } P \, l) \leq i \\ \text{dropWhile } P \, l & \text{otherwise} \end{cases}$$ where $\text{takeWhile } P \, l$ is the prefix of $l$ consisting of elements satisfying $P$, $\text{dropWhile } P \, l$ is the remainder of the list, and $\text{eraseIdx } l \, i$ is the list $l$ with the element at index $i$ removed.

For any type $I$ equipped with a decidable binary relation $\le$, and for any list $L$ of elements in $I$, the length of the list after applying the insertion sort algorithm using $\le$ is equal to the length of the original list $L$. That is, $|\text{insertionSort}(\le, L)| = |L|$.

Given a type $I$ with a decidable binary relation $\le$ (denoted as `le1`), a list $r$, and an element $r_0$, this function returns the index at which $r_0$ is placed when inserted into $r$ via the `List.orderedInsert` operation. The index is defined as the length of the prefix of $r$ consisting of elements $b$ such that the condition $r_0 \le b$ is false. The returned value is an index of type $\text{Fin}(n)$, where $n$ is the length of the list after insertion.

Given a type $I$ with a decidable binary relation $\le$ (denoted as `le1`), for any list $r$ in $I$ and any element $r_0 \in I$, the index $\text{orderedInsertPos}(\le, r, r_0)$ at which $r_0$ is inserted into $r$ is strictly less than the length of the list formed by prepending $r_0$ to $r$, denoted by $|r_0 :: r|$.

Let $I$ be a type with a decidable binary relation $\le$ (denoted as `le1`). For any list $r$ of elements in $I$ and any element $r_0$ in $I$, the element at index $i = \text{orderedInsertPos}(\le, r, r_0)$ in the list resulting from the ordered insertion $\text{orderedInsert}(\le, r_0, r)$ is $r_0$. That is, $(\text{orderedInsert } \le r_0 r)[i] = r_0$, where $i$ is the position at which $r_0$ is placed during the insertion.

Let $I$ be a type with a decidable binary relation $\le_1$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $i$ be the index where $r_0$ is placed when inserted into $r$ via the ordered insertion function `List.orderedInsert` (this index is given by `orderedInsertPos`). If the element at index $i$ is removed from the resulting list using `eraseIdx`, the remaining list is equal to the original list $r$.

Let $I$ be a type with a decidable binary relation $\le$. For a list $r$ and elements $r_0, r_1 \in I$, let $P(r, r_0)$ denote the index at which $r_0$ is placed when inserted into $r$ via an ordered insertion. Then the index $P(r_1 :: r, r_0)$ is given by: $$P(r_1 :: r, r_0) = \begin{cases} 0 & \text{if } r_0 \le r_1 \\ P(r, r_0) + 1 & \text{otherwise} \end{cases}$$

Let $I$ be a type with a decidable binary relation $\le$. Let $f : I \to \text{Type}$ be a type family. Consider a list $l$ of dependent pairs $\langle i, x \rangle$ (where $i \in I$ and $x \in f(i)$), and let $\text{pr}_1$ denote the projection map that sends $\langle i, x \rangle$ to $i$. For any $k \in I$ and $a \in f(k)$, the index at which the pair $\langle k, a \rangle$ is inserted into $l$ (using the relation defined by $\le$ on the first components) is equal to the index at which $k$ is inserted into the list $\text{map}(\text{pr}_1, l)$ using the relation $\le$.

Let $I$ be a type equipped with a decidable binary relation $\le$. For a list $r$ of elements in $I$ and an element $r_0 \in I$, let $p$ be the index where $r_0$ is inserted into $r$ using the ordered insertion operation `List.orderedInsert`. For any index $i < p$, the element at index $i$ in the list resulting from the insertion is equal to the element at index $i$ in the original list $r$.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and an element $r_0 \in I$, let $p$ be the index at which $r_0$ is inserted into $r$ via the ordered insertion operation (denoted by $\text{orderedInsertPos}(\le, r, r_0)$). Then, the prefix of the resulting list $\text{orderedInsert}(\le, r_0, r)$ consisting of the first $p$ elements is equal to the prefix of the original list $r$ obtained by taking elements $b$ such that the condition $r_0 \le b$ is false.

Let $I$ be a type equipped with a decidable binary relation $\le$. For a list $r$ of elements in $I$ and an element $r_0 \in I$, let $p = \text{orderedInsertPos}(\le, r, r_0)$ be the index where $r_0$ is inserted into $r$ via the ordered insertion operation. Then the first $p$ elements of the original list $r$ are identical to the first $p$ elements of the list resulting from the insertion. That is: \[ \text{List.take}(p, r) = \text{List.take}(p, \text{List.orderedInsert}(\le, r_0, r)) \]

For a type $I$ equipped with a decidable binary relation $\le$, a list $r$, and an element $r_0$, let $i$ be the position where $r_0$ is inserted into $r$ (formally defined as $i = \text{orderedInsertPos}(\le, r, r_0)$). Then the suffix of the original list $r$ starting at index $i$ is equal to the suffix of the list resulting from the ordered insertion starting at index $i+1$. That is: \[ \text{List.drop}(i, r) = \text{List.drop}(i + 1, \text{List.orderedInsert}(\le, r_0, r)) \]

For a type $I$ equipped with a decidable binary relation $\le$, a list $r$, and an element $r_0 \in I$, let $i$ be the index at which $r_0$ would be placed when inserted into $r$ via an ordered insertion operation (defined as $i = \text{orderedInsertPos}(\le, r, r_0)$). The theorem states that the prefix of the original list $r$ of length $i$ is equal to the prefix of $r$ obtained by taking elements $b$ as long as the condition $r_0 \le b$ is false. That is: \[ \text{List.take}(i, r) = \text{List.takeWhile}(\lambda b.\ \neg(r_0 \le b), r) \]

For a type $I$ equipped with a decidable binary relation $\le$, a list $r$, and an element $r_0$, let $i$ be the index at which $r_0$ is placed when inserted into $r$ via the ordered insertion operation (defined as $i = \text{orderedInsertPos}(\le, r, r_0)$). The theorem states that dropping the first $i$ elements of the original list $r$ is equivalent to dropping elements from the start of $r$ as long as the condition $r_0 \le b$ is false. That is: \[ \text{List.drop}(i, r) = \text{List.dropWhile}(\lambda b.\ \neg(r_0 \le b), r) \]

Let $I$ be a type equipped with a decidable binary relation $\le$. For a list $r$ of elements in $I$ and an element $r_0 \in I$, let $i$ be the index at which $r_0$ is placed when inserted into $r$ via the ordered insertion operation (`orderedInsert`). Then, the prefix of the resulting list (after insertion) of length $i+1$ is equal to the prefix of the original list $r$ consisting of elements $b$ for which the condition $r_0 \le b$ is false, followed by the element $r_0$.

Let $I$ be a type equipped with a decidable binary relation $\le$. For a list $r$ of elements in $I$ and an element $r_0 \in I$, let $i$ be the index at which $r_0$ is placed when inserted into $r$ via the ordered insertion operation (defined as $i = \text{orderedInsertPos}(\le, r, r_0)$). For any index $n$ of the list $r$, if $n < i$, then the element at that index $r_n$ satisfies $\neg(r_0 \le r_n)$.

Let $I$ be a type equipped with a decidable binary relation $\le$. Let $r$ be a list of elements in $I$ and $r_0 \in I$ be an element. Let $p = \text{orderedInsertPos}(\le, r, r_0)$ be the index at which $r_0$ is inserted into $r$ via the ordered insertion operation. For any index $n$ in the list resulting from this insertion, if $n < p$, then the element $x_n$ at that index satisfies $\neg(r_0 \le x_n)$.

Let $I$ be a type equipped with a decidable, total, and transitive binary relation $\le$. Let $r$ be a list of elements in $I$ that is sorted with respect to $\le$ (i.e., `List.Pairwise le1 r`). Let $r_0 \in I$ be an element, and let $p$ be the position where $r_0$ is placed when inserted into $r$ via the ordered insertion operation (the index of the first element $b$ in $r$ such that $r_0 \le b$ is true). For any index $n$ in the list $r$, if $n \ge p$, then $r_0 \le r_n$.

Let $I$ be a type with a decidable binary relation $\le$. Let $r$ be a list of elements in $I$, $r_0$ be an element in $I$, and $p$ be the position at which $r_0$ is inserted into $r$ via the `orderedInsert` operation (denoted by `orderedInsertPos le1 r r0`). Suppose that the condition $\neg(r_0 \le \cdot)$ is prefix-closed in $r$; that is, for any indices $j < k$, if $\neg(r_0 \le r_k)$, then $\neg(r_0 \le r_j)$. Then, for any index $i < p$, the result of erasing the element at index $i$ from the list after $r_0$ has been inserted is the same as inserting $r_0$ into the list after the element at index $i$ has been erased from $r$: $$\text{eraseIdx}(\text{orderedInsert}(\le, r_0, r), i) = \text{orderedInsert}(\le, r_0, \text{eraseIdx}(r, i))$$ where $\text{eraseIdx}(l, i)$ denotes the removal of the element at index $i$ from list $l$.

Let $I$ be a type equipped with a decidable binary relation $\le$. Let $r$ be a list of elements of type $I$ and $r_0$ be an element of $I$. Let $p = \text{orderedInsertPos}(\le, r, r_0)$ be the index where $r_0$ is placed when inserted into $r$ via the `orderedInsert` operation (specifically, the length of the prefix of $r$ where the condition $r_0 \le b$ is false). Suppose that for any indices $j$ and $k$ of the list $r$, if $j < k$ and the condition $r_0 \le r_k$ is false, then $r_0 \le r_j$ is also false. Then for any natural number $i$ such that $p \le i$, it holds that: $$\text{eraseIdx}(\text{orderedInsert}(\le, r_0, r), i + 1) = \text{orderedInsert}(\le, r_0, \text{eraseIdx}(r, i))$$ where $\text{orderedInsert}(\le, r_0, r)$ is the list $r$ with $r_0$ inserted at index $p$, and $\text{eraseIdx}(l, n)$ is the list $l$ with the element at index $n$ removed.

Let $I$ be a type with a decidable binary relation $\le$. Given a list $r$ and an element $r_0 \in I$, let $L_{ins} = \text{orderedInsert}(\le, r_0, r)$ be the list obtained by inserting $r_0$ into $r$ at the position $p = \text{orderedInsertPos}(\le, r, r_0)$. This definition provides an equivalence (bijection) between the set of indices of the prepended list $r_0 :: r$, denoted by $\text{Fin}(|r| + 1)$, and the set of indices of the list $L_{ins}$, denoted by $\text{Fin}(|L_{ins}|)$. Under this mapping, the index $0$ is sent to $p$, and the indices $\{1, \dots, |r|\}$ are mapped to the remaining positions in $L_{ins}$ such that the relative order of the original elements in $r$ is preserved.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $\phi = \text{orderedInsertEquiv}(\le, r, r_0)$ be the equivalence (bijection) that maps the indices of the prepended list $r_0 :: r$ to the indices of the list resulting from inserting $r_0$ into $r$ via the `orderedInsert` operation. Let $p = \text{orderedInsertPos}(\le, r, r_0)$ be the index at which $r_0$ is placed in the resulting list. Then the equivalence $\phi$ maps the first index $0$ to $p$, i.e., $\phi(0) = p$.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $p = \text{orderedInsertPos}(\le, r, r_0)$ be the position at which $r_0$ is inserted into $r$ by the $\text{orderedInsert}$ operation. Let $\phi$ be the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$ which maps indices of the prepended list $r_0 :: r$ to indices of the list resulting from the ordered insertion. Then for any natural number $n$ such that $n+1$ is a valid index of $r_0 :: r$, the equivalence satisfies: $$\phi(n+1) = \text{succAbove}_p(n)$$ where $\text{succAbove}_p(n)$ is defined as $n$ if $n < p$ and $n+1$ if $n \ge p$. This formula describes how the original indices of $r$ (shifted by 1 in $r_0 :: r$) are mapped to their new positions in the list after $r_0$ is inserted at position $p$.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $p = \text{orderedInsertPos}(\le, r, r_0)$ be the position at which $r_0$ is inserted into $r$ via the ordered insertion operation. Let $\phi$ denote the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$ which maps the set of indices of the prepended list $r_0 :: r$ to the set of indices of the list resulting from the insertion. For any index $n \in \text{Fin}(|r|)$, let $n+1$ be its successor in $\text{Fin}(|r|+1)$. Then it holds that: $$\phi(n+1) = \text{succAbove}_p(n)$$ where $\text{succAbove}_p(n)$ is the function that maps $n$ to $n$ if $n < p$ and to $n+1$ if $n \ge p$.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $\phi$ denote the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$ which maps the set of indices of the prepended list $r_0 :: r$ to the set of indices of the list resulting from the ordered insertion of $r_0$ into $r$. For any two indices $n, m \in \text{Fin}(|r|)$, if $\phi(n+1) < \phi(m+1)$, then it holds that $n < m$.

Let $\alpha$ be a type with a decidable binary relation $\le$. For any element $a \in \alpha$ and any two lists $l, l'$ of elements in $\alpha$, if $l = l'$, then the equivalence of indices $\text{orderedInsertEquiv}(\le, l, a)$ (which maps indices of $a :: l$ to indices of $\text{orderedInsert}(\le, a, l)$) is equal to the composition: $$\text{orderedInsertEquiv}(\le, l, a) = \text{cast}_2 \circ \text{orderedInsertEquiv}(\le, l', a) \circ \text{cast}_1$$ where $\text{cast}_1$ and $\text{cast}_2$ are the canonical isomorphisms between the respective index sets $\text{Fin}(|l|+1) \cong \text{Fin}(|l'|+1)$ and $\text{Fin}(|\text{orderedInsert}(\le, a, l')|) \cong \text{Fin}(|\text{orderedInsert}(\le, a, l)|)$ induced by the equality of the lists.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $L_{ins} = \text{orderedInsert}(\le, r_0, r)$ be the list resulting from the ordered insertion of $r_0$ into $r$. Let $\phi: \text{Fin}(|r| + 1) \cong \text{Fin}(|L_{ins}|)$ be the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$, which maps the indices of the prepended list $r_0 :: r$ to the corresponding indices in $L_{ins}$. Then, the element at index $i$ in the list $r_0 :: r$ is equal to the element at index $\phi(i)$ in $L_{ins}$. That is, the element retrieval functions satisfy: $$(r_0 :: r).\text{get} = L_{ins}.\text{get} \circ \phi$$

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $L_{ins} = \text{orderedInsert}(\le, r_0, r)$ be the list resulting from the ordered insertion of $r_0$ into $r$. Let $\phi: \text{Fin}(|r| + 1) \cong \text{Fin}(|L_{ins}|)$ be the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$, which maps the indices of the prepended list $r_0 :: r$ to the corresponding indices in $L_{ins}$, and let $\phi^{-1}$ be its inverse. Then, the element retrieval functions (the `get` operations) satisfy the identity: $$(r_0 :: r).\text{get} \circ \phi^{-1} = L_{ins}.\text{get}$$

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, let $L_{ins} = \text{orderedInsert}(\le, r_0, r)$ be the list resulting from the ordered insertion of $r_0$ into $r$. Let $\phi: \text{Fin}(|r| + 1) \cong \text{Fin}(|L_{ins}|)$ be the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$, which maps indices of the prepended list $r_0 :: r$ to the corresponding indices in $L_{ins}$. Then, removing the element at the index $\phi(0)$ from $L_{ins}$ using the `eraseIdx` function results in the original list $r$: $$(L_{ins}).\text{eraseIdx}(\phi(0)) = r$$

Let $I$ be a type with a decidable binary relation $\le$. Let $r$ be a list of elements in $I$ and $r_0$ be an element in $I$. Let $\phi$ be the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$, which maps the indices of the prepended list $r_0 :: r$ to the indices of the list resulting from inserting $r_0$ into $r$ (denoted by $\text{orderedInsert}(\le, r_0, r)$). Suppose that for any indices $i < j$ of the list $r$, the condition $\neg(r_0 \le \cdot)$ is prefix-closed, meaning $\neg(r_0 \le r_j) \implies \neg(r_0 \le r_i)$. Then, for any natural number $n$ such that $n+1$ is a valid index of $r_0 :: r$, it holds that: $$\text{eraseIdx}(\text{orderedInsert}(\le, r_0, r), \phi(n+1)) = \text{orderedInsert}(\le, r_0, \text{eraseIdx}(r, n))$$ where $\text{eraseIdx}(l, k)$ denotes the removal of the element at index $k$ from list $l$.

Let $I$ be a type with a decidable binary relation $\le$. Let $r$ be a list of elements in $I$ and $r_0$ be an element in $I$. Let $\phi$ be the index equivalence $\text{orderedInsertEquiv}(\le, r, r_0)$, which maps the indices of the prepended list $r_0 :: r$ to the indices of the list resulting from inserting $r_0$ into $r$ (denoted by $\text{orderedInsert}(\le, r_0, r)$). Suppose that for any indices $i < j$ of the list $r$, the condition $\neg(r_0 \le \cdot)$ is prefix-closed, meaning $\neg(r_0 \le r_j) \implies \neg(r_0 \le r_i)$. Then, for any index $n \in \text{Fin}(|r|)$, it holds that: $$\text{eraseIdx}(\text{orderedInsert}(\le, r_0, r), \phi(n+1)) = \text{orderedInsert}(\le, r_0, \text{eraseIdx}(r, n))$$ where $n+1$ is the successor index in $\text{Fin}(|r|+1)$ and $\text{eraseIdx}(l, k)$ denotes the removal of the element at index $k$ from list $l$.

Let $I$ be a type with a decidable binary relation $\le$, and $f : I \to \text{Type}$ be a type family. Let $l$ be a list of dependent pairs $\langle j, x \rangle$ where $j \in I$ and $x \in f(j)$, and let $\text{pr}_1$ denote the projection map $\langle j, x \rangle \mapsto j$. For any $i \in I$ and $a \in f(i)$, let $\le_\Sigma$ be the relation on the sigma type defined by the first components, i.e., $\langle j_1, x_1 \rangle \le_\Sigma \langle j_2, x_2 \rangle$ if and only if $j_1 \le j_2$. The index equivalence $\phi_\Sigma = \text{orderedInsertEquiv}(\le_\Sigma, l, \langle i, a \rangle)$, which maps indices of the prepended list $\langle i, a \rangle :: l$ to the indices of the list resulting from the ordered insertion of $\langle i, a \rangle$ into $l$, is equal to the index equivalence $\phi = \text{orderedInsertEquiv}(\le, \text{map}(\text{pr}_1, l), i)$ of the projected list. This equality holds identifying the respective index sets through their canonical isomorphisms.

Let $I$ be a type with a decidable binary relation $\le$. For any list $r$ of elements in $I$ and any element $r_0 \in I$, the list resulting from the ordered insertion of $r_0$ into $r$ is identical to the list obtained by inserting $r_0$ at the specific index $p = \text{orderedInsertPos}(\le, r, r_0)$ using the standard index-based insertion operation. Mathematically, this is expressed as: $$\text{orderedInsert}(\le, r_0, r) = \text{insertIdx}(r, p, r_0)$$ where $p$ is the index where $r_0$ is placed according to the ordering rule.