Lists from functions

Theorems and lemmas for dealing with List.ofFn, which converts a function on Fin n to a list of length n.

Main Statements

The main statements pertain to lists generated using List.ofFn

• List.length_ofFn, which tells us the length of such a list
• List.get?_ofFn, which tells us the nth element of such a list
• List.equivSigmaTuple, which is an Equiv between lists and the functions that generate them via List.ofFn.

@[simp]

theorem List.length_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) : List.length (List.ofFn f) = n

The length of a list converted from a function is the size of the domain.

@[simp]

theorem List.get_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (List.length (List.ofFn f))) : List.get (List.ofFn f) i = f (Fin.cast (_ : List.length (List.ofFn f) = n) i)

@[simp]

theorem List.get?_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ) : List.get? (List.ofFn f) i = List.ofFnNthVal f i

The nth element of a list

@[deprecated List.get_ofFn]

theorem List.nthLe_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin n) : List.nthLe (List.ofFn f) ↑i (_ : ↑i < List.length (List.ofFn f)) = f i

@[simp, deprecated List.get_ofFn]

theorem List.nthLe_ofFn' {α : Type u} {n : ℕ} (f : Fin n → α) {i : ℕ} (h : i < List.length (List.ofFn f)) : List.nthLe (List.ofFn f) i h = f { val := i, isLt := (_ : i < n) }

@[simp]

theorem List.map_ofFn {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β) : List.map g (List.ofFn f) = List.ofFn (g ∘ f)

theorem List.ofFn_congr {α : Type u} {m : ℕ} {n : ℕ} (h : m = n) (f : Fin m → α) : List.ofFn f = List.ofFn fun (i : Fin n) => f (Fin.cast (_ : n = m) i)

@[simp]

theorem List.ofFn_zero {α : Type u} (f : Fin 0 → α) : List.ofFn f = []

ofFn on an empty domain is the empty list.

@[simp]

theorem List.ofFn_succ {α : Type u} {n : ℕ} (f : Fin (Nat.succ n) → α) : List.ofFn f = f 0 :: List.ofFn fun (i : Fin n) => f (Fin.succ i)

theorem List.ofFn_succ' {α : Type u} {n : ℕ} (f : Fin (Nat.succ n) → α) : List.ofFn f = List.concat (List.ofFn fun (i : Fin n) => f (Fin.castSucc i)) (f (Fin.last n))

@[simp]

theorem List.ofFn_eq_nil_iff {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = [] ↔ n = 0

theorem List.last_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) (hn : optParam (n - 1 < n) (_ : Nat.pred (Nat.sub n 0) < Nat.sub n 0)) : List.getLast (List.ofFn f) h = f { val := n - 1, isLt := hn }

theorem List.last_ofFn_succ {α : Type u} {n : ℕ} (f : Fin (Nat.succ n) → α) (h : optParam (List.ofFn f ≠ []) (_ : ¬List.ofFn f = [])) : List.getLast (List.ofFn f) h = f (Fin.last n)

theorem List.ofFn_add {α : Type u} {m : ℕ} {n : ℕ} (f : Fin (m + n) → α) : List.ofFn f = (List.ofFn fun (i : Fin m) => f (Fin.castAdd n i)) ++ List.ofFn fun (j : Fin n) => f (Fin.natAdd m j)

Note this matches the convention of List.ofFn_succ', putting the Fin m elements first.

@[simp]

theorem List.ofFn_fin_append {α : Type u} {m : ℕ} {n : ℕ} (a : Fin m → α) (b : Fin n → α) : List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b

theorem List.ofFn_mul {α : Type u} {m : ℕ} {n : ℕ} (f : Fin (m * n) → α) : List.ofFn f = List.join (List.ofFn fun (i : Fin m) => List.ofFn fun (j : Fin n) => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })

This breaks a list of m*n items into m groups each containing n elements.

theorem List.ofFn_mul' {α : Type u} {m : ℕ} {n : ℕ} (f : Fin (m * n) → α) : List.ofFn f = List.join (List.ofFn fun (i : Fin n) => List.ofFn fun (j : Fin m) => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })

This breaks a list of m*n items into n groups each containing m elements.

theorem List.ofFn_get {α : Type u} (l : List α) : List.ofFn (List.get l) = l

@[deprecated List.ofFn_get]

theorem List.ofFn_nthLe {α : Type u} (l : List α) : (List.ofFn fun (i : Fin (List.length l)) => List.nthLe l ↑i (_ : ↑i < List.length l)) = l

theorem List.mem_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) (a : α) : a ∈ List.ofFn f ↔ a ∈ Set.range f

@[simp]

theorem List.forall_mem_ofFn_iff {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop} : (∀ i ∈ List.ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)

@[simp]

theorem List.ofFn_const {α : Type u} (n : ℕ) (c : α) : (List.ofFn fun (x : Fin n) => c) = List.replicate n c

@[simp]

theorem List.ofFn_fin_repeat {α : Type u} {m : ℕ} (a : Fin m → α) (n : ℕ) : List.ofFn (Fin.repeat n a) = List.join (List.replicate n (List.ofFn a))

@[simp]

theorem List.pairwise_ofFn {α : Type u} {R : α → α → Prop} {n : ℕ} {f : Fin n → α} : List.Pairwise R (List.ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

@[simp]

theorem List.equivSigmaTuple_apply_fst {α : Type u} (l : List α) : (List.equivSigmaTuple l).fst = List.length l

@[simp]

theorem List.equivSigmaTuple_apply_snd {α : Type u} (l : List α) : ∀ (a : Fin (List.length l)), (List.equivSigmaTuple l).snd a = List.get l a

@[simp]

theorem List.equivSigmaTuple_symm_apply {α : Type u} (f : (n : ℕ) × (Fin n → α)) : List.equivSigmaTuple.symm f = List.ofFn f.snd

def List.equivSigmaTuple {α : Type u} : List α ≃ (n : ℕ) × (Fin n → α)

Lists are equivalent to the sigma type of tuples of a given length.

Equations

• One or more equations did not get rendered due to their size.

def List.ofFnRec {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) (l : List α) : C l

A recursor for lists that expands a list into a function mapping to its elements.

This can be used with induction l using List.ofFnRec.

Equations

• List.ofFnRec h l = cast (_ : C (List.ofFn (List.get l)) = C l) (h (List.length l) (List.get l))

@[simp]

theorem List.ofFnRec_ofFn {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) {n : ℕ} (f : Fin n → α) : List.ofFnRec h (List.ofFn f) = h n f

theorem List.exists_iff_exists_tuple {α : Type u} {P : List α → Prop} : (∃ (l : List α), P l) ↔ ∃ (n : ℕ) (f : Fin n → α), P (List.ofFn f)

theorem List.forall_iff_forall_tuple {α : Type u} {P : List α → Prop} : (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (List.ofFn f)

theorem List.ofFn_inj' {α : Type u} {m : ℕ} {n : ℕ} {f : Fin m → α} {g : Fin n → α} : List.ofFn f = List.ofFn g ↔ { fst := m, snd := f } = { fst := n, snd := g }

Fin.sigma_eq_iff_eq_comp_cast may be useful to work with the RHS of this expression.

theorem List.ofFn_injective {α : Type u} {n : ℕ} : Function.Injective List.ofFn

Note we can only state this when the two functions are indexed by defeq n.

@[simp]

theorem List.ofFn_inj {α : Type u} {n : ℕ} {f : Fin n → α} {g : Fin n → α} : List.ofFn f = List.ofFn g ↔ f = g

A special case of List.ofFn_inj for when the two functions are indexed by defeq n.