data.list.func

# 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.

def list.func.neg {α : Type u} [has_neg α] (as : list α) :
list α

Elementwise negation of a list

Equations
@[simp]
def list.func.set {α : Type u} [inhabited α] (a : α) :
list αlist α

Update element of a list by index. If the index is out of range, extend the list with default elements

Equations
@[simp]
def list.func.get {α : Type u} [inhabited α] :
list α → α

Get element of a list by index. If the index is out of range, return the default element

Equations
def list.func.equiv {α : Type u} [inhabited α] (as1 as2 : list α) :
Prop

Pointwise equality of lists. If lists are different lengths, compare with the default element.

Equations
• as2 = ∀ (m : ), as1 = as2
@[simp]
def list.func.pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] (f : α → β → γ) :
list αlist βlist γ

Pointwise operations on lists. If lists are different lengths, use the default element.

Equations
def list.func.add {α : Type u} [has_zero α] [has_add α] :
list αlist αlist α

Pointwise addition on lists. If lists are different lengths, use zero.

Equations
def list.func.sub {α : Type u} [has_zero α] [has_sub α] :
list αlist αlist α

Pointwise subtraction on lists. If lists are different lengths, use zero.

Equations
theorem list.func.length_set {α : Type u} {a : α} [inhabited α] {m : } {as : list α} :
as {m a}.length = max as.length (m + 1)
@[simp]
theorem list.func.get_nil {α : Type u} [inhabited α] {k : } :
theorem list.func.get_eq_default_of_le {α : Type u} [inhabited α] (k : ) {as : list α} :
as.length k as =
@[simp]
theorem list.func.get_set {α : Type u} [inhabited α] {a : α} {k : } {as : list α} :
as {k a} = a
theorem list.func.eq_get_of_mem {α : Type u} [inhabited α] {a : α} {as : list α} :
a as(∃ (n : ), α → a = as)
theorem list.func.mem_get_of_le {α : Type u} [inhabited α] {n : } {as : list α} :
n < as.length as as
theorem list.func.mem_get_of_ne_zero {α : Type u} [inhabited α] {n : } {as : list α} :
as as as
theorem list.func.get_set_eq_of_ne {α : Type u} [inhabited α] {a : α} {as : list α} (k m : ) :
m k as {k a} = as
theorem list.func.get_map {α : Type u} {β : Type v} [inhabited α] [inhabited β] {f : α → β} {n : } {as : list α} :
n < as.length (list.map f as) = f as)
theorem list.func.get_map' {α : Type u} {β : Type v} [inhabited α] [inhabited β] {f : α → β} {n : } {as : list α} :
f (default α) = (list.map f as) = f as)
theorem list.func.forall_val_of_forall_mem {α : Type u} [inhabited α] {as : list α} {p : α → Prop} :
p (default α)(∀ (x : α), x asp x)∀ (n : ), p as)
theorem list.func.equiv_refl {α : Type u} {as : list α} [inhabited α] :
as
theorem list.func.equiv_symm {α : Type u} {as1 as2 : list α} [inhabited α] :
as2 as1
theorem list.func.equiv_trans {α : Type u} {as1 as2 as3 : list α} [inhabited α] :
as2 as3 as3
theorem list.func.equiv_of_eq {α : Type u} {as1 as2 : list α} [inhabited α] :
as1 = as2 as2
theorem list.func.eq_of_equiv {α : Type u} [inhabited α] {as1 as2 : list α} :
as1.length = as2.length as2as1 = as2
@[simp]
theorem list.func.get_neg {α : Type u} [add_group α] {k : } {as : list α} :
(list.func.neg as) = - as
@[simp]
theorem list.func.length_neg {α : Type u} [has_neg α] (as : list α) :
theorem list.func.nil_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} (bs : list β) :
= list.map (f (default α)) bs
theorem list.func.pointwise_nil {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} (as : list α) :
= 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 β) = ) (k : ) (as : list α) (bs : list β) :
as bs) = f as) bs)
theorem list.func.length_pointwise {α : Type u} {β : Type v} {γ : Type w} [inhabited α] [inhabited β] {f : α → β → γ} {as : list α} {bs : list β} :
as bs).length = max as.length bs.length
@[simp]
theorem list.func.get_add {α : Type u} [add_monoid α] {k : } {xs ys : list α} :
ys) = xs + ys
@[simp]
theorem list.func.length_add {α : Type u} [has_zero α] [has_add α] {xs ys : list α} :
ys).length = max xs.length ys.length
@[simp]
theorem list.func.nil_add {α : Type u} [add_monoid α] (as : list α) :
= as
@[simp]
theorem list.func.add_nil {α : Type u} [add_monoid α] (as : list α) :
= as
theorem list.func.map_add_map {α : Type u} [add_monoid α] (f g : α → α) {as : list α} :
list.func.add (list.map f as) (list.map g as) = list.map (λ (x : α), f x + g x) as
@[simp]
theorem list.func.get_sub {α : Type u} [add_group α] {k : } {xs ys : list α} :
ys) = xs - ys
@[simp]
theorem list.func.length_sub {α : Type u} [has_zero α] [has_sub α] {xs ys : list α} :
ys).length = max xs.length ys.length
@[simp]
theorem list.func.nil_sub {α : Type} [add_group α] (as : list α) :
@[simp]
theorem list.func.sub_nil {α : Type} [add_group α] (as : list α) :
= as