# Documentation

Std.Data.Array.Lemmas

@[simp]
theorem getElem_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i.val) :
a[i] = a[i.val]
@[simp]
theorem getElem?_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a i.val)] :
a[i]? = a[i.val]?
@[simp]
theorem getElem!_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a i.val)] [Inhabited Elem] :
a[i]! = a[i.val]!
theorem getElem?_pos {Cont : Type u_1} {Idx : Type u_2} {Elem : Type u_3} {Dom : ContIdxProp} [GetElem Cont Idx Elem Dom] (a : Cont) (i : Idx) (h : Dom a i) [Decidable (Dom a i)] :
a[i]? = some a[i]
theorem getElem?_neg {Cont : Type u_1} {Idx : Type u_2} {Elem : Type u_3} {Dom : ContIdxProp} [GetElem Cont Idx Elem Dom] (a : Cont) (i : Idx) (h : ¬Dom a i) [Decidable (Dom a i)] :
a[i]? = none
@[simp]
theorem mkArray_data {α : Type u_1} (n : Nat) (v : α) :
(mkArray n v).data =
@[simp]
theorem Array.singleton_def {α : Type u_1} (v : α) :
= #[v]
@[simp]
theorem Array.toArray_data {α : Type u_1} (a : ) :
List.toArray a.data = a
@[simp]
theorem Array.get_eq_getElem {α : Type u_1} (a : ) (i : Fin ()) :
= a[i.val]
@[simp]
theorem Array.get?_eq_getElem? {α : Type u_1} (a : ) (i : Nat) :
= a[i]?
theorem Array.getElem_fin_eq_data_get {α : Type u_1} (a : ) (i : Fin (List.length a.data)) :
a[i] = List.get a.data i
@[simp]
theorem Array.ugetElem_eq_getElem {α : Type u_1} (a : ) {i : USize} (h : ) :
a[i] = a[]
theorem Array.getElem?_eq_getElem {α : Type u_1} (a : ) (i : Nat) (h : i < ) :
a[i]? = some a[i]
theorem Array.get?_len_le {α : Type u_1} (a : ) (i : Nat) (h : i) :
a[i]? = none
theorem Array.getElem_mem_data {α : Type u_1} {i : Nat} (a : ) (h : i < ) :
a[i] a.data
theorem Array.getElem?_eq_data_get? {α : Type u_1} (a : ) (i : Nat) :
a[i]? = List.get? a.data i
theorem Array.get?_eq_data_get? {α : Type u_1} (a : ) (i : Nat) :
= List.get? a.data i
@[simp]
theorem Array.getD_eq_get? {α : Type u_1} (a : ) (n : Nat) (d : α) :
theorem Array.get!_eq_getD {α : Type u_1} {n : Nat} [] (a : ) :
= Array.getD a n default
@[simp]
theorem Array.get!_eq_get? {α : Type u_1} {n : Nat} [] (a : ) :
= Option.getD () default
@[simp]
theorem Array.back_eq_back? {α : Type u_1} [] (a : ) :
= Option.getD () default
@[simp]
theorem Array.back?_push {α : Type u_1} {x : α} (a : ) :
theorem Array.back_push {α : Type u_1} {x : α} [] (a : ) :
theorem Array.get?_push_lt {α : Type u_1} (a : ) (x : α) (i : Nat) (h : i < ) :
()[i]? = some a[i]
theorem Array.get?_push_eq {α : Type u_1} (a : ) (x : α) :
()[]? = some x
@[simp]
theorem Array.data_set {α : Type u_1} (a : ) (i : Fin ()) (v : α) :
(Array.set a i v).data = List.set a.data i.val v
@[simp]
theorem Array.get_set_eq {α : Type u_1} (a : ) (i : Fin ()) (v : α) :
(Array.set a i v)[i.val] = v
@[simp]
theorem Array.get_set_ne {α : Type u_1} (a : ) (i : Fin ()) {j : Nat} (v : α) (hj : j < ) (h : i.val j) :
(Array.set a i v)[j] = a[j]
@[simp]
theorem Array.get?_set_eq {α : Type u_1} (a : ) (i : Fin ()) (v : α) :
(Array.set a i v)[i.val]? = some v
@[simp]
theorem Array.get?_set_ne {α : Type u_1} (a : ) (i : Fin ()) {j : Nat} (v : α) (h : i.val j) :
(Array.set a i v)[j]? = a[j]?
theorem Array.get?_set {α : Type u_1} (a : ) (i : Fin ()) (j : Nat) (v : α) :
(Array.set a i v)[j]? = if i.val = j then some v else a[j]?
theorem Array.get_set {α : Type u_1} (a : ) (i : Fin ()) (j : Nat) (hj : j < ) (v : α) :
(Array.set a i v)[j] = if i.val = j then v else a[j]
theorem Array.set_set {α : Type u_1} (a : ) (i : Fin ()) (v : α) (v' : α) :
Array.set (Array.set a i v) { val := i.val, isLt := (_ : i.val < Array.size (Array.set a i v)) } v' = Array.set a i v'
theorem Array.swap_def {α : Type u_1} (a : ) (i : Fin ()) (j : Fin ()) :
Array.swap a i j = Array.set (Array.set a i ()) { val := j.val, isLt := (_ : j.val < Array.size (Array.set a i a[j.val])) } ()
theorem Array.data_swap {α : Type u_1} (a : ) (i : Fin ()) (j : Fin ()) :
(Array.swap a i j).data = List.set (List.set a.data i.val ()) j.val ()
theorem Array.get?_swap {α : Type u_1} (a : ) (i : Fin ()) (j : Fin ()) (k : Nat) :
(Array.swap a i j)[k]? = if j.val = k then some a[i.val] else if i.val = k then some a[j.val] else a[k]?
@[simp]
theorem Array.swapAt_def {α : Type u_1} (a : ) (i : Fin ()) (v : α) :
Array.swapAt a i v = (a[i.val], Array.set a i v)
theorem Array.swapAt!_def {α : Type u_1} (a : ) (i : Nat) (v : α) (h : i < ) :
= (a[i], Array.set a { val := i, isLt := h } v)
@[simp]
theorem Array.data_pop {α : Type u_1} (a : ) :
().data = List.dropLast a.data
@[simp]
theorem Array.pop_empty {α : Type u_1} :
Array.pop #[] = #[]
@[simp]
theorem Array.pop_push {α : Type u_1} {x : α} (a : ) :
theorem Array.SatisfiesM_foldrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] {as : } (motive : NatβProp) {init : β} (h0 : motive () init) {f : αβm β} (hf : ∀ (i : Fin ()) (b : β), motive (i.val + 1) bSatisfiesM (motive i.val) (f as[i] b)) :
SatisfiesM (motive 0) (Array.foldrM f init as ())
theorem Array.SatisfiesM_foldrM.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 + 1) bSatisfiesM (motive i.val) (f as[i] b)) {i : Nat} {b : β} (hi : i ) (H : motive i b) :
SatisfiesM (motive 0) (Array.foldrM.fold f as 0 i hi b)
theorem Array.foldr_induction {α : Type u_1} {β : Type u_2} {as : } (motive : NatβProp) {init : β} (h0 : motive () init) {f : αββ} (hf : (i : Fin ()) → (b : β) → motive (i.val + 1) bmotive i.val (f as[i] b)) :
motive 0 (Array.foldr f init as ())
theorem Array.mapM_eq_mapM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αm β) (arr : ) :
Array.mapM f arr = do let __do_lift ← List.mapM f arr.data pure { data := __do_lift }
theorem Array.SatisfiesM_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (as : ) (f : Fin ()αm β) (motive : ) (h0 : motive 0) (p : Fin ()βProp) (hs : ∀ (i : Fin ()), motive i.valSatisfiesM (fun x => p i x motive (i.val + 1)) (f i as[i])) :
SatisfiesM (fun arr => motive () eq, (i : Nat) → (h : i < ) → p { val := i, isLt := h } arr[i]) ()
theorem Array.SatisfiesM_mapIdxM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (as : ) (f : Fin ()αm β) (motive : ) (p : Fin ()βProp) (hs : ∀ (i : Fin ()), motive i.valSatisfiesM (fun x => p i x motive (i.val + 1)) (f i as[i])) {bs : } {i : Nat} {j : Nat} {h : i + j = } (h₁ : j = ) (h₂ : (i : Nat) → (h : i < ) → (h' : i < ) → p { val := i, isLt := h } bs[i]) (hm : motive j) :
SatisfiesM (fun arr => motive () eq, (i : Nat) → (h : i < ) → p { val := i, isLt := h } arr[i]) (Array.mapIdxM.map as f i j h bs)
theorem Array.mapIdx_induction {α : Type u_1} {β : Type u_2} (as : ) (f : Fin ()αβ) (motive : ) (h0 : motive 0) (p : Fin ()βProp) (hs : ∀ (i : Fin ()), motive i.valp i (f i as[i]) motive (i.val + 1)) :
motive () eq, (i : Nat) → (h : i < ) → p { val := i, isLt := h } (Array.mapIdx as f)[i]
theorem Array.mapIdx_induction' {α : Type u_1} {β : Type u_2} (as : ) (f : Fin ()αβ) (p : Fin ()βProp) (hs : (i : Fin ()) → p i (f i as[i])) :
eq, (i : Nat) → (h : i < ) → p { val := i, isLt := h } (Array.mapIdx as f)[i]
@[simp]
theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} (a : ) (f : Fin ()αβ) :
@[simp]
theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} (a : ) (f : Fin ()αβ) (i : Nat) (h : i < Array.size ()) :
()[i] = f { val := i, isLt := (_ : i < ) } a[i]
@[simp]
theorem Array.size_swap! {α : Type u_1} (a : ) (i : Nat) (j : Nat) (hi : i < ) (hj : j < ) :
@[simp]
theorem Array.size_reverse {α : Type u_1} (a : ) :
theorem Array.size_reverse.go {α : Type u_1} (as : ) (i : Nat) (j : Fin ()) :
@[simp]
theorem Array.reverse_data {α : Type u_1} (a : ) :
().data = List.reverse a.data
theorem Array.reverse_data.go {α : Type u_1} (a : ) (as : ) (i : Nat) (j : Nat) (hj : j < ) (h : i + j + 1 = ) (h₂ : ) (H : ∀ (k : Nat), List.get? as.data k = if i k k j then List.get? a.data k else List.get? (List.reverse a.data) k) (k : Nat) :
List.get? (Array.reverse.loop as i { val := j, isLt := hj }).data k = List.get? (List.reverse a.data) k
@[simp]
theorem Array.size_ofFn_go {α : Type u_1} {n : Nat} (f : Fin nα) (i : Nat) (acc : ) :
Array.size (Array.ofFn.go f i acc) = Array.size acc + (n - i)
@[simp]
theorem Array.size_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) :
= n
theorem Array.getElem_ofFn_go {n : Nat} {α : Type u_1} (f : Fin nα) (i : Nat) {acc : } {k : Nat} (hki : k < n) (hin : i n) (hi : i = Array.size acc) (hacc : ∀ (j : Nat) (hj : j < Array.size acc), acc[j] = f { val := j, isLt := (_ : j < n) }) :
(Array.ofFn.go f i acc)[k] = f { val := k, isLt := hki }
@[simp]
theorem Array.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) (i : Nat) (h : i < ) :
()[i] = f { val := i, isLt := (_ : i < n) }