One-way-liveness proof: PathNFA

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/PathNFA.lean

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.

structure Complexity.FiniteAutomaton.NMachineOn (Alpha Q : Type) : Type

A nondeterministic automaton on an arbitrary state type.

• initial : Q

  The initial control state.

• accepting : Set Q

  The accepting control states.

• transition : Q → Symbol Alpha → Set (Q × Move)

  The next control states and head moves for each scanned symbol.

• left_boundary (q q' : Q) : (q', Move.left) ∉ self.transition q Symbol.left
• right_boundary (q q' : Q) : (q', Move.right) ∉ self.transition q Symbol.right

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.NMachineOn.Config {Alpha Q : Type} (w : List Alpha) : Type

A position on the endmarked word and a nondeterministic control state.

Equations

• Complexity.FiniteAutomaton.NMachineOn.Config w = (Fin (w.length + 2) × Q)

def Complexity.FiniteAutomaton.NMachineOn.Step {Alpha Q : Type} (M : NMachineOn Alpha Q) (w : List Alpha) (c c' : Config w) : Prop

One nondeterministic transition on the scanned input symbol.

Equations

• M.Step w c c' = ∃ (d : Complexity.FiniteAutomaton.Move), (c'.2, d) ∈ M.transition c.2 (Complexity.FiniteAutomaton.scanned w c.1) ∧ d.Rel ↑c.1 ↑c'.1

def Complexity.FiniteAutomaton.NMachineOn.Accepts {Alpha Q : Type} (M : NMachineOn Alpha Q) (positive : Bool) (w : List Alpha) : Prop

Existence of a finite run reaching an accepting control state.

Equations

• M.Accepts positive w = ∃ (c : Complexity.FiniteAutomaton.NMachineOn.Config w), Complexity.FiniteAutomaton.FiniteRun positive (M.Step w) (⟨0, ⋯⟩, M.initial) c ∧ c.2 ∈ M.accepting

def Complexity.FiniteAutomaton.NMachineOn.relabel {Alpha Q : Type} (M : NMachineOn Alpha Q) {n : ℕ} (e : Q ≃ Fin n) : NMachine Alpha n

Number the states using an equivalence, preserving transitions and endmarkers.

Equations

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

theorem Complexity.FiniteAutomaton.NMachineOn.relabel_accepts {Alpha Q : Type} (M : NMachineOn Alpha Q) {n : ℕ} (e : Q ≃ Fin n) (positive : Bool) (w : List Alpha) : (M.relabel e).Accepts positive w ↔ M.Accepts positive w

theorem Complexity.FiniteAutomaton.NMachineOn.relabel_noLeft {Alpha Q : Type} (M : NMachineOn Alpha Q) {n : ℕ} (e : Q ≃ Fin n) (hm : ∀ (q : Q) (b : Symbol Alpha) (q' : Q), (q', Move.left) ∉ M.transition q b) : (M.relabel e).NoLeft

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.PathNFA.State (H : Type) : Type

none is the initial state. Boolean states are accept and reject.

Equations

• Complexity.FiniteAutomaton.PathNFA.State H = Option (H ⊕ Bool)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.PathNFA.path {H : Type} (p : H) : State H

A path state recording the current relation-product endpoint.

Equations

• Complexity.FiniteAutomaton.PathNFA.path p = some (Sum.inl p)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.PathNFA.accept {H : Type} : State H

The distinguished accepting state of the relation-product automaton.

Equations

• Complexity.FiniteAutomaton.PathNFA.accept = some (Sum.inr false)

def Complexity.FiniteAutomaton.PathNFA.rules {H : Type} : State H → Symbol (BRel H) → Set (State H × Move)

Choose a start vertex, follow relation edges, and accept at the right endmarker.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.FiniteAutomaton.PathNFA.rules (some (Sum.inl val)) Complexity.FiniteAutomaton.Symbol.right = {(Complexity.FiniteAutomaton.PathNFA.accept, Complexity.FiniteAutomaton.Move.stay)}
• Complexity.FiniteAutomaton.PathNFA.rules x✝¹ x✝ = ∅

theorem Complexity.FiniteAutomaton.PathNFA.rules_noLeft {H : Type} (q : State H) (b : Symbol (BRel H)) (q' : State H) : (q', Move.left) ∉ rules q b

def Complexity.FiniteAutomaton.PathNFA.machine {H : Type} : NMachineOn (BRel H) (State H)

The one-way endmarker automaton for nonempty relation products.

Equations

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

theorem Complexity.FiniteAutomaton.PathNFA.product_path {H : Type} (w : List (BRel H)) (a b : H) : w.prod.holds a b ↔ ∃ (p : ℕ → H), p 0 = a ∧ p w.length = b ∧ ∀ (i : ℕ) (hi : i < w.length), w[i].holds (p i) (p (i + 1))

A numbered path through a product, extended arbitrarily after its endpoint.

def Complexity.FiniteAutomaton.PathNFA.Good {H : Type} (w : List (BRel H)) (c : NMachineOn.Config w) : Prop

The accumulated product on every prefix reached by a path state.

Equations

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

theorem Complexity.FiniteAutomaton.PathNFA.scanned_letter_data {H : Type} (w : List (BRel H)) (i : Fin (w.length + 2)) (R : BRel H) (hs : scanned w i = Symbol.letter R) : ∃ (hi : ↑i - 1 < w.length), w[↑i - 1] = R

theorem Complexity.FiniteAutomaton.PathNFA.scanned_letter_cell {H : Type} (w : List (BRel H)) (i : ℕ) (hi : i < w.length) : scanned w ⟨i + 1, ⋯⟩ = Symbol.letter w[i]

theorem Complexity.FiniteAutomaton.PathNFA.good_step {H : Type} (w : List (BRel H)) (c c' : NMachineOn.Config w) (hg : Good w c) (hs : machine.Step w c c') : Good w c'

theorem Complexity.FiniteAutomaton.PathNFA.accepts_iff {H : Type} (positive : Bool) (w : List (BRel H)) : machine.Accepts positive w ↔ BRel.Live w

theorem Complexity.FiniteAutomaton.small_nfa (h : ℕ) : ∃ (N : NMachine (Alphabet h) (h + 3)), N.NoLeft ∧ ∀ (positive : Bool), N.Recognizes positive (oneWayLiveness h)

The explicit path automaton has h+3 states, including the unused rejector. It accepts only after at least two transitions, so both conventions agree.