HepLean Documentation

Init.Data.List.Range

Lemmas about List.range and List.enum #

Most of the results are deferred to Data.Init.List.Nat.Range, where more results about natural arithmetic are available.

Ranges and enumeration #

range' #

source
theorem List.range'_succ (s : Nat) (n : Nat) (step : Nat) :
List.range' s (n + 1) step = s :: List.range' (s + step) n step
source
@[simp]
theorem List.length_range' (s : Nat) (step : Nat) (n : Nat) :
(List.range' s n step).length = n
source
@[simp]
theorem List.range'_eq_nil {s : Nat} {n : Nat} {step : Nat} :
List.range' s n step = [] ↔ n = 0
source
theorem List.range'_ne_nil (s : Nat) {n : Nat} :
List.range' s n ≠ [] ↔ n ≠ 0
source
@[simp]
theorem List.range'_zero {s : Nat} {step : Nat} :
List.range' s 0 step = []
source
@[simp]
theorem List.range'_one {s : Nat} {step : Nat} :
List.range' s 1 step = [s]
source
@[simp]
theorem List.tail_range' {s : Nat} {step : Nat} (n : Nat) :
(List.range' s n step).tail = List.range' (s + step) (n - 1) step
source
@[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')
source
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
source
theorem List.getElem?_range' (s : Nat) (step : Nat) {m : Nat} {n : Nat} :
m < n → (List.range' s n step)[m]? = some (s + step * m)
source
@[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
source
theorem List.head?_range' {s : Nat} (n : Nat) :
(List.range' s n).head? = if n = 0 then none else some s
source
@[simp]
theorem List.head_range' {s : Nat} (n : Nat) (h : List.range' s n ≠ []) :
(List.range' s n).head h = s
source
@[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
source
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
source
@[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)
source
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
source
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
source
theorem List.range'_subset_right_1 {s : Nat} {m : Nat} {n : Nat} :
List.range' s m ⊆ List.range' s n ↔ m ≤ n
source
theorem List.range'_concat {step : Nat} (s : Nat) (n : Nat) :
List.range' s (n + 1) step = List.range' s n step ++ [s + step * n]
source
theorem List.range'_1_concat (s : Nat) (n : Nat) :
List.range' s (n + 1) = List.range' s n ++ [s + n]
source
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)

range #

source
theorem List.range_loop_range' (s : Nat) (n : Nat) :
List.range.loop s (List.range' s n) = List.range' 0 (n + s)
source
theorem List.range_eq_range' (n : Nat) :
List.range n = List.range' 0 n
source
theorem List.getElem?_range {m : Nat} {n : Nat} (h : m < n) :
(List.range n)[m]? = some m
source
@[simp]
theorem List.getElem_range {n : Nat} (m : Nat) (h : m < (List.range n).length) :
(List.range n)[m] = m
source
theorem List.range_succ_eq_map (n : Nat) :
List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
source
theorem List.range'_eq_map_range (s : Nat) (n : Nat) :
List.range' s n = List.map (fun (x : Nat) => s + x) (List.range n)
source
@[simp]
theorem List.length_range (n : Nat) :
(List.range n).length = n
source
@[simp]
theorem List.range_eq_nil {n : Nat} :
List.range n = [] ↔ n = 0
source
theorem List.range_ne_nil {n : Nat} :
List.range n ≠ [] ↔ n ≠ 0
source
@[simp]
theorem List.tail_range (n : Nat) :
(List.range n).tail = List.range' 1 (n - 1)
source
@[simp]
theorem List.range_sublist {m : Nat} {n : Nat} :
(List.range m).Sublist (List.range n) ↔ m ≤ n
source
@[simp]
theorem List.range_subset {m : Nat} {n : Nat} :
List.range m ⊆ List.range n ↔ m ≤ n
source
theorem List.range_succ (n : Nat) :
List.range n.succ = List.range n ++ [n]
source
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)
source
theorem List.head?_range (n : Nat) :
(List.range n).head? = if n = 0 then none else some 0
source
@[simp]
theorem List.head_range (n : Nat) (h : List.range n ≠ []) :
(List.range n).head h = 0
source
theorem List.getLast?_range (n : Nat) :
(List.range n).getLast? = if n = 0 then none else some (n - 1)
source
@[simp]
theorem List.getLast_range (n : Nat) (h : List.range n ≠ []) :
(List.range n).getLast h = n - 1

enumFrom #

source
@[simp]
theorem List.enumFrom_eq_nil {α : Type u_1} {n : Nat} {l : List α} :
List.enumFrom n l = [] ↔ l = []
source
@[simp]
theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} :
(List.enumFrom n l).length = l.length
source
@[simp]
theorem List.getElem?_enumFrom {α : Type u_1} (n : Nat) (l : List α) (m : Nat) :
(List.enumFrom n l)[m]? = Option.map (fun (a : α) => (n + m, a)) l[m]?
source
@[simp]
theorem List.getElem_enumFrom {α : Type u_1} (l : List α) (n : Nat) (i : Nat) (h : i < (List.enumFrom n l).length) :
(List.enumFrom n l)[i] = (n + i, l[i])
source
@[simp]
theorem List.tail_enumFrom {α : Type u_1} (l : List α) (n : Nat) :
(List.enumFrom n l).tail = List.enumFrom (n + 1) l.tail
source
theorem List.map_fst_add_enumFrom_eq_enumFrom {α : Type u_1} (l : List α) (n : Nat) (k : Nat) :
List.map (Prod.map (fun (x : Nat) => x + n) id) (List.enumFrom k l) = List.enumFrom (n + k) l
source
theorem List.map_fst_add_enum_eq_enumFrom {α : Type u_1} (l : List α) (n : Nat) :
List.map (Prod.map (fun (x : Nat) => x + n) id) l.enum = List.enumFrom n l
source
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)
source
@[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
source
@[simp]
theorem List.enumFrom_map_snd {α : Type u_1} (n : Nat) (l : List α) :
List.map Prod.snd (List.enumFrom n l) = l
source
theorem List.enumFrom_eq_zip_range' {α : Type u_1} (l : List α) {n : Nat} :
List.enumFrom n l = (List.range' n l.length).zip l
source
@[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 #

source
theorem List.enum_cons :
∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).enum = (0, a) :: List.enumFrom 1 as
source
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
source
theorem List.enum_eq_enumFrom {α : Type u_1} {l : List α} :
l.enum = List.enumFrom 0 l
source
theorem List.enumFrom_eq_map_enum {α : Type u_1} (l : List α) (n : Nat) :
List.enumFrom n l = List.map (Prod.map (fun (x : Nat) => x + n) id) l.enum