Lists as Functions #
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
@[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 = default α
- list.func.get 0 (a :: as) = a
- list.func.get 0 list.nil = 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 (default β)) (a :: as)
- list.func.pointwise f list.nil (b :: bs) = list.map (f (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
@[simp]
theorem
list.func.get_eq_default_of_le
{α : Type u}
[inhabited α]
(k : ℕ)
{as : list α} :
as.length ≤ k → list.func.get k as = default α
@[simp]
theorem
list.func.get_set
{α : Type u}
[inhabited α]
{a : α}
{k : ℕ}
{as : list α} :
list.func.get k as {k ↦ a} = a
theorem
list.func.eq_get_of_mem
{α : Type u}
[inhabited α]
{a : α}
{as : list α} :
a ∈ as → (∃ (n : ℕ), α → a = list.func.get n as)
theorem
list.func.mem_get_of_le
{α : Type u}
[inhabited α]
{n : ℕ}
{as : list α} :
n < as.length → list.func.get n as ∈ as
theorem
list.func.mem_get_of_ne_zero
{α : Type u}
[inhabited α]
{n : ℕ}
{as : list α} :
list.func.get n as ≠ 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 as {k ↦ a} = list.func.get m as
theorem
list.func.get_map
{α : Type u}
{β : Type v}
[inhabited α]
[inhabited β]
{f : α → β}
{n : ℕ}
{as : list α} :
n < as.length → list.func.get n (list.map f as) = f (list.func.get n as)
theorem
list.func.get_map'
{α : Type u}
{β : Type v}
[inhabited α]
[inhabited β]
{f : α → β}
{n : ℕ}
{as : list α} :
f (default α) = 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 (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
theorem
list.func.eq_of_equiv
{α : Type u}
[inhabited α]
{as1 as2 : list α} :
as1.length = as2.length → list.func.equiv as1 as2 → 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 (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 (default β)) as
theorem
list.func.get_pointwise
{α : Type u}
{β : Type v}
{γ : Type w}
[inhabited α]
[inhabited β]
[inhabited γ]
{f : α → β → γ}
(h1 : f (default α) (default β) = 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.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.nil_sub
{α : Type}
[add_group α]
(as : list α) :
list.func.sub list.nil as = list.func.neg as
@[simp]