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} [Neg α] (as : List α) : List α

Elementwise negation of a list

Equations

• List.Func.neg as = List.map (fun (a : α) => -a) as

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

• List.Func.set a (head :: as) 0 = a :: as
• List.Func.set a [] 0 = [a]
• List.Func.set a (h :: as) (Nat.succ k) = h :: List.Func.set a as k
• List.Func.set a [] (Nat.succ k) = default :: List.Func.set a [] k

def List.Func.«term_{_↦_}» : Lean.TrailingParserDescr

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} [Inhabited α] : ℕ → List α → α

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

Equations

• List.Func.get x [] = default
• List.Func.get 0 (a :: tail) = a
• List.Func.get (Nat.succ n) (head :: as) = List.Func.get n as

def List.Func.Equiv {α : Type u} [Inhabited α] (as1 : List α) (as2 : List α) : Prop

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

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

• List.Func.pointwise f [] [] = []
• List.Func.pointwise f [] (b :: bs) = List.map (f default) (b :: bs)
• List.Func.pointwise f (a :: as) [] = List.map (fun (x : α) => f x default) (a :: as)
• List.Func.pointwise f (a :: as) (b :: bs) = f a b :: List.Func.pointwise f as bs

def List.Func.add {α : Type u} [Zero α] [Add α] : List α → List α → List α

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

Equations

• List.Func.add = List.Func.pointwise fun (x x_1 : α) => x + x_1

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

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

Equations

• List.Func.sub = List.Func.pointwise Sub.sub

theorem List.Func.length_set {α : Type u} {a : α} [Inhabited α] {m : ℕ} {as : List α} : List.length (List.Func.set a as m) = max (List.length as) (m + 1)

theorem List.Func.get_nil {α : Type u} [Inhabited α] {k : ℕ} : List.Func.get k [] = default

theorem List.Func.get_eq_default_of_le {α : Type u} [Inhabited α] (k : ℕ) {as : List α} : List.length as ≤ k → List.Func.get k as = 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.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 < List.length as → 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 (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 α} : n < List.length as → 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_refl {α : Type u} {as : List α} [Inhabited α] : List.Func.Equiv as as

theorem List.Func.equiv_symm {α : Type u} {as1 : List α} {as2 : List α} [Inhabited α] : List.Func.Equiv as1 as2 → List.Func.Equiv as2 as1

theorem List.Func.equiv_trans {α : Type u} {as1 : List α} {as2 : List α} {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 : List α} {as2 : List α} [Inhabited α] : as1 = as2 → List.Func.Equiv as1 as2

theorem List.Func.eq_of_equiv {α : Type u} [Inhabited α] {as1 : List α} {as2 : List α} : List.length as1 = List.length as2 → List.Func.Equiv as1 as2 → as1 = as2

@[simp]

theorem List.Func.get_neg {α : Type u} [AddGroup α] {k : ℕ} {as : List α} : List.Func.get k (List.Func.neg as) = -List.Func.get k as

@[simp]

theorem List.Func.length_neg {α : Type u} [Neg α] (as : List α) : List.length (List.Func.neg as) = List.length as

theorem List.Func.nil_pointwise {α : Type u} {β : Type v} {γ : Type w} [Inhabited α] [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} [Inhabited α] [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} [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)

theorem List.Func.length_pointwise {α : Type u} {β : Type v} {γ : Type w} [Inhabited α] [Inhabited β] {f : α → β → γ} {as : List α} {bs : List β} : List.length (List.Func.pointwise f as bs) = max (List.length as) (List.length bs)

@[simp]

theorem List.Func.get_add {α : Type u} [AddMonoid α] {k : ℕ} {xs : List α} {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} [Zero α] [Add α] {xs : List α} {ys : List α} : List.length (List.Func.add xs ys) = max (List.length xs) (List.length ys)

@[simp]

theorem List.Func.nil_add {α : Type u} [AddMonoid α] (as : List α) : List.Func.add [] as = as

@[simp]

theorem List.Func.add_nil {α : Type u} [AddMonoid α] (as : List α) : List.Func.add as [] = as

theorem List.Func.map_add_map {α : Type u} [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} [AddGroup α] {k : ℕ} {xs : List α} {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} [Zero α] [Sub α] {xs : List α} {ys : List α} : List.length (List.Func.sub xs ys) = max (List.length xs) (List.length ys)

@[simp]

theorem List.Func.nil_sub {α : Type u_1} [AddGroup α] (as : List α) : List.Func.sub [] as = List.Func.neg as

@[simp]

theorem List.Func.sub_nil {α : Type u_1} [AddGroup α] (as : List α) : List.Func.sub as [] = as