# Lemmas about `Array.range'`, `Array.range`, and `Array.zipIdx` #

## Ranges and enumeration #

### range' #

source
theorem Array.range'_succ {s n step : Nat} :
range' s (n + 1) step = #[s] ++ range' (s + step) n step
source
@[simp]
theorem Array.range'_eq_empty_iff {s n step : Nat} :
range' s n step = #[] ↔ n = 0
source
theorem Array.range'_ne_empty_iff {s n step : Nat} :
range' s n step ≠ #[] ↔ n ≠ 0
source
@[simp]
theorem Array.range'_zero {s step : Nat} :
range' s 0 step = #[]
source
@[simp]
theorem Array.range'_one {s step : Nat} :
range' s 1 step = #[s]
source
@[simp]
theorem Array.range'_inj {s n s' n' : Nat} :
range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')
source
theorem Array.mem_range' {s step m n : Nat} :
m ∈ range' s n step ↔ ∃ (i : Nat), i < n ∧ m = s + step * i
source
@[simp]
theorem Array.pop_range' {s n step : Nat} :
(range' s n step).pop = range' s (n - 1) step
source
theorem Array.map_add_range' {a : Nat} (s n step : Nat) :
map (fun (x : Nat) => a + x) (range' s n step) = range' (a + s) n step
source
theorem Array.range'_succ_left {s n step : Nat} :
range' (s + 1) n step = map (fun (x : Nat) => x + 1) (range' s n step)
source
theorem Array.range'_append {s m n step : Nat} :
range' s m step ++ range' (s + step * m) n step = range' s (m + n) step
source
@[simp]
theorem Array.range'_append_1 {s m n : Nat} :
range' s m ++ range' (s + m) n = range' s (m + n)
source
theorem Array.range'_concat {step s n : Nat} :
range' s (n + 1) step = range' s n step ++ #[s + step * n]
source
theorem Array.range'_1_concat {s n : Nat} :
range' s (n + 1) = range' s n ++ #[s + n]
source
@[simp]
theorem Array.mem_range'_1 {s n m : Nat} :
m ∈ range' s n ↔ s ≤ m ∧ m < s + n
source
theorem Array.map_sub_range' {step a s : Nat} (h : a ≤ s) (n : Nat) :
map (fun (x : Nat) => x - a) (range' s n step) = range' (s - a) n step
source
@[simp]
theorem Array.range'_eq_singleton_iff {s n a : Nat} :
range' s n = #[a] ↔ s = a ∧ n = 1
source
theorem Array.range'_eq_append_iff {s n : Nat} {xs ys : Array Nat} :
range' s n = xs ++ ys ↔ ∃ (k : Nat), k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
source
@[simp]
theorem Array.find?_range'_eq_some {s n i : Nat} {p : Nat → Bool} :
find? p (range' s n) = some i ↔ p i = true ∧ i ∈ range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true
source
@[simp]
theorem Array.find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
find? p (range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true
source
theorem Array.erase_range' {s n i : Nat} :
(range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))
source
@[simp]
theorem Array.count_range' {a s n step : Nat} (h : 0 < step := by simp) :
count a (range' s n step) = if ∃ (i : Nat), i < n ∧ a = s + step * i then 1 else 0
source
@[simp]
theorem Array.count_range_1' {a s n : Nat} :
count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0

### range #

source
theorem Array.range_eq_range' {n : Nat} :
range n = range' 0 n
source
theorem Array.range_succ_eq_map {n : Nat} :
range (n + 1) = #[0] ++ map Nat.succ (range n)
source
theorem Array.range'_eq_map_range {s n : Nat} :
range' s n = map (fun (x : Nat) => s + x) (range n)
source
@[simp]
theorem Array.range_eq_empty_iff {n : Nat} :
range n = #[] ↔ n = 0
source
theorem Array.range_ne_empty_iff {n : Nat} :
range n ≠ #[] ↔ n ≠ 0
source
theorem Array.range_succ {n : Nat} :
range n.succ = range n ++ #[n]
source
theorem Array.range_add {n m : Nat} :
range (n + m) = range n ++ map (fun (x : Nat) => n + x) (range m)
source
theorem Array.reverse_range' {s n : Nat} :
(range' s n).reverse = map (fun (x : Nat) => s + n - 1 - x) (range n)
source
@[simp]
theorem Array.mem_range {m n : Nat} :
m ∈ range n ↔ m < n
source
theorem Array.not_mem_range_self {n : Nat} :
¬n ∈ range n
source
theorem Array.self_mem_range_succ {n : Nat} :
n ∈ range (n + 1)
source
@[simp]
theorem Array.take_range {i n : Nat} :
(range n).take i = range (min i n)
source
@[simp]
theorem Array.find?_range_eq_some {n i : Nat} {p : Nat → Bool} :
find? p (range n) = some i ↔ p i = true ∧ i ∈ range n ∧ ∀ (j : Nat), j < i → (!p j) = true
source
@[simp]
theorem Array.find?_range_eq_none {n : Nat} {p : Nat → Bool} :
find? p (range n) = none ↔ ∀ (i : Nat), i < n → (!p i) = true
source
theorem Array.erase_range {n i : Nat} :
(range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))
source
@[simp]
theorem Array.count_range {a n : Nat} :
count a (range n) = if a < n then 1 else 0

### zipIdx #

source
@[simp]
theorem Array.zipIdx_eq_empty_iff {α : Type u_1} {xs : Array α} {i : Nat} :
xs.zipIdx i = #[] ↔ xs = #[]
source
@[simp]
theorem Array.getElem?_zipIdx {α : Type u_1} {xs : Array α} {i j : Nat} :
(xs.zipIdx i)[j]? = Option.map (fun (a : α) => (a, i + j)) xs[j]?
source
theorem Array.map_snd_add_zipIdx_eq_zipIdx {α : Type u_1} {xs : Array α} {n k : Nat} :
map (Prod.map id fun (x : Nat) => x + n) (xs.zipIdx k) = xs.zipIdx (n + k)
source
@[simp]
theorem Array.zipIdx_map_snd {α : Type u_1} (i : Nat) (xs : Array α) :
map Prod.snd (xs.zipIdx i) = range' i xs.size
source
@[simp]
theorem Array.zipIdx_map_fst {α : Type u_1} (i : Nat) (xs : Array α) :
map Prod.fst (xs.zipIdx i) = xs
source
theorem Array.zipIdx_eq_zip_range' {α : Type u_1} {xs : Array α} {i : Nat} :
xs.zipIdx i = xs.zip (range' i xs.size)
source
@[simp]
theorem Array.unzip_zipIdx_eq_prod {α : Type u_1} {xs : Array α} {i : Nat} :
(xs.zipIdx i).unzip = (xs, range' i xs.size)
source
theorem Array.zipIdx_succ {α : Type u_1} {xs : Array α} {i : Nat} :
xs.zipIdx (i + 1) = map (fun (x : α × Nat) => match x with | (a, j) => (a, j + 1)) (xs.zipIdx i)

Replace `zipIdx` with a starting index `n+1` with `zipIdx` starting from `n`, followed by a `map` increasing the indices by one.

source
theorem Array.zipIdx_eq_map_add {α : Type u_1} {xs : Array α} {i : Nat} :
xs.zipIdx i = map (fun (x : α × Nat) => match x with | (a, j) => (a, i + j)) xs.zipIdx

Replace `zipIdx` with a starting index with `zipIdx` starting from 0, followed by a `map` increasing the indices.

source
@[simp]
theorem Array.zipIdx_singleton {α : Type u_1} {x : α} {k : Nat} :
#[x].zipIdx k = #[(x, k)]
source
theorem Array.mk_add_mem_zipIdx_iff_getElem? {α : Type u_1} {k i : Nat} {x : α} {xs : Array α} :
(x, k + i) ∈ xs.zipIdx k ↔ xs[i]? = some x
source
theorem Array.le_snd_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {k : Nat} {xs : Array α} (h : x ∈ xs.zipIdx k) :
k ≤ x.snd
source
theorem Array.snd_lt_add_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {k : Nat} {xs : Array α} (h : x ∈ xs.zipIdx k) :
x.snd < k + xs.size
source
theorem Array.snd_lt_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {k : Nat} {xs : Array α} (h : x ∈ xs.zipIdx k) :
x.snd < xs.size + k
source
theorem Array.map_zipIdx {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {k : Nat} :
map (Prod.map f id) (xs.zipIdx k) = (map f xs).zipIdx k
source
theorem Array.fst_mem_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {xs : Array α} {k : Nat} (h : x ∈ xs.zipIdx k) :
x.fst ∈ xs
source
theorem Array.fst_eq_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {xs : Array α} {k : Nat} (h : x ∈ xs.zipIdx k) :
x.fst = xs[x.snd - k]
source
theorem Array.mem_zipIdx {α : Type u_1} {x : α} {i : Nat} {xs : Array α} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
k ≤ i ∧ i < k + xs.size ∧ x = xs[i - k]
source
theorem Array.mem_zipIdx' {α : Type u_1} {x : α} {i : Nat} {xs : Array α} (h : (x, i) ∈ xs.zipIdx) :
i < xs.size ∧ x = xs[i]

Variant of `mem_zipIdx` specialized at `k = 0`.

source
theorem Array.zipIdx_map {α : Type u_1} {β : Type u_2} {xs : Array α} {k : Nat} {f : α → β} :
(map f xs).zipIdx k = map (Prod.map f id) (xs.zipIdx k)
source
theorem Array.zipIdx_append {α : Type u_1} {xs ys : Array α} {k : Nat} :
(xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.size)
source
theorem Array.zipIdx_eq_append_iff {α : Type u_1} {ys zs : Array (α × Nat)} {xs : Array α} {k : Nat} :
xs.zipIdx k = ys ++ zs ↔ ∃ (ys' : Array α), ∃ (zs' : Array α), xs = ys' ++ zs' ∧ ys = ys'.zipIdx k ∧ zs = zs'.zipIdx (k + ys'.size)