Lemmas about List.toArray. #
We prefer to pull List.toArray outwards past Array operations.
@[simp]
Unapplied variant of push_toArray, useful for monadic reasoning.
@[simp]
@[simp]
theorem
List.toArray_singleton
{α : Type u_1}
(a : α)
:
(List.singleton a).toArray = Array.singleton a
theorem
List.foldrM_toArray
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → β → m β)
(init : β)
(l : List α)
:
Array.foldrM f init l.toArray = List.foldrM f init l
theorem
List.foldlM_toArray
{m : Type u_1 → Type u_2}
{β : Type u_1}
{α : Type u_3}
[Monad m]
(f : β → α → m β)
(init : β)
(l : List α)
:
Array.foldlM f init l.toArray = List.foldlM f init l
theorem
List.foldr_toArray
{α : Type u_1}
{β : Type u_2}
(f : α → β → β)
(init : β)
(l : List α)
:
Array.foldr f init l.toArray = List.foldr f init l
theorem
List.foldl_toArray
{β : Type u_1}
{α : Type u_2}
(f : β → α → β)
(init : β)
(l : List α)
:
Array.foldl f init l.toArray = List.foldl f init l
@[simp]
theorem
List.foldrM_toArray'
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{start : Nat}
[Monad m]
(f : α → β → m β)
(init : β)
(l : List α)
(h : start = l.toArray.size)
:
Array.foldrM f init l.toArray start = List.foldrM f init l
Variant of foldrM_toArray with a side condition for the start argument.
@[simp]
theorem
List.foldlM_toArray'
{m : Type u_1 → Type u_2}
{β : Type u_1}
{α : Type u_3}
{stop : Nat}
[Monad m]
(f : β → α → m β)
(init : β)
(l : List α)
(h : stop = l.toArray.size)
:
Array.foldlM f init l.toArray 0 stop = List.foldlM f init l
Variant of foldlM_toArray with a side condition for the stop argument.
@[simp]
theorem
List.forM_toArray'
{m : Type u_1 → Type u_2}
{α : Type u_3}
{stop : Nat}
[Monad m]
(l : List α)
(f : α → m PUnit)
(h : stop = l.toArray.size)
:
Array.forM f l.toArray 0 stop = l.forM f
Variant of forM_toArray with a side condition for the stop argument.
theorem
List.forM_toArray
{m : Type u_1 → Type u_2}
{α : Type u_3}
[Monad m]
(l : List α)
(f : α → m PUnit)
:
Array.forM f l.toArray = l.forM f
@[simp]
theorem
List.foldr_toArray'
{α : Type u_1}
{β : Type u_2}
{start : Nat}
(f : α → β → β)
(init : β)
(l : List α)
(h : start = l.toArray.size)
:
Array.foldr f init l.toArray start = List.foldr f init l
Variant of foldr_toArray with a side condition for the start argument.
@[simp]
theorem
List.foldl_toArray'
{β : Type u_1}
{α : Type u_2}
{stop : Nat}
(f : β → α → β)
(init : β)
(l : List α)
(h : stop = l.toArray.size)
:
Array.foldl f init l.toArray 0 stop = List.foldl f init l
Variant of foldl_toArray with a side condition for the stop argument.
@[simp]
theorem
List.foldl_push
{α : Type u_1}
{l : List α}
{as : Array α}
:
List.foldl Array.push as l = as ++ l.toArray
@[simp]
theorem
List.foldr_push
{α : Type u_1}
{l : List α}
{as : Array α}
:
List.foldr (fun (a : α) (b : Array α) => b.push a) as l = as ++ l.reverse.toArray
@[simp]
theorem
List.findSomeM?_toArray
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → m (Option β))
(l : List α)
:
Array.findSomeM? f l.toArray = List.findSomeM? f l
theorem
List.findSomeRevM?_find_toArray
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → m (Option β))
(l : List α)
(i : Nat)
(h : i ≤ l.toArray.size)
:
Array.findSomeRevM?.find f l.toArray i h = List.findSomeM? f (List.take i l).reverse
theorem
List.findSomeRevM?_toArray
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → m (Option β))
(l : List α)
:
Array.findSomeRevM? f l.toArray = List.findSomeM? f l.reverse
theorem
List.findRevM?_toArray
{m : Type → Type u_1}
{α : Type}
[Monad m]
[LawfulMonad m]
(f : α → m Bool)
(l : List α)
:
Array.findRevM? f l.toArray = List.findM? f l.reverse
@[simp]
theorem
List.findM?_toArray
{m : Type → Type}
{α : Type}
[Monad m]
[LawfulMonad m]
(f : α → m Bool)
(l : List α)
:
Array.findM? f l.toArray = List.findM? f l
@[simp]
theorem
List.findSome?_toArray
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : List α)
:
Array.findSome? f l.toArray = List.findSome? f l
@[simp]
theorem
List.find?_toArray
{α : Type u_1}
(f : α → Bool)
(l : List α)
:
Array.find? f l.toArray = List.find? f l
@[simp]
theorem
List.zipWith_toArray
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(as : List α)
(bs : List β)
(f : α → β → γ)
:
as.toArray.zipWith bs.toArray f = (List.zipWith f as bs).toArray
@[irreducible]
@[simp]
@[irreducible]
theorem
List.takeWhile_go_succ
{α : Type u_1}
{r : Array α}
(p : α → Bool)
(a : α)
(l : List α)
(i : Nat)
:
Array.takeWhile.go p (a :: l).toArray (i + 1) r = Array.takeWhile.go p l.toArray i r
theorem
List.takeWhile_go_toArray
{α : Type u_1}
{r : Array α}
(p : α → Bool)
(l : List α)
(i : Nat)
:
Array.takeWhile.go p l.toArray i r = r ++ (List.takeWhile p (List.drop i l)).toArray
@[simp]
theorem
List.takeWhile_toArray
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
Array.takeWhile p l.toArray = (List.takeWhile p l).toArray
@[simp]
theorem
List.toArray_replicate
{α : Type u_1}
(n : Nat)
(v : α)
:
(List.replicate n v).toArray = mkArray n v
@[reducible, inline, deprecated List.toArray_replicate (since := "2024-12-13")]
abbrev
Array.mkArray_eq_toArray_replicate
{α : Type u_1}
(n : Nat)
(v : α)
:
(List.replicate n v).toArray = mkArray n v