Array.size_extract_loop
theorem Array.size_extract_loop :
∀ {α : Type u_1} (as bs : Array α) (size start : ℕ),
(Array.extract.loop as size start bs).size = bs.size + min size (as.size - start)
The theorem `Array.size_extract_loop` states that for any type `α`, arrays `as` and `bs`, and natural numbers `size` and `start`, the size of the array resulting from the `Array.extract.loop` operation on `as` with parameters `size` and `start` and initial array `bs` is equal to the size of `bs` plus the minimum of `size` and the difference between the size of `as` and `start`. In other words, it describes how the size of the output array is determined in the `Array.extract.loop` operation.
More concisely: The size of the array obtained by extracting `min (size : nat) (length as - start)` elements from array `as` starting at position `start` using `Array.extract.loop`, is equal to the length of the initial array `bs` plus the extracted number of elements.
|
Array.get_set_eq
theorem Array.get_set_eq : ∀ {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α), (a.set i v)[↑i] = v
This theorem states that for any array `a` of a certain type `α`, for any index `i` within the bounds of the array's size, and for any value `v` of type `α`, if we set the element at index `i` of the array `a` to the value `v`, then when we fetch the element at index `i` of the resulting array, we obtain the value `v`. In essence, it assures that the "set" operation correctly updates the specified position in the array with the given value.
More concisely: For any array `a` of type `α`, and any index `i` within its bounds, setting the `i`-th element of `a` to `v` results in an array `b` such that `b![i] = v`.
|
Array.filter_data
theorem Array.filter_data :
∀ {α : Type u_1} (p : α → Bool) (l : Array α), (Array.filter p l 0).data = List.filter p l.data
The theorem `Array.filter_data` states that for any type `α`, any function `p` from `α` to `Bool`, and any array `l` of elements of type `α`, the data of the result of filtering `l` using `p` starting from the 0th index is equal to the result of filtering the data of `l` using `p`. In other words, filtering an array using a certain function gives the same result as filtering the list representation of the array with the same function.
More concisely: For any type `α`, function `p` from `α` to `Bool`, and array `l` of length `n` in `α`, `[ filter (i : nat) (x : α) (l : array α) : bool | i < n := p x ] |> Data = filter (i : nat) (x : α) (Data l) : list α | i < length (Data l) := p x`.
|
Array.append_nil
theorem Array.append_nil : ∀ {α : Type u_1} (as : Array α), as ++ #[] = as
This theorem states that for any type `α` and any array of this type `as`, appending an empty array (`#[]`) to `as` will result in `as` itself. In other words, adding nothing to the end of any array does not change the array. This is analogous to the mathematical property that adding zero to any number does not change the number.
More concisely: For any type `α` and array `as : α array`, appending the empty array `#[]` to `as` results in the array `as` itself (i.e., `as ++ #[] = as`).
|
Array.extract_loop_zero
theorem Array.extract_loop_zero :
∀ {α : Type u_1} (as bs : Array α) (start : ℕ), Array.extract.loop as 0 start bs = bs
The theorem `Array.extract_loop_zero` states that for any type `α`, and any arrays `as` and `bs` of this type, and any natural number `start`, when we execute the `Array.extract.loop` function with `as` as the input array, `0` as the iteration count, `start` as the starting index, and `bs` as the base case array, the result is just the base case array `bs`. Essentially, this theorem is asserting that if we don't run any iterations of the `Array.extract.loop` function, the output will be the initial array `bs`.
More concisely: For any type `α`, and arrays `as:` `α`\[], `bs:` `α`\[], the result of applying `Array.extract.loop as 0 start bs` is equal to `bs`.
|
Array.get_set_ne
theorem Array.get_set_ne :
∀ {α : Type u_1} (a : Array α) (i : Fin a.size) {j : ℕ} (v : α) (hj : j < a.size), ↑i ≠ j → (a.set i v)[j] = a[j]
The theorem `Array.get_set_ne` states that for any array `a` of any type `α`, given an index `i` within the range of the array's size, another natural number index `j`, and a value `v` of type `α`, if `j` is also within the range of the array's size and `j` is not equal to `i`, then setting the element at index `i` of the array to `v` does not change the value at index `j` of the array. In other words, changing the value of an element at a specific index in an array does not affect the elements at different indices in the same array.
More concisely: For any array `a` of type `α`, and indices `i` and `j` within its range with `i ≠ j`, setting the `i`-th element of `a` to a value `v` does not alter the `j`-th element of `a`.
|