Rational hitting lists: list procedures

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/ListProcedures.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.RationalHitting.StackLanguage.Procedure.padEmpty (w : List Bool) : Procedure (fun (x : List Bool) => x) (fun (x : List Bool) => x) fun (a : List Bool) => if a = [] then w else a

Append an empty list component to a coded value.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.StackLanguage.Procedure.wordEmpty : Procedure (fun (x : List Bool) => x) boolCode fun (a : List Bool) => a.isEmpty

Test whether a raw input word is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.Feasible.listUncons {A : Type} (ca : A → List Bool) (z : A) : Feasible (listCode ca) (pairCode ca (listCode ca)) fun (a : List A) => (a.headD z, a.tail)

theorem Complexity.RationalHitting.StackLanguage.Feasible.listTail {A : Type} (ca : A → List Bool) (z : A) : Feasible (listCode ca) (listCode ca) List.tail

theorem Complexity.RationalHitting.StackLanguage.Feasible.listHeadD {A : Type} (ca : A → List Bool) (z : A) : Feasible (listCode ca) ca fun (a : List A) => a.headD z

theorem Complexity.RationalHitting.StackLanguage.Feasible.listEmpty {A : Type} (ca : A → List Bool) : Feasible (listCode ca) boolCode List.isEmpty

theorem Complexity.RationalHitting.StackLanguage.listCode_tail_le {A : Type} (ca : A → List Bool) (a : List A) : (listCode ca a.tail).length ≤ (listCode ca a).length

theorem Complexity.RationalHitting.StackLanguage.listCode_iterate_tail_le {A : Type} (ca : A → List Bool) (a : List A) (n : ℕ) : (listCode ca (List.tail^[n] a)).length ≤ (listCode ca a).length

theorem Complexity.RationalHitting.StackLanguage.Poly.listTail {A : Type} [Coding A] [Inhabited A] : Poly List.tail

theorem Complexity.RationalHitting.StackLanguage.Poly.listHeadD {A : Type} [Coding A] (z : A) : Poly fun (a : List A) => a.headD z

theorem Complexity.RationalHitting.StackLanguage.Poly.listEmpty {A : Type} [Coding A] : Poly List.isEmpty

theorem Complexity.RationalHitting.StackLanguage.Poly.iterate {A : Type} [Coding A] {f : A → A} (hf : Poly f) (Q : TimeBound) (hQ : ∀ (n : ℕ) (a : A), ∀ i ≤ n, (code (f^[i] a)).length ≤ Q.eval ((pairCode unaryCode code (n, a)).length + 1)) : Poly fun (a : Unary × A) => f^[a.1.val] a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.listDrop {A : Type} [Coding A] [Inhabited A] : Poly fun (a : Unary × List A) => List.drop a.1.val a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.listGetD {A : Type} [Coding A] [Inhabited A] (z : A) : Poly fun (a : Unary × List A) => (List.drop a.1.val a.2).headD z

def Complexity.RationalHitting.StackLanguage.recordCount : List Bool → ℕ

Count record delimiters, skipping both the escape bit and payload bit.

Equations

• Complexity.RationalHitting.StackLanguage.recordCount [] = 0
• Complexity.RationalHitting.StackLanguage.recordCount (true :: w) = Complexity.RationalHitting.StackLanguage.recordCount w + 1
• Complexity.RationalHitting.StackLanguage.recordCount [false] = 0
• Complexity.RationalHitting.StackLanguage.recordCount (false :: head :: w) = Complexity.RationalHitting.StackLanguage.recordCount w

@[simp]

theorem Complexity.RationalHitting.StackLanguage.recordCount_false (w : List Bool) : recordCount (false :: w) = recordCount w.tail

def Complexity.RationalHitting.StackLanguage.countRecordsBody : Program (Fin 2)

Consume one encoded record and increment a unary length counter.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.StackLanguage.countRecords : Program (Fin 2)

Count all records in an encoded list.

Equations

• Complexity.RationalHitting.StackLanguage.countRecords = Complexity.RationalHitting.StackLanguage.Program.loop 0 Complexity.RationalHitting.StackLanguage.countRecordsBody

theorem Complexity.RationalHitting.StackLanguage.drop_both_left (w v : List Bool) : Eval (Program.drop 0) (both 0 1 w v) (both 0 1 w.tail v) 1

theorem Complexity.RationalHitting.StackLanguage.push_both_right (w v : List Bool) (b : Bool) : Eval (Program.push 1 b) (both 0 1 w v) (both 0 1 w (b :: v)) 1

theorem Complexity.RationalHitting.StackLanguage.eval_countRecords (w v : List Bool) : ∃ t ≤ 5 * w.length + 1, Eval countRecords (both 0 1 w v) (single 1 (unaryCode (recordCount w) ++ v)) t

theorem Complexity.RationalHitting.StackLanguage.recordCount_codeWord (w tail : List Bool) : recordCount (codeWord w ++ tail) = recordCount tail + 1

theorem Complexity.RationalHitting.StackLanguage.recordCount_listCode {A : Type} (ca : A → List Bool) (l : List A) : recordCount (listCode ca l) = l.length

def Complexity.RationalHitting.StackLanguage.Procedure.listLength {A : Type} (ca : A → List Bool) : Procedure (listCode ca) unaryCode List.length

A polynomially bounded procedure computing encoded list length in unary.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.Poly.listLength {A : Type} [Coding A] : Poly fun (a : List A) => { val := a.length }

theorem Complexity.RationalHitting.StackLanguage.range_map_drop_headD {A : Type} (l : List A) (z : A) : List.map (fun (i : ℕ) => (List.drop i l).headD z) (List.range l.length) = l

theorem Complexity.RationalHitting.StackLanguage.Poly.listMap {A B C : Type} [Coding A] [Coding B] [Coding C] [Inhabited B] {f : A × B → C} (hf : Poly f) : Poly fun (a : A × List B) => List.map (fun (b : B) => f (a.1, b)) a.2