Lists as Functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Definitions for using lists as finite representations of finitely-supported functions with domain ℕ.
These include pointwise operations on lists, as well as get and set operations.
Notations #
An index notation is introduced in this file for setting a particular element of a list. With as
as a list m as an index, and a as a new element, the notation is as {m ↦ a}.
So, for example
[1, 3, 5] {1 ↦ 9} would result in [1, 9, 5]
This notation is in the locale list.func.
Elementwise negation of a list
Equations
- list.func.neg as = list.map (λ (a : α), -a) as
@[simp]
Update element of a list by index. If the index is out of range, extend the list with default elements
Equations
- list.func.set a (h :: as) (k + 1) = h :: list.func.set a as k
- list.func.set a (_x :: as) 0 = a :: as
- list.func.set a list.nil (k + 1) = inhabited.default :: list.func.set a list.nil k
- list.func.set a list.nil 0 = [a]
@[simp]
Get element of a list by index. If the index is out of range, return the default element
Equations
- list.func.get (n + 1) (a :: as) = list.func.get n as
- list.func.get n.succ list.nil = inhabited.default
- list.func.get 0 (a :: as) = a
- list.func.get 0 list.nil = inhabited.default
Pointwise equality of lists. If lists are different lengths, compare with the default element.
Equations
- list.func.equiv as1 as2 = ∀ (m : ℕ), list.func.get m as1 = list.func.get m as2
@[simp]
def
list.func.pointwise
{α : Type u}
{β : Type v}
{γ : Type w}
[inhabited α]
[inhabited β]
(f : α → β → γ) :
Pointwise operations on lists. If lists are different lengths, use the default element.
Equations
- list.func.pointwise f (a :: as) (b :: bs) = f a b :: list.func.pointwise f as bs
- list.func.pointwise f (a :: as) list.nil = list.map (λ (x : α), f x inhabited.default) (a :: as)
- list.func.pointwise f list.nil (b :: bs) = list.map (f inhabited.default) (b :: bs)
- list.func.pointwise f list.nil list.nil = list.nil
Pointwise addition on lists. If lists are different lengths, use zero.
Equations
Pointwise subtraction on lists. If lists are different lengths, use zero.
Equations
theorem
list.func.length_set
{α : Type u}
{a : α}
[inhabited α]
{m : ℕ}
{as : list α} :
(list.func.set a as m).length = linear_order.max as.length (m + 1)
@[simp]
theorem
list.func.get_eq_default_of_le
{α : Type u}
[inhabited α]
(k : ℕ)
{as : list α} :
as.length ≤ k → list.func.get k as = inhabited.default
@[simp]
theorem
list.func.get_set
{α : Type u}
[inhabited α]
{a : α}
{k : ℕ}
{as : list α} :
list.func.get k (list.func.set a as k) = a
theorem
list.func.mem_get_of_ne_zero
{α : Type u}
[inhabited α]
{n : ℕ}
{as : list α} :
list.func.get n as ≠ inhabited.default → list.func.get n as ∈ as
theorem
list.func.get_set_eq_of_ne
{α : Type u}
[inhabited α]
{a : α}
{as : list α}
(k m : ℕ) :
m ≠ k → list.func.get m (list.func.set a as k) = list.func.get m as
theorem
list.func.get_map'
{α : Type u}
{β : Type v}
[inhabited α]
[inhabited β]
{f : α → β}
{n : ℕ}
{as : list α} :
f inhabited.default = inhabited.default → list.func.get n (list.map f as) = f (list.func.get n as)
theorem
list.func.forall_val_of_forall_mem
{α : Type u}
[inhabited α]
{as : list α}
{p : α → Prop} :
p inhabited.default → (∀ (x : α), x ∈ as → p x) → ∀ (n : ℕ), p (list.func.get n as)
theorem
list.func.equiv_symm
{α : Type u}
{as1 as2 : list α}
[inhabited α] :
list.func.equiv as1 as2 → list.func.equiv as2 as1
theorem
list.func.equiv_trans
{α : Type u}
{as1 as2 as3 : list α}
[inhabited α] :
list.func.equiv as1 as2 → list.func.equiv as2 as3 → list.func.equiv as1 as3
theorem
list.func.equiv_of_eq
{α : Type u}
{as1 as2 : list α}
[inhabited α] :
as1 = as2 → list.func.equiv as1 as2
@[simp]
theorem
list.func.get_neg
{α : Type u}
[add_group α]
{k : ℕ}
{as : list α} :
list.func.get k (list.func.neg as) = -list.func.get k as
@[simp]
theorem
list.func.length_neg
{α : Type u}
[has_neg α]
(as : list α) :
(list.func.neg as).length = as.length
theorem
list.func.nil_pointwise
{α : Type u}
{β : Type v}
{γ : Type w}
[inhabited α]
[inhabited β]
{f : α → β → γ}
(bs : list β) :
list.func.pointwise f list.nil bs = list.map (f inhabited.default) bs
theorem
list.func.pointwise_nil
{α : Type u}
{β : Type v}
{γ : Type w}
[inhabited α]
[inhabited β]
{f : α → β → γ}
(as : list α) :
list.func.pointwise f as list.nil = list.map (λ (a : α), f a inhabited.default) as
theorem
list.func.get_pointwise
{α : Type u}
{β : Type v}
{γ : Type w}
[inhabited α]
[inhabited β]
[inhabited γ]
{f : α → β → γ}
(h1 : f inhabited.default inhabited.default = inhabited.default)
(k : ℕ)
(as : list α)
(bs : list β) :
list.func.get k (list.func.pointwise f as bs) = f (list.func.get k as) (list.func.get k bs)
@[simp]
theorem
list.func.get_add
{α : Type u}
[add_monoid α]
{k : ℕ}
{xs ys : list α} :
list.func.get k (list.func.add xs ys) = list.func.get k xs + list.func.get k ys
@[simp]
theorem
list.func.length_add
{α : Type u}
[has_zero α]
[has_add α]
{xs ys : list α} :
(list.func.add xs ys).length = linear_order.max xs.length ys.length
@[simp]
theorem
list.func.nil_add
{α : Type u}
[add_monoid α]
(as : list α) :
list.func.add list.nil as = as
@[simp]
theorem
list.func.add_nil
{α : Type u}
[add_monoid α]
(as : list α) :
list.func.add as list.nil = as
@[simp]
theorem
list.func.get_sub
{α : Type u}
[add_group α]
{k : ℕ}
{xs ys : list α} :
list.func.get k (list.func.sub xs ys) = list.func.get k xs - list.func.get k ys
@[simp]
theorem
list.func.length_sub
{α : Type u}
[has_zero α]
[has_sub α]
{xs ys : list α} :
(list.func.sub xs ys).length = linear_order.max xs.length ys.length
@[simp]
theorem
list.func.nil_sub
{α : Type u_1}
[add_group α]
(as : list α) :
list.func.sub list.nil as = list.func.neg as
@[simp]
theorem
list.func.sub_nil
{α : Type u_1}
[add_group α]
(as : list α) :
list.func.sub as list.nil = as