Array.push_data
theorem Array.push_data : ∀ {α : Type u_1} (arr : Array α) (a : α), (arr.push a).data = arr.data ++ [a]
This theorem, named `Array.push_data`, states that for all types `α`, given an array `arr` of type `α` and an element `a` of type `α`, when the element `a` is pushed onto the end of the array `arr` using the `Array.push` function, the underlying data of the resulting array is equivalent to appending the element `a` to the end of the underlying data of the original array `arr`. In other words, it states that the `push` operation for arrays in Lean 4 corresponds to the `append` operation for lists.
More concisely: For all types `α`, the operation of pushing an element `a` to the end of an array `arr` in Lean 4 results in an array with the same underlying data as appending `a` to the original array `arr`.
|
Array.foldlM_eq_foldlM_data
theorem Array.foldlM_eq_foldlM_data :
∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β)
(arr : Array α), Array.foldlM f init arr 0 = List.foldlM f init arr.data
This theorem, `Array.foldlM_eq_foldlM_data`, establishes the equivalence between the `foldlM` operation on an array and the `foldlM` operation on the list that represents the data of the array. More specifically, for any monad `m`, types `β` and `α`, a function `f` of type `β → α → m β`, an initial value `init` of type `β`, and an array `arr` of type `Array α`, applying `foldlM` with function `f` and initial value `init` to `arr` from the 0th index is equal to applying `foldlM` with the same function and initial value to the data of `arr` treated as a list. This implies that the fold with side effects (`foldlM`) over an array and over its corresponding list, starting from the first element, produce the same result.
More concisely: For any monad `m`, types `β` and `α`, function `f` of type `β → α → m β`, initial value `init` of type `β`, and array `arr` of type `Array α`, `foldlM f init arr` is equal to `foldlM f init (list.toList arr)`.
|
Array.getElem_eq_data_get
theorem Array.getElem_eq_data_get : ∀ {α : Type u_1} {i : ℕ} (a : Array α) (h : i < a.size), a[i] = a.data.get ⟨i, h⟩
This theorem states that for any type `α`, any natural number `i`, and any array `a` of type `α`, if `i` is less than the size of `a`, then the `i`th element of `a` is equal to the `i`th element of the list `a.data`. The index `i` is used with proof `h` that `i` is less than the size of the array. This is a fundamental property that links the array structure with its underlying list data structure in Lean 4.
More concisely: For any array `a` of type `α` and natural number `i`, if `i` is less than the array size, then the `i`th element of `a` equals the `i`th element of `a.data`.
|
Array.toList_eq
theorem Array.toList_eq : ∀ {α : Type u_1} (arr : Array α), arr.toList = arr.data
This theorem states that for all types `α` and for any array of `α` termed `arr`, the operation of converting the array to a list using the `Array.toList` function is equivalent to obtaining the underlying data of the array. In other words, the function `Array.toList` simply returns the data from the array `arr` in list form.
More concisely: For all types `α` and arrays `arr` of length `n` in `α`, `Array.toList arr` is equal to the list `[a_1, ..., a_n]` where `a_1, ..., a_n` are the elements of `arr`.
|
Array.get_push_eq
theorem Array.get_push_eq : ∀ {α : Type u_1} (a : Array α) (x : α), (a.push x)[a.size] = x
The theorem `Array.get_push_eq` states that for any type `α`, any array `a` of type `α`, and any element `x` of type `α`, if we push the element `x` onto the end of the array `a` to create a new array, then the element at the index corresponding to the original size of the array `a` in the new array is `x`. In other words, if you append an element to the end of an array, you can retrieve it using the original array's size as the index.
More concisely: For any type `α`, array `a` of length `n` over `α`, and `x ∈ α`, the element at position `n` in the array obtained by appending `x` to `a` is `x`.
|
Array.map_data
theorem Array.map_data :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α), (Array.map f arr).data = List.map f arr.data := by
sorry
The theorem `Array.map_data` states that for any function `f` that maps an element of type `α` to an element of type `β`, and for any array `arr` of type `α`, the data of the array obtained by mapping `f` over `arr` is the same as the list obtained by mapping `f` over the data of `arr`. In other words, mapping a function over an array, and then converting it to a list, gives the same result as first converting the array to a list and then mapping the function over the list.
More concisely: For any function `f` and array `arr` of type `α`, the data of the array obtained by mapping `f` is equal to the list obtained by mapping `f` to the list obtained from the array's data. In Lean notation, `(Array.map f arr) = List.map f (Array.toList arr)`.
|
Array.appendList_data
theorem Array.appendList_data : ∀ {α : Type u_1} (arr : Array α) (l : List α), (arr ++ l).data = arr.data ++ l := by
sorry
This theorem, `Array.appendList_data`, states that for any type `α` and for all arrays `arr` of type `α` and lists `l` of type `α`, the data of the array formed by appending the list `l` to the array `arr` is equal to the list formed by appending the list `l` to the data of the array `arr`. In other words, appending a list to an array in Lean 4 and then fetching the data is the same as appending the list to the array's data directly.
More concisely: For any type `α`, the data of the array obtained by appending list `l` to array `arr` in Lean 4 is equal to the list obtained by appending `l` to the data of `arr`.
|
Array.size_toArray
theorem Array.size_toArray : ∀ {α : Type u_1} (as : List α), (List.toArray as).size = as.length
This theorem states that for any list of elements of some type α (denoted as `as`), when we convert this list to an array using the `List.toArray` function, the size of the resulting array (as computed by the `Array.size` function) is equal to the length of the original list (as computed by the `List.length` function). In other words, converting a list to an array preserves its length or size. This theorem is a basic property that helps in understanding the relationship between lists and arrays in Lean 4.
More concisely: For any list `as : List α`, the size of `Array.toArray as` equals the length of `as`.
|
Array.foldl_data_eq_bind
theorem Array.foldl_data_eq_bind :
∀ {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β),
(∀ (acc : Array β) (a : α), (F acc a).data = acc.data ++ G a) →
(List.foldl F acc l).data = acc.data ++ l.bind G
This theorem states that for any list of elements of type `α`, an array of type `β`, a function `F` that takes an array of type `β` and an element of type `α` and returns an array of type `β`, and a function `G` that takes an element of type `α` and returns a list of elements of type `β`, if for all arrays of type `β` and elements of type `α`, the data of the result of applying `F` to the array and the element is equal to the concatenation of the data of the array and the result of applying `G` to the element, then the data of the result of folding `F` over the list starting with the array is equal to the concatenation of the data of the array and the result of binding the list with `G`. This can be seen as a relationship between the fold and bind operations on lists and arrays.
More concisely: If for all `β` arrays `a` and `α` elements `x`, the concatenation of `a` and `G x` is equal to the result of applying `F` to `a` and `x`, then the result of folding `F` over a list `[a] ++ xs` is equal to the array `a` concatenated with the list `map G xs`.
|
Array.foldl_data_eq_map
theorem Array.foldl_data_eq_map :
∀ {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (G : α → β),
(List.foldl (fun acc a => acc.push (G a)) acc l).data = acc.data ++ List.map G l
The theorem `Array.foldl_data_eq_map` states that for all types `α` and `β`, given a list `l` of elements of type `α`, an array `acc` of type `β`, and a function `G` that maps `α` to `β`, if we sequentially fold the list `l` by pushing each transformed element `(G a)` onto the array `acc`, then the resulting array's data is equivalent to appending the mapped list `(List.map G l)` to the original array's data. Specifically, it states that `(List.foldl (fun acc a => Array.push acc (G a)) acc l).data = acc.data ++ List.map G l`, where `++` represents list concatenation.
More concisely: For all types α and β, the data of the array obtained by folding a list of α's with function G into an initially empty array of β, is equal to the concatenation of the arrays formed by mapping G to the original list and the initial array.
|
Array.toListAppend_eq
theorem Array.toListAppend_eq : ∀ {α : Type u_1} (arr : Array α) (l : List α), arr.toListAppend l = arr.data ++ l := by
sorry
This theorem states that for any type `α`, given an `Array α` and a `List α`, the function `Array.toListAppend` that prepends the array onto the front of the list is equivalent to concatenating the array's data (converted to a list) with the list. In other words, applying `Array.toListAppend` with an array and a list as inputs produces the same result as appending the list representation of the array's data to the given list.
More concisely: For any type `α`, the function `Array.toListAppend` applying to an `Array α` and a `List α` is equivalent to the concatenation of the list representation of the array's data with the given list.
|
Array.mem_def
theorem Array.mem_def : ∀ {α : Type u_1} (a : α) (as : Array α), a ∈ as ↔ a ∈ as.data
This theorem, `Array.mem_def`, states that for any type α and for any instance `a` of the type `α` and any array `as` of the type `α`, `a` is a member of `as` if and only if `a` is a member of the underlying data of `as`. Essentially, it equates membership in the array with membership in the array's data.
More concisely: For any type α and array as of type α, an element a is in the array as if and only if a is in the underlying data of as.
|
Array.get_push_lt
theorem Array.get_push_lt :
∀ {α : Type u_1} (a : Array α) (x : α) (i : ℕ) (h : i < a.size),
let_fun this := ⋯;
(a.push x)[i] = a[i]
This theorem, called `Array.get_push_lt`, states that for any type `α`, given an array `a` of type `α`, an element `x` of type `α`, and a natural number `i` such that `i` is less than the size of the array `a`, if we push the element `x` onto the end of the array `a`, the `i`th element of the resulting array is the same as the `i`th element of the original array `a`. In other words, pushing an element onto the end of an array does not change the existing elements of the array.
More concisely: For any type `α`, given an array `a:` `α`^`n`, an element `x:` `α`, and a natural number `i` < `n`, `(Array.push x a).nth i = a.nth i`.
|
Array.foldl_eq_foldl_data
theorem Array.foldl_eq_foldl_data :
∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (arr : Array α),
Array.foldl f init arr 0 = List.foldl f init arr.data
The theorem `Array.foldl_eq_foldl_data` states that for all types `β` and `α`, and for any function `f : β → α → β`, initial value `init : β`, and array `arr : Array α`, the left fold function `Array.foldl` applied on the array `arr` starting from the 0th index is equal to the left fold function `List.foldl` applied on the list of data `arr.data` with the same function `f` and initial value `init`. This means that folding from the left over an array gives the same result as folding from the left over its corresponding list of data.
More concisely: For any type `β`, function `f : β → β → β`, initial value `init : β`, array `arr : Array α`, the left fold operation `Array.foldl f init arr` equals the left fold operation `List.foldl f init (arr.data : List α)`.
|
Array.foldr_eq_foldr_data
theorem Array.foldr_eq_foldr_data :
∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α),
Array.foldr f init arr arr.size = List.foldr f init arr.data
This theorem, `Array.foldr_eq_foldr_data`, states that for any types `α` and `β`, and for any function `f` from `α` to `β`, the "right-fold" function applied to an array `arr` using `f` and an initial value `init` produces the same result as applying the right-fold function to the data list of the array. In other words, the operation of right-folding over an array is equivalent to right-folding over its underlying list. The right-fold operation is defined as reducing the array or list from right to left, feeding each item and the cumulative result so far into the function `f`.
More concisely: For any type `α`, type `β`, and function `f` from `α` to `β`, the right-fold application to an array `arr` using `f` and an initial value `init` equals the right-fold application to the data list of `arr` using `f`. In other words, `Array.foldr arr init f = List.foldr (List.fromArray arr) init f`.
|
Array.append_data
theorem Array.append_data : ∀ {α : Type u_1} (arr arr' : Array α), (arr ++ arr').data = arr.data ++ arr'.data := by
sorry
This theorem, `Array.append_data`, states that for any two arrays `arr` and `arr'` of any type `α`, the data of the concatenated array (`arr ++ arr'`) is equal to the concatenation of the data of `arr` and `arr'`. In other words, it establishes that the operation of appending two arrays together in Lean 4 corresponds exactly to appending their underlying data together.
More concisely: For any type `α` and arrays `arr:` Array `α` and `arr':` Array `α`, the data of the concatenated array `arr ++ arr'` is equal to the concatenation of the data of `arr` and `arr'`.
|
Array.size_ofFn
theorem Array.size_ofFn : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α), (Array.ofFn f).size = n
The theorem `Array.size_ofFn` states that for any function `f` from the finite set of natural numbers less than `n` to some type `α`, the size of the array created by applying `f` to each element of the finite set (`Array.ofFn f`) is equal to `n`. In other words, if you create an array by mapping a function over each element in a set of size `n`, the size of the resulting array will also be `n`.
More concisely: For any function from a finite set of size n to type α, the size of the array obtained by applying the function to each element is equal to n.
|