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.

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

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

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

@[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.finRange n).Nodup

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem List.getElem_finRange {n : ℕ} {i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n)[i] = ⟨i, ⋯⟩

theorem List.get_finRange {n : ℕ} {i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩

@[deprecated List.get_range']

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

Alias of List.get_range'.

@[deprecated List.getElem_range'_1]

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

Alias of List.getElem_range'_1.

@[deprecated List.get_range]

theorem List.nthLe_range {n : ℕ} (i : ℕ) (H : i < (List.range n).length) : (List.range n).get ⟨i, H⟩ = i

Alias of List.get_range.

@[deprecated List.get_finRange]

theorem List.nthLe_finRange {n : ℕ} {i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩

Alias of List.get_finRange.

@[simp]

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

@[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

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

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

The members of l.ranges are pairwise disjoint

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

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

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

See List.ranges_join for the version about List.sum.

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

Any entry of any member of l.ranges is strictly smaller than Nat.sum l. See List.mem_mem_ranges_iff_lt_sum for the version about List.sum.

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

The members of l.ranges have no duplicate