Rational hitting lists: procedure pairs

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

Serialization of a typed pair. Only the first field needs a delimiter.

Equations

• Complexity.RationalHitting.StackLanguage.pairCode ca cb p = Complexity.RationalHitting.StackLanguage.codeWord (ca p.1) ++ cb p.2

@[simp]

theorem Complexity.RationalHitting.StackLanguage.pairCode_length {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (p : A × B) : (pairCode ca cb p).length = 2 * (ca p.1).length + 1 + (cb p.2).length

def Complexity.RationalHitting.StackLanguage.both {K : Type} [DecidableEq K] (a b : K) (x y : List Bool) : Store K

A store with two specified registers and all other registers empty.

Equations

• Complexity.RationalHitting.StackLanguage.both a b x y = Function.update (Complexity.RationalHitting.StackLanguage.single a x) b y

@[simp]

theorem Complexity.RationalHitting.StackLanguage.both_first {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (x y : List Bool) : both a b x y a = x

@[simp]

theorem Complexity.RationalHitting.StackLanguage.both_second {K : Type} [DecidableEq K] (a b : K) (x y : List Bool) : both a b x y b = y

theorem Complexity.RationalHitting.StackLanguage.both_comm {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (x y : List Bool) : both a b x y = both b a y x

@[simp]

theorem Complexity.RationalHitting.StackLanguage.both_nil_left {K : Type} [DecidableEq K] (a b : K) (y : List Bool) : both a b [] y = single b y

@[simp]

theorem Complexity.RationalHitting.StackLanguage.both_nil_right {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (x : List Bool) : both a b x [] = single a x

theorem Complexity.RationalHitting.StackLanguage.extend_single_both {K L : Type} [DecidableEq K] [DecidableEq L] (f : K → L) (hf : Function.Injective f) (i : K) (x : List Bool) (k : L) (y : List Bool) (hk : ∀ (a : K), f a ≠ k) : Function.extend f (single i x) (single k y) = both (f i) k x y

theorem Complexity.RationalHitting.StackLanguage.Eval.rename_both {K L : Type} [DecidableEq K] [DecidableEq L] {p : Program K} {i o : K} {x y : List Bool} {t : ℕ} (h : Eval p (single i x) (single o y) t) (f : K → L) (hf : Function.Injective f) (k : L) (z : List Bool) (hk : ∀ (a : K), f a ≠ k) : Eval (Program.rename f p) (both (f i) k x z) (both (f o) k y z) t

theorem Complexity.RationalHitting.StackLanguage.eval_copy_single {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (w : List Bool) : Eval (copy a b tmp) (single a w) (both a b w w) (7 * w.length + 7)

def Complexity.RationalHitting.StackLanguage.threeRegs {K : Type} (a b c : K) : Fin 3 → K

The register map selecting three named registers.

Equations

• Complexity.RationalHitting.StackLanguage.threeRegs a b c = ![a, b, c]

theorem Complexity.RationalHitting.StackLanguage.threeRegs_inj {K : Type} {a b c : K} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : Function.Injective (threeRegs a b c)

def Complexity.RationalHitting.StackLanguage.prependRecord {K : Type} (a b tmp : K) : Program K

Prefix a record in its original order, consuming the first stack.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_prependRecord {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (s : Store K) (ht : s tmp = []) : Eval (prependRecord a b tmp) s (Function.update (Function.update s a []) b (codeWord (s a) ++ s b)) (6 * (s a).length + 5)

theorem Complexity.RationalHitting.StackLanguage.eval_prependRecord_both {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (x y : List Bool) : Eval (prependRecord a b tmp) (both a b x y) (single b (codeWord x ++ y)) (6 * x.length + 5)

def Complexity.RationalHitting.StackLanguage.Procedure.pair {A B C : Type} {ca : A → List Bool} {cb : B → List Bool} {cc : C → List Bool} {f : A → B} {g : A → C} (p : Procedure ca cb f) (q : Procedure ca cc g) : Procedure ca (pairCode cb cc) fun (a : A) => (f a, g a)

Run two procedures on the same input and encode their pair of outputs.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_clear_both {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (x y : List Bool) : Eval (clear a) (both a b x y) (single b y) (2 * x.length + 1)

theorem Complexity.RationalHitting.StackLanguage.eval_reverse_both {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (x y : List Bool) : Eval (reverse a b) (both a b x y) (single b (x.reverse ++ y)) (2 * x.length + 1)

theorem Complexity.RationalHitting.StackLanguage.eval_reverse_single {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (x : List Bool) : Eval (reverse a b) (single a x) (single b x.reverse) (2 * x.length + 1)

theorem Complexity.RationalHitting.StackLanguage.eval_clear_single {K : Type} [DecidableEq K] (a : K) (x : List Bool) : Eval (clear a) (single a x) (fun (x : K) => []) (2 * x.length + 1)

def Complexity.RationalHitting.StackLanguage.pushWord {K : Type} (k : K) : List Bool → Program K

A finite literal is written by a finite sequence; it is not a primitive which can materialize a word of unbounded length in one step.

Equations

• Complexity.RationalHitting.StackLanguage.pushWord k [] = Complexity.RationalHitting.StackLanguage.Program.skip
• Complexity.RationalHitting.StackLanguage.pushWord k (b :: w) = (Complexity.RationalHitting.StackLanguage.pushWord k w).seq (Complexity.RationalHitting.StackLanguage.Program.push k b)

theorem Complexity.RationalHitting.StackLanguage.eval_pushWord {K : Type} [DecidableEq K] (k : K) (w : List Bool) (s : Store K) : Eval (pushWord k w) s (Function.update s k (w ++ s k)) (2 * w.length + 1)

theorem Complexity.RationalHitting.StackLanguage.eval_unpack_pair (x y : List Bool) : Eval unpackRecord (single 0 (codeWord x ++ y)) (both 0 1 y x.reverse) (5 * x.length + 8)

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

A clean finite-stack procedure producing a constant output.

Equations

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

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

Extract the first component of an encoded pair.

Equations

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

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

Extract the second component of an encoded pair.

Equations

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

def Complexity.RationalHitting.StackLanguage.Procedure.appendWord : Procedure (pairCode id id) id fun (p : List Bool × List Bool) => p.1 ++ p.2

Concatenate the two words of an encoded pair.

Equations

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

def Complexity.RationalHitting.StackLanguage.Procedure.reverseWord : Procedure id id List.reverse

Reverse an input word using a clean temporary register.

Equations

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