Lemmas about List.range and List.enum

Ranges and enumeration

range'

theorem List.range'_succ (s : Nat) (n : Nat) (step : Nat) : List.range' s (n + 1) step = s :: List.range' (s + step) n step

@[simp]

theorem List.length_range' (s : Nat) (step : Nat) (n : Nat) : (List.range' s n step).length = n

@[simp]

theorem List.range'_eq_nil {s : Nat} {n : Nat} {step : Nat} : List.range' s n step = [] ↔ n = 0

theorem List.range'_ne_nil (s : Nat) (n : Nat) : List.range' s n ≠ [] ↔ n ≠ 0

@[simp]

theorem List.range'_zero {s : Nat} : List.range' s 0 = []

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem List.head_range' {s : Nat} (n : Nat) (h : List.range' s n ≠ []) : (List.range' s n).head h = s

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

@[simp]

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

theorem List.pairwise_lt_range' (s : Nat) (n : Nat) (step : optParam Nat 1) (pos : autoParam (0 < step) _auto✝) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (List.range' s n step)

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

theorem List.nodup_range' (s : Nat) (n : Nat) (step : optParam Nat 1) (h : autoParam (0 < step) _auto✝) : (List.range' s n step).Nodup

@[simp]

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

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

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

@[simp]

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

theorem List.range'_sublist_right {step : Nat} {s : Nat} {m : Nat} {n : Nat} : (List.range' s m step).Sublist (List.range' s n step) ↔ m ≤ n

theorem List.range'_subset_right {step : Nat} {s : Nat} {m : Nat} {n : Nat} (step0 : 0 < step) : List.range' s m step ⊆ List.range' s n step ↔ m ≤ n

theorem List.range'_subset_right_1 {s : Nat} {m : Nat} {n : Nat} : List.range' s m ⊆ List.range' s n ↔ m ≤ n

theorem List.getElem?_range' (s : Nat) (step : Nat) {m : Nat} {n : Nat} : m < n → (List.range' s n step)[m]? = some (s + step * m)

@[simp]

theorem List.getElem_range' {n : Nat} {m : Nat} {step : Nat} (i : Nat) (H : i < (List.range' n m step).length) : (List.range' n m step)[i] = n + step * i

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

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

theorem List.range'_eq_cons_iff {s : Nat} {n : Nat} {a : Nat} {xs : List Nat} : List.range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = List.range' (a + 1) (n - 1)

@[simp]

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

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

@[simp]

theorem List.find?_range'_eq_some (s : Nat) (n : Nat) (i : Nat) (p : Nat → Bool) : List.find? p (List.range' s n) = some i ↔ p i = true ∧ i ∈ List.range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

@[simp]

theorem List.find?_range'_eq_none (s : Nat) (n : Nat) (p : Nat → Bool) : List.find? p (List.range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

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

range

theorem List.range_loop_range' (s : Nat) (n : Nat) : List.range.loop s (List.range' s n) = List.range' 0 (n + s)

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

theorem List.range_succ_eq_map (n : Nat) : List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)

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

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

@[simp]

theorem List.length_range (n : Nat) : (List.range n).length = n

@[simp]

theorem List.range_eq_nil {n : Nat} : List.range n = [] ↔ n = 0

theorem List.range_ne_nil (n : Nat) : List.range n ≠ [] ↔ n ≠ 0

@[simp]

theorem List.range_sublist {m : Nat} {n : Nat} : (List.range m).Sublist (List.range n) ↔ m ≤ n

@[simp]

theorem List.range_subset {m : Nat} {n : Nat} : List.range m ⊆ List.range n ↔ m ≤ n

@[simp]

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

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

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

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

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

theorem List.getElem?_range {m : Nat} {n : Nat} (h : m < n) : (List.range n)[m]? = some m

@[simp]

theorem List.getElem_range {n : Nat} (m : Nat) (h : m < (List.range n).length) : (List.range n)[m] = m

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

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

theorem List.head?_range (n : Nat) : (List.range n).head? = if n = 0 then none else some 0

@[simp]

theorem List.head_range (n : Nat) (h : List.range n ≠ []) : (List.range n).head h = 0

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

