Ranges of naturals as lists

This file shows basic results about List.iota, List.range, List.range' 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.

@[simp]

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

theorem List.pairwise_lt_range' (s : ℕ) (n : ℕ) (step : optParam ℕ 1) : autoParam (0 < step) _auto✝ → List.Pairwise (fun (x x_1 : ℕ) => x < x_1) (List.range' s n step)

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

@[simp]

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

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

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

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

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

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

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

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

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

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) ⋯

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem List.pairwise_lt_finRange (n : ℕ) : List.Pairwise (fun (x x_1 : Fin n) => x < x_1) (List.finRange n)

theorem List.pairwise_le_finRange (n : ℕ) : List.Pairwise (fun (x x_1 : Fin n) => x ≤ x_1) (List.finRange n)

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

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

theorem List.sum_range_succ' {α : Type u} [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.

theorem List.prod_range_succ' {α : Type u} [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.

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[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 := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem List.indexOf_finRange {k : ℕ} (i : Fin k) : List.indexOf i (List.finRange k) = ↑i

def List.ranges : List ℕ → List (List ℕ)

From l : List ℕ, construct l.ranges : List (List ℕ) such that l.ranges.map List.length = l and l.ranges.join = range l.sum

• Example: [1,2,3].ranges = [[0],[1,2],[3,4,5]]

Equations

• List.ranges [] = []
• List.ranges (a :: l) = List.range a :: List.map (List.map fun (x : ℕ) => a + x) (List.ranges l)

theorem List.ranges_disjoint (l : List ℕ) : List.Pairwise List.Disjoint (List.ranges l)

The members of l.ranges are pairwise disjoint

theorem List.ranges_length (l : List ℕ) : List.map List.length (List.ranges l) = l

The lengths of the members of l.ranges are those given by l

theorem List.ranges_join (l : List ℕ) : List.join (List.ranges l) = List.range (List.sum l)

theorem List.mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} : (∃ s ∈ List.ranges l, n ∈ s) ↔ n < List.sum l

Any entry of any member of l.ranges is strictly smaller than l.sum

theorem List.ranges_nodup {l : List ℕ} {s : List ℕ} (hs : s ∈ List.ranges l) : List.Nodup s

The members of l.ranges have no duplicate