Lemmas about List.range and List.enum

Ranges and enumeration

range'

@[simp]

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

theorem List.getLast?_range' {s n : Nat} : (range' s n).getLast? = if n = 0 then none else some (s + n - 1)

@[simp]

theorem List.getLast_range' {s n : Nat} (h : range' s n ≠ []) : (range' s n).getLast h = s + n - 1

theorem List.pairwise_lt_range' {s n : Nat} (step : Nat := 1) (pos : 0 < step := by simp) : Pairwise (fun (x1 x2 : Nat) => x1 < x2) (range' s n step)

theorem List.pairwise_le_range' {s n : Nat} (step : Nat := 1) : Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (range' s n step)

theorem List.nodup_range' {s n : Nat} (step : Nat := 1) (h : 0 < step := by simp) : (range' s n step).Nodup

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

@[simp]

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

theorem List.range'_eq_append_iff {s n step : Nat} {xs ys : List Nat} : range' s n step = xs ++ ys ↔ ∃ (k : Nat), k ≤ n ∧ xs = range' s k step ∧ ys = range' (s + k * step) (n - k) step

@[simp]

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

theorem List.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 List.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))

@[simp]

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

@[simp]

theorem List.count_range_1' {a s n : Nat} : count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0

@[simp]

theorem List.sum_range' {start n step : Nat} : (range' start n step).sum = n * start + n * (n - 1) * step / 2

@[simp]

theorem List.drop_range' {start n step k : Nat} : drop k (range' start n step) = range' (start + k * step) (n - k) step

@[simp]

theorem List.take_range'_of_length_le {n k start step : Nat} (h : n ≤ k) : take k (range' start n step) = range' start n step

@[simp]

theorem List.take_range'_of_length_ge {n k start step : Nat} (h : n ≥ k) : take k (range' start n step) = range' start k step

range

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

@[simp]

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

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

theorem List.self_mem_range_succ {n : Nat} : n ∈ range (n + 1)

theorem List.pairwise_lt_range {n : Nat} : Pairwise (fun (x1 x2 : Nat) => x1 < x2) (range n)

theorem List.pairwise_le_range {n : Nat} : Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (range n)

@[simp]

theorem List.take_range {i n : Nat} : take i (range n) = range (min i n)

theorem List.nodup_range {n : Nat} : (range n).Nodup

@[simp]

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

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

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

@[simp]

theorem List.count_range {a n : Nat} : count a (range n) = if a < n then 1 else 0

zipIdx

@[simp]

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

@[simp]

theorem List.head?_zipIdx {α : Type u_1} {l : List α} {k : Nat} : (l.zipIdx k).head? = Option.map (fun (a : α) => (a, k)) l.head?

@[simp]

theorem List.getLast?_zipIdx {α : Type u_1} {l : List α} {k : Nat} : (l.zipIdx k).getLast? = Option.map (fun (a : α) => (a, k + l.length - 1)) l.getLast?

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

theorem List.mk_mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {k i : Nat} {x : α} {l : List α} : (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

theorem List.mk_mem_zipIdx_iff_getElem? {α : Type u_1} {i : Nat} {x : α} {l : List α} : (x, i) ∈ l.zipIdx ↔ l[i]? = some x

Variant of mk_mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

theorem List.mem_zipIdx_iff_le_and_getElem?_sub {α : Type u_1} {x : α × Nat} {l : List α} {k : Nat} : x ∈ l.zipIdx k ↔ k ≤ x.snd ∧ l[x.snd - k]? = some x.fst

theorem List.mem_zipIdx_iff_getElem? {α : Type u_1} {x : α × Nat} {l : List α} : x ∈ l.zipIdx ↔ l[x.snd]? = some x.fst

Variant of mem_zipIdx_iff_le_and_getElem?_sub specialized at k = 0, to avoid the inequality and the subtraction.

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

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

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

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

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

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

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

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

Variant of mem_zipIdx specialized at k = 0.

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

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

theorem List.zipIdx_eq_cons_iff {α : Type u_1} {x : α × Nat} {l' : List (α × Nat)} {l : List α} {k : Nat} : l.zipIdx k = x :: l' ↔ ∃ (a : α), ∃ (as : List α), l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)

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