@[simp]

theorem List.getLast_range (n : Nat) (h : List.range n ≠ []) : (List.range n).getLast h = n - 1

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

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

@[simp]

theorem List.find?_range_eq_some (n : Nat) (i : Nat) (p : Nat → Bool) : List.find? p (List.range n) = some i ↔ p i = true ∧ i ∈ List.range n ∧ ∀ (j : Nat), j < i → (!p j) = true

@[simp]

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

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

iota

theorem List.iota_eq_reverse_range' (n : Nat) : List.iota n = (List.range' 1 n).reverse

@[simp]

theorem List.length_iota (n : Nat) : (List.iota n).length = n

@[simp]

theorem List.iota_eq_nil (n : Nat) : List.iota n = [] ↔ n = 0

theorem List.iota_ne_nil (n : Nat) : List.iota n ≠ [] ↔ n ≠ 0

@[simp]

theorem List.mem_iota {m : Nat} {n : Nat} : m ∈ List.iota n ↔ 0 < m ∧ m ≤ n

@[simp]

theorem List.iota_inj {n : Nat} {n' : Nat} : List.iota n = List.iota n' ↔ n = n'

theorem List.iota_eq_cons_iff {n : Nat} {a : Nat} {xs : List Nat} : List.iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = List.iota (n - 1)

theorem List.iota_eq_append_iff {n : Nat} {xs : List Nat} {ys : List Nat} : List.iota n = xs ++ ys ↔ ∃ (k : Nat), k ≤ n ∧ xs = (List.range' (k + 1) (n - k)).reverse ∧ ys = List.iota k

theorem List.pairwise_gt_iota (n : Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 > x2) (List.iota n)

theorem List.nodup_iota (n : Nat) : (List.iota n).Nodup

@[simp]

theorem List.head?_iota (n : Nat) : (List.iota n).head? = if n = 0 then none else some n

@[simp]

theorem List.head_iota (n : Nat) (h : List.iota n ≠ []) : (List.iota n).head h = n

@[simp]

theorem List.reverse_iota {n : Nat} : (List.iota n).reverse = List.range' 1 n

@[simp]

theorem List.getLast?_iota (n : Nat) : (List.iota n).getLast? = if n = 0 then none else some 1

@[simp]

theorem List.getLast_iota (n : Nat) (h : List.iota n ≠ []) : (List.iota n).getLast h = 1

@[simp]

theorem List.find?_iota_eq_none (n : Nat) (p : Nat → Bool) : List.find? p (List.iota n) = none ↔ ∀ (i : Nat), 0 < i → i ≤ n → (!p i) = true

@[simp]

theorem List.find?_iota_eq_some (n : Nat) (i : Nat) (p : Nat → Bool) : List.find? p (List.iota n) = some i ↔ p i = true ∧ i ∈ List.iota n ∧ ∀ (j : Nat), i < j → j ≤ n → (!p j) = true

enumFrom

@[simp]

theorem List.enumFrom_singleton {α : Type u_1} (x : α) (n : Nat) : List.enumFrom n [x] = [(n, x)]

@[simp]

theorem List.head?_enumFrom {α : Type u_1} (n : Nat) (l : List α) : (List.enumFrom n l).head? = Option.map (fun (a : α) => (n, a)) l.head?

@[simp]

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

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

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

theorem List.le_fst_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ List.enumFrom n l) : n ≤ x.fst

theorem List.fst_lt_add_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ List.enumFrom n l) : x.fst < n + l.length

theorem List.map_enumFrom {α : Type u_1} {β : Type u_2} (f : α → β) (n : Nat) (l : List α) : List.map (Prod.map id f) (List.enumFrom n l) = List.enumFrom n (List.map f l)

@[simp]

theorem List.enumFrom_map_fst {α : Type u_1} (n : Nat) (l : List α) : List.map Prod.fst (List.enumFrom n l) = List.range' n l.length

@[simp]

theorem List.enumFrom_map_snd {α : Type u_1} (n : Nat) (l : List α) : List.map Prod.snd (List.enumFrom n l) = l

