Array.data_toArray
theorem Array.data_toArray : ∀ {α : Type u_1} (as : List α), (List.toArray as).data = as
This theorem, named `Array.data_toArray`, states that for any type `α` and any list `as` of type `α`, the data of the array obtained by converting the list `as` to an array using the `List.toArray` function, is equal to the original list `as`. In other words, the function `List.toArray` preserves the data of the list when it is converted into an array.
More concisely: For any list `as` of type `α`, the array obtained by converting `as` to an array using `List.toArray` has the same elements as the original list.
|
Array.size_push
theorem Array.size_push : ∀ {α : Type u} (a : Array α) (v : α), (a.push v).size = a.size + 1
The theorem `Array.size_push` states that for any type `α`, any array `a` of type `α`, and any element `v` of type `α`, the size of the array obtained by pushing the element `v` onto the end of `a` is equal to the size of the original array `a` plus one. This reflects the expected behavior of the `push` operation in increasing the size of the array by one.
More concisely: For any type `α` and array `a` of length `n` over `α`, the size of the array obtained by appending an element to `a` is `n + 1`.
|
Array.size_set
theorem Array.size_set : ∀ {α : Type u} (a : Array α) (i : Fin a.size) (v : α), (a.set i v).size = a.size
The theorem `Array.size_set` states that for all types `α`, given an array `a` of type `α`, an element `v` of type `α`, and an index `i` which is a valid index for `a` (i.e., it is a member of the finite set `Fin (Array.size a)`), the size of the array that results from setting the element at index `i` of `a` to `v` is equal to the size of the original array `a`. In other words, updating the value of an element in an array does not change the size of the array.
More concisely: For all types `α` and arrays `a` of length `n` over `α`, setting the `i`-th element of `a` to a new value does not change the length `n` of `a`.
|
Array.ext
theorem Array.ext :
∀ {α : Type u_1} (a b : Array α),
a.size = b.size → (∀ (i : ℕ) (hi₁ : i < a.size) (hi₂ : i < b.size), a[i] = b[i]) → a = b
This theorem, `Array.ext`, states that for all arrays `a` and `b` of some type `α`, if `a` and `b` have the same size and all corresponding elements of `a` and `b` are equal (i.e., for all natural number indices `i` less than the size of `a` and `b`, the `i`-th element of `a` is equal to the `i`-th element of `b`), then `a` and `b` are equal. Essentially, this theorem formalizes the intuitive notion that two arrays are equal if and only if they have the same size and all their corresponding elements are equal.
More concisely: If two arrays of the same size and type have equal elements at corresponding indices, then they are equal.
|
Array.size_swap
theorem Array.size_swap : ∀ {α : Type u_1} (a : Array α) (i j : Fin a.size), (a.swap i j).size = a.size
This theorem, named `Array.size_swap`, states that for any type `α`, any array `a` of type `α`, and any two indices `i` and `j` within the size of the array `a`, swapping the entries at positions `i` and `j` in the array `a` does not change the size of the array. In other words, the size of the array after the swap operation remains the same as the original size of the array.
More concisely: For any type `α` and array `a` of length `n` over `α`, swapping the `i`-th and `j`-th elements of `a` does not change the length of `a`, i.e., `n = length (a.swap i j)`.
|
Array.size_pop
theorem Array.size_pop : ∀ {α : Type u_1} (a : Array α), a.pop.size = a.size - 1
This theorem, `Array.size_pop`, states that for all types `α` and every array `a` of type `α`, the size of the array obtained by "popping" `a` (i.e., removing its last element using the `Array.pop` operation) is equal to the size of the original array `a` minus 1. This is equivalent to saying that the `Array.pop` operation decreases the size of an array by one unit.
More concisely: For all types `α` and arrays `a` of length `n` of type `α`, the length of `Array.pop a` is `n - 1`.
|
Array.ext'
theorem Array.ext' : ∀ {α : Type u_1} {as bs : Array α}, as.data = bs.data → as = bs
This theorem, named `Array.ext'`, states that for any type α and any two arrays `as` and `bs` of type α, if the data of `as` is equal to the data of `bs`, then the arrays `as` and `bs` are equal themselves. This is essentially a statement about the equality of arrays in Lean 4, stating that two arrays are equal if and only if their contents are equal.
More concisely: Given arrays `as` and `bs` of type α in Lean 4, if their data are equal, then `as = bs`.
|