Documentation

Init.Data.Array.Lemmas

Bootstrapping theorems about arrays #

This file contains some theorems about Array and List needed for Init.Data.List.Impl.

@[simp]
theorem Array.singleton_def {α : Type u_1} (v : α) :
@[simp]
theorem Array.toArray_data {α : Type u_1} (a : Array α) :
List.toArray a.data = a
@[simp]
theorem Array.data_length {α : Type u_1} {l : Array α} :
l.data.length = l.size
@[simp]
theorem Array.mkEmpty_eq (α : Type u_1) (n : Nat) :
@[simp]
theorem Array.size_toArray {α : Type u_1} (as : List α) :
(List.toArray as).size = as.length
@[simp]
theorem Array.size_mk {α : Type u_1} (as : List α) :
{ data := as }.size = as.length
theorem Array.getElem_eq_data_getElem {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) :
a[i] = a.data[i]
@[deprecated Array.getElem_eq_data_getElem]
theorem Array.getElem_eq_data_get {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) :
a[i] = a.data.get i, h
@[irreducible]
theorem Array.foldlM_eq_foldlM_data.aux {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : βαm β) (arr : Array α) (i : Nat) (j : Nat) (H : arr.size i + j) (b : β) :
Array.foldlM.loop f arr arr.size 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} [Monad m] (f : βαm β) (init : β) (arr : Array α) :
Array.foldlM f init arr = List.foldlM f init arr.data
theorem Array.foldl_eq_foldl_data {β : Type u_1} {α : Type u_2} (f : βαβ) (init : β) (arr : Array α) :
Array.foldl f init 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} [Monad m] (f : αβm β) (arr : Array α) (init : β) (i : Nat) (h : i arr.size) :
List.foldlM (fun (x : β) (y : α) => f y x) init (List.take i arr.data).reverse = 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} [Monad m] (f : αβm β) (init : β) (arr : Array α) :
Array.foldrM f init arr = List.foldlM (fun (x : β) (y : α) => f y x) init arr.data.reverse
theorem Array.foldrM_eq_foldrM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αβm β) (init : β) (arr : Array α) :
Array.foldrM f init arr = List.foldrM f init arr.data
theorem Array.foldr_eq_foldr_data {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (arr : Array α) :
Array.foldr f init arr = List.foldr f init arr.data
@[simp]
theorem Array.push_data {α : Type u_1} (arr : Array α) (a : α) :
(arr.push a).data = arr.data ++ [a]
theorem Array.foldrM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αβm β) (init : β) (arr : Array α) (a : α) :
Array.foldrM f init (arr.push a) = do let initf a init Array.foldrM f init arr
@[simp]
theorem Array.foldrM_push' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αβm β) (init : β) (arr : Array α) (a : α) :
Array.foldrM f init (arr.push a) (arr.size + 1) = do let initf a init Array.foldrM f init arr
theorem Array.foldr_push {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (arr : Array α) (a : α) :
Array.foldr f init (arr.push a) = Array.foldr f (f a init) arr
@[simp]
theorem Array.foldr_push' {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (arr : Array α) (a : α) :
Array.foldr f init (arr.push a) (arr.size + 1) = Array.foldr f (f a init) arr
@[simp]
theorem Array.toListAppend_eq {α : Type u_1} (arr : Array α) (l : List α) :
arr.toListAppend l = arr.data ++ l
@[simp]
theorem Array.toList_eq {α : Type u_1} (arr : Array α) :
arr.toList = arr.data
@[inline]
def Array.toListRev {α : Type u_1} (arr : Array α) :
List α

A more efficient version of arr.toList.reverse.

Equations
Instances For
    @[simp]
    theorem Array.toListRev_eq {α : Type u_1} (arr : Array α) :
    arr.toListRev = arr.data.reverse
    theorem Array.get_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    let_fun this := ; (a.push x)[i] = a[i]
    @[simp]
    theorem Array.get_push_eq {α : Type u_1} (a : Array α) (x : α) :
    (a.push x)[a.size] = x
    theorem Array.get_push {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
    (a.push x)[i] = if h : i < a.size then a[i] else x
    theorem Array.mapM_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) (arr : Array α) :
    Array.mapM f arr = Array.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) #[] arr
    @[irreducible]
    theorem Array.mapM_eq_foldlM.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) (arr : Array α) (i : Nat) (r : Array β) :
    Array.mapM.map f arr i r = List.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) r (List.drop i arr.data)
    @[simp]
    theorem Array.map_data {α : Type u_1} {β : Type u_2} (f : αβ) (arr : Array α) :
    (Array.map f arr).data = List.map f arr.data
    @[simp]
    theorem Array.size_map {α : Type u_1} {β : Type u_2} (f : αβ) (arr : Array α) :
    (Array.map f arr).size = arr.size
    @[simp]
    theorem Array.pop_data {α : Type u_1} (arr : Array α) :
    arr.pop.data = arr.data.dropLast
    @[simp]
    theorem Array.append_eq_append {α : Type u_1} (arr : Array α) (arr' : Array α) :
    arr.append arr' = arr ++ arr'
    @[simp]
    theorem Array.append_data {α : Type u_1} (arr : Array α) (arr' : Array α) :
    (arr ++ arr').data = arr.data ++ arr'.data
    @[simp]
    theorem Array.appendList_eq_append {α : Type u_1} (arr : Array α) (l : List α) :
    arr.appendList l = arr ++ l
    @[simp]
    theorem Array.appendList_data {α : Type u_1} (arr : Array α) (l : List α) :
    (arr ++ l).data = arr.data ++ l
    @[simp]
    theorem Array.appendList_nil {α : Type u_1} (arr : Array α) :
    arr ++ [] = arr
    @[simp]
    theorem Array.appendList_cons {α : Type u_1} (arr : Array α) (a : α) (l : List α) :
    arr ++ a :: l = arr.push a ++ l
    theorem Array.foldl_data_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array βαArray β) (G : αList β) (H : ∀ (acc : Array β) (a : α), (F acc a).data = acc.data ++ G a) :
    (List.foldl F acc l).data = acc.data ++ l.bind G
    theorem Array.foldl_data_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (G : αβ) :
    (List.foldl (fun (acc : Array β) (a : α) => acc.push (G a)) acc l).data = acc.data ++ List.map G l
    theorem Array.size_uset {α : Type u_1} (a : Array α) (v : α) (i : USize) (h : i.toNat < a.size) :
    (a.uset i v h).size = a.size
    theorem Array.anyM_eq_anyM_loop {m : TypeType u_1} {α : Type u_2} [Monad m] (p : αm Bool) (as : Array α) (start : Nat) (stop : Nat) :
    Array.anyM p as start stop = Array.anyM.loop p as (min stop as.size) start
    theorem Array.anyM_stop_le_start {m : TypeType u_1} {α : Type u_2} [Monad m] (p : αm Bool) (as : Array α) (start : Nat) (stop : Nat) (h : min stop as.size start) :
    Array.anyM p as start stop = pure false
    theorem Array.mem_def {α : Type u_1} (a : α) (as : Array α) :
    a as a as.data

    get #

    @[simp]
    theorem Array.get_eq_getElem {α : Type u_1} (a : Array α) (i : Fin a.size) :
    a.get i = a[i]
    theorem Array.getElem?_lt {α : Type u_1} (a : Array α) {i : Nat} (h : i < a.size) :
    a[i]? = some a[i]
    theorem Array.getElem?_ge {α : Type u_1} (a : Array α) {i : Nat} (h : i a.size) :
    a[i]? = none
    @[simp]
    theorem Array.get?_eq_getElem? {α : Type u_1} (a : Array α) (i : Nat) :
    a.get? i = a[i]?
    theorem Array.getElem?_len_le {α : Type u_1} (a : Array α) {i : Nat} (h : a.size i) :
    a[i]? = none
    theorem Array.getD_get? {α : Type u_1} (a : Array α) (i : Nat) (d : α) :
    a[i]?.getD d = if p : i < a.size then a[i] else d
    @[simp]
    theorem Array.getD_eq_get? {α : Type u_1} (a : Array α) (n : Nat) (d : α) :
    a.getD n d = a[n]?.getD d
    theorem Array.get!_eq_getD {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) :
    a.get! n = a.getD n default
    @[simp]
    theorem Array.get!_eq_getElem? {α : Type u_1} [Inhabited α] (a : Array α) (i : Nat) :
    a.get! i = (a.get? i).getD default

    set #

    @[simp]
    theorem Array.getElem_set_eq {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (eq : i = j) (p : j < (a.set i v).size) :
    (a.set i v)[j] = v
    @[simp]
    theorem Array.getElem_set_ne {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size) (h : i j) :
    (a.set i v)[j] = a[j]
    theorem Array.getElem_set {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) (j : Nat) (h : j < (a.set i v).size) :
    (a.set i v)[j] = if i = j then v else a[j]
    @[simp]
    theorem Array.getElem?_set_eq {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) :
    (a.set i v)[i]? = some v
    @[simp]
    theorem Array.getElem?_set_ne {α : Type u_1} (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (ne : i j) :
    (a.set i v)[j]? = a[j]?

    setD #

    @[simp]
    theorem Array.size_setD {α : Type u_1} (a : Array α) (index : Nat) (val : α) :
    (a.setD index val).size = a.size
    @[simp]
    theorem Array.getElem_setD_eq {α : Type u_1} (a : Array α) {i : Nat} (v : α) (h : i < (a.setD i v).size) :
    (a.setD i v)[i] = v
    @[simp]
    theorem Array.getElem?_setD_eq {α : Type u_1} (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
    (a.setD i v)[i]? = some v
    @[simp]
    theorem Array.getD_get?_setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) (d : α) :
    (a.setD i v)[i]?.getD d = if i < a.size then v else d

    Simplifies a normal form from get!

    ofFn #

    @[simp, irreducible]
    theorem Array.size_ofFn_go {α : Type u_1} {n : Nat} (f : Fin nα) (i : Nat) (acc : Array α) :
    (Array.ofFn.go f i acc).size = acc.size + (n - i)
    @[simp]
    theorem Array.size_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) :
    (Array.ofFn f).size = n
    @[irreducible]
    theorem Array.getElem_ofFn_go {n : Nat} {α : Type u_1} (f : Fin nα) (i : Nat) {acc : Array α} {k : Nat} (hki : k < n) (hin : i n) (hi : i = acc.size) (hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f j, ) :
    (Array.ofFn.go f i acc)[k] = f k, hki
    @[simp]
    theorem Array.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) (i : Nat) (h : i < (Array.ofFn f).size) :
    (Array.ofFn f)[i] = f i,
    @[simp]
    theorem Array.mkArray_data {α : Type u_1} (n : Nat) (v : α) :
    (mkArray n v).data = List.replicate n v

    mkArray #

    @[simp]
    theorem Array.getElem_mkArray {α : Type u_1} {i : Nat} (n : Nat) (v : α) (h : i < (mkArray n v).size) :
    (mkArray n v)[i] = v
    theorem Array.mem_data {α : Type u_1} {a : α} {l : Array α} :
    a l.data a l

    mem #

    theorem Array.not_mem_nil {α : Type u_1} (a : α) :
    ¬a #[]
    theorem Array.getElem?_mem {α : Type u_1} {l : Array α} {i : Fin l.size} :
    l[i] l

    get lemmas #

    theorem Array.getElem_fin_eq_data_get {α : Type u_1} (a : Array α) (i : Fin a.data.length) :
    a[i] = a.data.get i
    @[simp]
    theorem Array.ugetElem_eq_getElem {α : Type u_1} (a : Array α) {i : USize} (h : i.toNat < a.size) :
    a[i] = a[i.toNat]
    theorem Array.getElem?_eq_getElem {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) :
    a[i]? = some a[i]
    theorem Array.get?_len_le {α : Type u_1} (a : Array α) (i : Nat) (h : a.size i) :
    a[i]? = none
    theorem Array.getElem_mem_data {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) :
    a[i] a.data
    theorem Array.getElem?_eq_data_get? {α : Type u_1} (a : Array α) (i : Nat) :
    a[i]? = a.data.get? i
    theorem Array.get?_eq_data_get? {α : Type u_1} (a : Array α) (i : Nat) :
    a.get? i = a.data.get? i
    theorem Array.get!_eq_get? {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) :
    a.get! n = (a.get? n).getD default
    @[simp]
    theorem Array.back_eq_back? {α : Type u_1} [Inhabited α] (a : Array α) :
    a.back = a.back?.getD default
    @[simp]
    theorem Array.back?_push {α : Type u_1} {x : α} (a : Array α) :
    (a.push x).back? = some x
    theorem Array.back_push {α : Type u_1} {x : α} [Inhabited α] (a : Array α) :
    (a.push x).back = x
    theorem Array.get?_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    (a.push x)[i]? = some a[i]
    theorem Array.get?_push_eq {α : Type u_1} (a : Array α) (x : α) :
    (a.push x)[a.size]? = some x
    theorem Array.get?_push {α : Type u_1} {x : α} {i : Nat} {a : Array α} :
    (a.push x)[i]? = if i = a.size then some x else a[i]?
    @[simp]
    theorem Array.get?_size {α : Type u_1} {a : Array α} :
    a[a.size]? = none
    @[simp]
    theorem Array.data_set {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) :
    (a.set i v).data = a.data.set (↑i) v
    theorem Array.get_set_eq {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) :
    (a.set i v)[i] = v
    theorem Array.get?_set_eq {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) :
    (a.set i v)[i]? = some v
    @[simp]
    theorem Array.get?_set_ne {α : Type u_1} (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (h : i j) :
    (a.set i v)[j]? = a[j]?
    theorem Array.get?_set {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
    (a.set i v)[j]? = if i = j then some v else a[j]?
    theorem Array.get_set {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
    (a.set i v)[j] = if i = j then v else a[j]
    @[simp]
    theorem Array.get_set_ne {α : Type u_1} (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size) (h : i j) :
    (a.set i v)[j] = a[j]
    theorem Array.getElem_setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < (a.setD i v).size) :
    (a.setD i v)[i] = v
    theorem Array.set_set {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) (v' : α) :
    (a.set i v).set i, v' = a.set i v'
    theorem Array.swap_def {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) :
    a.swap i j = (a.set i (a.get j)).set j, (a.get i)
    theorem Array.data_swap {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) :
    (a.swap i j).data = (a.data.set (↑i) (a.get j)).set (↑j) (a.get i)
    theorem Array.get?_swap {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) (k : Nat) :
    (a.swap i j)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]?
    @[simp]
    theorem Array.swapAt_def {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) :
    a.swapAt i v = (a[i], a.set i v)
    theorem Array.swapAt!_def {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
    a.swapAt! i v = (a[i], a.set i, h v)
    @[simp]
    theorem Array.data_pop {α : Type u_1} (a : Array α) :
    a.pop.data = a.data.dropLast
    @[simp]
    theorem Array.pop_empty {α : Type u_1} :
    #[].pop = #[]
    @[simp]
    theorem Array.pop_push {α : Type u_1} {x : α} (a : Array α) :
    (a.push x).pop = a
    @[simp]
    theorem Array.getElem_pop {α : Type u_1} (a : Array α) (i : Nat) (hi : i < a.pop.size) :
    a.pop[i] = a[i]
    theorem Array.eq_empty_of_size_eq_zero {α : Type u_1} {as : Array α} (h : as.size = 0) :
    as = #[]
    theorem Array.eq_push_pop_back_of_size_ne_zero {α : Type u_1} [Inhabited α] {as : Array α} (h : as.size 0) :
    as = as.pop.push as.back
    theorem Array.eq_push_of_size_ne_zero {α : Type u_1} {as : Array α} (h : as.size 0) :
    ∃ (bs : Array α), ∃ (c : α), as = bs.push c
    theorem Array.size_eq_length_data {α : Type u_1} (as : Array α) :
    as.size = as.data.length
    @[simp]
    theorem Array.size_swap! {α : Type u_1} (a : Array α) (i : Nat) (j : Nat) :
    (a.swap! i j).size = a.size
    @[simp]
    theorem Array.size_reverse {α : Type u_1} (a : Array α) :
    a.reverse.size = a.size
    @[irreducible]
    theorem Array.size_reverse.go {α : Type u_1} (as : Array α) (i : Nat) (j : Fin as.size) :
    (Array.reverse.loop as i j).size = as.size
    @[simp]
    theorem Array.size_range {n : Nat} :
    (Array.range n).size = n
    @[simp]
    theorem Array.reverse_data {α : Type u_1} (a : Array α) :
    a.reverse.data = a.data.reverse
    @[irreducible]
    theorem Array.reverse_data.go {α : Type u_1} (a : Array α) (as : Array α) (i : Nat) (j : Nat) (hj : j < as.size) (h : i + j + 1 = a.size) (h₂ : as.size = a.size) (H : ∀ (k : Nat), as.data.get? k = if i k k j then a.data.get? k else a.data.reverse.get? k) (k : Nat) :
    (Array.reverse.loop as i j, hj).data.get? k = a.data.reverse.get? k

    foldl / foldr #

    theorem Array.foldl_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {init : β} (h0 : motive 0 init) {f : βαβ} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) bmotive (i + 1) (f b as[i])) :
    motive as.size (Array.foldl f init as)
    @[irreducible]
    theorem Array.foldl_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {f : βαβ} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) bmotive (i + 1) (f b as[i])) {i : Nat} {j : Nat} {b : β} (h₁ : j as.size) (h₂ : as.size i + j) (H : motive j b) :
    motive as.size (Array.foldlM.loop f as as.size i j b)
    theorem Array.foldr_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {init : β} (h0 : motive as.size init) {f : αββ} (hf : ∀ (i : Fin as.size) (b : β), motive (i + 1) bmotive (↑i) (f as[i] b)) :
    motive 0 (Array.foldr f init as)
    @[irreducible]
    theorem Array.foldr_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {f : αββ} (hf : ∀ (i : Fin as.size) (b : β), motive (i + 1) bmotive (↑i) (f as[i] b)) {i : Nat} {b : β} (hi : i as.size) (H : motive i b) :
    motive 0 (Array.foldrM.fold f as 0 i hi b)

    map #

    @[simp]
    theorem Array.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : αβ} {l : Array α} :
    b Array.map f l ∃ (a : α), a l f a = b
    theorem Array.mapM_eq_mapM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) (arr : Array α) :
    Array.mapM f arr = do let __do_liftList.mapM f arr.data pure { data := __do_lift }
    @[irreducible]
    theorem Array.mapM_map_eq_foldl {α : Type u_1} {β : Type u_2} {b : Array β} (as : Array α) (f : αβ) (i : Nat) :
    Array.mapM.map f as i b = Array.foldl (fun (r : Array β) (a : α) => r.push (f a)) b as i
    theorem Array.map_eq_foldl {α : Type u_1} {β : Type u_2} (as : Array α) (f : αβ) :
    Array.map f as = Array.foldl (fun (r : Array β) (a : α) => r.push (f a)) #[] as
    theorem Array.map_induction {α : Type u_1} {β : Type u_2} (as : Array α) (f : αβ) (motive : NatProp) (h0 : motive 0) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive ip i (f as[i]) motive (i + 1)) :
    motive as.size ∃ (eq : (Array.map f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p i, h (Array.map f as)[i]
    theorem Array.map_spec {α : Type u_1} {β : Type u_2} (as : Array α) (f : αβ) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), p i (f as[i])) :
    ∃ (eq : (Array.map f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p i, h (Array.map f as)[i]
    @[simp]
    theorem Array.getElem_map {α : Type u_1} {β : Type u_2} (f : αβ) (as : Array α) (i : Nat) (h : i < (Array.map f as).size) :
    (Array.map f as)[i] = f as[i]

    mapIdx #

    theorem Array.mapIdx_induction {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin as.sizeαβ) (motive : NatProp) (h0 : motive 0) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive ip i (f i as[i]) motive (i + 1)) :
    motive as.size ∃ (eq : (as.mapIdx f).size = as.size), ∀ (i : Nat) (h : i < as.size), p i, h (as.mapIdx f)[i]
    theorem Array.mapIdx_induction.go {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin as.sizeαβ) (motive : NatProp) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive ip i (f i as[i]) motive (i + 1)) {bs : Array β} {i : Nat} {j : Nat} {h : i + j = as.size} (h₁ : j = bs.size) (h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i, h bs[i]) (hm : motive j) :
    let arr := Array.mapIdxM.map as f i j h bs; motive as.size ∃ (eq : arr.size = as.size), ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1, h arr[i_1]
    theorem Array.mapIdx_spec {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin as.sizeαβ) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), p i (f i as[i])) :
    ∃ (eq : (as.mapIdx f).size = as.size), ∀ (i : Nat) (h : i < as.size), p i, h (as.mapIdx f)[i]
    @[simp]
    theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin a.sizeαβ) :
    (a.mapIdx f).size = a.size
    @[simp]
    theorem Array.size_zipWithIndex {α : Type u_1} (as : Array α) :
    as.zipWithIndex.size = as.size
    @[simp]
    theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin a.sizeαβ) (i : Nat) (h : i < (a.mapIdx f).size) :
    (a.mapIdx f)[i] = f i, a[i]

    modify #

    @[simp]
    theorem Array.size_modify {α : Type u_1} (a : Array α) (i : Nat) (f : αα) :
    (a.modify i f).size = a.size
    theorem Array.get_modify {α : Type u_1} {f : αα} {arr : Array α} {x : Nat} {i : Nat} (h : i < arr.size) :
    (arr.modify x f).get i, = if x = i then f (arr.get i, h) else arr.get i, h

    filter #

    @[simp]
    theorem Array.filter_data {α : Type u_1} (p : αBool) (l : Array α) :
    (Array.filter p l).data = List.filter p l.data
    @[simp]
    theorem Array.filter_filter {α : Type u_1} {p : αBool} (q : αBool) (l : Array α) :
    Array.filter p (Array.filter q l) = Array.filter (fun (a : α) => decide (p a = true q a = true)) l
    @[simp]
    theorem Array.mem_filter :
    ∀ {α : Type u_1} {x : α} {p : αBool} {as : Array α}, x Array.filter p as x as p x = true
    theorem Array.mem_of_mem_filter {α : Type u_1} {p : αBool} {a : α} {l : Array α} (h : a Array.filter p l) :
    a l

    filterMap #

    @[simp]
    theorem Array.filterMap_data {α : Type u_1} {β : Type u_2} (f : αOption β) (l : Array α) :
    (Array.filterMap f l).data = List.filterMap f l.data
    @[simp]
    theorem Array.mem_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (l : Array α) {b : β} :
    b Array.filterMap f l ∃ (a : α), a l f a = some b

    empty #

    theorem Array.size_empty {α : Type u_1} :
    #[].size = 0
    theorem Array.empty_data {α : Type u_1} :
    #[].data = []

    append #

    theorem Array.push_eq_append_singleton {α : Type u_1} (as : Array α) (x : α) :
    as.push x = as ++ #[x]
    @[simp]
    theorem Array.mem_append {α : Type u_1} {a : α} {s : Array α} {t : Array α} :
    a s ++ t a s a t
    theorem Array.size_append {α : Type u_1} (as : Array α) (bs : Array α) :
    (as ++ bs).size = as.size + bs.size
    theorem Array.get_append_left {α : Type u_1} {i : Nat} {as : Array α} {bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
    (as ++ bs)[i] = as[i]
    theorem Array.get_append_right {α : Type u_1} {i : Nat} {as : Array α} {bs : Array α} {h : i < (as ++ bs).size} (hle : as.size i) (hlt : optParam (i - as.size < bs.size) ) :
    (as ++ bs)[i] = bs[i - as.size]
    @[simp]
    theorem Array.append_nil {α : Type u_1} (as : Array α) :
    as ++ #[] = as
    @[simp]
    theorem Array.nil_append {α : Type u_1} (as : Array α) :
    #[] ++ as = as
    theorem Array.append_assoc {α : Type u_1} (as : Array α) (bs : Array α) (cs : Array α) :
    as ++ bs ++ cs = as ++ (bs ++ cs)

    extract #

    theorem Array.extract_loop_zero {α : Type u_1} (as : Array α) (bs : Array α) (start : Nat) :
    Array.extract.loop as 0 start bs = bs
    theorem Array.extract_loop_succ {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (h : start < as.size) :
    Array.extract.loop as (size + 1) start bs = Array.extract.loop as size (start + 1) (bs.push as[start])
    theorem Array.extract_loop_of_ge {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (h : start as.size) :
    Array.extract.loop as size start bs = bs
    theorem Array.extract_loop_eq_aux {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) :
    Array.extract.loop as size start bs = bs ++ Array.extract.loop as size start #[]
    theorem Array.extract_loop_eq {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (h : start + size as.size) :
    Array.extract.loop as size start bs = bs ++ as.extract start (start + size)
    theorem Array.size_extract_loop {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) :
    (Array.extract.loop as size start bs).size = bs.size + min size (as.size - start)
    @[simp]
    theorem Array.size_extract {α : Type u_1} (as : Array α) (start : Nat) (stop : Nat) :
    (as.extract start stop).size = min stop as.size - start
    theorem Array.get_extract_loop_lt_aux {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hlt : i < bs.size) :
    i < (Array.extract.loop as size start bs).size
    theorem Array.get_extract_loop_lt {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hlt : i < bs.size) (h : optParam (i < (Array.extract.loop as size start bs).size) ) :
    (Array.extract.loop as size start bs)[i] = bs[i]
    theorem Array.get_extract_loop_ge_aux {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hge : i bs.size) (h : i < (Array.extract.loop as size start bs).size) :
    start + i - bs.size < as.size
    theorem Array.get_extract_loop_ge {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hge : i bs.size) (h : i < (Array.extract.loop as size start bs).size) (h' : optParam (start + i - bs.size < as.size) ) :
    (Array.extract.loop as size start bs)[i] = as[start + i - bs.size]
    theorem Array.get_extract_aux {α : Type u_1} {i : Nat} {as : Array α} {start : Nat} {stop : Nat} (h : i < (as.extract start stop).size) :
    start + i < as.size
    @[simp]
    theorem Array.get_extract {α : Type u_1} {i : Nat} {as : Array α} {start : Nat} {stop : Nat} (h : i < (as.extract start stop).size) :
    (as.extract start stop)[i] = as[start + i]
    @[simp]
    theorem Array.extract_all {α : Type u_1} (as : Array α) :
    as.extract 0 as.size = as
    theorem Array.extract_empty_of_stop_le_start {α : Type u_1} (as : Array α) {start : Nat} {stop : Nat} (h : stop start) :
    as.extract start stop = #[]
    theorem Array.extract_empty_of_size_le_start {α : Type u_1} (as : Array α) {start : Nat} {stop : Nat} (h : as.size start) :
    as.extract start stop = #[]
    @[simp]
    theorem Array.extract_empty {α : Type u_1} (start : Nat) (stop : Nat) :
    #[].extract start stop = #[]

    any #

    @[irreducible]
    theorem Array.anyM_loop_iff_exists {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) (h : stop as.size) :
    Array.anyM.loop p as stop h start = true ∃ (i : Fin as.size), start i i < stop p as[i] = true
    theorem Array.any_iff_exists {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) :
    as.any p start stop = true ∃ (i : Fin as.size), start i i < stop p as[i] = true
    theorem Array.any_eq_true {α : Type u_1} (p : αBool) (as : Array α) :
    as.any p = true ∃ (i : Fin as.size), p as[i] = true
    theorem Array.any_def {α : Type u_1} {p : αBool} (as : Array α) :
    as.any p = as.data.any p

    all #

    theorem Array.all_eq_not_any_not {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) :
    as.all p start stop = !as.any (fun (x : α) => !p x) start stop
    theorem Array.all_iff_forall {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) :
    as.all p start stop = true ∀ (i : Fin as.size), start i i < stopp as[i] = true
    theorem Array.all_eq_true {α : Type u_1} (p : αBool) (as : Array α) :
    as.all p = true ∀ (i : Fin as.size), p as[i] = true
    theorem Array.all_def {α : Type u_1} {p : αBool} (as : Array α) :
    as.all p = as.data.all p
    theorem Array.all_eq_true_iff_forall_mem {α : Type u_1} {p : αBool} {l : Array α} :
    l.all p = true ∀ (x : α), x lp x = true

    contains #

    theorem Array.contains_def {α : Type u_1} [DecidableEq α] {a : α} {as : Array α} :
    as.contains a = true a as
    instance Array.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (a : α) (as : Array α) :
    Decidable (a as)
    Equations

    swap #

    @[simp]
    theorem Array.get_swap_right {α : Type u_1} (a : Array α) {i : Fin a.size} {j : Fin a.size} :
    (a.swap i j)[j] = a[i]
    @[simp]
    theorem Array.get_swap_left {α : Type u_1} (a : Array α) {i : Fin a.size} {j : Fin a.size} :
    (a.swap i j)[i] = a[j]
    @[simp]
    theorem Array.get_swap_of_ne {α : Type u_1} {p : Nat} (a : Array α) {i : Fin a.size} {j : Fin a.size} (hp : p < a.size) (hi : p i) (hj : p j) :
    (a.swap i j)[p] = a[p]
    theorem Array.get_swap {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) (k : Nat) (hk : k < a.size) :
    (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]
    theorem Array.get_swap' {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
    (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]
    @[simp]
    theorem Array.swap_swap {α : Type u_1} (a : Array α) {i : Fin a.size} {j : Fin a.size} :
    (a.swap i j).swap i, j, = a
    theorem Array.swap_comm {α : Type u_1} (a : Array α) {i : Fin a.size} {j : Fin a.size} :
    a.swap i j = a.swap j i