Rational hitting lists: feasibility

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

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

theorem Complexity.RationalHitting.StackLanguage.Feasible.id {A : Type} (ca : A → List Bool) : Feasible ca ca fun (x : A) => x

theorem Complexity.RationalHitting.StackLanguage.Feasible.const {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (b : B) : Feasible ca cb fun (x : A) => b

theorem Complexity.RationalHitting.StackLanguage.Feasible.comp {A B C : Type} {ca : A → List Bool} {cb : B → List Bool} {cc : C → List Bool} {f : A → B} {g : B → C} (hg : Feasible cb cc g) (hf : Feasible ca cb f) : Feasible ca cc (g ∘ f)

theorem Complexity.RationalHitting.StackLanguage.Feasible.pair {A B C : Type} {ca : A → List Bool} {cb : B → List Bool} {cc : C → List Bool} {f : A → B} {g : A → C} (hf : Feasible ca cb f) (hg : Feasible ca cc g) : Feasible ca (pairCode cb cc) fun (a : A) => (f a, g a)

theorem Complexity.RationalHitting.StackLanguage.Feasible.fst {A B : Type} (ca : A → List Bool) (cb : B → List Bool) : Feasible (pairCode ca cb) ca Prod.fst

theorem Complexity.RationalHitting.StackLanguage.Feasible.snd {A B : Type} (ca : A → List Bool) (cb : B → List Bool) : Feasible (pairCode ca cb) cb Prod.snd

theorem Complexity.RationalHitting.StackLanguage.Feasible.prodMap {A B C D : Type} {ca : A → List Bool} {cb : B → List Bool} {cc : C → List Bool} {cd : D → List Bool} {f : A → B} {g : C → D} (hf : Feasible ca cb f) (hg : Feasible cc cd g) : Feasible (pairCode ca cc) (pairCode cb cd) (Prod.map f g)

theorem Complexity.RationalHitting.StackLanguage.Feasible.recode {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f : A → B} {A' B' : Type} (hf : Feasible ca cb f) (ca' : A' → List Bool) (cb' : B' → List Bool) (f' : A' → B') (e : A' → A) (hi : ∀ (a : A'), ca (e a) = ca' a) (ho : ∀ (a : A'), cb (f (e a)) = cb' (f' a)) : Feasible ca' cb' f'

theorem Complexity.RationalHitting.StackLanguage.Feasible.of_eq {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f g : A → B} (hf : Feasible ca cb f) (h : ∀ (a : A), f a = g a) : Feasible ca cb g

theorem Complexity.RationalHitting.StackLanguage.Feasible.branch {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f g : A → B} (hf : Feasible ca cb f) (hg : Feasible ca cb g) : Feasible (pairCode boolCode ca) cb fun (a : Bool × A) => if a.1 = true then f a.2 else g a.2

theorem Complexity.RationalHitting.StackLanguage.Feasible.cond {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {c : A → Bool} {f g : A → B} (hc : Feasible ca boolCode c) (hf : Feasible ca cb f) (hg : Feasible ca cb g) : Feasible ca cb fun (a : A) => if c a = true then f a else g a

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

theorem Complexity.RationalHitting.StackLanguage.Feasible.appendWord : Feasible (pairCode (fun (x : List Bool) => x) fun (x : List Bool) => x) (fun (x : List Bool) => x) fun (a : List Bool × List Bool) => a.1 ++ a.2

theorem Complexity.RationalHitting.StackLanguage.Feasible.reverseWord : Feasible (fun (x : List Bool) => x) (fun (x : List Bool) => x) List.reverse

def Complexity.RationalHitting.TimeBound.power (p : TimeBound) : ℕ → TimeBound

A natural power of a polynomial time-bound expression.

Equations

• p.power 0 = 1
• p.power n.succ = p.power n * p

@[instance_reducible]

instance Complexity.RationalHitting.TimeBound.instPowNat : Pow TimeBound ℕ

Equations

• Complexity.RationalHitting.TimeBound.instPowNat = { pow := Complexity.RationalHitting.TimeBound.power }

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_pow (p : TimeBound) (k n : ℕ) : (p ^ k).eval n = p.eval n ^ k

theorem Complexity.RationalHitting.StackLanguage.add_bits_length (a b : ℕ) : (a + b).bits.length ≤ a.bits.length + b.bits.length

theorem Complexity.RationalHitting.StackLanguage.eval_normalize_single {K : Type} [DecidableEq K] {a tmp flag : K} (hat : a ≠ tmp) (haf : a ≠ flag) (htf : tmp ≠ flag) (w : List Bool) : ∃ t ≤ 7 * w.length + 16, Eval (normalize a tmp flag) (single a w) (single a (wordValue w).bits) t

def Complexity.RationalHitting.StackLanguage.addClean : Program (Fin 5)

Binary addition followed by output normalization.

Equations

• Complexity.RationalHitting.StackLanguage.addClean = (Complexity.RationalHitting.StackLanguage.add 0 1 2 3 4).seq (Complexity.RationalHitting.StackLanguage.normalize 0 3 4)

theorem Complexity.RationalHitting.StackLanguage.eval_addClean (a b : ℕ) : ∃ t ≤ 50 * (a.bits.length + b.bits.length + 1) ^ 2, Eval addClean (both 0 1 a.bits b.bits) (single 0 (a + b).bits) t

def Complexity.RationalHitting.StackLanguage.Procedure.binaryAdd : Procedure (pairCode Nat.bits Nat.bits) Nat.bits fun (a : ℕ × ℕ) => a.1 + a.2

A polynomially bounded clean procedure for binary addition.

Equations

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

def Complexity.RationalHitting.StackLanguage.Procedure.binaryMul : Procedure (pairCode Nat.bits Nat.bits) Nat.bits fun (a : ℕ × ℕ) => a.1 * a.2

A polynomially bounded clean procedure for binary multiplication.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Feasible.binaryAdd : Feasible (pairCode Nat.bits Nat.bits) Nat.bits fun (a : ℕ × ℕ) => a.1 + a.2

theorem Complexity.RationalHitting.StackLanguage.Feasible.binaryMul : Feasible (pairCode Nat.bits Nat.bits) Nat.bits fun (a : ℕ × ℕ) => a.1 * a.2

theorem Complexity.RationalHitting.StackLanguage.Feasible.unaryAdd : Feasible (pairCode unaryCode unaryCode) unaryCode fun (a : ℕ × ℕ) => a.1 + a.2