Ranges of naturals as lists

This file shows basic results about List.iota, List.range, List.range' (all defined in data.list.defs) and defines List.finRange. finRange n is the list of elements of Fin n. iota n = [n, n - 1, ..., 1] and range n = [0, ..., n - 1] are basic list constructions used for tactics. range' a b = [a, ..., a + b - 1] is there to help prove properties about them. Actual maths should use List.Ico instead.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

theorem List.map_sub_range' (a : ℕ) (s : ℕ) (n : ℕ) : a ≤ s → List.map (fun x => x - a) (List.range' s n) = List.range' (s - a) n

ink

theorem List.chain_succ_range' (s : ℕ) (n : ℕ) : List.Chain (fun a b => b = Nat.succ a) s (List.range' (s + 1) n)

ink

theorem List.chain_lt_range' (s : ℕ) (n : ℕ) : List.Chain (fun x x_1 => x < x_1) s (List.range' (s + 1) n)

ink

theorem List.pairwise_lt_range' (s : ℕ) (n : ℕ) : List.Pairwise (fun x x_1 => x < x_1) (List.range' s n)

ink

theorem List.nodup_range' (s : ℕ) (n : ℕ) : List.Nodup (List.range' s n)

ink

@[simp]

theorem List.range'_append (s : ℕ) (m : ℕ) (n : ℕ) : List.range' s m ++ List.range' (s + m) n = List.range' s (n + m)

ink

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

ink

theorem List.range'_subset_right {s : ℕ} {m : ℕ} {n : ℕ} : List.range' s m ⊆ List.range' s n ↔ m ≤ n

ink

theorem List.get?_range' (s : ℕ) {m : ℕ} {n : ℕ} : m < n → List.get? (List.range' s n) m = some (s + m)

ink

@[simp]

theorem List.get_range' {n : ℕ} {m : ℕ} (i : ℕ) (H : i < List.length (List.range' n m)) : List.get (List.range' n m) { val := i, isLt := H } = n + i

ink

@[simp]

theorem List.nthLe_range' {n : ℕ} {m : ℕ} (i : ℕ) (H : i < List.length (List.range' n m)) : List.nthLe (List.range' n m) i H = n + i

ink

theorem List.range'_concat (s : ℕ) (n : ℕ) : List.range' s (n + 1) = List.range' s n ++ [s + n]

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem List.pairwise_lt_range (n : ℕ) : List.Pairwise (fun x x_1 => x < x_1) (List.range n)

ink

theorem List.pairwise_le_range (n : ℕ) : List.Pairwise (fun x x_1 => x ≤ x_1) (List.range n)

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

theorem List.get?_range {m : ℕ} {n : ℕ} (h : m < n) : List.get? (List.range n) m = some m

ink

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

ink

@[simp]

theorem List.range_zero : List.range 0 = []

ink

theorem List.chain'_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) : List.Chain' r (List.range (Nat.succ n)) ↔ (m : ℕ) → m < n → r m (Nat.succ m)

ink

theorem List.chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) (a : ℕ) : List.Chain r a (List.range (Nat.succ n)) ↔ r a 0 ∧ ((m : ℕ) → m < n → r m (Nat.succ m))

ink

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

ink

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

ink

@[simp]

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

ink

theorem List.pairwise_gt_iota (n : ℕ) : List.Pairwise (fun x x_1 => x > x_1) (List.iota n)

ink

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

ink

theorem List.mem_iota {m : ℕ} {n : ℕ} : m ∈ List.iota n ↔ 1 ≤ m ∧ m ≤ n

ink

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

ink

def List.finRange (n : ℕ) : List (Fin n)

All elements of Fin n, from 0 to n-1. The corresponding finset is Finset.univ.

Equations

• List.finRange n = List.pmap Fin.mk (List.range n) (_ : ∀ (x : ℕ), x ∈ List.range n → x < n)

ink

@[simp]

theorem List.finRange_zero : List.finRange 0 = []

ink

@[simp]

theorem List.mem_finRange {n : ℕ} (a : Fin n) : a ∈ List.finRange n

ink

theorem List.nodup_finRange (n : ℕ) : List.Nodup (List.finRange n)

ink

@[simp]

theorem List.length_finRange (n : ℕ) : List.length (List.finRange n) = n

ink

@[simp]

theorem List.finRange_eq_nil {n : ℕ} : List.finRange n = [] ↔ n = 0

ink

theorem List.sum_range_succ {α : Type u} [inst : AddMonoid α] (f : ℕ → α) (n : ℕ) : List.sum (List.map f (List.range (Nat.succ n))) = List.sum (List.map f (List.range n)) + f n

ink

theorem List.prod_range_succ {α : Type u} [inst : Monoid α] (f : ℕ → α) (n : ℕ) : List.prod (List.map f (List.range (Nat.succ n))) = List.prod (List.map f (List.range n)) * f n

ink

theorem List.sum_range_succ' {α : Type u} [inst : AddMonoid α] (f : ℕ → α) (n : ℕ) : List.sum (List.map f (List.range (Nat.succ n))) = f 0 + List.sum (List.map (fun i => f (Nat.succ i)) (List.range n))

A variant of sum_range_succ which pulls off the first term in the sum rather than the last.

ink

theorem List.prod_range_succ' {α : Type u} [inst : Monoid α] (f : ℕ → α) (n : ℕ) : List.prod (List.map f (List.range (Nat.succ n))) = f 0 * List.prod (List.map (fun i => f (Nat.succ i)) (List.range n))

A variant of prod_range_succ which pulls off the first term in the product rather than the last.

ink

@[simp]

theorem List.enum_from_map_fst {α : Type u} (n : ℕ) (l : List α) : List.map Prod.fst (List.enumFrom n l) = List.range' n (List.length l)

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

theorem List.enum_from_eq_zip_range' {α : Type u} (l : List α) {n : ℕ} : List.enumFrom n l = List.zip (List.range' n (List.length l)) l

ink

@[simp]

theorem List.unzip_enum_from_eq_prod {α : Type u} (l : List α) {n : ℕ} : List.unzip (List.enumFrom n l) = (List.range' n (List.length l), l)

ink

@[simp]

theorem List.get_range {n : ℕ} (i : ℕ) (H : i < List.length (List.range n)) : List.get (List.range n) { val := i, isLt := H } = i

ink

@[simp]

theorem List.nthLe_range {n : ℕ} (i : ℕ) (H : i < List.length (List.range n)) : List.nthLe (List.range n) i H = i

ink

@[simp]

theorem List.get_finRange {n : ℕ} {i : ℕ} (h : i < List.length (List.finRange n)) : List.get (List.finRange n) { val := i, isLt := h } = { val := i, isLt := (_ : i < n) }

ink

@[simp]

theorem List.finRange_map_get {α : Type u} (l : List α) : List.map (List.get l) (List.finRange (List.length l)) = l

ink

@[simp]

theorem List.nthLe_finRange {n : ℕ} {i : ℕ} (h : i < List.length (List.finRange n)) : List.nthLe (List.finRange n) i h = { val := i, isLt := (_ : i < n) }