theorem List.snd_mem_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ List.enumFrom n l) : x.snd ∈ l

theorem List.snd_eq_of_mem_enumFrom {α : Type u_1} {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ List.enumFrom n l) : x.snd = l[x.fst - n]

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

theorem List.enumFrom_cons' {α : Type u_1} (n : Nat) (x : α) (xs : List α) : List.enumFrom n (x :: xs) = (n, x) :: List.map (Prod.map (fun (x : Nat) => x + 1) id) (List.enumFrom n xs)

theorem List.enumFrom_map {α : Type u_1} {β : Type u_2} (n : Nat) (l : List α) (f : α → β) : List.enumFrom n (List.map f l) = List.map (Prod.map id f) (List.enumFrom n l)

theorem List.enumFrom_append {α : Type u_1} (xs : List α) (ys : List α) (n : Nat) : List.enumFrom n (xs ++ ys) = List.enumFrom n xs ++ List.enumFrom (n + xs.length) ys

theorem List.enumFrom_eq_zip_range' {α : Type u_1} (l : List α) {n : Nat} : List.enumFrom n l = (List.range' n l.length).zip l

@[simp]

theorem List.unzip_enumFrom_eq_prod {α : Type u_1} (l : List α) {n : Nat} : (List.enumFrom n l).unzip = (List.range' n l.length, l)

enum

theorem List.enum_cons : ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).enum = (0, a) :: List.enumFrom 1 as

theorem List.enum_cons' {α : Type u_1} (x : α) (xs : List α) : (x :: xs).enum = (0, x) :: List.map (Prod.map (fun (x : Nat) => x + 1) id) xs.enum

@[simp]

theorem List.enum_eq_nil {α : Type u_1} {l : List α} : l.enum = [] ↔ l = []

@[simp]

theorem List.enum_singleton {α : Type u_1} (x : α) : [x].enum = [(0, x)]

@[simp]

theorem List.enum_length : ∀ {α : Type u_1} {l : List α}, l.enum.length = l.length

@[simp]

theorem List.getElem?_enum {α : Type u_1} (l : List α) (n : Nat) : l.enum[n]? = Option.map (fun (a : α) => (n, a)) l[n]?

@[simp]

theorem List.getElem_enum {α : Type u_1} (l : List α) (i : Nat) (h : i < l.enum.length) : l.enum[i] = (i, l[i])

@[simp]

theorem List.head?_enum {α : Type u_1} (l : List α) : l.enum.head? = Option.map (fun (a : α) => (0, a)) l.head?

@[simp]

theorem List.getLast?_enum {α : Type u_1} (l : List α) : l.enum.getLast? = Option.map (fun (a : α) => (l.length - 1, a)) l.getLast?

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

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

theorem List.fst_lt_of_mem_enum {α : Type u_1} {x : Nat × α} {l : List α} (h : x ∈ l.enum) : x.fst < l.length

theorem List.snd_mem_of_mem_enum {α : Type u_1} {x : Nat × α} {l : List α} (h : x ∈ l.enum) : x.snd ∈ l

theorem List.snd_eq_of_mem_enum {α : Type u_1} {x : Nat × α} {l : List α} (h : x ∈ l.enum) : x.snd = l[x.fst]

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

theorem List.map_enum {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map (Prod.map id f) l.enum = (List.map f l).enum

@[simp]

theorem List.enum_map_fst {α : Type u_1} (l : List α) : List.map Prod.fst l.enum = List.range l.length

@[simp]

theorem List.enum_map_snd {α : Type u_1} (l : List α) : List.map Prod.snd l.enum = l

theorem List.enum_map {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : (List.map f l).enum = List.map (Prod.map id f) l.enum

theorem List.enum_append {α : Type u_1} (xs : List α) (ys : List α) : (xs ++ ys).enum = xs.enum ++ List.enumFrom xs.length ys

theorem List.enum_eq_zip_range {α : Type u_1} (l : List α) : l.enum = (List.range l.length).zip l

@[simp]

theorem List.unzip_enum_eq_prod {α : Type u_1} (l : List α) : l.enum.unzip = (List.range l.length, l)