Auxiliary lemmas for Array

def Array.eraseDups {α : Type u_1} [BEq α] (xs : Array α) : Array α

Remove duplicates from an array while preserving first occurrences.

def Array.isBoolean {R : Type u_2} [Zero R] [One R] (a : Array R) : Prop

Checks if an array of elements from a type R is a boolean array, i.e., if every element is either 0 or 1.

def Array.toNum {R : Type u_2} [Zero R] [DecidableEq R] (a : Array R) : ℕ

Interpret an array as the binary representation of a number, sending 0 to 0 and ≠ 0 to 1.

theorem Array.leftpad_toList {α : Type u_1} {a : Array α} {n : ℕ} {unit : α} : leftpad n unit a = { toList := List.leftpad n unit a.toList }

theorem Array.rightpad_toList {α : Type u_1} {a : Array α} {n : ℕ} {unit : α} : rightpad n unit a = { toList := List.rightpad n unit a.toList }

theorem Array.rightpad_getElem_eq_getD {α : Type u_1} {a : Array α} {n : ℕ} {unit : α} {i : ℕ} (h : i < (rightpad n unit a).size) : (rightpad n unit a)[i] = a.getD i unit

@[reducible]

def Array.matchSize {α : Type u_1} (a b : Array α) (unit : α) : Array α × Array α

Array version of List.matchSize, which rightpads the arrays to the same length.

theorem Array.matchSize_toList {α : Type u_1} {a b : Array α} {unit : α} : a.matchSize b unit = match a.toList.matchSize b.toList unit with | (a', b') => ({ toList := a' }, { toList := b' })

theorem Array.getElem?_eq_toList {α : Type u_1} {a : Array α} {i : ℕ} : a.toList[i]? = a[i]?

theorem Array.getD_map_of_lt {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) (d : β) {i : ℕ} (hi : i < xs.size) : (map f xs).getD i d = f xs[i]

Array.map and getD agree with indexed access on in-bounds indices.

theorem Array.foldl_zipIdx_eq_foldl_toList_zipIdx {α : Type u_1} {β : Type u_2} (f : β → α × ℕ → β) (init : β) (a : Array α) : foldl f init a.zipIdx = List.foldl f init a.toList.zipIdx

theorem Array.foldl_zipIdx_eq_foldl_toList_zipIdx_size {α : Type u_1} {β : Type u_2} (f : β → α × ℕ → β) (init : β) (a : Array α) : foldl f init a.zipIdx 0 a.size = List.foldl f init a.toList.zipIdx

theorem Array.mem_foldl_append_of_mem {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) {x : α} {y : β} (hx : x ∈ xs.toList) (hy : y ∈ (f x).toList) : y ∈ (foldl (fun (out : Array β) (x : α) => out ++ f x) #[] xs).toList

theorem Array.mem_flatten_map_of_mem {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) {x : α} {y : β} (hx : x ∈ xs.toList) (hy : y ∈ (f x).toList) : y ∈ (map f xs).flatten

def Array.findIdxRev? {α : Type u_1} (cond : α → Bool) (as : Array α) : Option (Fin as.size)

find index from the end of an array

@[irreducible]

def Array.findIdxRev?.find {α : Type u_1} (cond : α → Bool) (as : Array α) : Fin (as.size + 1) → Option (Fin as.size)

theorem Array.findIdxRev?_def {α : Type u_1} {cond : α → Bool} {as : Array α} {k : Fin as.size} : findIdxRev? cond as = some k → cond as[k] = true

if findIdxRev? finds an index, the condition is satisfied on that element

theorem Array.findIdxRev?_maximal {α : Type u_1} {cond : α → Bool} {as : Array α} {k : Fin as.size} : findIdxRev? cond as = some k → ∀ j > k, ¬cond as[j] = true

if findIdxRev? finds an index, then for every greater index the condition doesn't hold

theorem Array.findIdxRev?_eq_none {α : Type u_1} {cond : α → Bool} {as : Array α} (h : ∀ (i : ℕ) (hi : i < as.size), ¬cond as[i] = true) : findIdxRev? cond as = none

if the condition is false on all elements, then findIdxRev? finds nothing

theorem Array.findIdxRev?_eq_none.aux {α : Type u_1} {cond : α → Bool} {as : Array α} (h : ∀ (i : ℕ) (hi : i < as.size), ¬cond as[i] = true) (i : Fin (as.size + 1)) : findIdxRev?.find cond as i = none

theorem Array.findIdxRev?_empty_none {α : Type u_1} {cond : α → Bool} {as : Array α} (h : as = #[]) : findIdxRev? cond as = none

theorem Array.findIdxRev?_eq_some {α : Type u_1} {cond : α → Bool} {as : Array α} (h : ∃ (i : ℕ) (hi : i < as.size), cond as[i] = true) : ∃ (k : Fin as.size), findIdxRev? cond as = some k

if the condition is true on some element, then findIdxRev? finds something

theorem Array.findIdxRev?_eq_some.aux {α : Type u_1} {cond : α → Bool} {as : Array α} (h : ∃ (i : ℕ) (hi : i < as.size), cond as[i] = true) (i : Fin (as.size + 1)) (h' : ∃ (i' : Fin as.size), ↑i' < ↑i ∧ cond as[i'] = true) : ∃ (k : Fin as.size), findIdxRev?.find cond as i = some k

def Array.rightpadPowerOfTwo {α : Type u_1} (unit : α) (a : Array α) : Array α

Right-pads an array with unit elements until its length is a power of two. Returns the padded array and the number of elements added.

@[simp]

theorem Array.rightpadPowerOfTwo_size {α : Type u_1} (unit : α) (a : Array α) : (rightpadPowerOfTwo unit a).size = 2 ^ Nat.clog 2 a.size

def Array.getLast {α : Type u_1} (a : Array α) (h : a.size > 0) : α

Get the last element of an array, assuming the array is non-empty.

def Array.getLastD {α : Type u_1} (a : Array α) (v₀ : α) : α

Get the last element of an array, or v₀ if the array is empty.

@[simp]

theorem Array.popWhile_nil_or_last_false {α : Type u_1} (p : α → Bool) (as : Array α) (h : (popWhile p as).size > 0) : ¬p ((popWhile p as).getLast h) = true