Documentation

Std.Data.Array.Init.Lemmas

This file contains some theorems about Array and List needed for Std.List.Basic.

@[simp]
theorem Array.mkEmpty_eq (α : Type u_1) (n : Nat) :
= #[]
@[simp]
theorem Array.size_toArray {α : Type u_1} (as : List α) :
=
@[simp]
theorem Array.size_mk {α : Type u_1} (as : List α) :
Array.size { data := as } =
theorem Array.getElem_eq_data_get {α : Type u_1} {i : Nat} (a : ) (h : i < ) :
a[i] = List.get a.data { val := i, isLt := h }
theorem Array.foldlM_eq_foldlM_data.aux {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [] (f : βαm β) (arr : ) (i : Nat) (j : Nat) (H : Array.size arr i + j) (b : β) :
Array.foldlM.loop f arr (Array.size arr) (_ : Array.size arr Array.size arr) i j b = List.foldlM f b (List.drop j arr.data)
theorem Array.foldlM_eq_foldlM_data {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [] (f : βαm β) (init : β) (arr : ) :
Array.foldlM f init arr 0 (Array.size arr) = List.foldlM f init arr.data
theorem Array.foldl_eq_foldl_data {β : Type u_1} {α : Type u_2} (f : βαβ) (init : β) (arr : ) :
Array.foldl f init arr 0 (Array.size arr) = List.foldl f init arr.data
theorem Array.foldrM_eq_reverse_foldlM_data.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm β) (arr : ) (init : β) (i : Nat) (h : i Array.size arr) :
List.foldlM (fun x y => f y x) init (List.reverse (List.take i arr.data)) = Array.foldrM.fold f arr 0 i h init
theorem Array.foldrM_eq_reverse_foldlM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm β) (init : β) (arr : ) :
Array.foldrM f init arr (Array.size arr) = List.foldlM (fun x y => f y x) init (List.reverse arr.data)
theorem Array.foldrM_eq_foldrM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm β) (init : β) (arr : ) :
Array.foldrM f init arr (Array.size arr) = List.foldrM f init arr.data
theorem Array.foldr_eq_foldr_data {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (arr : ) :
Array.foldr f init arr (Array.size arr) = List.foldr f init arr.data
@[simp]
theorem Array.push_data {α : Type u_1} (arr : ) (a : α) :
(Array.push arr a).data = arr.data ++ [a]
theorem Array.foldrM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm β) (init : β) (arr : ) (a : α) :
Array.foldrM f init (Array.push arr a) (Array.size (Array.push arr a)) = do let init ← f a init Array.foldrM f init arr (Array.size arr)
@[simp]
theorem Array.foldrM_push' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm β) (init : β) (arr : ) (a : α) :
Array.foldrM f init (Array.push arr a) (Array.size arr + 1) = do let init ← f a init Array.foldrM f init arr (Array.size arr)
theorem Array.foldr_push {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (arr : ) (a : α) :
Array.foldr f init (Array.push arr a) (Array.size (Array.push arr a)) = Array.foldr f (f a init) arr (Array.size arr)
@[simp]
theorem Array.foldr_push' {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (arr : ) (a : α) :
Array.foldr f init (Array.push arr a) (Array.size arr + 1) = Array.foldr f (f a init) arr (Array.size arr)
@[simp]
theorem Array.toListAppend_eq {α : Type u_1} (arr : ) (l : List α) :
= arr.data ++ l
@[simp]
theorem Array.toList_eq {α : Type u_1} (arr : ) :
Array.toList arr = arr.data
@[inline]
def Array.toListRev {α : Type u_1} (arr : ) :
List α

A more efficient version of arr.toList.reverse.

Instances For
@[simp]
theorem Array.toListRev_eq {α : Type u_1} (arr : ) :
= List.reverse arr.data
theorem Array.SatisfiesM_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] {as : } (motive : NatβProp) {init : β} (h0 : motive 0 init) {f : βαm β} (hf : ∀ (i : Fin ()) (b : β), motive i.val bSatisfiesM (motive (i.val + 1)) (f b as[i])) :
SatisfiesM (motive ()) (Array.foldlM f init as 0 ())
theorem Array.SatisfiesM_foldlM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] {as : } (motive : NatβProp) {f : βαm β} (hf : ∀ (i : Fin ()) (b : β), motive i.val bSatisfiesM (motive (i.val + 1)) (f b as[i])) {i : Nat} {j : Nat} {b : β} (h₁ : j ) (h₂ : i + j) (H : motive j b) :
SatisfiesM (motive ()) (Array.foldlM.loop f as () (_ : ) i j b)
theorem Array.foldl_induction {α : Type u_1} {β : Type u_2} {as : } (motive : NatβProp) {init : β} (h0 : motive 0 init) {f : βαβ} (hf : (i : Fin ()) → (b : β) → motive i.val bmotive (i.val + 1) (f b as[i])) :
motive () (Array.foldl f init as 0 ())
theorem Array.get_push_lt {α : Type u_1} (a : ) (x : α) (i : Nat) (h : i < ) :
()[i] = a[i]
@[simp]
theorem Array.get_push_eq {α : Type u_1} (a : ) (x : α) :
()[] = x
theorem Array.get_push {α : Type u_1} (a : ) (x : α) (i : Nat) (h : i < Array.size ()) :
()[i] = if h : i < then a[i] else x
theorem Array.mapM_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αm β) (arr : ) :
Array.mapM f arr = Array.foldlM (fun bs a => <$> f a) #[] arr 0 (Array.size arr) theorem Array.mapM_eq_foldlM.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αm β) (arr : ) (i : Nat) (r : ) : Array.mapM.map f arr i r = List.foldlM (fun bs a => <$> f a) r (List.drop i arr.data)
theorem Array.SatisfiesM_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (as : ) (f : αm β) (motive : ) (h0 : motive 0) (p : Fin ()βProp) (hs : ∀ (i : Fin ()), motive i.valSatisfiesM (fun x => p i x motive (i.val + 1)) (f as[i])) :
SatisfiesM (fun arr => motive () eq, (i : Nat) → (h : i < ) → p { val := i, isLt := h } arr[i]) (Array.mapM f as)
theorem Array.SatisfiesM_mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (as : ) (f : αm β) (p : Fin ()βProp) (hs : ∀ (i : Fin ()), SatisfiesM (p i) (f as[i])) :
SatisfiesM (fun arr => eq, (i : Nat) → (h : i < ) → p { val := i, isLt := h } arr[i]) (Array.mapM f as)
theorem Array.size_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αm β) (as : ) :
SatisfiesM (fun arr => Array.size arr = ) (Array.mapM f as)
@[simp]
theorem Array.map_data {α : Type u_1} {β : Type u_2} (f : αβ) (arr : ) :
(Array.map f arr).data = List.map f arr.data
@[simp]
theorem Array.size_map {α : Type u_1} {β : Type u_2} (f : αβ) (arr : ) :
@[simp]
theorem Array.getElem_map {α : Type u_1} {β : Type u_2} (f : αβ) (arr : ) (i : Nat) (h : i < Array.size (Array.map f arr)) :
(Array.map f arr)[i] = f arr[i]
@[simp]
theorem Array.pop_data {α : Type u_1} (arr : ) :
(Array.pop arr).data = List.dropLast arr.data
@[simp]
theorem Array.append_eq_append {α : Type u_1} (arr : ) (arr' : ) :
Array.append arr arr' = arr ++ arr'
@[simp]
theorem Array.append_data {α : Type u_1} (arr : ) (arr' : ) :
(arr ++ arr').data = arr.data ++ arr'.data
@[simp]
theorem Array.appendList_eq_append {α : Type u_1} (arr : ) (l : List α) :
Array.appendList arr l = arr ++ l
@[simp]
theorem Array.appendList_data {α : Type u_1} (arr : ) (l : List α) :
(arr ++ l).data = arr.data ++ l
theorem Array.foldl_data_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : ) (F : α) (G : αList β) (H : ∀ (acc : ) (a : α), (F acc a).data = acc.data ++ G a) :
(List.foldl F acc l).data = acc.data ++
theorem Array.foldl_data_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (acc : ) (G : αβ) :
(List.foldl (fun acc a => Array.push acc (G a)) acc l).data = acc.data ++ List.map G l
theorem Array.size_uset {α : Type u_1} (a : ) (v : α) (i : USize) (h : ) :