Size bounds for readable list encodings

The pure interface and instances are moved unchanged from the quantitative fold provider. The framed-list upper bound retains its original statement and proof from the list provider.

class Turing.MultiTapeTM.SizedListEncoding {α : Type u_1} (encA : α ↪ List Bool) (encL : List α ↪ List Bool) : Prop

A list encoding whose encoded lists are at least as long as their elements, their suffixes and their lengths.

• length_le (l : List α) : l.length ≤ (encL l).length
• length_elem_le (l : List α) (a : α) : a ∈ l → (encA a).length ≤ (encL l).length
• length_drop_le (l : List α) (i : ℕ) : (encL (List.drop i l)).length ≤ (encL l).length

instance Turing.MultiTapeTM.instSizedListEncodingEncList {α : Type u_1} (enc : α ↪ List Bool) : SizedListEncoding enc (encList enc)

instance Turing.MultiTapeTM.instSizedListEncodingBoolEncBoolEncBits : SizedListEncoding encBool encBits

theorem Turing.MultiTapeTM.length_encList_le {α : Type} (enc : α ↪ List Bool) (l : List α) {b : ℕ} (h : ∀ a ∈ l, (enc a).length ≤ b) : ((encList enc) l).length ≤ l.length * (2 * b + 1)

A list of elements of bounded size has bounded size.

theorem Turing.MultiTapeTM.length_encList_sublist {α : Type u_1} (enc : α ↪ List Bool) {l₁ l₂ : List α} (h : l₁.Sublist l₂) : ((encList enc) l₁).length ≤ ((encList enc) l₂).length

Sublists do not increase framed list encoding length.

theorem Turing.MultiTapeTM.length_encList_map_le {α : Type u_1} {β : Type u_2} (ea : α ↪ List Bool) (eb : β ↪ List Bool) {f : α → β} {l : List α} (hf : ∀ x ∈ l, (eb (f x)).length ≤ (ea x).length) : ((encList eb) (List.map f l)).length ≤ ((encList ea) l).length

Elementwise encoding-length bounds lift across List.map on framed list encodings.