Documentation

Regex.Data.Array.Lemmas

theorem Array.sizeOf_head?_of_mem {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) :
theorem Array.sizeOf_head?_of_tail {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) :
sizeOf as' < sizeOf as
theorem Array.sizeOf_dropLast_cons {α : Type u_1} [SizeOf α] (a : α) (as : List α) :
sizeOf (a :: as).dropLast < sizeOf (a :: as)
theorem Array.sizeOf_dropLast_non_empty {α : Type u_1} [SizeOf α] (as : List α) (h : 0 < as.length) :
theorem Array.sizeOf_pop_non_empty {α : Type u_1} [SizeOf α] (as : Array α) (h : 0 < as.toList.length) :
theorem Array.sizeOf_pop? {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.pop? = some (a, as')) :
sizeOf as' < sizeOf as
theorem Array.size_one {α : Type u_1} (a : α) :
theorem Array.default_size_zero {α : Type u_1} (arr : Array α) (h : arr = default) :
arr.size = 0
theorem Array.non_empty_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) :
0 < arr.size
theorem Array.pop?_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) :
(arr' : Array α), arr.pop? = some (last, arr')
theorem Array.pop?_of_non_empty {α : Type u_1} (arr : Array α) (h : 0 < arr.size) :
(arr' : Array α), (last : α), arr.pop? = some (last, arr')
theorem Array.last?_eq_getLast {α : Type u_1} {last : α} (a : Array α) (h1 : a.last? = some last) (h2 : a.toList []) :
a.toList.getLast h2 = last
theorem Array.lt_of_pop?_eq_last? {α : Type u_1} {last : α} {arr' arr : Array α} (h : arr.pop? = some (last, arr')) :
theorem Array.get_last_of_pop? {α : Type u_1} {last : α} {arr' arr : Array α} (h1 : arr.pop? = some (last, arr')) (h2 : arr.toList.length - 1 < arr.toList.length) :
arr.toList.get arr.toList.length - 1, h2 = last
theorem Array.concat_of_pop? {α : Type u_1} {last : α} {arr' arr : Array α} (h : arr.pop? = some (last, arr')) :
arr.toList = arr'.toList ++ [last]
theorem Array.get_eq_get?_some {α : Type u_1} {i : Nat} {a : α} {as : Array α} (hlt : i < as.size) (h : a = as[i]) :
as[i]? = some a
@[simp]
theorem Array.size_of_head?_lt {α : Type u_1} {a : α} (as : Array α) (h : as.toList.head? = some a) :
0 < as.size
theorem Array.unique.mem_of_mem_unqiue {α : Type u_1} {a : α} [DecidableEq α] [LE α] (as : Array α) :
a as.uniquea as
@[simp]
theorem Array.mem_unique {α : Type u_1} {a : α} [DecidableEq α] [LE α] (as : Array α) :
a as.unique a as
@[simp]
theorem Array.nodup_unique {α : Type u_1} [DecidableEq α] [LE α] [LT α] [Std.IsPreorder α] [Std.LawfulOrderLT α] [Std.Antisymm fun (x1 x2 : α) => x1 x2] (as : Array α) (h : List.Pairwise LE.le as.toList) :
@[simp]
theorem Array.mergeSort_toList_eq {α : Type u_1} (as bs : Array α) (le : ααBool := by exact fun a b => a ≤ b) (h : bs = as.mergeSort le) :
@[simp]
theorem Array.mem_mergeSort {α : Type u_1} {a : α} [LT α] (as : Array α) (le : ααBool := by exact (· ≤ ·)) :
a as.mergeSort le a as
theorem Array.minWith_spec {α : Type u_1} [ord : Ord α] [Std.TransOrd α] (as : Array α) (init : α) (f : ααα) (hf : (fun (min x : α) => if compare x min = Ordering.lt then x else min) = f) (lt_iff : ∀ (a b : α), a < b a b ¬b a) (le_notLt : ∀ (a b : α), ¬a < b b a) :
True foldlM f init as Std.Do.PostCond.noThrow fun (r : α) => r init ∀ (a : α), a asr a
theorem Array.min_le_mem {α : Type u_1} {m : α} [ord : Ord α] [Std.TransOrd α] (xs : Array α) (h : xs.min? = some m) (lt_iff : ∀ (a b : α), a < b a b ¬b a) (le_notLt : ∀ (a b : α), ¬a < b b a) (a : α) :
a xsm a
theorem Array.mem_le_max {α : Type u_1} {m : α} [ord : Ord α] [Std.TransOrd α] (xs : Array α) (h : xs.max? = some m) (lt_iff : ∀ (a b : α), a < b a b ¬b a) (le_iff : ∀ (a b : α), ¬a < b b a) (a : α) :
a xsa m