# Lemmas about `Array.extract` #

This file follows the contents of `Init.Data.List.TakeDrop` and `Init.Data.List.Nat.TakeDrop`.

### extract #

source
@[simp]
theorem Array.extract_of_size_lt {α : Type u_1} {as : Array α} {i j : Nat} (h : as.size < j) :
as.extract i j = as.extract i
source
theorem Array.size_extract_le {α : Type u_1} {as : Array α} {i j : Nat} :
(as.extract i j).size ≤ j - i
source
theorem Array.size_extract_le' {α : Type u_1} {as : Array α} {i j : Nat} :
(as.extract i j).size ≤ as.size - i
source
theorem Array.size_extract_of_le {α : Type u_1} {as : Array α} {i j : Nat} (h : j ≤ as.size) :
(as.extract i j).size = j - i
source
theorem Array.extract_push {α : Type u_1} {as : Array α} {b : α} {start stop : Nat} :
(as.push b).extract start stop = if stop ≤ as.size then as.extract start stop else if start ≤ as.size then (as.extract start).push b else #[]
source
@[simp]
theorem Array.extract_push_of_le {α : Type u_1} {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
(as.push b).extract start stop = as.extract start stop
source
@[simp]
theorem Array.extract_eq_pop {α : Type u_1} {as : Array α} {stop : Nat} (h : stop = as.size - 1) :
as.extract 0 stop = as.pop
source
@[simp]
theorem Array.extract_append_extract {α : Type u_1} {as : Array α} {i j k : Nat} :
as.extract i j ++ as.extract j k = as.extract (min i j) (max j k)
source
@[simp]
theorem Array.extract_eq_empty_iff {α : Type u_1} {i j : Nat} {as : Array α} :
as.extract i j = #[] ↔ min j as.size ≤ i
source
theorem Array.extract_eq_empty_of_le {α : Type u_1} {j i : Nat} {as : Array α} (h : min j as.size ≤ i) :
as.extract i j = #[]
source
theorem Array.lt_of_extract_ne_empty {α : Type u_1} {i j : Nat} {as : Array α} (h : as.extract i j ≠ #[]) :
i < min j as.size
source
@[simp]
theorem Array.extract_eq_self_iff {α : Type u_1} {i j : Nat} {as : Array α} :
as.extract i j = as ↔ as.size = 0 ∨ i = 0 ∧ as.size ≤ j
source
theorem Array.extract_eq_self_of_le {α : Type u_1} {j : Nat} {as : Array α} (h : as.size ≤ j) :
as.extract 0 j = as
source
theorem Array.le_of_extract_eq_self {α : Type u_1} {i j : Nat} {as : Array α} (h : as.extract i j = as) :
as.size ≤ j
source
@[simp]
theorem Array.extract_size_left {α : Type u_1} {j : Nat} {as : Array α} :
as.extract as.size j = #[]
source
@[simp]
theorem Array.push_extract_getElem {α : Type u_1} {as : Array α} {i j : Nat} (h : j < as.size) :
(as.extract i j).push as[j] = as.extract (min i j) (j + 1)
source
theorem Array.extract_succ_right {α : Type u_1} {as : Array α} {i j : Nat} (w : i < j + 1) (h : j < as.size) :
as.extract i (j + 1) = (as.extract i j).push as[j]
source
theorem Array.extract_sub_one {α : Type u_1} {as : Array α} {i j : Nat} (h : j < as.size) :
as.extract i (j - 1) = (as.extract i j).pop
source
@[simp]
theorem Array.getElem?_extract_of_lt {α : Type u_1} {as : Array α} {i j k : Nat} (h : k < min j as.size - i) :
(as.extract i j)[k]? = some as[i + k]
source
theorem Array.getElem?_extract_of_succ {α : Type u_1} {as : Array α} {j : Nat} :
(as.extract 0 (j + 1))[j]? = as[j]?
source
@[simp]
theorem Array.extract_extract {α : Type u_1} {as : Array α} {i j k l : Nat} :
(as.extract i j).extract k l = as.extract (i + k) (min (i + l) j)
source
theorem Array.extract_eq_empty_of_eq_empty {α : Type u_1} {as : Array α} {i j : Nat} (h : as = #[]) :
as.extract i j = #[]
source
theorem Array.ne_empty_of_extract_ne_empty {α : Type u_1} {as : Array α} {i j : Nat} (h : as.extract i j ≠ #[]) :
as ≠ #[]
source
theorem Array.extract_set {α : Type u_1} {as : Array α} {i j k : Nat} (h : k < as.size) {a : α} :
(as.set k a h).extract i j = if x : k < i then as.extract i j else if x_1 : k < min j as.size then (as.extract i j).set (k - i) a ⋯ else as.extract i j
source
theorem Array.set_extract {α : Type u_1} {as : Array α} {i j k : Nat} (h : k < (as.extract i j).size) {a : α} :
(as.extract i j).set k a h = (as.set (i + k) a ⋯).extract i j
source
@[simp]
theorem Array.extract_append {α : Type u_1} {as bs : Array α} {i j : Nat} :
(as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size)
source
theorem Array.extract_append_left {α : Type u_1} {as bs : Array α} :
(as ++ bs).extract 0 as.size = as.extract
source
theorem Array.extract_append_right {α : Type u_1} {i : Nat} {as bs : Array α} :
(as ++ bs).extract as.size (as.size + i) = bs.extract 0 i
source
@[simp]
theorem Array.map_extract {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {as : Array α} {i j : Nat} :
map f (as.extract i j) = (map f as).extract i j
source
@[simp]
theorem Array.extract_replicate {α : Type u_1} {a : α} {n i j : Nat} :
(replicate n a).extract i j = replicate (min j n - i) a
source
@[reducible, inline, deprecated Array.extract_replicate (since := "2025-03-18")]
abbrev Array.extract_mkArray {α : Type u_1} {a : α} {n i j : Nat} :
(replicate n a).extract i j = replicate (min j n - i) a
Equations

- @Array.extract_mkArray = @Array.extract_replicate

Instances For

source
theorem Array.extract_eq_extract_right {α : Type u_1} {as : Array α} {i j j' : Nat} :
as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i)
source
theorem Array.extract_eq_extract_left {α : Type u_1} {as : Array α} {i i' j : Nat} :
as.extract i j = as.extract i' j ↔ min j as.size - i = min j as.size - i'
source
theorem Array.extract_add_left {α : Type u_1} {as : Array α} {i j k : Nat} :
as.extract (i + j) k = (as.extract i k).extract j (k - i)
source
theorem Array.mem_extract_iff_getElem {α : Type u_1} {as : Array α} {a : α} {i j : Nat} :
a ∈ as.extract i j ↔ ∃ (k : Nat), ∃ (hm : k < min j as.size - i), as[i + k] = a
source
theorem Array.set_eq_push_extract_append_extract {α : Type u_1} {as : Array α} {i : Nat} (h : i < as.size) {a : α} :
as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1)
source
theorem Array.extract_reverse {α : Type u_1} {as : Array α} {i j : Nat} :
as.reverse.extract i j = (as.extract (as.size - j) (as.size - i)).reverse
source
theorem Array.reverse_extract {α : Type u_1} {as : Array α} {i j : Nat} :
(as.extract i j).reverse = as.reverse.extract (as.size - j) (as.size - i)

### takeWhile #

source
theorem Array.takeWhile_map {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {as : Array α} :
takeWhile p (map f as) = map f (takeWhile (p ∘ f) as)
source
theorem Array.popWhile_map {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {as : Array α} :
popWhile p (map f as) = map f (popWhile (p ∘ f) as)
source
theorem Array.takeWhile_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {as : Array α} :
takeWhile p (filterMap f as) = filterMap f (takeWhile (fun (a : α) => Option.all p (f a)) as)
source
theorem Array.popWhile_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {as : Array α} :
popWhile p (filterMap f as) = filterMap f (popWhile (fun (a : α) => Option.all p (f a)) as)
source
theorem Array.takeWhile_filter {α : Type u_1} {p q : α → Bool} {as : Array α} :
takeWhile q (filter p as) = filter p (takeWhile (fun (a : α) => !p a || q a) as)
source
theorem Array.popWhile_filter {α : Type u_1} {p q : α → Bool} {as : Array α} :
popWhile q (filter p as) = filter p (popWhile (fun (a : α) => !p a || q a) as)
source
theorem Array.takeWhile_append {α : Type u_1} {p : α → Bool} {xs ys : Array α} :
takeWhile p (xs ++ ys) = if (takeWhile p xs).size = xs.size then xs ++ takeWhile p ys else takeWhile p xs
source
@[simp]
theorem Array.takeWhile_append_of_pos {α : Type u_1} {p : α → Bool} {xs ys : Array α} (h : ∀ (a : α), a ∈ xs → p a = true) :
takeWhile p (xs ++ ys) = xs ++ takeWhile p ys
source
theorem Array.popWhile_append {α : Type u_1} {p : α → Bool} {xs ys : Array α} :
popWhile p (xs ++ ys) = if (popWhile p ys).isEmpty = true then popWhile p xs else xs ++ popWhile p ys
source
@[simp]
theorem Array.popWhile_append_of_pos {α : Type u_1} {p : α → Bool} {xs ys : Array α} (h : ∀ (a : α), a ∈ ys → p a = true) :
popWhile p (xs ++ ys) = popWhile p xs
source
@[simp]
theorem Array.takeWhile_replicate_eq_filter {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
takeWhile p (replicate n a) = filter p (replicate n a)
source
@[reducible, inline, deprecated Array.takeWhile_replicate_eq_filter (since := "2025-03-18")]
abbrev Array.takeWhile_mkArray_eq_filter {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
takeWhile p (replicate n a) = filter p (replicate n a)
Equations

- @Array.takeWhile_mkArray_eq_filter = @Array.takeWhile_replicate_eq_filter

Instances For

source
theorem Array.takeWhile_replicate {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
takeWhile p (replicate n a) = if p a = true then replicate n a else #[]
source
@[reducible, inline, deprecated Array.takeWhile_replicate (since := "2025-03-18")]
abbrev Array.takeWhile_mkArray {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
takeWhile p (replicate n a) = if p a = true then replicate n a else #[]
Equations

- @Array.takeWhile_mkArray = @Array.takeWhile_replicate

Instances For

source
@[simp]
theorem Array.popWhile_replicate_eq_filter_not {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
popWhile p (replicate n a) = filter (fun (a : α) => !p a) (replicate n a)
source
@[reducible, inline, deprecated Array.popWhile_replicate_eq_filter_not (since := "2025-03-18")]
abbrev Array.popWhile_mkArray_eq_filter_not {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
popWhile p (replicate n a) = filter (fun (a : α) => !p a) (replicate n a)
Equations

- @Array.popWhile_mkArray_eq_filter_not = @Array.popWhile_replicate_eq_filter_not

Instances For

source
theorem Array.popWhile_replicate {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
popWhile p (replicate n a) = if p a = true then #[] else replicate n a
source
@[reducible, inline, deprecated Array.popWhile_replicate (since := "2025-03-18")]
abbrev Array.popWhile_mkArray {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
popWhile p (replicate n a) = if p a = true then #[] else replicate n a
Equations

- @Array.popWhile_mkArray = @Array.popWhile_replicate

Instances For

source
theorem Array.extract_takeWhile {α : Type u_1} {p : α → Bool} {as : Array α} {i : Nat} :
(takeWhile p as).extract 0 i = takeWhile p (as.extract 0 i)
source
@[simp]
theorem Array.all_takeWhile {α : Type u_1} {p : α → Bool} {as : Array α} :
(takeWhile p as).all p = true
source
@[simp]
theorem Array.any_popWhile {α : Type u_1} {p : α → Bool} {as : Array α} :
((popWhile p as).any fun (a : α) => !p a) = !as.all p
source
theorem Array.takeWhile_eq_extract_findIdx_not {α : Type u_1} {xs : Array α} {p : α → Bool} :
takeWhile p xs = xs.extract 0 (findIdx (fun (a : α) => !p a) xs)