Mathlib.Data.List.Range

Module docstring

{"# 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. "}

List.getElem_range'_1 theorem

{n m} (i) (H : i < (range' n m).length) : (range' n m)[i] = n + i

Full source

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

Element Access in `range'` List: $(range'\, n\, m)[i] = n + i$ for $i < length(range'\, n\, m)$

Informal description

For any natural numbers $n$ and $m$, and any index $i$ such that $i$ is less than the length of the list `range' n m`, the $i$-th element of `range' n m` is equal to $n + i$.

List.chain'_range_succ theorem

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

Full source

theorem chain'_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
    Chain'Chain' r (range n.succ) ↔ ∀ m < n, r m m.succ := by
  rw [range_succ]
  induction' n with n hn
  · simp
  · rw [range_succ]
    simp only [append_assoc, singleton_append, chain'_append_cons_cons, chain'_singleton, and_true]
    rw [hn, forall_lt_succ]

Chain Condition for Successor Range List: $\operatorname{Chain}'\, r\, [0, \ldots, n] \leftrightarrow \forall m < n, r(m, m+1)$

Informal description

For any binary relation $r$ on natural numbers and any natural number $n$, the list $\operatorname{range}(n+1) = [0, \ldots, n]$ satisfies the chain condition $\operatorname{Chain}'\, r$ if and only if for every natural number $m < n$, the relation $r(m, m+1)$ holds.

List.chain_range_succ theorem

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

Full source

theorem chain_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :
    ChainChain r a (range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ := by
  rw [range_succ_eq_map, chain_cons, and_congr_right_iff, ← chain'_range_succ, range_succ_eq_map]
  exact fun _ => Iff.rfl

Chain Condition for Successor Range List with Initial Element: $\operatorname{Chain}\, r\, a\, [0, \ldots, n] \leftrightarrow r(a, 0) \land \forall m < n, r(m, m+1)$

Informal description

For any binary relation $r$ on natural numbers and natural numbers $n$ and $a$, the list $\operatorname{range}(n+1) = [0, \ldots, n]$ satisfies the chain condition $\operatorname{Chain}\, r\, a$ if and only if $r(a, 0)$ holds and for every natural number $m < n$, the relation $r(m, m+1)$ holds.

List.ranges definition

: List ℕ → List (List ℕ)

Full source

/-- 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]]` -/
def ranges : List ℕ → List (List ℕ)
  | [] => nil
  | a::l => range a::(ranges l).map (map (a + ·))

List of ranges corresponding to natural numbers

Informal description

Given a list of natural numbers `l`, the function `ranges` constructs a list of lists of natural numbers such that: 1. The lengths of the sublists correspond to the elements of `l`, i.e., `l.ranges.map List.length = l`. 2. The concatenation of all sublists is the list `[0, 1, ..., (l.sum) - 1]`. For example, `[1, 2, 3].ranges = [[0], [1, 2], [3, 4, 5]]`.

List.ranges_disjoint theorem

(l : List ℕ) : Pairwise Disjoint (ranges l)

Full source

/-- The members of `l.ranges` are pairwise disjoint -/
theorem ranges_disjoint (l : List ℕ) :
    Pairwise Disjoint (ranges l) := by
  induction l with
  | nil => exact Pairwise.nil
  | cons a l hl =>
    simp only [ranges, pairwise_cons]
    constructor
    · intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rintro ⟨v, _, rfl⟩
      rw [mem_range] at hu
      omega
    · rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel

Pairwise Disjointness of Sublists in `ranges` Construction

Informal description

For any list of natural numbers $l$, the sublists in $l.\text{ranges}$ are pairwise disjoint. That is, for any two distinct sublists $L_1$ and $L_2$ in $l.\text{ranges}$, their intersection is empty: $L_1 \cap L_2 = \emptyset$.

List.ranges_length theorem

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

Full source

/-- The lengths of the members of `l.ranges` are those given by `l` -/
theorem ranges_length (l : List ℕ) :
    l.ranges.map length = l := by
  induction l with
  | nil => simp only [ranges, map_nil]
  | cons a l hl => -- (a :: l)
    simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]

Lengths of Sublists in `ranges` Match Original List

Informal description

For any list of natural numbers $l$, the list obtained by mapping the `length` function over the sublists produced by `l.ranges` is equal to $l$ itself. In other words, the lengths of the sublists in `l.ranges` correspond exactly to the elements of $l$.