Rational hitting lists: stack words

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/StackWords.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.clear {K : Type} (a : K) : Program K

Empty a stack by repeatedly dropping its head.

Equations

• Complexity.RationalHitting.StackLanguage.clear a = Complexity.RationalHitting.StackLanguage.Program.loop a (Complexity.RationalHitting.StackLanguage.Program.drop a)

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

Move a stack onto another stack in reverse order.

Equations

• Complexity.RationalHitting.StackLanguage.reverse a b = Complexity.RationalHitting.StackLanguage.Program.loop a (Complexity.RationalHitting.StackLanguage.Program.transfer a b)

theorem Complexity.RationalHitting.StackLanguage.eval_clear {K : Type} [DecidableEq K] (a : K) (s : Store K) : Eval (clear a) s (Function.update s a []) (2 * (s a).length + 1)

theorem Complexity.RationalHitting.StackLanguage.transfer_cons {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (s : Store K) (x : Bool) (l : List Bool) (hs : s a = x :: l) : transfer a b s = Function.update (Function.update s a l) b (x :: s b)

theorem Complexity.RationalHitting.StackLanguage.eval_reverse {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (s : Store K) : Eval (reverse a b) s (Function.update (Function.update s a []) b ((s a).reverse ++ s b)) (2 * (s a).length + 1)

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

Copy a nonempty head to another register without consuming it.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_copyHead {K : Type} [DecidableEq K] {a b : K} (s : Store K) (x : Bool) (l : List Bool) (hs : s a = x :: l) : Eval (copyHead a b) s (Function.update s b (x :: s b)) 2

def Complexity.RationalHitting.StackLanguage.duplicateReverse {K : Type} (a b c : K) : Program K

Two simultaneous reversed copies of a word, consuming the operand.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_duplicateReverse {K : Type} [DecidableEq K] {a b c : K} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (s : Store K) : Eval (duplicateReverse a b c) s (Function.update (Function.update (Function.update s a []) b ((s a).reverse ++ s b)) c ((s a).reverse ++ s c)) (5 * (s a).length + 1)

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

Copy an arbitrary binary word, restoring the operand and clearing temporary storage; all registers have fixed indices.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_copy {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (s : Store K) : Eval (copy a b tmp) s (Function.update (Function.update s b (s a)) tmp []) (7 * (s a).length + 2 * (s b).length + 2 * (s tmp).length + 7)

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

Little-endian binary words; zero has the empty word.

Equations

• Complexity.RationalHitting.StackLanguage.wordValue [] = 0
• Complexity.RationalHitting.StackLanguage.wordValue (b :: l) = (if b = true then 1 else 0) + 2 * Complexity.RationalHitting.StackLanguage.wordValue l

def Complexity.RationalHitting.StackLanguage.incrementWord : List Bool → List Bool

Increment a little-endian binary word, allowing a new high bit.

Equations

• Complexity.RationalHitting.StackLanguage.incrementWord [] = [true]
• Complexity.RationalHitting.StackLanguage.incrementWord (false :: l) = true :: l
• Complexity.RationalHitting.StackLanguage.incrementWord (true :: l) = false :: Complexity.RationalHitting.StackLanguage.incrementWord l

@[simp]

theorem Complexity.RationalHitting.StackLanguage.incrementWord_value (l : List Bool) : wordValue (incrementWord l) = wordValue l + 1

def Complexity.RationalHitting.StackLanguage.carrySplit : List Bool → ℕ × List Bool

Separate the initial carry chain from the incremented remainder.

Equations

• Complexity.RationalHitting.StackLanguage.carrySplit [] = (0, [true])
• Complexity.RationalHitting.StackLanguage.carrySplit (false :: l) = (0, true :: l)
• Complexity.RationalHitting.StackLanguage.carrySplit (true :: l) = ((Complexity.RationalHitting.StackLanguage.carrySplit l).1 + 1, (Complexity.RationalHitting.StackLanguage.carrySplit l).2)

theorem Complexity.RationalHitting.StackLanguage.carrySplit_spec (l : List Bool) : incrementWord l = List.replicate (carrySplit l).1 false ++ (carrySplit l).2

theorem Complexity.RationalHitting.StackLanguage.carrySplit_length (l : List Bool) : (carrySplit l).1 ≤ l.length

theorem Complexity.RationalHitting.StackLanguage.incrementWord_length (l : List Bool) : (incrementWord l).length ≤ l.length + 1

def Complexity.RationalHitting.StackLanguage.incrementBody {K : Type} (a tmp flag : K) : Program K

One carry-propagation step of binary increment.

Equations

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

def Complexity.RationalHitting.StackLanguage.incrementLoop {K : Type} (a tmp flag : K) : Program K

Propagate the increment carry until the flag is cleared.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_incrementLoop {K : Type} [DecidableEq K] {a tmp flag : K} (hat : a ≠ tmp) (haf : a ≠ flag) (htf : tmp ≠ flag) (s : Store K) (hf : s flag = [true]) : ∃ t ≤ 5 * (s a).length + 10, Eval (incrementLoop a tmp flag) s (Function.update (Function.update (Function.update s a (carrySplit (s a)).2) tmp (List.replicate (carrySplit (s a)).1 false ++ s tmp)) flag []) t

def Complexity.RationalHitting.StackLanguage.increment {K : Type} (a tmp flag : K) : Program K

Increment a binary stack word and restore its orientation.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_increment {K : Type} [DecidableEq K] {a tmp flag : K} (hat : a ≠ tmp) (haf : a ≠ flag) (htf : tmp ≠ flag) (s : Store K) : ∃ t ≤ 7 * (s a).length + 2 * (s tmp).length + 2 * (s flag).length + 18, Eval (increment a tmp flag) s (Function.update (Function.update (Function.update s a (incrementWord (s a))) tmp []) flag []) t