Rational hitting lists: tabulation

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Tabulation.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.listCode {A : Type} (ca : A → List Bool) (l : List A) : List Bool

Reusable dense records. Individual word lengths need not be fixed.

Equations

• Complexity.RationalHitting.StackLanguage.listCode ca l = List.flatMap (fun (a : A) => Complexity.RationalHitting.StackLanguage.codeWord (ca a)) l

@[simp]

theorem Complexity.RationalHitting.StackLanguage.listCode_nil {A : Type} (ca : A → List Bool) : listCode ca [] = []

@[simp]

theorem Complexity.RationalHitting.StackLanguage.listCode_cons {A : Type} (ca : A → List Bool) (a : A) (l : List A) : listCode ca (a :: l) = codeWord (ca a) ++ listCode ca l

@[simp]

theorem Complexity.RationalHitting.StackLanguage.listCode_append {A : Type} (ca : A → List Bool) (l m : List A) : listCode ca (l ++ m) = listCode ca l ++ listCode ca m

theorem Complexity.RationalHitting.StackLanguage.listCode_singleton {A : Type} (ca : A → List Bool) (a : A) : listCode ca [a] = codeWord (ca a)

theorem Complexity.RationalHitting.StackLanguage.length_le_listCode {A : Type} (ca : A → List Bool) (l : List A) : l.length ≤ (listCode ca l).length

theorem Complexity.RationalHitting.StackLanguage.listCode_length_le {A : Type} (ca : A → List Bool) (l : List A) (B : ℕ) (h : ∀ a ∈ l, (ca a).length ≤ B) : (listCode ca l).length ≤ l.length * (2 * B + 1)

theorem Complexity.RationalHitting.StackLanguage.listCode_element {A : Type} (ca : A → List Bool) (l : List A) (a : A) (h : a ∈ l) : (ca a).length ≤ (listCode ca l).length

theorem Complexity.RationalHitting.StackLanguage.Feasible.listCons {A : Type} (ca : A → List Bool) : Feasible (pairCode ca (listCode ca)) (listCode ca) fun (a : A × List A) => a.1 :: a.2

theorem Complexity.RationalHitting.StackLanguage.Feasible.listSingleton {A : Type} (ca : A → List Bool) : Feasible ca (listCode ca) fun (a : A) => [a]

theorem Complexity.RationalHitting.StackLanguage.Feasible.listAppend {A : Type} (ca : A → List Bool) : Feasible (pairCode (listCode ca) (listCode ca)) (listCode ca) fun (a : List A × List A) => a.1 ++ a.2

theorem Complexity.RationalHitting.StackLanguage.Feasible.unarySucc : Feasible unaryCode unaryCode Nat.succ

def Complexity.RationalHitting.StackLanguage.tableStep {A B : Type} (f : A × ℕ → B) (a : A × ℕ × List B) : A × ℕ × List B

A complete uniform table-building step: evaluation of a compiled callback, indexed counter update, and append of an escaped dense record.

Equations

• Complexity.RationalHitting.StackLanguage.tableStep f a = (a.1, a.2.1 + 1, a.2.2 ++ [f (a.1, a.2.1)])

