AFTD Auto-Formalizing Theoretical Domains

decider_class_eq_co

theoremverified

Any complexity class defined by a family of deciders that is closed under negation equals its complement class.

Statement

theorem decider_class_eq_co {α : Type*} (D : (List α → Bool) → Prop)
    (hD : ∀ f, D f → D (fun w => !f w)) :
    ∀ L : Language α, (∃ f, D f ∧ ∀ w, w ∈ L ↔ f w = true) ↔
      CoClass (fun L' : Language α => ∃ f, D f ∧ ∀ w, w ∈ L' ↔ f w = true) L
Source
Sipser, Theorem 7.12
Verified
07 Sep 2026
Axioms
Classical.choiceQuot.soundpropext
Built on 2
  • CoClassThe complement class co(C) of a complexity class C on languages over alphabet α consists of all languages L whose complement is in C.
  • class_closed_under_compl_iff_eq_coA complexity class C is closed under complement if and only if C equals its complement class co(C).
Used by 1

Read back from the Lean

Given a type α and a predicate D : (List α → Bool) → Prop on functions from List α to Bool, assume that D is closed under pointwise Boolean negation (i.e., for every f, if D f holds, then D (fun w => !f w) holds). Then for every language L : Language α, L is decided by some function satisfying D (there exists f such that D f and for all w, w ∈ L ↔ f w = true) if and only if L belongs to the CoClass of languages decided by functions satisfying D.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- A deterministic complexity class defined by deciders closed under negation equals its complement class. -/
theorem decider_class_eq_co {α : Type*} (D : (List α → Bool) → Prop)
    (hD : ∀ f, D f → D (fun w => !f w)) :
    ∀ L : Language α, (∃ f, D f ∧ ∀ w, w ∈ L ↔ f w = true) ↔
      CoClass (fun L' : Language α => ∃ f, D f ∧ ∀ w, w ∈ L' ↔ f w = true) L := by
  let C : Language α → Prop := fun L' => ∃ f, D f ∧ ∀ w, w ∈ L' ↔ f w = true
  have h_compl : ∀ L, C L → C Lᶜ := by
    intro L ⟨f, hfD, hfL⟩
    refine ⟨fun w => !f w, hD f hfD, ?_⟩
    intro w
    change (w ∉ L) ↔ (!f w) = true
    rw [hfL w]
    cases f w <;> simp
  exact (class_closed_under_compl_iff_eq_co C).mp h_compl
Discuss this resultChallenge it