PhyslibSearch

theorem

Mapping a function over a list commutes with element insertion: $(r.\text{insertIdx}(i, r_0)).\text{map}(f) = (r.\text{map}(f)).\text{insertIdx}(i, f(r_0))$

Let $I$ and $J$ be types and $f: I \to J$ be a function. For any index $i \in \mathbb{N}$ , any list $r$ of elements in $I$ , and any element $r_0 \in I$ , the list obtained by inserting $r_0$ into $r$ at index $i$ and then applying $f$ to each element of the resulting list is equal to the list obtained by applying $f$ to each element of $r$ and then inserting $f(r_0)$ at index $i$ . That is, $(\text{insertIdx}(r, i, r_0)).\text{map}(f) = \text{insertIdx}(r.\text{map}(f), i, f(r_0))$

theorem

Erasing an element preserves the pairwise property of a list

#eraseIdx_sorted

Let $I$ be a type and $\le$ be a binary relation on $I$ . For any list $r$ of elements in $I$ and any index $n \in \mathbb{N}$ , if $r$ satisfies the pairwise relation $\le$ (meaning $\le$ holds for all pairs of elements in the list in their original order), then the list obtained by erasing the element at index $n$ also satisfies the pairwise relation $\le$ .

theorem

$i \in l.\text{eraseIdx } n \iff i \in l \land i \neq l[n]$ for lists with no duplicates

#mem_eraseIdx_nodup

Let $l$ be a list of elements of type $I$ and $n$ be a natural number representing an index such that $n < \text{length}(l)$ . If $l$ contains no duplicate elements ( $\text{Nodup } l$ ), then for any element $i \in I$ , $i$ is a member of the list obtained by erasing the element at index $n$ (denoted $l.\text{eraseIdx } n$ ) if and only if $i$ is a member of the original list $l$ and $i$ is not equal to the element of $l$ at index $n$ (denoted $l[n]$ ).

theorem

$\text{insertIdx}(r, n, i) = \text{take}(n, r) \mathbin{+\mkern-10mu+} [i] \mathbin{+\mkern-10mu+} \text{drop}(n, r)$

#insertIdx_eq_take_drop

Let $r$ be a list of elements of type $I$ and $i$ be an element of type $I$ . For any index $n$ such that $0 \le n \le \text{length}(r)$ , the list obtained by inserting $i$ into $r$ at position $n$ is equal to the concatenation of the first $n$ elements of $r$ , the element $i$ , and the remaining elements of $r$ starting from index $n$ . Mathematically, this is expressed as: $\text{insertIdx}(r, n, i) = \text{take}(n, r) \mathbin{+\mkern-10mu+} (i :: \text{drop}(n, r))$ where $\text{take}(n, r)$ is the prefix of $r$ of length $n$ , and $\text{drop}(n, r)$ is the suffix of $r$ starting after the first $n$ elements.

theorem

$\text{length}(\text{insertIdx}(r, n, i)) = \text{length}(r) + 1$

#insertIdx_length_fin

Let $r$ be a list of elements of type $I$ and $i \in I$ be an element. For any index $n$ in the range $0 \le n \le \text{length}(r)$ , the length of the list obtained by inserting $i$ into $r$ at position $n$ is equal to $\text{length}(r) + 1$ .

theorem

$(r.\text{insertIdx}(k, i))[k.\text{succAbove}(m)] = r[m]$

#insertIdx_getElem_fin

Let $r$ be a list of elements of type $I$ , $i \in I$ be an element, $k \in \{0, \dots, |r|\}$ be an insertion index, and $m \in \{0, \dots, |r|-1\}$ be an index. Let $r'$ be the list obtained by inserting $i$ into $r$ at index $k$ (i.e., `List.insertIdx r k i`). Then the element at position $m$ in the original list $r$ is equal to the element at the shifted index $j$ in $r'$ , where $j = k.\text{succAbove}(m)$ . The mapping $k.\text{succAbove}(m)$ is defined such that $j = m$ if $m < k$ and $j = m + 1$ if $m \geq k$ .

theorem

Inserting $r[k]$ at index $k$ after erasing it restores $r$

#insertIdx_eraseIdx_fin

For any list $r$ and any valid index $k$ such that $0 \le k < \text{length}(r)$ , inserting the original element $r[k]$ at index $k$ into the list formed by erasing the element at index $k$ from $r$ results in the original list $r$ .

