Documentation

Init.Data.List.Nat.Range

Lemmas about List.range and List.enum #

Ranges and enumeration #

range' #

@[simp]
theorem List.mem_range'_1 {s : Nat} {n : Nat} {m : Nat} :
m List.range' s n s m m < s + n
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
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
@[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 : NatBool} :
List.find? p (List.range' s n) = some i p i = true i List.range' s n ∀ (j : Nat), s jj < i(!p j) = true
theorem List.find?_range'_eq_none {s : Nat} {n : Nat} {p : NatBool} :
List.find? p (List.range' s n) = none ∀ (i : Nat), s ii < 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.reverse_range' (s : Nat) (n : Nat) :
(List.range' s n).reverse = List.map (fun (x : Nat) => s + n - 1 - x) (List.range n)
@[simp]
theorem List.mem_range {m : Nat} {n : Nat} :
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.take_range (m : Nat) (n : Nat) :
theorem List.nodup_range (n : Nat) :
(List.range n).Nodup
@[simp]
theorem List.find?_range_eq_some {n : Nat} {i : Nat} {p : NatBool} :
List.find? p (List.range n) = some i p i = true i List.range n ∀ (j : Nat), j < i(!p j) = true
theorem List.find?_range_eq_none {n : Nat} {p : NatBool} :
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 #

@[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} :
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.tail_iota (n : Nat) :
(List.iota n).tail = List.iota (n - 1)
@[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
theorem List.find?_iota_eq_none {n : Nat} {p : NatBool} :
List.find? p (List.iota n) = none ∀ (i : Nat), 0 < ii n(!p i) = true
@[simp]
theorem List.find?_iota_eq_some {n : Nat} {i : Nat} {p : NatBool} :
List.find? p (List.iota n) = some i p i = true i List.iota n ∀ (j : Nat), i < jj 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 α) :
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_map {α : Type u_1} {β : Type u_2} (n : Nat) (l : List α) (f : αβ) :
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_cons_iff {α : Type u_1} {x : Nat × α} {l' : List (Nat × α)} {l : List α} {n : Nat} :
List.enumFrom n l = x :: l' ∃ (a : α), ∃ (as : List α), l = a :: as x = (n, a) l' = List.enumFrom (n + 1) as
theorem List.enumFrom_eq_append_iff {α : Type u_1} {l₁ : List (Nat × α)} {l₂ : List (Nat × α)} {l : List α} {n : Nat} :
List.enumFrom n l = l₁ ++ l₂ ∃ (l₁' : List α), ∃ (l₂' : List α), l = l₁' ++ l₂' l₁ = List.enumFrom n l₁' l₂ = List.enumFrom (n + l₁'.length) l₂'

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?
@[simp]
theorem List.tail_enum {α : Type u_1} (l : List α) :
l.enum.tail = List.enumFrom 1 l.tail
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)
theorem List.enum_eq_cons_iff {α : Type u_1} {x : Nat × α} {l' : List (Nat × α)} {l : List α} :
l.enum = x :: l' ∃ (a : α), ∃ (as : List α), l = a :: as x = (0, a) l' = List.enumFrom 1 as
theorem List.enum_eq_append_iff {α : Type u_1} {l₁ : List (Nat × α)} {l₂ : List (Nat × α)} {l : List α} :
l.enum = l₁ ++ l₂ ∃ (l₁' : List α), ∃ (l₂' : List α), l = l₁' ++ l₂' l₁ = l₁'.enum l₂ = List.enumFrom l₁'.length l₂'