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

Ranges and enumeration

range'

@[simp]

theorem Vector.toArray_range' (start size step : Nat) : (range' start size step).toArray = Array.range' start size step

theorem Vector.range'_eq_mk_range' (start size step : Nat) : range' start size step = { toArray := Array.range' start size step, size_toArray := ⋯ }

@[simp]

theorem Vector.getElem_range' (start size step i : Nat) (h : i < size) : (range' start size step)[i] = start + step * i

@[simp]

theorem Vector.getElem?_range' (start size step i : Nat) : (range' start size step)[i]? = if i < size then some (start + step * i) else none

theorem Vector.range'_succ (s n step : Nat) : range' s (n + 1) step = Vector.cast ⋯ ({ toArray := #[s], size_toArray := ⋯ } ++ range' (s + step) n step)

theorem Vector.range'_zero {s step : Nat} : range' s 0 step = { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.range'_one {s step : Nat} : range' s 1 step = { toArray := #[s], size_toArray := ⋯ }

@[simp]

theorem Vector.range'_inj {s n s' : Nat} : range' s n = range' s' n ↔ n = 0 ∨ s = s'

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

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

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

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

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

@[simp]

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

theorem Vector.range'_concat {step : Nat} (s n : Nat) : range' s (n + 1) step = range' s n step ++ { toArray := #[s + step * n], size_toArray := ⋯ }

theorem Vector.range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ { toArray := #[s + n], size_toArray := ⋯ }

@[simp]

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

theorem Vector.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

theorem Vector.range'_eq_append_iff {s n m : Nat} {xs : Vector Nat n} {ys : Vector Nat m} : range' s (n + m) = xs ++ ys ↔ xs = range' s n ∧ ys = range' (s + n) m

@[simp]

theorem Vector.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 Vector.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

range

@[simp]

theorem Vector.getElem_range {n : Nat} (i : Nat) (hi : i < n) : (range n)[i] = i

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

theorem Vector.range_succ_eq_map (n : Nat) : range (n + 1) = Vector.cast ⋯ ({ toArray := #[0], size_toArray := ⋯ } ++ map Nat.succ (range n))

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

theorem Vector.range_succ (n : Nat) : range n.succ = range n ++ { toArray := #[n], size_toArray := ⋯ }

theorem Vector.range_add (n m : Nat) : range (n + m) = range n ++ map (fun (x : Nat) => n + x) (range m)

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

@[simp]

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

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

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

@[simp]

theorem Vector.take_range (n i : Nat) : (range n).take i = range (min i n)

@[simp]

theorem Vector.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 Vector.find?_range_eq_none {n : Nat} {p : Nat → Bool} : find? p (range n) = none ↔ ∀ (i : Nat), i < n → (!p i) = true

zipIdx

@[simp]

theorem Vector.getElem?_zipIdx {α : Type u_1} {n : Nat} (xs : Vector α n) (i j : Nat) : (xs.zipIdx i)[j]? = Option.map (fun (a : α) => (a, i + j)) xs[j]?

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

@[simp]

theorem Vector.zipIdx_map_snd {α : Type u_1} {n : Nat} (i : Nat) (xs : Vector α n) : map Prod.snd (xs.zipIdx i) = range' i n

@[simp]

theorem Vector.zipIdx_map_fst {α : Type u_1} {n : Nat} (i : Nat) (xs : Vector α n) : map Prod.fst (xs.zipIdx i) = xs

theorem Vector.zipIdx_eq_zip_range' {α : Type u_1} {n i : Nat} (xs : Vector α n) : xs.zipIdx i = xs.zip (range' i n)

@[simp]

theorem Vector.unzip_zipIdx_eq_prod {α : Type u_1} {n : Nat} (xs : Vector α n) {i : Nat} : (xs.zipIdx i).unzip = (xs, range' i n)

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

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

theorem Vector.zipIdx_eq_map_add {α : Type u_1} {n : Nat} (xs : Vector α n) (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.

@[simp]

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

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

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

theorem Vector.snd_lt_add_of_mem_zipIdx {α : Type u_1} {n : Nat} {x : α × Nat} {k : Nat} {xs : Vector α n} (h : x ∈ xs.zipIdx k) : x.snd < k + n

theorem Vector.snd_lt_of_mem_zipIdx {α : Type u_1} {n : Nat} {x : α × Nat} {k : Nat} {xs : Vector α n} (h : x ∈ xs.zipIdx k) : x.snd < n + k

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

theorem Vector.fst_mem_of_mem_zipIdx {α : Type u_1} {n : Nat} {x : α × Nat} {xs : Vector α n} {k : Nat} (h : x ∈ xs.zipIdx k) : x.fst ∈ xs

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

theorem Vector.mem_zipIdx {α : Type u_1} {n : Nat} {x : α} {i : Nat} {xs : Vector α n} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) : k ≤ i ∧ i < k + n ∧ x = xs[i - k]

theorem Vector.mem_zipIdx' {α : Type u_1} {n : Nat} {x : α} {i : Nat} {xs : Vector α n} (h : (x, i) ∈ xs.zipIdx) : i < n ∧ x = xs[i]

Variant of mem_zipIdx specialized at k = 0.

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

theorem Vector.zipIdx_append {α : Type u_1} {n m : Nat} (xs : Vector α n) (ys : Vector α m) (k : Nat) : (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + n)

theorem Vector.zipIdx_eq_append_iff {α : Type u_1} {n m : Nat} {ys : Vector (α × Nat) n} {zs : Vector (α × Nat) m} {xs : Vector α (n + m)} {k : Nat} : xs.zipIdx k = ys ++ zs ↔ ∃ (ys' : Vector α n), ∃ (zs' : Vector α m), xs = ys' ++ zs' ∧ ys = ys'.zipIdx k ∧ zs = zs'.zipIdx (k + n)