theorem

$\text{insertIdx} (\phi_s \mathbin{+\!+} \phi_s', |\phi_s|, \phi) = \phi_s \mathbin{+\!+} (\phi :: \phi_s')$

#insertIdx_length_fst_append

For any type $I$ , an element $\phi \in I$ , and two lists $\phi_s, \phi_s'$ of elements of $I$ , the result of inserting $\phi$ into the concatenated list $\phi_s \mathbin{+\!+} \phi_s'$ at the index equal to the length of $\phi_s$ is equal to $\phi_s \mathbin{+\!+} (\phi :: \phi_s')$ .

theorem

$r.\text{get} = (\text{List.insertIdx } r \ k \ i).\text{get} \circ k.\text{succAbove}$

#get_eq_insertIdx_succAbove

Let $r$ be a list of elements of type $I$ and $i \in I$ be an element. For any insertion index $k \in \{0, \dots, |r|\}$ , the function that retrieves the $m$ -th element of $r$ (for $0 \le m < |r|$ ) is equal to the composition of the index mapping $k.\text{succAbove}$ and the retrieval function of the list obtained by inserting $i$ into $r$ at index $k$ . In other words, for any $m \in \{0, \dots, |r|-1\}$ : $r[m] = (\text{List.insertIdx } r \ k \ i)[k.\text{succAbove}(m)]$ where the mapping $k.\text{succAbove}(m)$ is defined as $m$ if $m < k$ and $m + 1$ if $m \ge k$ .

theorem

$\text{List.take } n (\text{List.insertIdx } r \, n \, i) = \text{List.take } n \, r$

#take_insert_same

For any list $r$ of elements of type $I$ , an element $i \in I$ , and a natural number $n$ , the first $n$ elements of the list obtained by inserting $i$ into $r$ at index $n$ is equal to the first $n$ elements of the original list $r$ : $\text{List.take } n (\text{List.insertIdx } r \, n \, i) = \text{List.take } n \, r$

theorem

$\text{take } n (\text{eraseIdx } r \ n) = \text{take } n \ r$

#take_eraseIdx_same

For any list $r$ of elements of type $I$ and any natural number $n$ , taking the first $n$ elements of the list obtained by erasing the element at index $n$ from $r$ is equal to taking the first $n$ elements of the original list $r$ . In symbols, $\text{take } n (\text{eraseIdx } r \ n) = \text{take } n \ r$ .

theorem

$r[n] :: \text{drop}(n, \text{eraseIdx}(r, n)) = \text{drop}(n, r)$

#drop_eraseIdx_succ

For any list $r$ of elements of type $I$ and any natural number $n$ such that $n < \text{length}(r)$ , it holds that: $r[n] :: \text{drop}(n, \text{eraseIdx}(r, n)) = \text{drop}(n, r)$ where $r[n]$ denotes the $n$ -th element of the list, $\text{eraseIdx}(r, n)$ is the list $r$ with the element at index $n$ removed, $\text{drop}(n, r)$ is the sublist of $r$ starting from index $n$ , and $::$ denotes the operation of prepending an element to a list.

theorem

Taking $n$ elements is invariant under insertion at index $m > n$

#take_insert_gt

For any type $I$ , an element $i \in I$ , natural numbers $n$ and $m$ such that $n < m$ , and a list $r$ of elements from $I$ , the first $n$ elements of the list obtained by inserting $i$ into $r$ at index $m$ are the same as the first $n$ elements of the original list $r$ .

theorem

Taking $n + 1$ elements after insertion at index $m \leq n$ is a permutation of $i$ prepended to taking $n$ elements

#take_insert_let

Let $I$ be a type, $i$ an element of $I$ , and $r$ a list of elements of $I$ . For any natural numbers $n$ and $m$ such that $m \leq n$ and $m$ is less than or equal to the length of $r$ , the first $n + 1$ elements of the list obtained by inserting $i$ into $r$ at index $m$ is a permutation of the list formed by prepending $i$ to the first $n$ elements of $r$ .

Physlib.Mathematics.List.InsertIdx

Mapping a function over a list commutes with element insertion: (r.insertIdx(i,r0)).map(f)=(r.map(f)).insertIdx(i,f(r0))(r.\text{insertIdx}(i, r_0)).\text{map}(f) = (r.\text{map}(f)).\text{insertIdx}(i, f(r_0))(r.insertIdx(i,r0​)).map(f)=(r.map(f)).insertIdx(i,f(r0​))

Erasing an element preserves the pairwise property of a list

i∈l.eraseIdx n ⟺ i∈l∧i≠l[n]i \in l.\text{eraseIdx } n \iff i \in l \land i \neq l[n]i∈l.eraseIdx n⟺i∈l∧i=l[n] for lists with no duplicates

insertIdx(r,n,i)=take(n,r)++[i]++drop(n,r)\text{insertIdx}(r, n, i) = \text{take}(n, r) \mathbin{+\mkern-10mu+} [i] \mathbin{+\mkern-10mu+} \text{drop}(n, r)insertIdx(r,n,i)=take(n,r)++[i]++drop(n,r)

length(insertIdx(r,n,i))=length(r)+1\text{length}(\text{insertIdx}(r, n, i)) = \text{length}(r) + 1length(insertIdx(r,n,i))=length(r)+1

(r.insertIdx(k,i))[k.succAbove(m)]=r[m](r.\text{insertIdx}(k, i))[k.\text{succAbove}(m)] = r[m](r.insertIdx(k,i))[k.succAbove(m)]=r[m]

Inserting r[k]r[k]r[k] at index kkk after erasing it restores rrr

insertIdx(ϕs+ ⁣+ϕs′,∣ϕs∣,ϕ)=ϕs+ ⁣+(ϕ::ϕs′)\text{insertIdx} (\phi_s \mathbin{+\!+} \phi_s', |\phi_s|, \phi) = \phi_s \mathbin{+\!+} (\phi :: \phi_s')insertIdx(ϕs​++ϕs′​,∣ϕs​∣,ϕ)=ϕs​++(ϕ::ϕs′​)

r.get=(List.insertIdx r k i).get∘k.succAbover.\text{get} = (\text{List.insertIdx } r \ k \ i).\text{get} \circ k.\text{succAbove}r.get=(List.insertIdx r k i).get∘k.succAbove

List.take n(List.insertIdx r n i)=List.take n r\text{List.take } n (\text{List.insertIdx } r \, n \, i) = \text{List.take } n \, rList.take n(List.insertIdx rni)=List.take nr

take n(eraseIdx r n)=take n r\text{take } n (\text{eraseIdx } r \ n) = \text{take } n \ rtake n(eraseIdx r n)=take n r

r[n]::drop(n,eraseIdx(r,n))=drop(n,r)r[n] :: \text{drop}(n, \text{eraseIdx}(r, n)) = \text{drop}(n, r)r[n]::drop(n,eraseIdx(r,n))=drop(n,r)

Taking nnn elements is invariant under insertion at index m>nm > nm>n

Taking n+1n + 1n+1 elements after insertion at index m≤nm \leq nm≤n is a permutation of iii prepended to taking nnn elements

Mapping a function over a list commutes with element insertion: $(r.\text{insertIdx}(i, r_0)).\text{map}(f) = (r.\text{map}(f)).\text{insertIdx}(i, f(r_0))$

$i \in l.\text{eraseIdx } n \iff i \in l \land i \neq l[n]$ for lists with no duplicates

$\text{insertIdx}(r, n, i) = \text{take}(n, r) \mathbin{+\mkern-10mu+} [i] \mathbin{+\mkern-10mu+} \text{drop}(n, r)$

$\text{length}(\text{insertIdx}(r, n, i)) = \text{length}(r) + 1$

$(r.\text{insertIdx}(k, i))[k.\text{succAbove}(m)] = r[m]$

Inserting $r[k]$ at index $k$ after erasing it restores $r$

$\text{insertIdx} (\phi_s \mathbin{+\!+} \phi_s', |\phi_s|, \phi) = \phi_s \mathbin{+\!+} (\phi :: \phi_s')$

$r.\text{get} = (\text{List.insertIdx } r \ k \ i).\text{get} \circ k.\text{succAbove}$

$\text{List.take } n (\text{List.insertIdx } r \, n \, i) = \text{List.take } n \, r$

$\text{take } n (\text{eraseIdx } r \ n) = \text{take } n \ r$

$r[n] :: \text{drop}(n, \text{eraseIdx}(r, n)) = \text{drop}(n, r)$

Taking $n$ elements is invariant under insertion at index $m > n$

Taking $n + 1$ elements after insertion at index $m \leq n$ is a permutation of $i$ prepended to taking $n$ elements