Auxiliary lemmas for Array

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.

Equations

• a.isBoolean = ∀ (i : Fin a.size), a[i] = 0 ∨ a[i] = 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.

Equations

• a.toNum = Array.foldl (fun (acc elem : ℕ) => acc * 2 + elem) 0 (Array.map (fun (r : R) => if r = 0 then 0 else 1) a).reverse

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.

Equations

• a.matchSize b unit = (Array.rightpad b.size unit a, Array.rightpad a.size unit b)

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]?

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

find index from the end of an array

Equations

• Array.findIdxRev? cond as = Array.findIdxRev?.find cond as ⟨as.size, ⋯⟩

@[irreducible]

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

Equations

• Array.findIdxRev?.find cond as ⟨0, ⋯⟩ = none
• Array.findIdxRev?.find cond as ⟨i.succ, h⟩ = if cond as[i] = true then some ⟨i, ⋯⟩ else Array.findIdxRev?.find cond as ⟨i, ⋯⟩

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

@[irreducible]

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

@[irreducible]

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.

Equations

• Array.rightpadPowerOfTwo unit a = Array.rightpad (2 ^ Nat.clog 2 a.size) unit a

@[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.

Equations

• a.getLast h = a[a.size - 1]

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

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

Equations

• a.getLastD v₀ = a.getD (a.size - 1) v₀

@[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