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.
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
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
theorem
List.chain_succ_range'
(s : ℕ)
(n : ℕ)
:
List.Chain (fun a b => b = Nat.succ a) s (List.range' (s + 1) n)
theorem
List.chain_lt_range'
(s : ℕ)
(n : ℕ)
:
List.Chain (fun x x_1 => x < x_1) s (List.range' (s + 1) n)
theorem
List.pairwise_lt_range'
(s : ℕ)
(n : ℕ)
:
List.Pairwise (fun x x_1 => x < x_1) (List.range' s n)
@[simp]
theorem
List.range'_append
(s : ℕ)
(m : ℕ)
(n : ℕ)
:
List.range' s m ++ List.range' (s + m) n = List.range' s (n + m)
theorem
List.range'_sublist_right
{s : ℕ}
{m : ℕ}
{n : ℕ}
:
List.Sublist (List.range' s m) (List.range' s n) ↔ m ≤ n
@[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
@[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
theorem
List.range_loop_range'
(s : ℕ)
(n : ℕ)
:
List.range.loop s (List.range' s n) = List.range' 0 (n + s)
theorem
List.range'_eq_map_range
(s : ℕ)
(n : ℕ)
:
List.range' s n = List.map (fun x => s + x) (List.range n)
theorem
List.chain'_range_succ
(r : ℕ → ℕ → Prop)
(n : ℕ)
:
List.Chain' r (List.range (Nat.succ n)) ↔ (m : ℕ) → m < n → r m (Nat.succ m)
theorem
List.range_add
(a : ℕ)
(b : ℕ)
:
List.range (a + b) = List.range a ++ List.map (fun x => a + x) (List.range b)
theorem
List.reverse_range'
(s : ℕ)
(n : ℕ)
:
List.reverse (List.range' s n) = List.map (fun i => s + n - 1 - i) (List.range 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)
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.
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.
@[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)
@[simp]
theorem
List.enum_map_fst
{α : Type u}
(l : List α)
:
List.map Prod.fst (List.enum l) = List.range (List.length l)
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.enum_from_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_enum_from_eq_prod
{α : Type u}
(l : List α)
{n : ℕ}
:
List.unzip (List.enumFrom n l) = (List.range' n (List.length l), l)
@[simp]
theorem
List.get_range
{n : ℕ}
(i : ℕ)
(H : i < List.length (List.range n))
:
List.get (List.range n) { val := i, isLt := H } = i
@[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 := (_ : i < n) }
@[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 := (_ : i < n) }