def Complexity.RationalHitting.StackLanguage.tableStateCode {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (p : A × ℕ × List B) : List Bool

Encode a tabulation state consisting of input, counter, and accumulated outputs.

Equations

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

@[simp]

theorem Complexity.RationalHitting.StackLanguage.tableStateCode_length {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (a : A × ℕ × List B) : (tableStateCode ca cb a).length = 2 * (ca a.1).length + 2 * a.2.1 + (listCode cb a.2.2).length + 2

theorem Complexity.RationalHitting.StackLanguage.tableStep_iterate_fields {A B : Type} (f : A × ℕ → B) (a : A × ℕ × List B) (j : ℕ) : ((tableStep f)^[j] a).1 = a.1 ∧ ((tableStep f)^[j] a).2.1 = a.2.1 + j

theorem Complexity.RationalHitting.StackLanguage.tableStep_iterate_size {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f : A × ℕ → B} (p : Procedure (pairCode ca unaryCode) cb f) (n : ℕ) (a : A × ℕ × List B) (j : ℕ) (hj : j ≤ n) : (tableStateCode ca cb ((tableStep f)^[j] a)).length ≤ (TimeBound.variable * (2 * p.bound + 4)).eval ((pairCode unaryCode (tableStateCode ca cb) (n, a)).length + 1)

theorem Complexity.RationalHitting.StackLanguage.tableStep_iterate_start {A B : Type} (f : A × ℕ → B) (a : A) (n : ℕ) : (tableStep f)^[n] (a, 0, []) = (a, n, List.map (fun (i : ℕ) => f (a, i)) (List.range n))

theorem Complexity.RationalHitting.StackLanguage.Feasible.tableStep {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f : A × ℕ → B} (hf : Feasible (pairCode ca unaryCode) cb f) : Feasible (tableStateCode ca cb) (tableStateCode ca cb) (StackLanguage.tableStep f)

theorem Complexity.RationalHitting.StackLanguage.Feasible.tabulate {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f : A × ℕ → B} (hf : Feasible (pairCode ca unaryCode) cb f) : Feasible (pairCode unaryCode ca) (listCode cb) fun (a : ℕ × A) => List.map (fun (i : ℕ) => f (a.2, i)) (List.range a.1)

Polynomial-time tabulation of an arbitrary polynomial-time callback. The construction uses only one finite stack program, including all indexing, record layout, and loop control; the counter is unary.

class Complexity.RationalHitting.StackLanguage.Coding (A : Type) : Type

Canonical storage format for the compositional finite-program proofs.

• code : A → List Bool

  The canonical Boolean encoding.

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingNat : Coding ℕ

Equations

• Complexity.RationalHitting.StackLanguage.instCodingNat = { code := Nat.bits }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingBool : Coding Bool

Equations

• Complexity.RationalHitting.StackLanguage.instCodingBool = { code := Complexity.RationalHitting.StackLanguage.boolCode }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingProd {A B : Type} [Coding A] [Coding B] : Coding (A × B)

Equations

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

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingList {A : Type} [Coding A] : Coding (List A)

Equations

• Complexity.RationalHitting.StackLanguage.instCodingList = { code := Complexity.RationalHitting.StackLanguage.listCode Complexity.RationalHitting.StackLanguage.code }

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingSubtype {A : Type} [Coding A] (P : A → Prop) : Coding { a : A // P a }

Equations

• Complexity.RationalHitting.StackLanguage.instCodingSubtype P = { code := fun (a : { a : A // P a }) => Complexity.RationalHitting.StackLanguage.code ↑a }

structure Complexity.RationalHitting.StackLanguage.Unary : Type

A natural number whose computation interface uses unary encoding.

• val : ℕ

  The natural number represented in unary.

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instDecidableEqUnary : DecidableEq Unary

Equations

• Complexity.RationalHitting.StackLanguage.instDecidableEqUnary = Complexity.RationalHitting.StackLanguage.instDecidableEqUnary.decEq

def Complexity.RationalHitting.StackLanguage.instDecidableEqUnary.decEq (x✝ x✝¹ : Unary) : Decidable (x✝ = x✝¹)

Equations

• Complexity.RationalHitting.StackLanguage.instDecidableEqUnary.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingUnary : Coding Unary

Equations

• Complexity.RationalHitting.StackLanguage.instCodingUnary = { code := fun (n : Complexity.RationalHitting.StackLanguage.Unary) => Complexity.RationalHitting.StackLanguage.unaryCode n.val }

structure Complexity.RationalHitting.StackLanguage.BitWord : Type

A Boolean word whose computation interface uses its raw bits.

• val : List Bool

  The raw Boolean word.

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instDecidableEqBitWord : DecidableEq BitWord

Equations

• Complexity.RationalHitting.StackLanguage.instDecidableEqBitWord = Complexity.RationalHitting.StackLanguage.instDecidableEqBitWord.decEq

def Complexity.RationalHitting.StackLanguage.instDecidableEqBitWord.decEq (x✝ x✝¹ : BitWord) : Decidable (x✝ = x✝¹)

Equations

• Complexity.RationalHitting.StackLanguage.instDecidableEqBitWord.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingBitWord : Coding BitWord

Equations

• Complexity.RationalHitting.StackLanguage.instCodingBitWord = { code := Complexity.RationalHitting.StackLanguage.BitWord.val }

def Complexity.RationalHitting.StackLanguage.Poly {A B : Type} [Coding A] [Coding B] (f : A → B) : Prop

Polynomial time means a concrete finite clean stack program and actual step bound, through Procedure. It is not machine advice or an oracle.

Equations

• Complexity.RationalHitting.StackLanguage.Poly f = Complexity.RationalHitting.StackLanguage.Feasible Complexity.RationalHitting.StackLanguage.code Complexity.RationalHitting.StackLanguage.code f

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

theorem Complexity.RationalHitting.StackLanguage.Poly.const {A B : Type} [Coding A] [Coding B] (b : B) : Poly fun (x : A) => b

theorem Complexity.RationalHitting.StackLanguage.Poly.comp {A B C : Type} [Coding A] [Coding B] [Coding C] {f : A → B} {g : B → C} (hg : Poly g) (hf : Poly f) : Poly fun (a : A) => g (f a)

theorem Complexity.RationalHitting.StackLanguage.Poly.pair {A B C : Type} [Coding A] [Coding B] [Coding C] {f : A → B} {g : A → C} (hf : Poly f) (hg : Poly g) : Poly fun (a : A) => (f a, g a)

theorem Complexity.RationalHitting.StackLanguage.Poly.fst {A B : Type} [Coding A] [Coding B] : Poly Prod.fst

theorem Complexity.RationalHitting.StackLanguage.Poly.snd {A B : Type} [Coding A] [Coding B] : Poly Prod.snd

theorem Complexity.RationalHitting.StackLanguage.Poly.subtypeVal {A : Type} [Coding A] (P : A → Prop) : Poly Subtype.val

theorem Complexity.RationalHitting.StackLanguage.Poly.subtypeMk {A B : Type} [Coding A] [Coding B] {f : A → B} {P : B → Prop} (hf : Poly f) (h : ∀ (a : A), P (f a)) : Poly fun (a : A) => ⟨f a, ⋯⟩

theorem Complexity.RationalHitting.StackLanguage.Poly.of_eq {A B : Type} [Coding A] [Coding B] {f g : A → B} (hf : Poly f) (h : ∀ (a : A), f a = g a) : Poly g

theorem Complexity.RationalHitting.StackLanguage.Poly.cond {A B : Type} [Coding A] [Coding B] {c : A → Bool} {f g : A → B} (hc : Poly c) (hf : Poly f) (hg : Poly g) : Poly fun (a : A) => if c a = true then f a else g a

theorem Complexity.RationalHitting.StackLanguage.Poly.natAdd : Poly fun (a : ℕ × ℕ) => a.1 + a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.natMul : Poly fun (a : ℕ × ℕ) => a.1 * a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.unarySucc : Poly fun (a : Unary) => { val := a.val + 1 }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryAdd : Poly fun (a : Unary × Unary) => { val := a.1.val + a.2.val }

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

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

theorem Complexity.RationalHitting.StackLanguage.Poly.listAppend {A : Type} [Coding A] : Poly fun (a : List A × List A) => a.1 ++ a.2

theorem Complexity.RationalHitting.StackLanguage.Poly.wordAppend : Poly fun (a : BitWord × BitWord) => { val := a.1.val ++ a.2.val }

theorem Complexity.RationalHitting.StackLanguage.Poly.tabulate {A B : Type} [Coding A] [Coding B] {f : A × Unary → B} (hf : Poly f) : Poly fun (a : Unary × A) => List.map (fun (i : ℕ) => f (a.2, { val := i })) (List.range a.1.val)