Defaulted list lookup and updates

Main results

• List.getD_mem_or, List.getD_idxOf: a defaulted lookup returns a member or the default, and returns a member at its first index.
• List.getD_set_self, List.getD_set_ne: reading an updated entry or an unchanged entry.
• List.forall_mem_set_of_forall_mem, List.getD_le_of_forall_le: preserve invariants under updates and bound defaulted reads of numeric register files.
• List.getD_map_range: read a function tabulated over a bounded range.
• List.map_range_eq_ofFn: runtime tabulation agrees with the finite coordinate view.

theorem List.getD_set_self {α : Type u_1} {l : List α} {i : ℕ} {x d : α} (h : i < l.length) : (l.set i x).getD i d = x

Reading the updated entry of a list.

theorem List.getD_set_ne {α : Type u_1} {l : List α} {i j : ℕ} {x d : α} (h : i ≠ j) : (l.set i x).getD j d = l.getD j d

Reading another entry of an updated list.

theorem List.forall_mem_set_of_forall_mem {α : Type u_1} {p : α → Prop} {l : List α} {i : ℕ} {x : α} (h : ∀ (a : α), a ∈ l → p a) (hx : p x) (a : α) : a ∈ l.set i x → p a

A property of all the entries of a list holds of all the entries of an update by a value having it.

theorem List.getD_le_of_forall_le {l : List ℕ} {B : ℕ} (h : ∀ (a : ℕ), a ∈ l → a ≤ B) (j : ℕ) : l.getD j 0 ≤ B

The entries of a list of numbers at most B, read with default 0, are at most B.

theorem List.getD_mem_or {α : Type u_1} (l : List α) (j : ℕ) (d : α) : l.getD j d ∈ l ∨ l.getD j d = d

A defaulted lookup returns a member of the list or the default value.

theorem List.getD_idxOf {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {x : α} (hx : x ∈ l) (d : α) : l.getD (idxOf x l) d = x

Looking up the first index of a member of a list returns that member.

theorem List.getD_map_range {α : Type u_1} (f : ℕ → α) (d : α) {n i : ℕ} (hi : i < n) : (map f (range n)).getD i d = f i

Reading a mapped range at a valid index applies the map to that index.

theorem List.map_range_eq_ofFn {α : Type u_1} (n : ℕ) (f : ℕ → α) : map f (range n) = ofFn fun (i : Fin n) => f ↑i

Tabulating a natural-indexed function over a range agrees with its finite coordinate view.