Lemmas about List.toArray.

We prefer to pull List.toArray outwards past Array operations.

@[simp]

theorem Array.toList_set {α : Type u_1} (xs : Array α) (i : Nat) (x : α) (h : i < xs.size) : (xs.set i x h).toList = xs.toList.set i x

theorem Array.swap_def {α : Type u_1} (xs : Array α) (i j : Nat) (hi : i < xs.size) (hj : j < xs.size) : xs.swap i j hi hj = (xs.set i xs[j] hi).set j xs[i] ⋯

@[simp]

theorem Array.toList_swap {α : Type u_1} (xs : Array α) (i j : Nat) (hi : i < xs.size) (hj : j < xs.size) : (xs.swap i j hi hj).toList = (xs.toList.set i xs[j]).set j xs[i]

theorem List.toArray_inj {α : Type u_1} {as bs : List α} (h : as.toArray = bs.toArray) : as = bs

theorem List.toArray_eq_iff {α : Type u_1} {as : List α} {bs : Array α} : as.toArray = bs ↔ as = bs.toList

theorem List.eq_toArray_iff {α : Type u_1} {as : Array α} {bs : List α} : as = bs.toArray ↔ as.toList = bs

@[simp]

theorem List.size_toArrayAux {α : Type u_1} {as : List α} {xs : Array α} : (as.toArrayAux xs).size = xs.size + as.length

