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₂.getD: related lists are related at every in-range defaulted lookup.
• List.getD_append_cons_length, List.getD_append_cons_of_ne: reading the entry at index front.length of front ++ x :: back, and the reads that do not depend on it.
• List.getD_take_drop: reading an in-range entry of (l.drop k).take w reads index k + i of l.
• List.getD_ofFn_of_lt, List.getD_ofFn: reading List.ofFn f at a valid index returns f.
• 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.
• List.find?_range_getD_eq_sInf: the least index below m passing a test, or m, as a search over a range.

theorem List.Forall₂.getD {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} (h : Forall₂ R l₁ l₂) {i : ℕ} (hi : i < l₁.length) (d₁ : α) (d₂ : β) : R (l₁.getD i d₁) (l₂.getD i d₂)

Related lists are related at every in-range defaulted lookup, whatever the defaults.

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.getD_append_cons_length {α : Type u_1} (front back : List α) (x d : α) : (front ++ x :: back).getD front.length d = x

The entry at index front.length of front ++ x :: back is x.

theorem List.getD_append_cons_of_ne {α : Type u_1} (front back : List α) (x y d : α) {i : ℕ} (h : i ≠ front.length) : (front ++ x :: back).getD i d = (front ++ y :: back).getD i d

Reads of front ++ x :: back away from index front.length do not depend on x.

theorem List.getD_take_drop {α : Type u_1} (l : List α) (k : ℕ) {w i : ℕ} (hi : i < w) (d : α) : (take w (drop k l)).getD i d = l.getD (k + i) d

Reading the i-th entry below w of (l.drop k).take w reads index k + i of l.

theorem List.getD_ofFn_of_lt {α : Type u_1} {n : ℕ} (f : Fin n → α) {i : ℕ} (hi : i < n) (d : α) : (ofFn f).getD i d = f ⟨i, hi⟩

Reading List.ofFn f at a valid index returns the function value, whatever the default.

theorem List.getD_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n) (d : α) : (ofFn f).getD (↑i) d = f i

Reading List.ofFn f at i : Fin n returns f i, whatever the default.

theorem List.forall_mem_set_of_forall_mem {α : Type u_1} {p : α → Prop} {l : List α} {i : ℕ} {x : α} (h : ∀ 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 ∈ 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.

theorem List.find?_range_getD_eq_sInf (m : ℕ) (p : ℕ → Bool) : (find? p (range m)).getD m = sInf {i : ℕ | i = m ∨ p i = true}

The least index below m passing a test, or m, as a search over List.range m.