Lemmas about Array.extract

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

extract

@[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

theorem Array.size_extract_le {α : Type u_1} {as : Array α} {i j : Nat} : (as.extract i j).size ≤ j - i

theorem Array.size_extract_le' {α : Type u_1} {as : Array α} {i j : Nat} : (as.extract i j).size ≤ as.size - i

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

@[simp]

theorem Array.extract_push {α : Type u_1} {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) : (as.push b).extract start stop = as.extract start stop

@[simp]

theorem Array.extract_eq_pop {α : Type u_1} {as : Array α} {stop : Nat} (h : stop = as.size - 1) : as.extract 0 stop = as.pop

@[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)

@[simp]

theorem Array.extract_eq_empty_iff {α : Type u_1} {i j : Nat} {as : Array α} : as.extract i j = #[] ↔ min j as.size ≤ i

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 = #[]

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

@[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

theorem Array.extract_eq_self_of_le {α : Type u_1} {j : Nat} {as : Array α} (h : as.size ≤ j) : as.extract 0 j = as

theorem Array.le_of_extract_eq_self {α : Type u_1} {i j : Nat} {as : Array α} (h : as.extract i j = as) : as.size ≤ j

@[simp]

theorem Array.extract_size_left {α : Type u_1} {j : Nat} {as : Array α} : as.extract as.size j = #[]

@[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)

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]

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

@[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]

theorem Array.getElem?_extract_of_succ {α : Type u_1} {as : Array α} {j : Nat} : (as.extract 0 (j + 1))[j]? = as[j]?

@[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)

theorem Array.extract_eq_empty_of_eq_empty {α : Type u_1} {as : Array α} {i j : Nat} (h : as = #[]) : as.extract i j = #[]

theorem Array.ne_empty_of_extract_ne_empty {α : Type u_1} {as : Array α} {i j : Nat} (h : as.extract i j ≠ #[]) : as ≠ #[]

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

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

@[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)

theorem Array.extract_append_left {α : Type u_1} {as bs : Array α} : (as ++ bs).extract 0 as.size = as.extract

@[simp]

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

@[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

@[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

@[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

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)

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'

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)

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

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)

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

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

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)

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)

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)

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)

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)

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)

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

@[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

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

@[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

@[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)

@[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

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 #[]

@[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

@[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)

@[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

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

@[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

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)

@[simp]

theorem Array.all_takeWhile {α : Type u_1} {p : α → Bool} {as : Array α} : (takeWhile p as).all p = true

@[simp]

theorem Array.any_popWhile {α : Type u_1} {p : α → Bool} {as : Array α} : ((popWhile p as).any fun (a : α) => !p a) = !as.all p

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)