Documentation

Mathlib.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}↦ a}.

So, for example [1, 3, 5] {1 ↦ 9}↦ 9} would result in [1, 9, 5]

This notation is in the locale list.func.

def List.Func.neg {α : Type u} [inst : Neg α] (as : List α) :
List α

Elementwise negation of a list

Equations
def List.Func.set {α : Type u} [inst : 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

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

Equations
  • One or more equations did not get rendered due to their size.
def List.Func.get {α : Type u} [inst : 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} [inst : Inhabited α] (as1 : List α) (as2 : List α) :

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

Equations
def List.Func.pointwise {α : Type u} {β : Type v} {γ : Type w} [inst : Inhabited α] [inst : 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} [inst : Zero α] [inst : Add α] :
List αList αList α

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

Equations
def List.Func.sub {α : Type u} [inst : Zero α] [inst : Sub α] :
List αList αList α

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

Equations
theorem List.Func.length_set {α : Type u} {a : α} [inst : Inhabited α] {m : } {as : List α} :
theorem List.Func.get_nil {α : Type u} [inst : Inhabited α] {k : } :
List.Func.get k [] = default
theorem List.Func.get_eq_default_of_le {α : Type u} [inst : Inhabited α] (k : ) {as : List α} :
List.length as kList.Func.get k as = default
@[simp]
theorem List.Func.get_set {α : Type u} [inst : Inhabited α] {a : α} {k : } {as : List α} :
theorem List.Func.eq_get_of_mem {α : Type u} [inst : Inhabited α] {a : α} {as : List α} :
a asn, a = List.Func.get n as
theorem List.Func.mem_get_of_le {α : Type u} [inst : Inhabited α] {n : } {as : List α} :
n < List.length asList.Func.get n as as
theorem List.Func.mem_get_of_ne_zero {α : Type u} [inst : Inhabited α] {n : } {as : List α} :
List.Func.get n as defaultList.Func.get n as as
theorem List.Func.get_set_eq_of_ne {α : Type u} [inst : Inhabited α] {a : α} {as : List α} (k : ) (m : ) :
theorem List.Func.get_map {α : Type u} {β : Type v} [inst : Inhabited α] [inst : Inhabited β] {f : αβ} {n : } {as : List α} :
n < List.length asList.Func.get n (List.map f as) = f (List.Func.get n as)
theorem List.Func.get_map' {α : Type u} {β : Type v} [inst : Inhabited α] [inst : Inhabited β] {f : αβ} {n : } {as : List α} :
f default = defaultList.Func.get n (List.map f as) = f (List.Func.get n as)
theorem List.Func.forall_val_of_forall_mem {α : Type u} [inst : Inhabited α] {as : List α} {p : αProp} :
p default((x : α) → x asp x) → (n : ) → p (List.Func.get n as)
theorem List.Func.equiv_refl {α : Type u} {as : List α} [inst : Inhabited α] :
theorem List.Func.equiv_symm {α : Type u} {as1 : List α} {as2 : List α} [inst : Inhabited α] :
List.Func.Equiv as1 as2List.Func.Equiv as2 as1
theorem List.Func.equiv_trans {α : Type u} {as1 : List α} {as2 : List α} {as3 : List α} [inst : Inhabited α] :
List.Func.Equiv as1 as2List.Func.Equiv as2 as3List.Func.Equiv as1 as3
theorem List.Func.equiv_of_eq {α : Type u} {as1 : List α} {as2 : List α} [inst : Inhabited α] :
as1 = as2List.Func.Equiv as1 as2
theorem List.Func.eq_of_equiv {α : Type u} [inst : Inhabited α] {as1 : List α} {as2 : List α} :
List.length as1 = List.length as2List.Func.Equiv as1 as2as1 = as2
@[simp]
theorem List.Func.get_neg {α : Type u} [inst : AddGroup α] {k : } {as : List α} :
@[simp]
theorem List.Func.length_neg {α : Type u} [inst : Neg α] (as : List α) :
theorem List.Func.nil_pointwise {α : Type u} {β : Type v} {γ : Type w} [inst : Inhabited α] [inst : Inhabited β] {f : αβγ} (bs : List β) :
List.Func.pointwise f [] bs = List.map (f default) bs
theorem List.Func.pointwise_nil {α : Type u} {β : Type v} {γ : Type w} [inst : Inhabited α] [inst : Inhabited β] {f : αβγ} (as : List α) :
List.Func.pointwise f as [] = List.map (fun a => f a default) as
theorem List.Func.get_pointwise {α : Type u} {β : Type v} {γ : Type w} [inst : Inhabited α] [inst : Inhabited β] [inst : Inhabited γ] {f : αβγ} (h1 : f default default = default) (k : ) (as : List α) (bs : List β) :
theorem List.Func.length_pointwise {α : Type u} {β : Type v} {γ : Type w} [inst : Inhabited α] [inst : Inhabited β] {f : αβγ} {as : List α} {bs : List β} :
@[simp]
theorem List.Func.get_add {α : Type u} [inst : AddMonoid α] {k : } {xs : List α} {ys : List α} :
@[simp]
theorem List.Func.length_add {α : Type u} [inst : Zero α] [inst : Add α] {xs : List α} {ys : List α} :
@[simp]
theorem List.Func.nil_add {α : Type u} [inst : AddMonoid α] (as : List α) :
List.Func.add [] as = as
@[simp]
theorem List.Func.add_nil {α : Type u} [inst : AddMonoid α] (as : List α) :
List.Func.add as [] = as
theorem List.Func.map_add_map {α : Type u} [inst : AddMonoid α] (f : αα) (g : αα) {as : List α} :
List.Func.add (List.map f as) (List.map g as) = List.map (fun x => f x + g x) as
@[simp]
theorem List.Func.get_sub {α : Type u} [inst : AddGroup α] {k : } {xs : List α} {ys : List α} :
@[simp]
theorem List.Func.length_sub {α : Type u} [inst : Zero α] [inst : Sub α] {xs : List α} {ys : List α} :
@[simp]
theorem List.Func.nil_sub {α : Type} [inst : AddGroup α] (as : List α) :
@[simp]
theorem List.Func.sub_nil {α : Type} [inst : AddGroup α] (as : List α) :
List.Func.sub as [] = as