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.

ink

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

Elementwise negation of a list

Equations

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

ink

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

• 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

ink

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.

ink

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

• 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

ink

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

ink

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

• 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

ink

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

• List.Func.add = List.Func.pointwise fun x x_1 => x + x_1

ink

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

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

ink

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

ink

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

ink

theorem List.Func.get_eq_default_of_le {α : Type u} [inst : Inhabited α] (k : ℕ) {as : List α} : List.length as ≤ k → List.Func.get k as = default

ink

@[simp]

theorem List.Func.get_set {α : Type u} [inst : Inhabited α] {a : α} {k : ℕ} {as : List α} : List.Func.get k (List.Func.set a as k) = a

ink

theorem List.Func.eq_get_of_mem {α : Type u} [inst : Inhabited α] {a : α} {as : List α} : a ∈ as → ∃ n, a = List.Func.get n as

ink

theorem List.Func.mem_get_of_le {α : Type u} [inst : Inhabited α] {n : ℕ} {as : List α} : n < List.length as → List.Func.get n as ∈ as

ink

theorem List.Func.mem_get_of_ne_zero {α : Type u} [inst : Inhabited α] {n : ℕ} {as : List α} : List.Func.get n as ≠ default → List.Func.get n as ∈ as

ink

theorem List.Func.get_set_eq_of_ne {α : Type u} [inst : Inhabited α] {a : α} {as : List α} (k : ℕ) (m : ℕ) : m ≠ k → List.Func.get m (List.Func.set a as k) = List.Func.get m as

ink

theorem List.Func.get_map {α : Type u} {β : Type v} [inst : Inhabited α] [inst : Inhabited β] {f : α → β} {n : ℕ} {as : List α} : n < List.length as → List.Func.get n (List.map f as) = f (List.Func.get n as)

ink

theorem List.Func.get_map' {α : Type u} {β : Type v} [inst : Inhabited α] [inst : Inhabited β] {f : α → β} {n : ℕ} {as : List α} : f default = default → List.Func.get n (List.map f as) = f (List.Func.get n as)

ink

theorem List.Func.forall_val_of_forall_mem {α : Type u} [inst : Inhabited α] {as : List α} {p : α → Prop} : p default → ((x : α) → x ∈ as → p x) → (n : ℕ) → p (List.Func.get n as)

ink

theorem List.Func.equiv_refl {α : Type u} {as : List α} [inst : Inhabited α] : List.Func.Equiv as as

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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 β) : List.Func.get k (List.Func.pointwise f as bs) = f (List.Func.get k as) (List.Func.get k bs)

ink

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

ink

@[simp]

theorem List.Func.get_add {α : Type u} [inst : 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

ink

@[simp]

theorem List.Func.length_add {α : Type u} [inst : Zero α] [inst : Add α] {xs : List α} {ys : List α} : List.length (List.Func.add xs ys) = max (List.length xs) (List.length ys)

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

theorem List.Func.get_sub {α : Type u} [inst : 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

ink

@[simp]

theorem List.Func.length_sub {α : Type u} [inst : Zero α] [inst : Sub α] {xs : List α} {ys : List α} : List.length (List.Func.sub xs ys) = max (List.length xs) (List.length ys)

ink

@[simp]

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

ink

@[simp]

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