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

Ranges and enumeration

range'

theorem Array.range'_succ (s n step : Nat) : range' s (n + 1) step = #[s] ++ range' (s + step) n step

@[simp]

theorem Array.range'_eq_empty_iff {s n step : Nat} : range' s n step = #[] ↔ n = 0

theorem Array.range'_ne_empty_iff (s : Nat) {n step : Nat} : range' s n step ≠ #[] ↔ n ≠ 0

@[simp]

theorem Array.range'_zero {s step : Nat} : range' s 0 step = #[]

@[simp]

theorem Array.range'_one {s step : Nat} : range' s 1 step = #[s]

@[simp]

theorem Array.range'_inj {s n s' n' : Nat} : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')

theorem Array.mem_range' {s step m n : Nat} : m ∈ range' s n step ↔ ∃ (i : Nat), i < n ∧ m = s + step * i

theorem Array.pop_range' {s n step : Nat} : (range' s n step).pop = range' s (n - 1) step

theorem Array.map_add_range' (a s n step : Nat) : map (fun (x : Nat) => a + x) (range' s n step) = range' (a + s) n step

theorem Array.range'_succ_left {s n step : Nat} : range' (s + 1) n step = map (fun (x : Nat) => x + 1) (range' s n step)

theorem Array.range'_append (s m n step : Nat) : range' s m step ++ range' (s + step * m) n step = range' s (m + n) step

@[simp]

theorem Array.range'_append_1 (s m n : Nat) : range' s m ++ range' (s + m) n = range' s (m + n)

theorem Array.range'_concat {step : Nat} (s n : Nat) : range' s (n + 1) step = range' s n step ++ #[s + step * n]

theorem Array.range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ #[s + n]

@[simp]

theorem Array.mem_range'_1 {s n m : Nat} : m ∈ range' s n ↔ s ≤ m ∧ m < s + n

theorem Array.map_sub_range' {step : Nat} (a s n : Nat) (h : a ≤ s) : map (fun (x : Nat) => x - a) (range' s n step) = range' (s - a) n step

@[simp]

theorem Array.range'_eq_singleton_iff {s n a : Nat} : range' s n = #[a] ↔ s = a ∧ n = 1

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)

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

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

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

range

theorem Array.range_eq_range' (n : Nat) : range n = range' 0 n

theorem Array.range_succ_eq_map (n : Nat) : range (n + 1) = #[0] ++ map Nat.succ (range n)

theorem Array.range'_eq_map_range (s n : Nat) : range' s n = map (fun (x : Nat) => s + x) (range n)

@[simp]

theorem Array.range_eq_empty_iff {n : Nat} : range n = #[] ↔ n = 0

theorem Array.range_ne_empty_iff {n : Nat} : range n ≠ #[] ↔ n ≠ 0

theorem Array.range_succ (n : Nat) : range n.succ = range n ++ #[n]

theorem Array.range_add (a b : Nat) : range (a + b) = range a ++ map (fun (x : Nat) => a + x) (range b)

theorem Array.reverse_range' (s n : Nat) : (range' s n).reverse = map (fun (x : Nat) => s + n - 1 - x) (range n)

@[simp]

theorem Array.mem_range {m n : Nat} : m ∈ range n ↔ m < n

theorem Array.not_mem_range_self {n : Nat} : ¬n ∈ range n

theorem Array.self_mem_range_succ (n : Nat) : n ∈ range (n + 1)

@[simp]

theorem Array.take_range (m n : Nat) : (range n).take m = range (min m n)

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

@[simp]

theorem Array.find?_range_eq_none {n : Nat} {p : Nat → Bool} : find? p (range n) = none ↔ ∀ (i : Nat), i < n → (!p i) = true

theorem Array.erase_range {n i : Nat} : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))

zipIdx

@[simp]

theorem Array.zipIdx_eq_empty_iff {α : Type u_1} {l : Array α} {n : Nat} : l.zipIdx n = #[] ↔ l = #[]

@[simp]

theorem Array.getElem?_zipIdx {α : Type u_1} (l : Array α) (n m : Nat) : (l.zipIdx n)[m]? = Option.map (fun (a : α) => (a, n + m)) l[m]?

theorem Array.map_snd_add_zipIdx_eq_zipIdx {α : Type u_1} (l : Array α) (n k : Nat) : map (Prod.map id fun (x : Nat) => x + n) (l.zipIdx k) = l.zipIdx (n + k)

@[simp]

theorem Array.zipIdx_map_snd {α : Type u_1} (n : Nat) (l : Array α) : map Prod.snd (l.zipIdx n) = range' n l.size

@[simp]

theorem Array.zipIdx_map_fst {α : Type u_1} (n : Nat) (l : Array α) : map Prod.fst (l.zipIdx n) = l

theorem Array.zipIdx_eq_zip_range' {α : Type u_1} (l : Array α) {n : Nat} : l.zipIdx n = l.zip (range' n l.size)

@[simp]

theorem Array.unzip_zipIdx_eq_prod {α : Type u_1} (l : Array α) {n : Nat} : (l.zipIdx n).unzip = (l, range' n l.size)

theorem Array.zipIdx_succ {α : Type u_1} (l : Array α) (n : Nat) : l.zipIdx (n + 1) = map (fun (x : α × Nat) => match x with | (a, i) => (a, i + 1)) (l.zipIdx n)

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

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

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

@[simp]

theorem Array.zipIdx_singleton {α : Type u_1} (x : α) (k : Nat) : #[x].zipIdx k = #[(x, k)]

theorem Array.mk_add_mem_zipIdx_iff_getElem? {α : Type u_1} {k i : Nat} {x : α} {l : Array α} : (x, k + i) ∈ l.zipIdx k ↔ l[i]? = some x

theorem Array.le_snd_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {k : Nat} {l : Array α} (h : x ∈ l.zipIdx k) : k ≤ x.snd

theorem Array.snd_lt_add_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ l.zipIdx k) : x.snd < k + l.size

theorem Array.snd_lt_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ l.zipIdx k) : x.snd < l.size + k

theorem Array.map_zipIdx {α : Type u_1} {β : Type u_2} (f : α → β) (l : Array α) (k : Nat) : map (Prod.map f id) (l.zipIdx k) = (map f l).zipIdx k

theorem Array.fst_mem_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ l.zipIdx k) : x.fst ∈ l

theorem Array.fst_eq_of_mem_zipIdx {α : Type u_1} {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ l.zipIdx k) : x.fst = l[x.snd - k]

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]

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.

theorem Array.zipIdx_map {α : Type u_1} {β : Type u_2} (l : Array α) (k : Nat) (f : α → β) : (map f l).zipIdx k = map (Prod.map f id) (l.zipIdx k)

theorem Array.zipIdx_append {α : Type u_1} (xs ys : Array α) (k : Nat) : (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.size)

theorem Array.zipIdx_eq_append_iff {α : Type u_1} {l₁ l₂ : Array (α × Nat)} {l : Array α} {k : Nat} : l.zipIdx k = l₁ ++ l₂ ↔ ∃ (l₁' : Array α), ∃ (l₂' : Array α), l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)