Module docstring
{"### Lemmas about List.toArray.
We prefer to pull List.toArray outwards past Array operations.
"}
Array.toList_set
theorem
(xs : Array α) (i x h) : (xs.set i x).toList = xs.toList.set i x
Informal description
For any array `xs` of type `α`, index `i`, element `x`, and proof `h` that `i` is within bounds, converting the array `xs.set i x` to a list is equal to replacing the `i`-th element of the list `xs.toList` with `x`.
Array.swap_def
theorem
(xs : Array α) (i j : Nat) (hi hj) : xs.swap i j hi hj = (xs.set i xs[j]).set j xs[i] (by simpa using hj)
Informal description
For any array `xs` of type `Array α`, indices `i` and `j` of type `Nat`, and proofs `hi` and `hj` that `i` and `j` are within bounds, swapping elements at positions `i` and `j` in `xs` is equivalent to first setting the `i`-th element to `xs[j]` and then setting the `j`-th element to `xs[i]`.
Array.toList_swap
theorem
(xs : Array α) (i j : Nat) (hi hj) : (xs.swap i j hi hj).toList = (xs.toList.set i xs[j]).set j xs[i]
Informal description
For any array `xs` of type `Array α`, indices `i` and `j` of type `Nat`, and proofs `hi` and `hj` that `i` and `j` are within bounds, converting the swapped array `xs.swap i j hi hj` to a list is equal to first replacing the `i`-th element of `xs.toList` with `xs[j]` and then replacing the `j`-th element with `xs[i]`.
List.toArray_inj
theorem
{as bs : List α} (h : as.toArray = bs.toArray) : as = bs
Informal description
For any two lists `as` and `bs` of elements of type `α`, if their array conversions are equal (i.e., `as.toArray = bs.toArray`), then the original lists are equal (`as = bs`).
List.toArray_eq_iff
theorem
{as : List α} {bs : Array α} : as.toArray = bs ↔ as = bs.toList
Full source
theorem toArray_eq_iff {as : List α} {bs : Array α} : as.toArray = bs ↔ as = bs.toList := by
cases bs
simpInformal description
For any list `as` of elements of type `alpha` and any array `bs` of the same type, the conversion of `as` to an array equals `bs` if and only if `as` equals the conversion of `bs` to a list. In other words, $as.\text{toArray} = bs \leftrightarrow as = bs.\text{toList}$.
List.size_toArrayAux
theorem
{as : List α} {xs : Array α} : (as.toArrayAux xs).size = xs.size + as.length
Full source
@[simp] theorem size_toArrayAux {as : List α} {xs : Array α} :
(as.toArrayAux xs).size = xs.size + as.length := by
simp [size]Informal description
For any list `as` of elements of type `α` and any array `xs` of elements of type `α`, the size of the array obtained by converting `as` to an array while appending to `xs` is equal to the sum of the size of `xs` and the length of `as`. That is, $\text{size}(\text{toArrayAux}\ as\ xs) = \text{size}(xs) + \text{length}(as)$.
List.toArray_cons
theorem
(a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArray
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, converting the list $a :: l$ to an array is equal to concatenating the singleton array $[a]$ with the array obtained by converting $l$. That is, $(a :: l).\text{toArray} = [a] \mathbin{+\kern-1.0ex+} l.\text{toArray}$.
List.push_toArray
theorem
(l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, pushing $a$ to the array obtained from converting $l$ is equal to converting the list obtained by appending $[a]$ to $l$. In other words, $l.\mathtt{toArray}.\mathtt{push}\ a = (l \mathbin{+\kern-1.0ex+} [a]).\mathtt{toArray}$.
List.push_toArray_fun
theorem
(l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray
Informal description
For any list $l$ of elements of type $\alpha$, the function that pushes an element $a$ to the array obtained from converting $l$ is equal to the function that converts the list obtained by appending $[a]$ to $l$. In other words, $(\mathtt{toArray}\ l).\mathtt{push} = \lambda a, \mathtt{toArray}(l \mathbin{+\kern-1.0ex+} [a])$.
List.isEmpty_toArray
theorem
(l : List α) : l.toArray.isEmpty = l.isEmpty
Full source
@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
cases l <;> simp [Array.isEmpty]Informal description
For any list $l$ of elements of type $\alpha$, the array obtained by converting $l$ to an array is empty if and only if $l$ is empty. In other words, $\text{isEmpty}(l.\text{toArray}) = \text{isEmpty}(l)$.
List.toArray_singleton
theorem
(a : α) : (List.singleton a).toArray = Array.singleton a
Full source
@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rflInformal description
For any element $a$ of type $\alpha$, converting the singleton list $[a]$ to an array yields the same result as constructing a singleton array directly, i.e., $\text{toArray}([a]) = \#[a]$.
List.back!_toArray
theorem
[Inhabited α] (l : List α) : l.toArray.back! = l.getLast!
Full source
@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
simp only [back!, size_toArray, getElem!_toArray, getLast!_eq_getElem!]Informal description
For any list $l$ of elements of type $\alpha$ (where $\alpha$ is an inhabited type), the last element of the array obtained by converting $l$ to an array (accessed with panic if empty) equals the last element of $l$ (accessed with panic if empty). That is, $\text{toArray}(l).\text{back!} = l.\text{getLast!}$.
List.back?_toArray
theorem
(l : List α) : l.toArray.back? = l.getLast?
Full source
@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
simp [back?, List.getLast?_eq_getElem?]Informal description
For any list $l$ of elements of type $\alpha$, the optional last element of the array obtained by converting $l$ to an array is equal to the optional last element of $l$, i.e., $\text{toArray}(l).\text{back?} = l.\text{getLast?}$.
List.back_toArray
theorem
(l : List α) (h) : l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h)
Full source
@[simp] theorem back_toArray (l : List α) (h) :
l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h) := by
simp [back, List.getLast_eq_getElem]Informal description
For any non-empty list $l$ of elements of type $\alpha$, the last element of the array obtained by converting $l$ to an array is equal to the last element of $l$.
Array.getLast!_toList
theorem
[Inhabited α] (xs : Array α) : xs.toList.getLast! = xs.back!
Informal description
For any array `xs` of elements of type `α` (where `α` is an inhabited type), the last element of the list obtained by converting `xs` to a list (accessed with panic if empty) equals the last element of `xs` (accessed with panic if empty). That is, $\text{toList}(xs).\text{getLast!} = xs.\text{back!}$.
Array.getLast?_toList
theorem
(xs : Array α) : xs.toList.getLast? = xs.back?
Full source
@[simp] theorem _root_.Array.getLast?_toList (xs : Array α) :
xs.toList.getLast? = xs.back? := by
rcases xs with ⟨xs⟩
simpInformal description
For any array `xs` of elements of type `α`, the optional last element of the list obtained by converting `xs` to a list is equal to the optional last element of `xs`. In symbols:
$$\text{toList}(xs).\text{getLast?} = xs.\text{back?}$$
Array.getLast_toList
theorem
(xs : Array α) (h) : xs.toList.getLast h = xs.back (by simpa [ne_nil_iff_length_pos] using h)
Full source
@[simp] theorem _root_.Array.getLast_toList (xs : Array α) (h) :
xs.toList.getLast h = xs.back (by simpa [ne_nil_iff_length_pos] using h) := by
rcases xs with ⟨xs⟩
simpInformal description
For any non-empty array `xs` of elements of type `α`, the last element of the list obtained by converting `xs` to a list is equal to the last element of `xs`.
List.set_toArray
theorem
(l : List α) (i : Nat) (a : α) (h : i < l.length) : (l.toArray.set i a) = (l.set i a).toArray
Informal description
For any list $l$ of elements of type $\alpha$, natural number index $i$, and element $a$ of type $\alpha$, if $i$ is a valid index for $l$ (i.e., $i < \text{length}(l)$), then setting the $i$-th element of the array conversion of $l$ to $a$ is equivalent to first setting the $i$-th element of $l$ to $a$ and then converting the resulting list to an array. In symbols:
$$(l.\text{toArray}).\text{set}(i, a) = (l.\text{set}(i, a)).\text{toArray}$$
List.forIn'_loop_toArray
theorem
[Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat) (h : i ≤ l.length) (b : β) :
Array.forIn'.loop l.toArray f i h b =
forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b)
Full source
@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
(h : i ≤ l.length) (b : β) :
Array.forIn'.loop l.toArray f i h b =
forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
induction i generalizing l b with
| zero =>
simp [Array.forIn'.loop]
| succ i ih =>
simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
have t : drop (l.length - (i + 1)) l = l[l.length - i - 1]l[l.length - i - 1] :: drop (l.length - i) l := by
simp only [Nat.sub_add_eq]
rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
simp only [Option.toList_some, singleton_append]
simp [t]
have t : l.length - 1 - i = l.length - i - 1 := by omega
simp only [t]
congrInformal description
Let $m$ be a monad, $l$ a list of elements of type $\alpha$, and $f$ a function that takes an element $a \in l.\text{toArray}$, a state $\beta$, and returns a monadic step. For any natural number $i$ such that $i \leq \text{length}(l)$ and any initial state $b \in \beta$, the monadic loop iteration over the array $l.\text{toArray}$ with function $f$ and index $i$ is equal to the iteration over the suffix of $l$ obtained by dropping the first $\text{length}(l) - i$ elements, with a modified function that adjusts the membership proof.
List.forIn'_toArray
theorem
[Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b)
Full source
@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
change Array.forIn' _ _ _ = List.forIn' _ _ _
rw [Array.forIn', forIn'_loop_toArray]
simpInformal description
For any monad $m$, list $l$ of elements of type $\alpha$, initial state $b$ of type $\beta$, and function $f : \alpha \to (a \in l.\text{toArray}) \to \beta \to m (\text{ForInStep}\ \beta)$, the monadic iteration over the array conversion of $l$ is equal to the monadic iteration over $l$ itself with a modified function that adjusts the membership proof. That is,
$$\text{forIn'}\ l.\text{toArray}\ b\ f = \text{forIn'}\ l\ b\ (\lambda a\ m\ b, f\ a\ (\text{mem\_toArray.mpr}\ m)\ b).$$
List.forIn_toArray
theorem
[Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : forIn l.toArray b f = forIn l b f
Full source
@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
forIn l.toArray b f = forIn l b f := by
simpa using forIn'_toArray l b fun a m b => f a bInformal description
For any monad $m$, list $l$ of elements of type $\alpha$, initial state $b$ of type $\beta$, and function $f : \alpha \to \beta \to m (\text{ForInStep}\ \beta)$, the monadic iteration over the array conversion of $l$ is equal to the monadic iteration over $l$ itself. That is,
$$\text{forIn}\ l.\text{toArray}\ b\ f = \text{forIn}\ l\ b\ f.$$
List.foldrM_toArray
theorem
[Monad m] (f : α → β → m β) (init : β) (l : List α) : l.toArray.foldrM f init = l.foldrM f init
Full source
theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
l.toArray.foldrM f init = l.foldrM f init := by
rw [foldrM_eq_reverse_foldlM_toList]
simpInformal description
For any monad $m$, function $f : \alpha \to \beta \to m \beta$, initial value $init : \beta$, and list $l : \text{List}\ \alpha$, the monadic right fold of the array conversion of $l$ equals the monadic right fold of $l$ itself. That is,
$$\text{foldrM}\ f\ init\ (l.\text{toArray}) = \text{foldrM}\ f\ init\ l.$$
List.foldlM_toArray
theorem
[Monad m] (f : β → α → m β) (init : β) (l : List α) : l.toArray.foldlM f init = l.foldlM f init
Full source
theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
l.toArray.foldlM f init = l.foldlM f init := by
rw [foldlM_toList]Informal description
For any monad $m$, function $f : \beta \to \alpha \to m \beta$, initial value $init : \beta$, and list $l : \text{List}\ \alpha$, the monadic left fold operation applied to $f$ and $init$ over the array conversion of $l$ is equal to the monadic left fold operation applied to $f$ and $init$ over $l$ itself. That is,
$$\text{foldlM}\ f\ init\ (l.\text{toArray}) = \text{foldlM}\ f\ init\ l.$$
List.foldr_toArray
theorem
(f : α → β → β) (init : β) (l : List α) : l.toArray.foldr f init = l.foldr f init
Full source
theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
l.toArray.foldr f init = l.foldr f init := by
rw [foldr_toList]Informal description
For any function $f : \alpha \to \beta \to \beta$, initial value $init : \beta$, and list $l : \text{List } \alpha$, the right fold of the array obtained from converting $l$ to an array is equal to the right fold of $l$ itself. That is,
$$\text{foldr } f \text{ init } (l.\text{toArray}) = \text{foldr } f \text{ init } l.$$
List.foldl_toArray
theorem
(f : β → α → β) (init : β) (l : List α) : l.toArray.foldl f init = l.foldl f init
Full source
theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
l.toArray.foldl f init = l.foldl f init := by
rw [foldl_toList]Informal description
For any binary operation $f : \beta \to \alpha \to \beta$, initial value $init \in \beta$, and list $l$ of elements of type $\alpha$, the left fold of $f$ over the array obtained by converting $l$ to an array is equal to the left fold of $f$ over $l$ itself. That is,
$$\text{foldl}\ f\ init\ (l.\text{toArray}) = \text{foldl}\ f\ init\ l.$$
List.foldrM_toArray'
theorem
[Monad m] (f : α → β → m β) (init : β) (l : List α) (h : start = l.toArray.size) :
l.toArray.foldrM f init start 0 = l.foldrM f init
Full source
/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
(h : start = l.toArray.size) :
l.toArray.foldrM f init start 0 = l.foldrM f init := by
subst h
rw [foldrM_eq_reverse_foldlM_toList]
simpInformal description
Let $m$ be a monad, $f : \alpha \to \beta \to m \beta$ a function, $init$ an element of type $\beta$, and $l$ a list of type $\alpha$. If $start$ equals the size of the array obtained by converting $l$ to an array, then the monadic right fold of this array starting at index $start$ with function $f$ and initial value $init$ is equal to the monadic right fold of the original list $l$ with the same function and initial value.
List.foldlM_toArray'
theorem
[Monad m] (f : β → α → m β) (init : β) (l : List α) (h : stop = l.toArray.size) :
l.toArray.foldlM f init 0 stop = l.foldlM f init
Full source
/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/
@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
(h : stop = l.toArray.size) :
l.toArray.foldlM f init 0 stop = l.foldlM f init := by
subst h
rw [foldlM_toList]Informal description
Let $m$ be a monad, $f : \beta \to \alpha \to m \beta$ a function, $init$ an element of type $\beta$, and $l$ a list of type $\alpha$. If $stop$ equals the size of the array obtained by converting $l$ to an array, then the monadic left fold of this array from index $0$ to $stop$ with function $f$ and initial value $init$ is equal to the monadic left fold of the original list $l$ with the same function and initial value.
List.forM_toArray'
theorem
[Monad m] (l : List α) (f : α → m PUnit) (h : stop = l.toArray.size) : (l.toArray.forM f 0 stop) = l.forM f
Full source
/-- Variant of `forM_toArray` with a side condition for the `stop` argument. -/
@[simp] theorem forM_toArray' [Monad m] (l : List α) (f : α → m PUnit) (h : stop = l.toArray.size) :
(l.toArray.forM f 0 stop) = l.forM f := by
subst h
rw [Array.forM]
simp only [size_toArray, foldlM_toArray']
induction l <;> simp_allInformal description
Let $m$ be a monad, $f : \alpha \to m \text{PUnit}$ a function, and $l$ a list of elements of type $\alpha$. If $stop$ equals the size of the array obtained by converting $l$ to an array, then applying the monadic operation $f$ to each element of the array from index $0$ to $stop$ is equivalent to applying $f$ to each element of the original list $l$.
List.forM_toArray
theorem
[Monad m] (l : List α) (f : α → m PUnit) : (forM l.toArray f) = l.forM f
Full source
@[simp]
theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
(forM l.toArray f) = l.forM f :=
forM_toArray' l f rflInformal description
For any monad $m$ and function $f : \alpha \to m \text{PUnit}$, applying $f$ to each element of an array obtained by converting a list $l$ of type $\text{List } \alpha$ is equivalent to applying $f$ to each element of $l$ directly. That is, $\text{forM } (l.\text{toArray}) f = l.\text{forM } f$.
List.foldr_toArray'
theorem
(f : α → β → β) (init : β) (l : List α) (h : start = l.toArray.size) : l.toArray.foldr f init start 0 = l.foldr f init
Full source
/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
(h : start = l.toArray.size) :
l.toArray.foldr f init start 0 = l.foldr f init := by
subst h
rw [foldr_toList]Informal description
For any function $f : \alpha \to \beta \to \beta$, initial value $init : \beta$, and list $l : \text{List } \alpha$, if $start$ equals the size of the array obtained by converting $l$ to an array, then the right fold of the array with function $f$, initial value $init$, starting index $start$, and ending index $0$ is equal to the right fold of the list $l$ with the same function and initial value. That is, $l.\text{toArray}.\text{foldr } f \text{ init start } 0 = l.\text{foldr } f \text{ init}$.
List.foldl_toArray'
theorem
(f : β → α → β) (init : β) (l : List α) (h : stop = l.toArray.size) : l.toArray.foldl f init 0 stop = l.foldl f init
Full source
/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
(h : stop = l.toArray.size) :
l.toArray.foldl f init 0 stop = l.foldl f init := by
subst h
rw [foldl_toList]Informal description
For any binary operation $f : \beta \to \alpha \to \beta$, initial value $init : \beta$, and list $l$ of elements of type $\alpha$, if $stop$ is equal to the size of the array obtained by converting $l$ to an array, then the left fold of $f$ over the array from index $0$ to $stop$ with initial value $init$ is equal to the left fold of $f$ over the list $l$ with the same initial value.
List.sum_toArray
theorem
[Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum
Informal description
For any type $\alpha$ equipped with an addition operation and a zero element, and for any list $l$ of elements of type $\alpha$, the sum of the elements in the array obtained by converting $l$ to an array is equal to the sum of the elements in $l$. That is, $\text{toArray}(l).\text{sum} = l.\text{sum}$.
List.append_toArray
theorem
(l₁ l₂ : List α) : l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the concatenation of their array conversions equals the array conversion of their concatenation. That is, $\text{toArray}(l_1) +\!\!+ \text{toArray}(l_2) = \text{toArray}(l_1 +\!\!+ l_2)$.
List.push_append_toArray
theorem
{as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a :: bs).toArray
Informal description
For any array `as` of elements of type `α`, any element `a` of type `α`, and any list `bs` of elements of type `α`, the concatenation of the array obtained by pushing `a` to `as` with the array conversion of `bs` is equal to the concatenation of `as` with the array conversion of the list `a :: bs`. That is, $\text{as.push}\ a \mathbin{+\kern-1.0ex+} \text{bs.toArray} = \text{as} \mathbin{+\kern-1.0ex+} (a :: \text{bs}).\text{toArray}$.
List.foldl_push
theorem
{l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray
Full source
@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
induction l generalizing as <;> simp [*]Informal description
For any list $l$ of elements of type $\alpha$ and any array $as$ of elements of type $\alpha$, the left fold of $l$ using the `Array.push` operation with initial value $as$ is equal to the concatenation of $as$ with the array conversion of $l$. That is, $\text{foldl}\ \text{Array.push}\ as\ l = as \mathbin{+\kern-1.0ex+} l.\text{toArray}$.
List.foldr_push
theorem
{l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray
Full source
@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
rw [foldr_eq_foldl_reverse, foldl_push]Informal description
For any list $l$ of elements of type $\alpha$ and any array $as$ of elements of type $\alpha$, the right fold of $l$ using the operation $\lambda a\ bs \mapsto \text{push}(bs, a)$ with initial value $as$ is equal to the concatenation of $as$ with the array conversion of the reversed list $l$. That is, $\text{foldr}\ (\lambda a\ bs \mapsto \text{push}(bs, a))\ as\ l = as \mathbin{+\kern-1.0ex+} l.\text{reverse}.\text{toArray}$.
List.findSomeM?_toArray
theorem
[Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : l.toArray.findSomeM? f = l.findSomeM? f
Full source
@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
l.toArray.findSomeM? f = l.findSomeM? f := by
rw [Array.findSomeM?]
simp only [bind_pure_comp, map_pure, forIn_toArray]
induction l with
| nil => simp
| cons a l ih =>
simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?]
congr
ext1 (_|_) <;> simp [ih]Informal description
For any monad $m$ that satisfies the monad laws, any function $f : \alpha \to m (\text{Option}\ \beta)$, and any list $l$ of elements of type $\alpha$, the monadic find-first-some operation on the array conversion of $l$ is equal to the same operation applied directly to $l$. That is,
$$\text{findSomeM?}\ (l.\text{toArray})\ f = \text{findSomeM?}\ l\ f.$$
List.findSomeRevM?_find_toArray
theorem
[Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) (i : Nat) (h) :
findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f
Full source
theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
(i : Nat) (h) :
findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by
induction i generalizing l with
| zero => simp [Array.findSomeRevM?.find.eq_def]
| succ i ih =>
rw [size_toArray] at h
rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
simp only [ih, reverse_append]
congr
ext1 (_|_) <;> simpInformal description
For any monad `m` satisfying the monad laws, any function `f : α → m (Option β)`, any list `l : List α`, any natural number index `i`, and a proof `h` that `i` is a valid index for `l.toArray`, the result of the reverse search operation `findSomeRevM?.find` applied to `f`, `l.toArray`, `i`, and `h` is equal to the reverse search operation `findSomeM?` applied to `f` and the reverse of the first `i` elements of `l`.
List.findSomeRevM?_toArray
theorem
[Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : l.toArray.findSomeRevM? f = l.reverse.findSomeM? f
Full source
theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by
simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]Informal description
For any monad `m` that satisfies the monad laws, any function `f : α → m (Option β)`, and any list `l : List α`, the result of applying the reverse monadic search operation `findSomeRevM?` to the array obtained from converting `l` is equal to applying the monadic search operation `findSomeM?` to the reverse of `l`. That is, `l.toArray.findSomeRevM? f = l.reverse.findSomeM? f`.
List.findRevM?_toArray
theorem
[Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : l.toArray.findRevM? f = l.reverse.findM? f
Full source
theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
l.toArray.findRevM? f = l.reverse.findM? f := by
rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]Informal description
For any monad `m` that satisfies the monad laws, any monadic predicate `f : α → m Bool`, and any list `l : List α`, the result of applying the reverse monadic find operation `findRevM?` to the array obtained from converting `l` is equal to applying the monadic find operation `findM?` to the reverse of `l`. That is, `l.toArray.findRevM? f = l.reverse.findM? f`.
List.findM?_toArray
theorem
[Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : l.toArray.findM? f = l.findM? f
Full source
@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
l.toArray.findM? f = l.findM? f := by
rw [Array.findM?]
simp only [bind_pure_comp, map_pure, forIn_toArray]
induction l with
| nil => simp
| cons a l ih =>
simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
congr
ext1 (_|_) <;> simp [ih]Informal description
For any monad $m$ that satisfies the monad laws, any monadic predicate $f : \alpha \to m \mathtt{Bool}$, and any list $l : \mathtt{List}\ \alpha$, the monadic find operation on the array obtained from converting $l$ is equal to the monadic find operation on $l$ itself. That is,
$$\mathtt{findM?}\ (l.\mathtt{toArray})\ f = \mathtt{findM?}\ l\ f.$$
List.findSome?_toArray
theorem
(f : α → Option β) (l : List α) : l.toArray.findSome? f = l.findSome? f
Full source
@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
l.toArray.findSome? f = l.findSome? f := by
rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]Informal description
For any function $f : \alpha \to \text{Option}\ \beta$ and any list $l$ of elements of type $\alpha$, the result of applying the `findSome?` operation to the array obtained from converting $l$ is equal to applying the same operation directly to $l$. That is,
$$\text{findSome?}\ (l.\text{toArray})\ f = \text{findSome?}\ l\ f.$$
List.find?_toArray
theorem
(f : α → Bool) (l : List α) : l.toArray.find? f = l.find? f
Full source
@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
l.toArray.find? f = l.find? f := by
rw [Array.find?]
simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
induction l with
| nil => simp
| cons a l ih =>
simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
by_cases f a <;> simp_allInformal description
For any predicate $f : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the result of finding the first element satisfying $f$ in the array conversion of $l$ is equal to the result of finding the first element satisfying $f$ in $l$ itself. That is,
$$\text{find?}(f, l.\text{toArray}) = \text{find?}(f, l)$$
List.findFinIdx?_toArray
theorem
(p : α → Bool) (l : List α) : l.toArray.findFinIdx? p = l.findFinIdx? p
Full source
@[simp] theorem findFinIdx?_toArray (p : α → Bool) (l : List α) :
l.toArray.findFinIdx? p = l.findFinIdx? p := by
rw [Array.findFinIdx?, findFinIdx?, findFinIdx?_loop_toArray]
simpInformal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the result of finding the first index satisfying $p$ in the array conversion of $l$ is equal to the result of finding the first index satisfying $p$ in $l$ itself.
More precisely, let $\text{findFinIdx?}(p, a)$ denote the operation that finds the first index $i$ (as a bounded natural number) in array $a$ where $p(a[i])$ holds, or returns $\text{none}$ if no such index exists. Then:
$$\text{findFinIdx?}(p, l.\text{toArray}) = \text{findFinIdx?}(p, l)$$
List.findIdx?_toArray
theorem
(p : α → Bool) (l : List α) : l.toArray.findIdx? p = l.findIdx? p
Full source
@[simp] theorem findIdx?_toArray (p : α → Bool) (l : List α) :
l.toArray.findIdx? p = l.findIdx? p := by
rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]
simpInformal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the result of finding the first index satisfying $p$ in the array conversion of $l$ is equal to the result of finding the first index satisfying $p$ in $l$ itself.
More precisely, let $\text{findIdx?}(p, a)$ denote the operation that finds the first index $i$ (as a natural number) in array $a$ where $p(a[i])$ holds, or returns $\text{none}$ if no such index exists. Then:
$$\text{findIdx?}(p, l.\text{toArray}) = \text{findIdx?}(p, l)$$
List.finIdxOf?_toArray
theorem
[BEq α] (a : α) (l : List α) : l.toArray.finIdxOf? a = l.finIdxOf? a
Full source
@[simp] theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) :
l.toArray.finIdxOf? a = l.finIdxOf? a := by
rw [Array.finIdxOf?, finIdxOf?, findFinIdx?]
simp [idxAuxOf_toArray]Informal description
For any type $\alpha$ with a boolean equality relation and any element $a \in \alpha$, the first occurrence index of $a$ in the array obtained by converting a list $l$ to an array is equal to the first occurrence index of $a$ in the list $l$ itself. That is, $\text{finIdxOf?}(l.\text{toArray}, a) = \text{finIdxOf?}(l, a)$.
List.idxOf?_toArray
theorem
[BEq α] (a : α) (l : List α) : l.toArray.idxOf? a = l.idxOf? a
Full source
@[simp] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) :
l.toArray.idxOf? a = l.idxOf? a := by
rw [Array.idxOf?, idxOf?]
simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val]Informal description
For any type $\alpha$ with a boolean equality relation and any element $a \in \alpha$, the first occurrence index of $a$ in the array obtained by converting a list $l$ to an array is equal to the first occurrence index of $a$ in the list $l$ itself. That is, $\text{idxOf?}(l.\text{toArray}, a) = \text{idxOf?}(l, a)$.
List.findIdx_toArray
theorem
{as : List α} {p : α → Bool} : as.toArray.findIdx p = as.findIdx p
Full source
@[simp] theorem findIdx_toArray {as : List α} {p : α → Bool} :
as.toArray.findIdx p = as.findIdx p := by
rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?]Informal description
For any list `as` of elements of type `α` and any predicate `p : α → Bool`, the index of the first element in the array obtained by converting `as` to an array that satisfies `p` is equal to the index of the first element in `as` that satisfies `p`. That is, $\text{findIdx}(p, \text{as.toArray}) = \text{findIdx}(p, \text{as})$.
List.idxOf_toArray
theorem
[BEq α] {as : List α} {a : α} : as.toArray.idxOf a = as.idxOf a
Full source
@[simp] theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
as.toArray.idxOf a = as.idxOf a := by
rw [Array.idxOf, findIdx_toArray, idxOf]Informal description
For any type $\alpha$ with a boolean equality relation and any list `as` of elements of type $\alpha$, the first occurrence index of an element $a$ in the array obtained by converting `as` to an array is equal to the first occurrence index of $a$ in the list `as$. That is, $\text{idxOf}(a, \text{as.toArray}) = \text{idxOf}(a, \text{as})$.
List.isPrefixOfAux_toArray_succ
theorem
[BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i
Full source
theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
rw [Array.isPrefixOfAux]
conv => rhs; rw [Array.isPrefixOfAux]
simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail]
split <;> rename_i h₁ <;> split <;> rename_i h₂
· rw [isPrefixOfAux_toArray_succ]
· omega
· omega
· rflInformal description
For any type $\alpha$ with a boolean equality relation and any lists $l_1, l_2$ of elements of type $\alpha$ such that the length of $l_1$ is less than or equal to the length of $l_2$, and for any natural number index $i$, the prefix check function applied to the array conversions of $l_1$ and $l_2$ at index $i+1$ is equal to the prefix check function applied to the array conversions of the tails of $l_1$ and $l_2$ at index $i$.
List.isPrefixOfAux_toArray_succ'
theorem
[BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
Array.isPrefixOfAux (l₁.drop (i + 1)).toArray (l₂.drop (i + 1)).toArray (by simp; omega) 0
Full source
theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by
induction i generalizing l₁ l₂ with
| zero => simp [isPrefixOfAux_toArray_succ]
| succ i ih =>
rw [isPrefixOfAux_toArray_succ, ih]
simpInformal description
For any type $\alpha$ with a boolean equality relation and any lists $l_1, l_2$ of elements of type $\alpha$ such that the length of $l_1$ is less than or equal to the length of $l_2$, and for any natural number index $i$, the prefix check function applied to the array conversions of $l_1$ and $l_2$ at index $i+1$ is equal to the prefix check function applied to the array conversions of the lists obtained by dropping the first $i+1$ elements of $l_1$ and $l_2$ at index $0$.
List.isPrefixOfAux_toArray_zero
theorem
[BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 = l₁.isPrefixOf l₂
Full source
theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 =
l₁.isPrefixOf l₂ := by
rw [Array.isPrefixOfAux]
match l₁, l₂ with
| [], _ => rw [dif_neg] <;> simp
| _::_, [] => simp at hle
| a::l₁, b::l₂ =>
simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]Informal description
For any type $\alpha$ with a boolean equality relation and any lists $l_1, l_2$ of elements of type $\alpha$ such that the length of $l_1$ is less than or equal to the length of $l_2$, the prefix check function applied to the array conversions of $l_1$ and $l_2$ at index $0$ is equal to the result of the list prefix check between $l_1$ and $l_2$.
List.isPrefixOf_toArray
theorem
[BEq α] (l₁ l₂ : List α) : l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂
Full source
@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by
rw [Array.isPrefixOf]
split <;> rename_i h
· simp [isPrefixOfAux_toArray_zero]
· simp only [Bool.false_eq]
induction l₁ generalizing l₂ with
| nil => simp at h
| cons a l₁ ih =>
cases l₂ with
| nil => simp
| cons b l₂ =>
simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
intro w
rw [ih]
simp_allInformal description
For any type $\alpha$ with a boolean equality relation and any lists $l_1, l_2$ of elements of type $\alpha$, the boolean result of checking whether the array conversion of $l_1$ is a prefix of the array conversion of $l_2$ is equal to the boolean result of checking whether $l_1$ is a prefix of $l_2$.
List.zipWithAux_toArray_succ
theorem
(as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (xs : Array γ) :
zipWithAux as.toArray bs.toArray f (i + 1) xs = zipWithAux as.tail.toArray bs.tail.toArray f i xs
Full source
theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (xs : Array γ) :
zipWithAux as.toArray bs.toArray f (i + 1) xs = zipWithAux as.tail.toArray bs.tail.toArray f i xs := by
rw [zipWithAux]
conv => rhs; rw [zipWithAux]
simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]
split <;> rename_i h₁
· split <;> rename_i h₂
· rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ]
· rw [dif_pos (by omega)]
rw [dif_neg (by omega)]
· rw [dif_neg (by omega)]Informal description
For any lists `as : List α` and `bs : List β`, a function `f : α → β → γ`, a natural number index `i`, and an accumulator array `xs : Array γ`, the auxiliary zip operation satisfies:
\[
\text{zipWithAux}\ (\text{as.toArray})\ (\text{bs.toArray})\ f\ (i + 1)\ xs = \text{zipWithAux}\ (\text{as.tail.toArray})\ (\text{bs.tail.toArray})\ f\ i\ xs
\]
List.zipWithAux_toArray_succ'
theorem
(as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (xs : Array γ) :
zipWithAux as.toArray bs.toArray f (i + 1) xs = zipWithAux (as.drop (i + 1)).toArray (bs.drop (i + 1)).toArray f 0 xs
Full source
theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (xs : Array γ) :
zipWithAux as.toArray bs.toArray f (i + 1) xs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 xs := by
induction i generalizing as bs xs with
| zero => simp [zipWithAux_toArray_succ]
| succ i ih =>
rw [zipWithAux_toArray_succ, ih]
simpInformal description
For any lists `as : List α` and `bs : List β`, a function `f : α → β → γ`, a natural number index `i`, and an accumulator array `xs : Array γ`, the auxiliary zip operation satisfies:
\[
\text{zipWithAux}\ (\text{as.toArray})\ (\text{bs.toArray})\ f\ (i + 1)\ xs = \text{zipWithAux}\ (\text{as.drop}\ (i + 1).\text{toArray})\ (\text{bs.drop}\ (i + 1).\text{toArray})\ f\ 0\ xs
\]
List.zipWithAux_toArray_zero
theorem
(f : α → β → γ) (as : List α) (bs : List β) (xs : Array γ) :
zipWithAux as.toArray bs.toArray f 0 xs = xs ++ (List.zipWith f as bs).toArray
Full source
theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (xs : Array γ) :
zipWithAux as.toArray bs.toArray f 0 xs = xs ++ (List.zipWith f as bs).toArray := by
rw [Array.zipWithAux]
match as, bs with
| [], _ => simp
| _, [] => simp
| a :: as, b :: bs =>
simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]Informal description
For any function $f : \alpha \to \beta \to \gamma$, lists $as : \text{List } \alpha$ and $bs : \text{List } \beta$, and array $xs : \text{Array } \gamma$, the auxiliary zip operation satisfies:
\[
\text{zipWithAux}(as.\text{toArray}, bs.\text{toArray}, f, 0, xs) = xs \mathbin{+\kern-1.0ex+} (\text{List.zipWith } f \text{ } as \text{ } bs).\text{toArray}
\]
List.zipWith_toArray
theorem
(as : List α) (bs : List β) (f : α → β → γ) : Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray
Full source
@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray := by
rw [Array.zipWith]
simp [zipWithAux_toArray_zero]Informal description
For any lists $as$ of elements of type $\alpha$ and $bs$ of elements of type $\beta$, and any function $f : \alpha \to \beta \to \gamma$, the element-wise application of $f$ to the arrays obtained from $as$ and $bs$ equals the array obtained from the element-wise application of $f$ to $as$ and $bs$ as lists. That is,
\[
\text{Array.zipWith}\ f\ as.\text{toArray}\ bs.\text{toArray} = (\text{List.zipWith}\ f\ as\ bs).\text{toArray}.
\]
List.zip_toArray
theorem
(as : List α) (bs : List β) : Array.zip as.toArray bs.toArray = (List.zip as bs).toArray
Informal description
For any lists $as$ of elements of type $\alpha$ and $bs$ of elements of type $\beta$, the zipping of the arrays obtained from $as$ and $bs$ equals the array obtained from zipping $as$ and $bs$ as lists. That is,
\[
\text{Array.zip}(as.\text{toArray}, bs.\text{toArray}) = (\text{List.zip}(as, bs)).\text{toArray}.
\]
List.zipWithAll_go_toArray
theorem
(as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (xs : Array γ) :
zipWithAll.go f as.toArray bs.toArray i xs = xs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray
Full source
theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (xs : Array γ) :
zipWithAll.go f as.toArray bs.toArray i xs = xs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by
unfold zipWithAll.go
split <;> rename_i h
· rw [zipWithAll_go_toArray]
simp at h
simp only [getElem?_toArray, push_append_toArray]
if ha : i < as.length then
if hb : i < bs.length then
rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb]
simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons]
else
simp only [Nat.not_lt] at hb
rw [List.drop_eq_getElem_cons ha]
rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)]
simp only [zipWithAll_nil, map_drop, map_cons]
rw [getElem?_eq_getElem ha]
rw [getElem?_eq_none hb]
else
if hb : i < bs.length then
simp only [Nat.not_lt] at ha
rw [List.drop_eq_getElem_cons hb]
rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]
simp only [nil_zipWithAll, map_drop, map_cons]
rw [getElem?_eq_getElem hb]
rw [getElem?_eq_none ha]
else
omega
· simp only [size_toArray, Nat.not_lt] at h
rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)]
simp
termination_by max as.length bs.length - i
decreasing_by simp_wf; decreasing_trivial_pre_omegaInformal description
For any lists `as` and `bs` of elements of types `α` and `β` respectively, a function `f : Option α → Option β → γ`, a natural number `i`, and an array `xs : Array γ`, the result of applying the `zipWithAll.go` function to the arrays obtained from `as` and `bs` with starting index `i` and accumulator `xs` is equal to the concatenation of `xs` with the array obtained from applying `List.zipWithAll` to the suffixes of `as` and `bs` starting at index `i`.
In symbols:
$$\text{zipWithAll.go}\ f\ \text{as.toArray}\ \text{bs.toArray}\ i\ xs = xs \mathbin{+\!\!+} \text{List.zipWithAll}\ f\ (\text{as.drop}\ i)\ (\text{bs.drop}\ i).\text{toArray}$$
List.zipWithAll_toArray
theorem
(f : Option α → Option β → γ) (as : List α) (bs : List β) :
Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray
Full source
@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray := by
simp [Array.zipWithAll, zipWithAll_go_toArray]Informal description
For any function $f : \text{Option }\alpha \to \text{Option }\beta \to \gamma$ and any lists $as$ of type $\alpha$ and $bs$ of type $\beta$, the element-wise application of $f$ to the arrays obtained from $as$ and $bs$ equals the array obtained from the element-wise application of $f$ to $as$ and $bs$ as lists.
In symbols:
$$\text{Array.zipWithAll}\ f\ \text{as.toArray}\ \text{bs.toArray} = (\text{List.zipWithAll}\ f\ as\ bs).\text{toArray}$$
List.toArray_appendList
theorem
(l₁ l₂ : List α) : l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray
Full source
@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
apply ext'
simpInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the array obtained by converting $l_1$ to an array and then appending $l_2$ is equal to the array obtained by first concatenating $l_1$ and $l_2$ and then converting the result to an array. In symbols:
$$ \text{toArray}(l_1) \mathbin{+\!\!+} l_2 = \text{toArray}(l_1 \mathbin{+\!\!+} l_2) $$
List.pop_toArray
theorem
(l : List α) : l.toArray.pop = l.dropLast.toArray
Informal description
For any list $l$ of elements of type $\alpha$, the array obtained by first converting $l$ to an array and then removing its last element is equal to the array obtained by first removing the last element of $l$ and then converting the resulting list to an array. In symbols:
$$ \text{toArray}(l).\text{pop} = \text{toArray}(l.\text{dropLast}) $$
List.takeWhile_go_succ
theorem
(p : α → Bool) (a : α) (l : List α) (i : Nat) :
takeWhile.go p (a :: l).toArray (i + 1) r = takeWhile.go p l.toArray i r
Full source
theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
rw [takeWhile.go, takeWhile.go]
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right,
getElem_toArray, getElem_cons_succ]
split
rw [takeWhile_go_succ]
rflInformal description
For any predicate $p : \alpha \to \text{Bool}$, element $a : \alpha$, list $l : \text{List } \alpha$, and natural number index $i : \mathbb{N}$, the following equality holds between the `takeWhile.go` operations:
$$ \text{takeWhile.go } p \ (\text{toArray}(a :: l)) \ (i + 1) \ r = \text{takeWhile.go } p \ (\text{toArray}(l)) \ i \ r $$
where $r$ is an accumulator array.
List.takeWhile_go_toArray
theorem
(p : α → Bool) (l : List α) (i : Nat) : Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray
Full source
theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
induction l generalizing i r with
| nil => simp [takeWhile.go]
| cons a l ih =>
rw [takeWhile.go]
cases i with
| zero =>
simp [takeWhile_go_succ, ih, takeWhile_cons]
split <;> simp
| succ i =>
simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right,
getElem_toArray, getElem_cons_succ, drop_succ_cons]
split <;> rename_i h₁
· rw [takeWhile_go_succ, ih]
rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
split <;> simp_all
· simp_all [drop_eq_nil_of_le]Informal description
For any predicate $p : \alpha \to \text{Bool}$, list $l : \text{List } \alpha$, and natural number index $i : \mathbb{N}$, the auxiliary function `Array.takeWhile.go` applied to the array conversion of $l$ satisfies:
$$ \text{Array.takeWhile.go } p \ (\text{toArray}(l)) \ i \ r = r \mathbin{+\kern-1.0ex+} \text{toArray}(\text{takeWhile } p \ (\text{drop}(l, i))) $$
where $r$ is an accumulator array.
List.takeWhile_toArray
theorem
(p : α → Bool) (l : List α) : l.toArray.takeWhile p = (l.takeWhile p).toArray
Full source
@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
l.toArray.takeWhile p = (l.takeWhile p).toArray := by
simp [Array.takeWhile, takeWhile_go_toArray]Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the array obtained by first converting $l$ to an array and then taking the longest prefix of elements satisfying $p$ is equal to the array obtained by first taking the longest prefix of $l$ satisfying $p$ and then converting to an array.
In symbols:
$$\text{takeWhile}(p, \text{toArray}(l)) = \text{toArray}(\text{takeWhile}(p, l))$$
List.popWhile_toArray
theorem
(p : α → Bool) (l : List α) : l.toArray.popWhile p = (l.reverse.dropWhile p).reverse.toArray
Informal description
For any predicate $p$ on elements of type $\alpha$ and any list $l$ of elements of type $\alpha$, the array obtained by converting $l$ to an array and then removing the longest suffix of elements satisfying $p$ is equal to the array obtained by first reversing $l$, dropping the longest prefix of elements satisfying $p$, reversing back, and then converting to an array.
In symbols:
$$\text{toArray}(\text{popWhile}(p, \text{toArray}(l))) = \text{toArray}\left(\left(\text{dropWhile}(p, l^{\text{reverse}})\right)^{\text{reverse}}\right)$$
List.setIfInBounds_toArray
theorem
(l : List α) (i : Nat) (a : α) : l.toArray.setIfInBounds i a = (l.set i a).toArray
Full source
@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
l.toArray.setIfInBounds i a = (l.set i a).toArray := by
apply ext'
simp only [setIfInBounds]
split
· simp
· simp_all [List.set_eq_of_length_le]Informal description
For any list $l$ of elements of type $\alpha$, any natural number index $i$, and any element $a$ of type $\alpha$, the operation of converting $l$ to an array and then conditionally setting the $i$-th element to $a$ (if $i$ is within bounds) is equivalent to first setting the $i$-th element of $l$ to $a$ (if $i$ is within bounds) and then converting the resulting list to an array. In other words, $\text{toArray}(l).\text{setIfInBounds}(i, a) = \text{toArray}(l.\text{set}(i, a))$.
List.toArray_replicate
theorem
(n : Nat) (v : α) : (List.replicate n v).toArray = Array.replicate n v
Full source
@[simp] theorem toArray_replicate (n : Nat) (v : α) :
(List.replicate n v).toArray = Array.replicate n v := rflInformal description
For any natural number $n$ and any element $v$ of type $\alpha$, converting a list of $n$ copies of $v$ to an array is equal to creating an array directly with $n$ copies of $v$. That is, $\text{List.toArray}(\text{List.replicate}(n, v)) = \text{Array.replicate}(n, v)$.
Array.replicate_eq_toArray_replicate
theorem
: Array.replicate n v = (List.replicate n v).toArray
Full source
theorem _root_.Array.replicate_eq_toArray_replicate :
Array.replicate n v = (List.replicate n v).toArray := by
simpInformal description
For any natural number $n$ and any element $v$ of type $\alpha$, the array obtained by replicating $v$ $n$ times is equal to the array obtained by converting a list of $n$ copies of $v$ to an array. In other words, $\text{Array.replicate}(n, v) = \text{List.toArray}(\text{List.replicate}(n, v))$.
Array.mkArray_eq_toArray_replicate
abbrev
Full source
@[deprecated _root_.Array.replicate_eq_toArray_replicate (since := "2025-03-18")]
abbrev _root_.Array.mkArray_eq_toArray_replicate := @_root_.Array.replicate_eq_toArray_replicateInformal description
For any natural number $n$ and any element $v$ of type $\alpha$, the array constructed by `Array.mkArray` with $n$ copies of $v$ is equal to the array obtained by converting a list of $n$ copies of $v$ to an array. That is, $\text{Array.mkArray}(n, v) = \text{List.toArray}(\text{List.replicate}(n, v))$.
List.flatMap_empty
theorem
{β} (f : α → Array β) : (#[] : Array α).flatMap f = #[]
Informal description
For any function $f : \alpha \to \text{Array } \beta$, applying the flatMap operation to the empty array results in the empty array, i.e., $\text{flatMap } f \text{ } \#[] = \#[]$.
List.flatMap_toArray_cons
theorem
{β} (f : α → Array β) (a : α) (as : List α) : (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f
Full source
theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
(a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
simp [Array.flatMap]
suffices ∀ xs, List.foldl (fun ys a => ys ++ f a) (f a ++ xs) as =
f a ++ List.foldl (fun ys a => ys ++ f a) xs as by
erw [empty_append] -- Why doesn't this work via `simp`?
simpa using this #[]
intro xs
induction as generalizing xs <;> simp_allInformal description
For any function $f : \alpha \to \text{Array } \beta$, element $a : \alpha$, and list $as : \text{List } \alpha$, the flat map operation on the array obtained from the list $a :: as$ satisfies:
$$(a :: as).\text{toArray}.\text{flatMap } f = f a \mathbin{+\!\!+} (as.\text{toArray}.\text{flatMap } f)$$
List.flatMap_toArray
theorem
{β} (f : α → Array β) (as : List α) : as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray
Informal description
For any function $f : \alpha \to \text{Array } \beta$ and any list $as$ of elements of type $\alpha$, the flat map operation on the array obtained from $as$ is equal to the array obtained by first flat mapping $f$ over $as$ (converting each result to a list) and then converting the resulting list back to an array. That is:
$$\text{flatMap}(f, as.\text{toArray}) = \left(as.\text{flatMap} (\lambda a, (f a).\text{toList})\right).\text{toArray}$$
List.swap_toArray
theorem
(l : List α) (i j : Nat) {hi hj} : l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray
Informal description
For any list $l$ of elements of type $\alpha$ and indices $i, j$ with proofs $hi : i < l.toArray.size$ and $hj : j < l.toArray.size$, swapping elements at positions $i$ and $j$ in the array obtained from $l$ is equivalent to first replacing the $i$-th element of $l$ with $l[j]$, then replacing the $j$-th element with $l[i]$, and finally converting the resulting list to an array. Symbolically:
$$ (l.toArray).swap\ i\ j\ hi\ hj = (l.set\ i\ l[j]).set\ j\ l[i]).toArray $$
List.eraseIdx_toArray
theorem
(l : List α) (i : Nat) (h : i < l.toArray.size) : l.toArray.eraseIdx i h = (l.eraseIdx i).toArray
Full source
@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
rw [Array.eraseIdx]
split <;> rename_i h'
· rw [eraseIdx_toArray]
simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
simp
· simp at h h'
have t : i = l.length - 1 := by omega
simp [t]
termination_by l.length - i
decreasing_by
rename_i h
simp at h
simp
omegaInformal description
For any list $l$ of elements of type $\alpha$ and any natural number $i$ such that $i$ is less than the size of the array obtained from $l$, the array obtained by removing the element at index $i$ from $l.toArray$ is equal to the array obtained by first removing the element at index $i$ from $l$ and then converting the resulting list to an array. In symbols:
$$ l.toArray.eraseIdx\ i\ h = (l.eraseIdx\ i).toArray $$
List.eraseIdxIfInBounds_toArray
theorem
(l : List α) (i : Nat) : l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray
Full source
@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
rw [Array.eraseIdxIfInBounds]
split
· simp
· simp_all [eraseIdx_eq_self.2]Informal description
For any list $l$ of elements of type $\alpha$ and any natural number index $i$, the array obtained by converting $l$ to an array and then removing the element at index $i$ (if $i$ is within bounds) is equal to the array obtained by first removing the element at index $i$ from $l$ and then converting the resulting list to an array. In symbols:
$$ l.toArray.eraseIdxIfInBounds\ i = (l.eraseIdx\ i).toArray $$
List.eraseP_toArray
theorem
{as : List α} {p : α → Bool} : as.toArray.eraseP p = (as.eraseP p).toArray
Full source
@[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} :
as.toArray.eraseP p = (as.eraseP p).toArray := by
rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]
split <;> simp [*, findIdx?_eq_map_findFinIdx?_val]Informal description
For any list `as` of elements of type `α` and any predicate `p : α → Bool`, the array obtained by converting `as` to an array and then removing the first element satisfying `p` is equal to the array obtained by first removing the first element satisfying `p` from `as` and then converting the resulting list to an array. In symbols:
$$ \text{as.toArray.eraseP}\ p = (\text{as.eraseP}\ p).\text{toArray} $$
List.erase_toArray
theorem
[BEq α] {as : List α} {a : α} : as.toArray.erase a = (as.erase a).toArray
Full source
@[simp] theorem erase_toArray [BEq α] {as : List α} {a : α} :
as.toArray.erase a = (as.erase a).toArray := by
rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx]
rw [idxOf?_eq_map_finIdxOf?_val]
split <;> simp_allInformal description
For any list `as` of elements of type `α` with a boolean equality relation and any element `a` of type `α`, the array obtained by converting `as` to an array and then removing the first occurrence of `a` is equal to the array obtained by first removing the first occurrence of `a` from `as` and then converting the resulting list to an array. In symbols:
$$ \text{as.toArray.erase}(a) = (\text{as.erase}(a)).\text{toArray} $$
List.insertIdx_toArray
theorem
(l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size) : l.toArray.insertIdx i a = (l.insertIdx i a).toArray
Full source
@[simp] theorem insertIdx_toArray (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size):
l.toArray.insertIdx i a = (l.insertIdx i a).toArray := by
rw [Array.insertIdx]
rw [insertIdx_loop_toArray (h := h)]
ext j h₁ h₂
· simp at h
simp [length_insertIdx, h]
omega
· simp [length_insertIdx] at h₁ h₂
simp [getElem_insertIdx]
split <;> rename_i h₃
· rw [getElem_append_left (by simp; split at h₂ <;> omega)]
simp only [getElem_take]
rw [getElem_append_left]
· rw [getElem_append_right (by simp; omega)]
rw [getElem_cons]
simp
split <;> rename_i h₄
· rw [dif_pos (by omega)]
· rw [dif_neg (by omega)]
congr
omegaInformal description
For any list $l$ of elements of type $\alpha$, natural number index $i$, and element $a$ of type $\alpha$ such that $i$ is at most the size of the array obtained from converting $l$, inserting $a$ at index $i$ in the converted array is equivalent to converting the list obtained by inserting $a$ at index $i$ in $l$. That is,
$$ l.\mathtt{toArray}.\mathtt{insertIdx}\ i\ a = (l.\mathtt{insertIdx}\ i\ a).\mathtt{toArray} $$
List.insertIdxIfInBounds_toArray
theorem
(l : List α) (i : Nat) (a : α) : l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray
Full source
@[simp] theorem insertIdxIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray := by
rw [Array.insertIdxIfInBounds]
split <;> rename_i h'
· simp
· simp only [size_toArray, Nat.not_le] at h'
rw [List.insertIdx_of_length_lt (h := h')]Informal description
For any list $l$ of elements of type $\alpha$, natural number index $i$, and element $a$ of type $\alpha$, inserting $a$ at index $i$ in the array obtained from converting $l$ (if $i$ is within bounds) is equivalent to converting the list obtained by inserting $a$ at index $i$ in $l$ to an array. That is,
$$ l.\mathtt{toArray}.\mathtt{insertIdxIfInBounds}\ i\ a = (l.\mathtt{insertIdx}\ i\ a).\mathtt{toArray} $$
List.replace_toArray
theorem
[BEq α] [LawfulBEq α] (l : List α) (a b : α) : l.toArray.replace a b = (l.replace a b).toArray
Full source
@[simp]
theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
l.toArray.replace a b = (l.replace a b).toArray := by
rw [Array.replace]
split <;> rename_i i h
· simp only [finIdxOf?_toArray, finIdxOf?_eq_none_iff] at h
rw [replace_of_not_mem]
simpa
· simp_all only [finIdxOf?_toArray, finIdxOf?_eq_some_iff, Fin.getElem_fin, set_toArray,
mk.injEq]
apply List.ext_getElem
· simp
· intro j h₁ h₂
rw [List.getElem_replace, List.getElem_set]
by_cases h₃ : j < i
· rw [if_neg (by omega), if_neg]
simp only [length_set] at h₁ h₃
simpa using h.2 ⟨j, by omega⟩ h₃
· by_cases h₃ : j = i
· rw [if_pos (by omega), if_pos, if_neg]
· simp only [mem_take_iff_getElem, not_exists]
intro k hk
simpa using h.2 ⟨k, by omega⟩ (by show k < i.1; omega)
· subst h₃
simpa using h.1
· rw [if_neg (by omega)]
split
· rw [if_pos]
· simp_all
· simp only [mem_take_iff_getElem]
simp only [length_set] at h₁
exact ⟨i, by omega, h.1⟩
· rflInformal description
For any type $\alpha$ with a boolean equality relation and a lawful instance, and for any list $l$ of elements in $\alpha$, the array obtained by first converting $l$ to an array and then replacing all occurrences of $a$ with $b$ is equal to the array obtained by first replacing all occurrences of $a$ with $b$ in $l$ and then converting the result to an array.
In symbols:
$$\text{replace}(l.\text{toArray}, a, b) = (\text{replace}(l, a, b)).\text{toArray}$$
List.leftpad_toArray
theorem
(n : Nat) (a : α) (l : List α) : Array.leftpad n a l.toArray = (leftpad n a l).toArray
Full source
@[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
Array.leftpad n a l.toArray = (leftpad n a l).toArray := by
simp [leftpad, Array.leftpad, ← toArray_replicate]Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the left padding of the array conversion of $l$ is equal to the array conversion of the left padding of $l$. That is, $\text{Array.leftpad}(n, a, l.\text{toArray}) = (\text{leftpad}(n, a, l)).\text{toArray}$.
List.rightpad_toArray
theorem
(n : Nat) (a : α) (l : List α) : Array.rightpad n a l.toArray = (rightpad n a l).toArray
Full source
@[simp] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) :
Array.rightpad n a l.toArray = (rightpad n a l).toArray := by
simp [rightpad, Array.rightpad, ← toArray_replicate]Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the right-padded array obtained by converting $l$ to an array and then right-padding it to length $n$ with $a$ is equal to the array obtained by converting the right-padded list (right-padded to length $n$ with $a$) to an array.
In symbols:
$$\text{Array.rightpad}\ n\ a\ (l.\text{toArray}) = (\text{rightpad}\ n\ a\ l).\text{toArray}$$