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 < (range' n m).length) : (range' n m)[i] = n + i

theorem List.isChain_range (r : ℕ → ℕ → Prop) (n : ℕ) : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ

theorem List.isChain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) : IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

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

@[deprecated List.isChain_cons_range_succ (since := "2025-09-21")]

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

Alias of List.isChain_cons_range_succ.

@[deprecated List.isChain_range_succ (since := "2025-09-24")]

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

Alias of List.isChain_range_succ.

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 ℕ) : Pairwise Disjoint l.ranges

The members of l.ranges are pairwise disjoint

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

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