Bootstrapping theorems about arrays #
This file contains some theorems about Array
and List
needed for Init.Data.List.Impl
.
@[simp]
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 0 = 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 0 = 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 arr.size = 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 arr.size = 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 arr.size = List.foldr f init arr.data
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.push a).size = do
let init ← f a init
Array.foldrM f init arr arr.size
@[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 init ← f a init
Array.foldrM f init arr arr.size
theorem
Array.foldr_push
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(init : β)
(arr : Array α)
(a : α)
:
Array.foldr f init (arr.push a) (arr.push a).size = Array.foldr f (f a init) arr arr.size
@[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 arr.size
@[inline]
A more efficient version of arr.toList.reverse
.
Equations
- arr.toListRev = Array.foldl (fun (l : List α) (t : α) => t :: l) [] arr 0
Instances For
@[simp]
@[simp]
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 0
@[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.anyM_eq_anyM_loop
{m : Type → Type 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
get #
set #
setD #
ofFn #
@[simp]
@[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 #
@[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]
@[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) b → motive (↑i + 1) (f b as[i]))
:
motive as.size (Array.foldl f init as 0)
@[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) b → motive (↑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) b → motive (↑i) (f as[i] b))
:
motive 0 (Array.foldr f init as as.size)
@[irreducible]
map #
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_lift ← List.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 0
mapIdx #
theorem
Array.mapIdx_induction.go
{α : Type u_1}
{β : Type u_2}
(as : Array α)
(f : Fin as.size → α → β)
(motive : Nat → Prop)
(p : Fin as.size → β → Prop)
(hs : ∀ (i : Fin as.size), motive ↑i → p 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]
@[simp]
modify #
filter #
@[simp]
theorem
Array.filter_data
{α : Type u_1}
(p : α → Bool)
(l : Array α)
:
(Array.filter p l 0).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 0) 0 = Array.filter (fun (a : α) => decide (p a = true ∧ q a = true)) l 0
theorem
Array.mem_of_mem_filter
{α : Type u_1}
{p : α → Bool}
{a : α}
{l : Array α}
(h : a ∈ Array.filter p l 0)
:
a ∈ l
filterMap #
@[simp]
theorem
Array.filterMap_data
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : Array α)
:
(Array.filterMap f l 0).data = List.filterMap f l.data
empty #
append #
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.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
{α : 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]
any #
all #
contains #
instance
Array.instDecidableMemOfDecidableEq
{α : Type u_1}
[DecidableEq α]
(a : α)
(as : Array α)
:
Equations
- Array.instDecidableMemOfDecidableEq a as = decidable_of_iff (as.contains a = true) ⋯