Langlib

Langlib.Classes.DeterministicContextFree.Closure.Complement

Deterministic Context-Free Closure Under Complement #

This file is the deterministic context-free class-level view of complement closure. The substantive work lives at the automaton level in Langlib.Automata.DeterministicPushdown.ClosureProperties.Complement: the construction DPDA.complement flips the accepting states, DPDA.complement_isTotal shows totality is preserved, and is_DCF_complement totalizes an arbitrary final-state DPDA (DPDA.exists_equivalent_total) before complementing it, so that no DPDA.IsTotal hypothesis on the input is needed.

This file simply re-exports the headline DCF_closedUnderComplement under the deterministic context-free class namespace.

source
theorem DCF_closedUnderComplement {T : Type} [Fintype T] :
ClosedUnderComplement is_DCF

Deterministic context-free languages are closed under complement.

This is is_DCF_closedUnderComplement, proven at the automaton level by totalizing an arbitrary DPDA and then complementing it.