theorem List.toArray_cons {α : Type u_1} (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArray

@[simp]

theorem List.push_toArray {α : Type u_1} (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray

@[simp]

theorem List.push_toArray_fun {α : Type u_1} (l : List α) : l.toArray.push = fun (a : α) => (l ++ [a]).toArray

Unapplied variant of push_toArray, useful for monadic reasoning.

@[simp]

theorem List.isEmpty_toArray {α : Type u_1} (l : List α) : l.toArray.isEmpty = l.isEmpty

@[simp]

theorem List.toArray_singleton {α : Type u_1} (a : α) : (List.singleton a).toArray = Array.singleton a

@[simp]

theorem List.back!_toArray {α : Type u_1} [Inhabited α] (l : List α) : l.toArray.back! = l.getLast!

@[simp]

theorem List.back?_toArray {α : Type u_1} (l : List α) : l.toArray.back? = l.getLast?

@[simp]

theorem List.back_toArray {α : Type u_1} (l : List α) (h : 0 < l.toArray.size) : l.toArray.back h = l.getLast ⋯

@[simp]

theorem Array.getLast!_toList {α : Type u_1} [Inhabited α] (xs : Array α) : xs.toList.getLast! = xs.back!

@[simp]

theorem Array.getLast?_toList {α : Type u_1} (xs : Array α) : xs.toList.getLast? = xs.back?

@[simp]

theorem Array.getLast_toList {α : Type u_1} (xs : Array α) (h : xs.toList ≠ []) : xs.toList.getLast h = xs.back ⋯

@[simp]

theorem List.set_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) (h : i < l.length) : l.toArray.set i a h = (l.set i a).toArray

@[simp]

theorem List.forIn'_loop_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat) (h : i ≤ l.length) (b : β) : Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun (a : α) (m : a ∈ drop (l.length - i) l) (b : β) => f a ⋯ b

@[simp]

theorem List.forIn'_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) : forIn' l.toArray b f = forIn' l b fun (a : α) (m : a ∈ l) (b : β) => f a ⋯ b

@[simp]

theorem List.forIn_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : forIn l.toArray b f = forIn l b f

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 = 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 = foldlM f init l

theorem List.foldr_toArray {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α) : Array.foldr f init l.toArray = foldr f init l

theorem List.foldl_toArray {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (l : List α) : Array.foldl f init l.toArray = 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 = 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 = 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.

@[simp]

theorem List.forM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (l : List α) (f : α → m PUnit) : forM l.toArray f = 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 = 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 = foldl f init l

Variant of foldl_toArray with a side condition for the stop argument.

@[simp]

theorem List.sum_toArray {α : Type u_1} [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum

@[simp]

theorem List.prod_toArray {α : Type u_1} [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod

@[simp]

theorem List.append_toArray {α : Type u_1} (l₁ l₂ : List α) : l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray

@[simp]

theorem List.push_append_toArray {α : Type u_1} {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a :: bs).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 = findSomeM? f l

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 = 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 = findM? f l.reverse

@[simp]

theorem List.findM?_toArray {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : Array.findM? f l.toArray = findM? f l

@[simp]

theorem List.findSome?_toArray {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : Array.findSome? f l.toArray = findSome? f l

@[simp]

theorem List.find?_toArray {α : Type u_1} (f : α → Bool) (l : List α) : Array.find? f l.toArray = find? f l

@[simp]

theorem List.findFinIdx?_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.findFinIdx? p l.toArray = findFinIdx? p l

@[simp]

theorem List.findIdx?_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.findIdx? p l.toArray = findIdx? p l

@[simp]

theorem List.finIdxOf?_toArray {α : Type u_1} [BEq α] (a : α) (l : List α) : l.toArray.finIdxOf? a = finIdxOf? a l

@[simp]

theorem List.idxOf?_toArray {α : Type u_1} [BEq α] (a : α) (l : List α) : l.toArray.idxOf? a = idxOf? a l

@[simp]

theorem List.findIdx_toArray {α : Type u_1} {as : List α} {p : α → Bool} : Array.findIdx p as.toArray = findIdx p as

@[simp]

theorem List.idxOf_toArray {α : Type u_1} [BEq α] {as : List α} {a : α} : Array.idxOf a as.toArray = idxOf a as

theorem List.isPrefixOfAux_toArray_succ {α : Type u_1} [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) = l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ i

theorem List.isPrefixOfAux_toArray_succ' {α : Type u_1} [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) = (drop (i + 1) l₁).toArray.isPrefixOfAux (drop (i + 1) l₂).toArray ⋯ 0

theorem List.isPrefixOfAux_toArray_zero {α : Type u_1} [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) : l₁.toArray.isPrefixOfAux l₂.toArray hle 0 = l₁.isPrefixOf l₂

@[simp]

theorem List.isPrefixOf_toArray {α : Type u_1} [BEq α] (l₁ l₂ : List α) : l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂

theorem List.zipWithMAux_toArray_succ {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [Monad m] (as : List α) (bs : List β) (f : α → β → m γ) (i : Nat) (xs : Array γ) : as.toArray.zipWithMAux bs.toArray f (i + 1) xs = as.tail.toArray.zipWithMAux bs.tail.toArray f i xs

theorem List.zipWithMAux_toArray_succ' {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [Monad m] (as : List α) (bs : List β) (f : α → β → m γ) (i : Nat) (xs : Array γ) : as.toArray.zipWithMAux bs.toArray f (i + 1) xs = (drop (i + 1) as).toArray.zipWithMAux (drop (i + 1) bs).toArray f 0 xs

theorem List.zipWithMAux_toArray_zero {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (f : α → β → m γ) (as : List α) (bs : List β) (xs : Array γ) : as.toArray.zipWithMAux bs.toArray f 0 xs = do let __do_lift ← zipWithM f as bs pure (xs ++ __do_lift.toArray)

@[simp]

theorem List.zipWith_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : α → β → γ) : Array.zipWith f as.toArray bs.toArray = (zipWith f as bs).toArray

@[simp]

theorem List.zip_toArray {α : Type u_1} {β : Type u_2} (as : List α) (bs : List β) : as.toArray.zip bs.toArray = (as.zip bs).toArray

@[simp]

theorem List.zipWithAll_toArray {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (as : List α) (bs : List β) : Array.zipWithAll f as.toArray bs.toArray = (zipWithAll f as bs).toArray

@[simp]

theorem List.zipWithM_toArray {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (f : α → β → m γ) (as : List α) (bs : List β) : Array.zipWithM f as.toArray bs.toArray = do let __do_lift ← zipWithM f as bs pure __do_lift.toArray

@[simp]

theorem List.toArray_appendList {α : Type u_1} (l₁ l₂ : List α) : l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray

@[simp]

theorem List.pop_toArray {α : Type u_1} (l : List α) : l.toArray.pop = l.dropLast.toArray

@[simp]

theorem List.takeWhile_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.takeWhile p l.toArray = (takeWhile p l).toArray

@[simp]

theorem List.popWhile_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.popWhile p l.toArray = (dropWhile p l.reverse).reverse.toArray

@[simp]

theorem List.setIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) : l.toArray.setIfInBounds i a = (l.set i a).toArray

@[simp]

theorem List.toArray_replicate {α : Type u_1} (n : Nat) (v : α) : (replicate n v).toArray = Array.replicate n v

theorem Array.replicate_eq_toArray_replicate {n : Nat} {α✝ : Type u_1} {v : α✝} : replicate n v = (List.replicate n v).toArray

@[simp]

theorem Array.flatMap_empty {α : Type u_1} {β : Type u_2} (f : α → Array β) : flatMap f #[] = #[]

theorem List.flatMap_toArray_cons {α : Type u_1} {β : Type u_2} (f : α → Array β) (a : α) (as : List α) : Array.flatMap f (a :: as).toArray = f a ++ Array.flatMap f as.toArray

@[simp]

theorem List.flatMap_toArray {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : List α) : Array.flatMap f as.toArray = (flatMap (fun (a : α) => (f a).toList) as).toArray

@[simp]

theorem List.swap_toArray {α : Type u_1} (l : List α) (i j : Nat) {hi : i < l.toArray.size} {hj : j < l.toArray.size} : l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray

@[simp]

theorem List.eraseIdx_toArray {α : Type u_1} (l : List α) (i : Nat) (h : i < l.toArray.size) : l.toArray.eraseIdx i h = (l.eraseIdx i).toArray

@[simp]

theorem List.eraseIdxIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) : l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray

@[simp]

theorem List.eraseP_toArray {α : Type u_1} {as : List α} {p : α → Bool} : as.toArray.eraseP p = (eraseP p as).toArray

@[simp]

theorem List.erase_toArray {α : Type u_1} [BEq α] {as : List α} {a : α} : as.toArray.erase a = (as.erase a).toArray

@[simp]

theorem List.insertIdx_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size) : l.toArray.insertIdx i a h = (l.insertIdx i a).toArray

@[simp]

theorem List.insertIdxIfInBounds_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) : l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray

@[simp]

theorem List.replace_toArray {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a b : α) : l.toArray.replace a b = (l.replace a b).toArray

@[simp]

theorem List.leftpad_toArray {α : Type u_1} (n : Nat) (a : α) (l : List α) : Array.leftpad n a l.toArray = (leftpad n a l).toArray

@[simp]

theorem List.rightpad_toArray {α : Type u_1} (n : Nat) (a : α) (l : List α) : Array.rightpad n a l.toArray = (rightpad n a l).toArray