module

public import Mathlib
@[expose]
public section

/-!
# Langlib: the extended Chomsky hierarchy

This is the independent, Mathlib-only statement surface for the Palomar Registry.
It records the ordinary unrestricted-grammar definitions of the language classes,
the finite, pushdown, linearly bounded, and Turing automaton presentations, the
strict hierarchy (with explicit alphabet-size hypotheses), the proved
grammar/automaton equivalences, the incomparability of linear and deterministic
context-free languages, and the closure and non-closure results.

The wider repository also proves decidability and undecidability results.  Those
results are deliberately outside this challenge.

The definitions below are transparent copies of the definitions proved about in
`Langlib`.  In particular, a context-sensitive grammar may have the distinguished
rule `S -> epsilon`, provided `S` never occurs on a right-hand side. The strict
inclusions range over arbitrary finite alphabets with explicit lower bounds on
their size; no strictness claim is made below the stated bound.
-/

open Relation Turing

/-! ## Unrestricted grammars and grammar-defined language classes -/

/-- A grammar symbol is either a terminal or a nonterminal. -/
inductive symbol (T : Type) (N : Type) where
  | terminal : T -> symbol T N
  | nonterminal : N -> symbol T N
deriving DecidableEq

/-- An unrestricted rule represents `u A v -> w`. -/
structure grule (T : Type) (N : Type) where
  input_L : List (symbol T N)
  input_N : N
  input_R : List (symbol T N)
  output_string : List (symbol T N)

/-- An unrestricted grammar has a nonterminal type, start symbol, and finite rule list. -/
structure grammar (T : Type) where
  nt : Type
  initial : nt
  rules : List (grule T nt)

variable {T : Type}

/-- One unrestricted rewrite step, in an arbitrary surrounding context. -/
def grammar_transforms (g : grammar T) (w1 w2 : List (symbol T g.nt)) : Prop :=
  exists r : grule T g.nt, r ∈ g.rules ∧
    exists u v : List (symbol T g.nt),
      w1 = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v ∧
      w2 = u ++ r.output_string ++ v

/-- Zero or more unrestricted rewrite steps. -/
def grammar_derives (g : grammar T) :
    List (symbol T g.nt) -> List (symbol T g.nt) -> Prop :=
  Relation.ReflTransGen (grammar_transforms g)

/-- An unrestricted grammar generates a terminal word from its start symbol. -/
def grammar_generates (g : grammar T) (w : List T) : Prop :=
  grammar_derives g [symbol.nonterminal g.initial] (List.map symbol.terminal w)

/-- The language generated by an unrestricted grammar. -/
def grammar_language (g : grammar T) : Language T := Set.ofPred (grammar_generates g)

/-- Right-regular outputs are `aB`, `a`, or the empty word. -/
def right_regular_output {N : Type} (s : List (symbol T N)) : Prop :=
  (exists a : T, exists B : N, s = [symbol.terminal a, symbol.nonterminal B]) ∨
  (exists a : T, s = [symbol.terminal a]) ∨ s = []

/-- A right-regular unrestricted grammar has context-free rules with right-regular outputs. -/
def grammar_right_regular (g : grammar T) : Prop :=
  forall r, r ∈ g.rules ->
    r.input_L = [] ∧ r.input_R = [] ∧ right_regular_output r.output_string

/-- A regular language is generated by a right-regular unrestricted grammar. -/
def is_RG (L : Language T) : Prop :=
  exists g : grammar T, grammar_right_regular g ∧ grammar_language g = L

/-- The class of regular languages. -/
def RG : Set (Language T) := Set.ofPred is_RG

/-- A linear output contains at most one nonterminal. -/
def linear_output {N : Type} (s : List (symbol T N)) : Prop :=
  (forall x, x ∈ s -> exists t, x = symbol.terminal t) ∨
  (exists (u : List T) (B : N) (v : List T),
    s = List.map symbol.terminal u ++ [symbol.nonterminal B] ++ List.map symbol.terminal v)

/-- A linear unrestricted grammar has context-free rules with linear outputs. -/
def grammar_linear (g : grammar T) : Prop :=
  forall r, r ∈ g.rules ->
    r.input_L = [] ∧ r.input_R = [] ∧ linear_output r.output_string

/-- A linear language is generated by a linear unrestricted grammar. -/
def is_Linear (L : Language T) : Prop :=
  exists g : grammar T, grammar_linear g ∧ grammar_language g = L

/-- The class of linear languages. -/
def Linear : Set (Language T) := Set.ofPred is_Linear

/-- A context-free unrestricted grammar rewrites one nonterminal without context. -/
def grammar_context_free (g : grammar T) : Prop :=
  forall r, r ∈ g.rules -> r.input_L = [] ∧ r.input_R = []

/-- A context-free language is generated by a context-free unrestricted grammar. -/
def is_CF (L : Language T) : Prop :=
  exists g : grammar T, grammar_context_free g ∧ grammar_language g = L

/-- The class of context-free languages. -/
def CF : Set (Language T) := Set.ofPred is_CF

/-- The optional distinguished erasing rule is exactly `S -> epsilon`. -/
def initial_epsilon_rule (g : grammar T) (r : grule T g.nt) : Prop :=
  r.input_L = [] ∧ r.input_N = g.initial ∧ r.input_R = [] ∧ r.output_string = []

/-- A rule is non-contracting when its output is no shorter than its input. -/
def grule_noncontracting {N : Type} (r : grule T N) : Prop :=
  r.output_string.length ≥ r.input_L.length + 1 + r.input_R.length

/-- The start symbol occurs on no rule's right-hand side. -/
def initial_not_on_rhs (g : grammar T) : Prop :=
  forall r, r ∈ g.rules -> symbol.nonterminal g.initial ∉ r.output_string

/-- A context-sensitive grammar is non-contracting apart from a controlled `S -> epsilon`. -/
def grammar_context_sensitive (g : grammar T) : Prop :=
  (forall r, r ∈ g.rules -> initial_epsilon_rule g r ∨ grule_noncontracting r) ∧
  ((exists r, r ∈ g.rules ∧ initial_epsilon_rule g r) -> initial_not_on_rhs g)

/-- A context-sensitive language is generated by a context-sensitive unrestricted grammar. -/
def is_CS (L : Language T) : Prop :=
  exists g : grammar T, grammar_context_sensitive g ∧ grammar_language g = L

/-- The class of context-sensitive languages. -/
def CS : Set (Language T) := Set.ofPred is_CS

/-- A recursively enumerable language is generated by an unrestricted grammar. -/
def is_RE (L : Language T) : Prop :=
  exists g : grammar T, grammar_language g = L

/-- The class of recursively enumerable languages. -/
def RE : Set (Language T) := Set.ofPred is_RE

/-! ## Automata and the remaining extended-hierarchy classes -/

/-- Recognition by a finite-state Mathlib deterministic automaton. -/
def is_DFA (L : Language T) : Prop :=
  exists sigma : Type, exists _ : Fintype sigma, exists M : DFA T sigma, M.accepts = L

/-- The class recognized by Mathlib deterministic finite automata. -/
def DFA.Class : Set (Language T) := Set.ofPred is_DFA

/-- Recognition by a finite-state Mathlib nondeterministic automaton. -/
def is_NFA (L : Language T) : Prop :=
  exists sigma : Type, exists _ : Fintype sigma, exists M : NFA T sigma, M.accepts = L

/-- The class recognized by Mathlib nondeterministic finite automata. -/
def NFA.Class : Set (Language T) := Set.ofPred is_NFA

/-- A nondeterministic pushdown automaton with input and epsilon transitions. -/
structure PDA (Q T S : Type) [Fintype Q] [Fintype T] [Fintype S] where
  initial_state : Q
  start_symbol : S
  final_states : Set Q
  transition_fun : Q -> T -> S -> Set (Q × List S)
  transition_fun' : Q -> S -> Set (Q × List S)
  finite (q : Q) (a : T) (Z : S) : (transition_fun q a Z).Finite
  finite' (q : Q) (Z : S) : (transition_fun' q Z).Finite

namespace PDA

variable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S]

/-- A PDA configuration records state, unread input, and stack. -/
structure conf (p : PDA Q T S) where
  state : Q
  input : List T
  stack : List S

variable {pda : PDA Q T S}

/-- The set of one-step PDA successors. -/
def step (r1 : conf pda) : Set (conf pda) :=
  match r1 with
  | ⟨q, a :: w, Z :: alpha⟩ =>
      {r2 | exists p beta, (p, beta) ∈ pda.transition_fun q a Z ∧
        r2 = ⟨p, w, beta ++ alpha⟩} ∪
      {r2 | exists p beta, (p, beta) ∈ pda.transition_fun' q Z ∧
        r2 = ⟨p, a :: w, beta ++ alpha⟩}
  | ⟨q, [], Z :: alpha⟩ =>
      {r2 | exists p beta, (p, beta) ∈ pda.transition_fun' q Z ∧
        r2 = ⟨p, [], beta ++ alpha⟩}
  | ⟨_, _, []⟩ => ∅

/-- One PDA transition. -/
def Reaches₁ (r1 r2 : conf pda) : Prop := r2 ∈ step r1

/-- Zero or more PDA transitions. -/
def Reaches : conf pda -> conf pda -> Prop := Relation.ReflTransGen Reaches₁

/-- Empty-stack acceptance after consuming the whole input. -/
def acceptsByEmptyStack (pda : PDA Q T S) : Language T :=
  {w | exists q : Q,
    Reaches (⟨pda.initial_state, w, [pda.start_symbol]⟩ : conf pda) ⟨q, [], []⟩}

/-- Final-state acceptance after consuming the whole input. -/
def acceptsByFinalState (pda : PDA Q T S) : Language T :=
  {w | exists q, q ∈ pda.final_states ∧ exists gamma : List S,
    Reaches (⟨pda.initial_state, w, [pda.start_symbol]⟩ : conf pda) ⟨q, [], gamma⟩}

variable {T : Type} [Fintype T]

/-- Recognition by a finite-state, finite-stack-alphabet PDA using empty-stack acceptance. -/
def is_PDA_emptyStack (L : Language T) : Prop :=
  exists (Q S : Type) (_ : Fintype Q) (_ : Fintype S),
    exists M : PDA Q T S, M.acceptsByEmptyStack = L

/-- The default PDA recognizability predicate uses empty-stack acceptance. -/
abbrev is_PDA (L : Language T) : Prop := is_PDA_emptyStack L

/-- Recognition by a PDA using final-state acceptance. -/
def is_PDA_finalState (L : Language T) : Prop :=
  exists (Q S : Type) (_ : Fintype Q) (_ : Fintype S),
    exists M : PDA Q T S, M.acceptsByFinalState = L

/-- The PDA class under empty-stack acceptance. -/
def EmptyStackClass : Set (Language T) := Set.ofPred is_PDA

/-- The default PDA-recognizable class. -/
alias Class := PDA.EmptyStackClass

/-- The PDA class under final-state acceptance. -/
def FinalStateClass : Set (Language T) := Set.ofPred is_PDA_finalState

end PDA

/-- A deterministic PDA has partial functional transitions and forbids mixed epsilon/input moves. -/
structure DPDA (Q T S : Type) [Fintype Q] [Fintype T] [Fintype S] where
  initial_state : Q
  start_symbol : S
  final_states : Set Q
  transition : Q -> T -> S -> Option (Q × List S)
  epsilon_transition : Q -> S -> Option (Q × List S)
  no_mixed : forall q Z, epsilon_transition q Z ≠ none -> forall a, transition q a Z = none

namespace DPDA

variable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S]

/-- Forget determinism, viewing each optional transition as an empty set or singleton. -/
@[reducible]
noncomputable def toPDA (M : DPDA Q T S) : PDA Q T S where
  initial_state := M.initial_state
  start_symbol := M.start_symbol
  final_states := M.final_states
  transition_fun q a Z :=
    match M.transition q a Z with
    | some p => {p}
    | none => ∅
  transition_fun' q Z :=
    match M.epsilon_transition q Z with
    | some p => {p}
    | none => ∅
  finite q a Z := by
    cases M.transition q a Z with
    | none => exact Set.toFinite ∅
    | some p => exact Set.toFinite {p}
  finite' q Z := by
    cases M.epsilon_transition q Z with
    | none => exact Set.toFinite ∅
    | some p => exact Set.toFinite {p}

/-- A DPDA accepts by final state through its underlying PDA. -/
def acceptsByFinalState (M : DPDA Q T S) : Language T := M.toPDA.acceptsByFinalState

end DPDA

variable {T : Type} [Fintype T]

/-- Recognition by a DPDA using final-state acceptance. -/
def is_DPDA (L : Language T) : Prop :=
  exists (Q S : Type) (_ : Fintype Q) (_ : Fintype S) (M : DPDA Q T S),
    M.acceptsByFinalState = L

/-- The DPDA-recognizable class. -/
def DPDA.Class : Set (Language T) := Set.ofPred is_DPDA

/-- Deterministic context-free languages are precisely DPDA-recognizable languages. -/
def is_DCF (L : Language T) : Prop := is_DPDA L

/-- The deterministic context-free language class. -/
def DCF : Set (Language T) := DPDA.Class

/-! ### LR grammars -/

/-! #### Context-free grammar compatibility presentation -/

/-- A context-free grammar has rules `A -> w`. -/
structure CF_grammar (T : Type) where
  nt : Type
  initial : nt
  rules : List (nt × List (symbol T nt))

/-- One context-free rewrite step. -/
def CF_transforms (g : CF_grammar T) (w1 w2 : List (symbol T g.nt)) : Prop :=
  exists r : g.nt × List (symbol T g.nt), exists u v : List (symbol T g.nt),
    r ∈ g.rules ∧ w1 = u ++ [symbol.nonterminal r.fst] ++ v ∧ w2 = u ++ r.snd ++ v

/-- Zero or more context-free rewrite steps. -/
def CF_derives (g : CF_grammar T) :
    List (symbol T g.nt) -> List (symbol T g.nt) -> Prop :=
  Relation.ReflTransGen (CF_transforms g)

/-- A sentential form is generated from the context-free grammar's start symbol. -/
def CF_generates_str (g : CF_grammar T) (s : List (symbol T g.nt)) : Prop :=
  CF_derives g [symbol.nonterminal g.initial] s

/-- A terminal word is generated by a context-free grammar. -/
def CF_generates (g : CF_grammar T) (w : List T) : Prop :=
  CF_generates_str g (List.map symbol.terminal w)

/-- A context-free grammar's generated language. -/
def CF_language (g : CF_grammar T) : Language T := Set.ofPred (CF_generates g)

namespace CF_grammar

/-- A rightmost rewrite replaces a nonterminal followed only by terminals. -/
def RewritesRightmost {N : Type} (r : N × List (symbol T N))
    (u v : List (symbol T N)) : Prop :=
  exists (p : List (symbol T N)) (lookahead : List T),
    u = p ++ [symbol.nonterminal r.1] ++ lookahead.map symbol.terminal ∧
    v = p ++ r.2 ++ lookahead.map symbol.terminal

variable (g : CF_grammar T)

/-- A rightmost grammar step. -/
def ProducesRightmost (u v : List (symbol T g.nt)) : Prop :=
  exists r, r ∈ g.rules ∧ RewritesRightmost r u v

/-- Zero or more rightmost grammar steps. -/
abbrev DerivesRightmost : List (symbol T g.nt) -> List (symbol T g.nt) -> Prop :=
  Relation.ReflTransGen g.ProducesRightmost

/-- The first `k` terminals of LR lookahead. -/
def lrLookahead (k : Nat) (w : List T) : List T := w.take k

/-- Embed a symbol into a grammar with a fresh optional start symbol. -/
def augmentSymbol {N : Type} : symbol T N -> symbol T (Option N)
  | symbol.terminal t => symbol.terminal t
  | symbol.nonterminal A => symbol.nonterminal (some A)

/-- Embed a sentential form into the fresh-start grammar. -/
def augmentString {N : Type} (w : List (symbol T N)) : List (symbol T (Option N)) :=
  w.map augmentSymbol

/-- Embed an original production into the fresh-start grammar. -/
def augmentRule {N : Type} (r : N × List (symbol T N)) :
    Option N × List (symbol T (Option N)) := (some r.1, augmentString r.2)

/-- The new start production `S' -> S`. -/
def augmentStartRule : Option g.nt × List (symbol T (Option g.nt)) :=
  (none, [symbol.nonterminal (some g.initial)])

/-- Fresh-start augmentation of a context-free grammar. -/
def augment : CF_grammar T where
  nt := Option g.nt
  initial := none
  rules := augmentStartRule g :: g.rules.map augmentRule

/-- Knuth's semantic LR(k) handle-uniqueness condition before augmentation. -/
def CoreIsLRk (k : Nat) : Prop :=
  forall (r1 r2 : g.nt × List (symbol T g.nt)), r1 ∈ g.rules -> r2 ∈ g.rules ->
    forall (p1 p2 : List (symbol T g.nt)) (s1 s2 y : List T),
      g.DerivesRightmost [symbol.nonterminal g.initial]
          (p1 ++ [symbol.nonterminal r1.1] ++ s1.map symbol.terminal) ->
      g.DerivesRightmost [symbol.nonterminal g.initial]
          (p2 ++ [symbol.nonterminal r2.1] ++ s2.map symbol.terminal) ->
      p2 ++ r2.2 ++ s2.map symbol.terminal = p1 ++ r1.2 ++ y.map symbol.terminal ->
      lrLookahead k s1 = lrLookahead k y -> p1 = p2 ∧ r1 = r2

/-- An LR(k) grammar satisfies handle uniqueness after fresh-start augmentation. -/
def IsLRk (k : Nat) : Prop := g.augment.CoreIsLRk k

end CF_grammar

/-! #### Canonical unrestricted-grammar presentation -/

/-- A rightmost use of an unrestricted rule. -/
def grammar.RewritesRightmost {N : Type} (r : grule T N)
    (u v : List (symbol T N)) : Prop :=
  exists (p : List (symbol T N)) (lookahead : List T),
    u = p ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++
        lookahead.map symbol.terminal ∧
      v = p ++ r.output_string ++ lookahead.map symbol.terminal

namespace grammar

variable (g : grammar T)

/-- A single rightmost derivation step in an unrestricted grammar. -/
def ProducesRightmost (u v : List (symbol T g.nt)) : Prop :=
  exists r, r ∈ g.rules ∧ RewritesRightmost r u v

/-- Rightmost derivation in an unrestricted grammar. -/
abbrev DerivesRightmost :
    List (symbol T g.nt) -> List (symbol T g.nt) -> Prop :=
  Relation.ReflTransGen g.ProducesRightmost

/-- The first `k` terminals of LR lookahead. -/
def lrLookahead (k : Nat) (w : List T) : List T := w.take k

/-- Embed a symbol into an unrestricted grammar with a fresh start symbol. -/
def augmentSymbol {N : Type} : symbol T N -> symbol T (Option N)
  | symbol.terminal t => symbol.terminal t
  | symbol.nonterminal A => symbol.nonterminal (some A)

/-- Embed a sentential form into the fresh-start unrestricted grammar. -/
def augmentString {N : Type} (w : List (symbol T N)) :
    List (symbol T (Option N)) :=
  w.map augmentSymbol

/-- Embed an unrestricted production into the fresh-start grammar. -/
def augmentRule {N : Type} (r : grule T N) : grule T (Option N) where
  input_L := augmentString r.input_L
  input_N := some r.input_N
  input_R := augmentString r.input_R
  output_string := augmentString r.output_string

/-- The new start production `S' -> S`. -/
def augmentStartRule : grule T (Option g.nt) where
  input_L := []
  input_N := none
  input_R := []
  output_string := [symbol.nonterminal (some g.initial)]

/-- Fresh-start augmentation of an unrestricted grammar. -/
def augment : grammar T where
  nt := Option g.nt
  initial := none
  rules := augmentStartRule g :: g.rules.map augmentRule

/-- Knuth's semantic LR(k) handle-uniqueness condition directly on
unrestricted rules, before augmentation. -/
def CoreIsLRk (k : Nat) : Prop :=
  forall (r1 r2 : grule T g.nt), r1 ∈ g.rules -> r2 ∈ g.rules ->
    forall (p1 p2 : List (symbol T g.nt)) (s1 s2 y : List T),
      g.DerivesRightmost [symbol.nonterminal g.initial]
          (p1 ++ r1.input_L ++ [symbol.nonterminal r1.input_N] ++ r1.input_R ++
            s1.map symbol.terminal) ->
      g.DerivesRightmost [symbol.nonterminal g.initial]
          (p2 ++ r2.input_L ++ [symbol.nonterminal r2.input_N] ++ r2.input_R ++
            s2.map symbol.terminal) ->
      p2 ++ r2.output_string ++ s2.map symbol.terminal =
          p1 ++ r1.output_string ++ y.map symbol.terminal ->
      lrLookahead k s1 = lrLookahead k y -> p1 = p2 ∧ r1 = r2

/-- Handle uniqueness after fresh-start augmentation. -/
def IsLRk (k : Nat) : Prop := g.augment.CoreIsLRk k

end grammar

/-- An unrestricted grammar is LR(k) when it is context-free and satisfies
the augmented handle-uniqueness condition. -/
def grammar_lrk (k : Nat) (g : grammar T) : Prop :=
  grammar_context_free g ∧ g.IsLRk k

/-- Compatibility presentation through context-free grammars. -/
def is_LRk_via_cfg (k : Nat) (L : Language T) : Prop :=
  exists g : CF_grammar T, g.IsLRk k ∧ CF_language g = L

/-- A language is LR(k) if generated by an LR(k) unrestricted grammar. -/
def is_LRk (k : Nat) (L : Language T) : Prop :=
  exists g : grammar T, grammar_lrk k g ∧ grammar_language g = L

/-- The LR(k) language class. -/
def LRk (k : Nat) : Set (Language T) := Set.ofPred (is_LRk k)

/-- A language is LR if it is LR(k) for some finite `k`. -/
def is_LR (L : Language T) : Prop := exists k : Nat, is_LRk k L

/-- The LR language class. -/
def LR : Set (Language T) := Set.ofPred is_LR

/-! ### Indexed grammars -/

/-- An indexed right-hand symbol is a terminal or a nonterminal with an optional pushed flag. -/
inductive IRhsSymbol (T : Type) (N : Type) (F : Type) where
  | terminal : T -> IRhsSymbol T N F
  | nonterminal : N -> Option F -> IRhsSymbol T N F
deriving DecidableEq

/-- An indexed rule may pop one flag and push flags on right-hand nonterminals. -/
structure IRule (T : Type) (N : Type) (F : Type) where
  lhs : N
  consume : Option F
  rhs : List (IRhsSymbol T N F)

/-- An indexed grammar has nonterminals, flags, a start symbol, and finitely many rules. -/
structure IndexedGrammar (T : Type) where
  nt : Type
  flag : Type
  initial : nt
  rules : List (IRule T nt flag)

namespace IndexedGrammar

/-- A sentential symbol is a terminal or a nonterminal carrying its flag stack. -/
inductive ISym (g : IndexedGrammar T) where
  | terminal : T -> ISym g
  | indexed : g.nt -> List g.flag -> ISym g

/-- Expand a rule right-hand side while distributing and optionally extending its stack. -/
def expandRhs (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag))
    (sigma : List g.flag) : List (ISym g) :=
  rhs.map fun s => match s with
    | IRhsSymbol.terminal t => ISym.terminal t
    | IRhsSymbol.nonterminal n none => ISym.indexed n sigma
    | IRhsSymbol.nonterminal n (some f) => ISym.indexed n (f :: sigma)

/-- One indexed-grammar step, consuming and distributing a nonterminal's stack. -/
def Transforms (g : IndexedGrammar T) (w1 w2 : List (ISym g)) : Prop :=
  exists (r : IRule T g.nt g.flag) (u v : List (ISym g)) (sigma : List g.flag),
    r ∈ g.rules ∧
    (match r.consume with
      | none => w1 = u ++ [ISym.indexed r.lhs sigma] ++ v
      | some f => w1 = u ++ [ISym.indexed r.lhs (f :: sigma)] ++ v) ∧
    w2 = u ++ expandRhs g r.rhs sigma ++ v

/-- Zero or more indexed-grammar steps. -/
def Derives (g : IndexedGrammar T) : List (ISym g) -> List (ISym g) -> Prop :=
  Relation.ReflTransGen (Transforms g)

/-- Generation starts with the initial nonterminal carrying an empty stack. -/
def Generates (g : IndexedGrammar T) (w : List T) : Prop :=
  Derives g [ISym.indexed g.initial []] (w.map ISym.terminal)

/-- The language generated by an indexed grammar. -/
def Language (g : IndexedGrammar T) : _root_.Language T := Set.ofPred (Generates g)

end IndexedGrammar

/-- A language is indexed if it is generated by an indexed grammar. -/
def is_Indexed (L : Language T) : Prop :=
  exists g : IndexedGrammar T, g.Language = L

/-- The indexed language class. -/
def Indexed : Set (Language T) := Set.ofPred is_Indexed

/-! ### Linearly bounded and unrestricted Turing automata -/

namespace DLBA

/-- A bounded-tape head can move left, right, or stay. -/
public inductive Dir where | left | right | stay
deriving DecidableEq, Repr, Inhabited

instance : Fintype Dir where
  elems := {Dir.left, Dir.right, Dir.stay}
  complete d := by cases d <;> simp

/-- A tape of `n + 1` cells with a head position. -/
public structure BoundedTape (Gamma : Type*) (n : Nat) where
  contents : Fin (n + 1) -> Gamma
  head : Fin (n + 1)
deriving DecidableEq

/-- Read the bounded tape under its head. -/
@[simp]
public def BoundedTape.read {Gamma : Type*} {n : Nat} (t : BoundedTape Gamma n) : Gamma :=
  t.contents t.head

/-- Write the bounded tape under its head. -/
@[reducible]
public def BoundedTape.write {Gamma : Type*} {n : Nat} (t : BoundedTape Gamma n) (a : Gamma) :
    BoundedTape Gamma n := {t with contents := Function.update t.contents t.head a}

/-- Move the head while clamping it to the tape boundaries. -/
@[reducible]
public def BoundedTape.moveHead {Gamma : Type*} {n : Nat} (t : BoundedTape Gamma n) (d : Dir) :
    BoundedTape Gamma n := {t with head := match d with
      | Dir.stay => t.head
      | Dir.left => if h : 0 < t.head.val then
          ⟨t.head.val - 1, lt_trans (Nat.sub_lt h (Nat.zero_lt_succ 0)) t.head.isLt⟩
        else t.head
      | Dir.right => if h : t.head.val < n then
          ⟨t.head.val + 1, Nat.add_lt_add_right h 1⟩
        else t.head}

/-- A bounded-machine configuration is a state and bounded tape. -/
public structure Cfg (Gamma : Type*) (Lambda : Type*) (n : Nat) where
  state : Lambda
  tape : BoundedTape Gamma n
deriving DecidableEq

end DLBA

namespace LBA

/-- A nondeterministic linearly bounded machine. -/
structure Machine (Gamma : Type*) (Lambda : Type*) where
  transition : Lambda -> Gamma -> Set (Lambda × Gamma × DLBA.Dir)
  accept : Lambda -> Bool
  initial : Lambda

/-- One nondeterministic bounded-tape transition. -/
def Step {Gamma Lambda : Type*} {n : Nat}
    (M : Machine Gamma Lambda) (cfg cfg' : DLBA.Cfg Gamma Lambda n) : Prop :=
  exists q' a d, (q', a, d) ∈ M.transition cfg.state cfg.tape.read ∧
    cfg' = ⟨q', (cfg.tape.write a).moveHead d⟩

/-- Zero or more bounded-tape transitions. -/
def Reaches {Gamma Lambda : Type*} {n : Nat}
    (M : Machine Gamma Lambda) : DLBA.Cfg Gamma Lambda n -> DLBA.Cfg Gamma Lambda n -> Prop :=
  Relation.ReflTransGen (Step M)

/-- An LBA accepts when some run reaches a state marked accepting. -/
def Accepts {Gamma Lambda : Type*} {n : Nat}
    (M : Machine Gamma Lambda) (cfg : DLBA.Cfg Gamma Lambda n) : Prop :=
  exists cfg' : DLBA.Cfg Gamma Lambda n, Reaches M cfg cfg' ∧ M.accept cfg'.state = true

variable {T Gamma : Type*}

/-- Endmarker tape alphabet: interior symbols plus distinct left and right markers. -/
abbrev EndAlpha (T Gamma : Type*) : Type _ := Option (T ⊕ Gamma) ⊕ Bool

/-- The left endmarker. -/
abbrev leftMark : EndAlpha T Gamma := Sum.inr false

/-- The right endmarker. -/
abbrev rightMark : EndAlpha T Gamma := Sum.inr true

/-- Load `left-marker, input, right-marker` on a bounded tape. -/
noncomputable def loadEnd (w : List T) : DLBA.BoundedTape (EndAlpha T Gamma) (w.length + 1) :=
  ⟨fun k => if k.val = 0 then leftMark
    else if h : k.val - 1 < w.length then Sum.inl (some (Sum.inl (w.get ⟨k.val - 1, h⟩)))
    else rightMark, ⟨0, Nat.succ_pos _⟩⟩

/-- Initial endmarker-LBA configuration, with the head on the left marker. -/
noncomputable def initCfgEnd {Lambda : Type*} (M : Machine (EndAlpha T Gamma) Lambda)
    (w : List T) : DLBA.Cfg (EndAlpha T Gamma) Lambda (w.length + 1) :=
  ⟨M.initial, loadEnd w⟩

/-- The language accepted by an endmarker LBA, including its ordinary run on the empty word. -/
noncomputable def LanguageEnd {Lambda : Type*} (M : Machine (EndAlpha T Gamma) Lambda) :
    Language T := fun w => Accepts M (initCfgEnd M w)

end LBA

/-- Recognition by a finite nondeterministic endmarker LBA. -/
def is_LBA {T : Type} [Fintype T] [DecidableEq T] (L : Language T) : Prop :=
  exists (Gamma Lambda : Type) (_ : Fintype Gamma) (_ : Fintype Lambda)
    (_ : DecidableEq Gamma) (_ : DecidableEq Lambda)
    (M : LBA.Machine (LBA.EndAlpha T Gamma) Lambda), LBA.LanguageEnd M = L

/-- The linearly bounded automaton language class. -/
def LBA {T : Type} [Fintype T] [DecidableEq T] : Set (Language T) := Set.ofPred is_LBA

/-- Turing recognition uses Mathlib's TM0 over a finite work alphabet and halting acceptance. -/
def is_TM {T : Type} [Fintype T] (L : Language T) : Prop :=
  exists (Gamma : Type) (_ : Fintype Gamma)
    (Lambda : Type) (_ : Inhabited Lambda) (_ : Fintype Lambda)
    (M : Turing.TM0.Machine (Option (T ⊕ Gamma)) Lambda),
    forall w : List T,
      w ∈ L ↔ (Turing.TM0.eval M (w.map fun t => some (Sum.inl t))).Dom

/-- The Turing-recognizable language class. -/
def TM {T : Type} [Fintype T] : Set (Language T) := Set.ofPred is_TM

/-- A recursive language has an always-halting Mathlib TM0 decider with Boolean accepting states. -/
def is_Recursive {T : Type} (L : Language T) : Prop :=
  exists (Gamma : Type) (_ : Fintype Gamma)
    (Lambda : Type) (_ : Inhabited Lambda) (_ : Fintype Lambda)
    (M : TM0.Machine (Option (T ⊕ Gamma)) Lambda) (accept : Lambda -> Bool),
    (forall w : List T,
      (StateTransition.eval (TM0.step M)
        (TM0.init (w.map fun t => some (Sum.inl t)))).Dom) ∧
    (forall w : List T,
      forall h : (StateTransition.eval (TM0.step M)
        (TM0.init (w.map fun t => some (Sum.inl t)))).Dom,
      w ∈ L ↔ accept ((StateTransition.eval (TM0.step M)
        (TM0.init (w.map fun t => some (Sum.inl t)))).get h).q = true)

/-- The recursive (decidable-language) class. -/
def Recursive : Set (Language T) := Set.ofPred is_Recursive

/-! ## Language operations and abstract closure predicates -/

namespace Language

/-- Substitution replaces every letter by a word from its assigned language. -/
def subst {alpha beta : Type} (L : Language alpha) (f : alpha -> Language beta) : Language beta :=
  {u | exists w, w ∈ L ∧ u ∈ (w.map f).prod}

/-- The right quotient contains `w` when `w ++ v` is in `L` for some `v` in `R`. -/
def rightQuotient {alpha : Type*} (L R : Language alpha) : Language alpha :=
  {w | exists v, v ∈ R ∧ w ++ v ∈ L}

/-- The direct image of a language under the word homomorphism induced by `h`. -/
def homomorphicImage {alpha beta : Type} (L : Language alpha) (h : alpha -> List beta) :
    Language beta := L.subst (fun a => ({h a} : Language beta))

end Language

/-- A word homomorphism is epsilon-free when no letter maps to the empty word. -/
def IsEpsFreeHomomorphism {alpha beta : Type} (h : alpha -> List beta) : Prop :=
  forall a, h a ≠ []

variable {alpha : Type*}

/-- Closure under union. -/
def ClosedUnderUnion (P : Language alpha -> Prop) : Prop :=
  forall L1 L2, P L1 -> P L2 -> P (L1 + L2)

/-- Closure under intersection. -/
def ClosedUnderIntersection (P : Language alpha -> Prop) : Prop :=
  forall L1 L2, P L1 -> P L2 -> P (L1 ⊓ L2)

/-- Closure under complement. -/
def ClosedUnderComplement (P : Language alpha -> Prop) : Prop :=
  forall L, P L -> P Lᶜ

/-- Closure under language concatenation. -/
def ClosedUnderConcatenation (P : Language alpha -> Prop) : Prop :=
  forall L1 L2, P L1 -> P L2 -> P (L1 * L2)

/-- Closure under Kleene star. -/
def ClosedUnderKleeneStar (P : Language alpha -> Prop) : Prop :=
  forall L, P L -> P (KStar.kstar L)

/-- Closure under word reversal. -/
def ClosedUnderReverse (P : Language alpha -> Prop) : Prop :=
  forall L, P L -> P L.reverse

/-- Closure under intersection with a regular language. -/
def ClosedUnderIntersectionWithRegular (P : Language alpha -> Prop) : Prop :=
  forall L, P L -> forall R, R.IsRegular -> P (L ⊓ R)

/-- Closure under right quotient by another language in the class. -/
def ClosedUnderRightQuotient (P : Language alpha -> Prop) : Prop :=
  forall L1 L2, P L1 -> P L2 -> P (Language.rightQuotient L1 L2)

/-- Closure under right quotient by a regular language. -/
def ClosedUnderRightQuotientWithRegular (P : Language alpha -> Prop) : Prop :=
  forall L, P L -> forall R, R.IsRegular -> P (Language.rightQuotient L R)

/-- Uniform finite-alphabet closure under word homomorphism. -/
def ClosedUnderHomomorphism
    (isP : forall {alpha : Type} [Fintype alpha], Language alpha -> Prop) : Prop :=
  forall {alpha beta : Type} [Fintype alpha] [Fintype beta]
    (L : Language alpha) (h : alpha -> List beta), isP L -> isP (L.homomorphicImage h)

/-- Uniform finite-alphabet closure under epsilon-free word homomorphism. -/
def ClosedUnderEpsFreeHomomorphism
    (isP : forall {alpha : Type} [Fintype alpha], Language alpha -> Prop) : Prop :=
  forall {alpha beta : Type} [Fintype alpha] [Fintype beta]
    (L : Language alpha) (h : alpha -> List beta),
    IsEpsFreeHomomorphism h -> isP L -> isP (L.homomorphicImage h)

/-- Uniform finite-alphabet closure under inverse word homomorphism. -/
def ClosedUnderInverseHomomorphism
    (isP : forall {alpha : Type} [Fintype alpha], Language alpha -> Prop) : Prop :=
  forall {alpha beta : Type} [Fintype alpha] [Fintype beta]
    (L : Language beta) (h : alpha -> List beta), isP L -> isP {w | w.flatMap h ∈ L}

/-- Uniform finite-alphabet closure under substitution. -/
def ClosedUnderSubstitution
    (isP : forall {alpha : Type} [Fintype alpha], Language alpha -> Prop) : Prop :=
  forall {alpha beta : Type} [Fintype alpha] [Fintype beta]
    (L : Language alpha) (f : alpha -> Language beta),
    isP L -> (forall a, isP (f a)) -> isP (L.subst f)

/-! ## Grammar/automaton equivalences -/

/-! ### Finite-state automata -/

/-- The grammar-defined regular class equals the Mathlib-DFA class. -/
theorem RG_eq_DFA {T : Type} [Fintype T] :
    (RG : Set (Language T)) = DFA.Class := by sorry

/-- The Mathlib-NFA and Mathlib-DFA language classes coincide. -/
theorem NFA_eq_DFA {T : Type} :
    (NFA.Class : Set (Language T)) = DFA.Class := by sorry

/-! ### Pushdown automata -/

/-- Context-free grammars and nondeterministic PDAs recognize the same class. -/
theorem CF_eq_PDA_Class {T : Type} [Fintype T] :
    (CF : Set (Language T)) = PDA.Class := by sorry

/-- The PDA classes under final-state and empty-stack acceptance coincide. -/
theorem PDA_FinalStateClass_eq_Class {T : Type} [Fintype T] :
    (PDA.FinalStateClass : Set (Language T)) = PDA.Class := by sorry

/-! ### Deterministic pushdown automata and LR grammars -/

/-- The grammar-side LR class equals the DPDA-recognizable class. -/
theorem LR_eq_DPDA {T : Type} [Fintype T] :
    (LR : Set (Language T)) = DPDA.Class := by sorry

/-- The grammar-side LR and deterministic context-free classes coincide. -/
theorem LR_eq_DCF {T : Type} [Fintype T] :
    (LR : Set (Language T)) = DCF := by sorry

/-! ### Linearly bounded automata -/

/-- Context-sensitive grammars and nondeterministic endmarker LBAs recognize the same class. -/
theorem CS_eq_LBA {T : Type} [Fintype T] [DecidableEq T] :
    (CS : Set (Language T)) = LBA := by sorry

/-! ### Turing machines -/

/-- Unrestricted grammars and Mathlib TM0 recognizers define the same class. -/
theorem TM_eq_RE {T : Type} [DecidableEq T] [Fintype T] :
    (TM : Set (Language T)) = RE := by sorry

/-! ## Strict extended Chomsky hierarchy -/

namespace ChomskyHierarchy

/-- Over every finite alphabet with at least 2 elements, regular languages are
strictly contained in linear languages. -/
theorem RG_strict_subclass_Linear_of_card {T : Type} [Fintype T]
    (hT : 2 ≤ Fintype.card T) :
    (RG : Set (Language T)) ⊂ (Linear : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 4 elements, linear languages are
strictly contained in context-free languages. -/
theorem Linear_strict_subclass_CF_of_card {T : Type} [Fintype T]
    (hT : 4 ≤ Fintype.card T) :
    (Linear : Set (Language T)) ⊂ (CF : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 2 elements, regular languages are
strictly contained in deterministic context-free languages. -/
theorem RG_strict_subclass_DCF_of_card {T : Type} [Fintype T]
    (hT : 2 ≤ Fintype.card T) :
    (RG : Set (Language T)) ⊂ (DCF : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 3 elements, deterministic
context-free languages are a strict subclass of context-free languages. -/
theorem DCF_strict_subclass_CF_of_card {T : Type} [Fintype T]
    (hT : 3 ≤ Fintype.card T) :
    (DCF : Set (Language T)) ⊂ (CF : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 4 elements, the linear and
DPDA-recognizable classes are incomparable: neither contains the other, and in
particular they are unequal. -/
theorem Linear_incomp_DPDA_of_card {T : Type} [Fintype T]
    (hT : 4 ≤ Fintype.card T) :
    IncompRel (· ⊆ ·) (Linear : Set (Language T))
      (DPDA.Class : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 3 elements, context-free languages are
strictly contained in indexed languages. -/
theorem CF_strict_subclass_Indexed {T : Type} [Fintype T]
    (hT : 3 ≤ Fintype.card T) :
    (CF : Set (Language T)) ⊂ (Indexed : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 2 elements, indexed languages are
strictly contained in context-sensitive languages. -/
theorem Indexed_strict_subclass_CS {T : Type} [Fintype T]
    (hT : 2 ≤ Fintype.card T) :
    (Indexed : Set (Language T)) ⊂ (CS : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 1 element, context-sensitive
languages are strictly contained in recursive languages. -/
theorem CS_strict_subclass_Recursive_of_card {T : Type} [Fintype T]
    (hT : 1 ≤ Fintype.card T) :
    (CS : Set (Language T)) ⊂ (Recursive : Set (Language T)) := by sorry

/-- Over every finite alphabet with at least 1 element, recursive languages are
strictly contained in recursively enumerable languages. -/
theorem Recursive_strict_subclass_RE_of_card {T : Type} [Fintype T]
    (hT : 1 ≤ Fintype.card T) :
    (Recursive : Set (Language T)) ⊂ (RE : Set (Language T)) := by sorry

end ChomskyHierarchy

/-! ## Closure and non-closure results

Each statement is the full abstract closure property.  A negated statement is
witnessed in the proof development by concrete languages over the indicated
finite alphabet; it does not claim failure over every alphabet.
-/

/-! ### Linear languages -/

/-- Linear languages are not closed under concatenation when the alphabet has at least 4 elements. -/
theorem Linear_not_closedUnderConcatenation {T : Type} (e : Fin 4 ↪ T) :
    ¬ ClosedUnderConcatenation (@is_Linear T) := by sorry

/-! ### Regular languages -/
theorem RG_closedUnderUnion {alpha : Type} [Fintype alpha] : ClosedUnderUnion (@is_RG alpha) := by sorry
theorem RG_closedUnderIntersection {alpha : Type} [Fintype alpha] : ClosedUnderIntersection (@is_RG alpha) := by sorry
theorem RG_closedUnderComplement {alpha : Type} [Fintype alpha] : ClosedUnderComplement (@is_RG alpha) := by sorry
theorem RG_closedUnderConcatenation {alpha : Type} [Fintype alpha] : ClosedUnderConcatenation (@is_RG alpha) := by sorry
theorem RG_closedUnderKleeneStar {alpha : Type} [Fintype alpha] : ClosedUnderKleeneStar (@is_RG alpha) := by sorry
namespace Language
theorem RG_closedUnderHomomorphism : ClosedUnderHomomorphism is_RG := by sorry
theorem RG_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism is_RG := by sorry
end Language
theorem RG_closedUnderSubstitution : ClosedUnderSubstitution is_RG := by sorry
theorem RG_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_RG := by sorry
theorem RG_closedUnderReverse {alpha : Type} [Fintype alpha] : ClosedUnderReverse (@is_RG alpha) := by sorry
theorem RG_closedUnderIntersectionWithRegular {alpha : Type} [Fintype alpha] : ClosedUnderIntersectionWithRegular (@is_RG alpha) := by sorry
theorem RG_closedUnderRightQuotient {alpha : Type} [Fintype alpha] : ClosedUnderRightQuotient (@is_RG alpha) := by sorry
theorem RG_closedUnderRightQuotientWithRegular {alpha : Type} [Fintype alpha] : ClosedUnderRightQuotientWithRegular (@is_RG alpha) := by sorry

/-! ### Deterministic context-free languages -/
theorem DCF_notClosedUnderUnion : ¬ ClosedUnderUnion (alpha := Fin 3) is_DCF := by sorry
theorem DCF_notClosedUnderIntersection : ¬ ClosedUnderIntersection (alpha := Fin 3) is_DCF := by sorry
theorem DCF_closedUnderComplement {T : Type} [Fintype T] :
    ClosedUnderComplement (alpha := T) is_DCF := by sorry
namespace DCFConcatenation
theorem DCF_notClosedUnderConcatenation :
    ¬ ClosedUnderConcatenation (alpha := Bool ⊕ Fin 3) is_DCF := by sorry
end DCFConcatenation
namespace DCFStar
theorem DCF_notClosedUnderKleeneStar :
    ¬ ClosedUnderKleeneStar (alpha := Bool ⊕ Fin 3) is_DCF := by sorry
end DCFStar
namespace DCFHomomorphism
theorem DCF_notClosedUnderHomomorphism : ¬ ClosedUnderHomomorphism is_DCF := by sorry
theorem DCF_notClosedUnderEpsFreeHomomorphism : ¬ ClosedUnderEpsFreeHomomorphism is_DCF := by sorry
end DCFHomomorphism
theorem DCF_notClosedUnderSubstitution : ¬ ClosedUnderSubstitution is_DCF := by sorry
theorem DCF_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_DCF := by sorry
theorem DCF_notClosedUnderReverse :
    ¬ ClosedUnderReverse (alpha := Bool ⊕ Fin 3) is_DCF := by sorry
theorem DCF_closedUnderIntersectionWithRegular {T : Type} [Fintype T] :
    ClosedUnderIntersectionWithRegular (alpha := T) is_DCF := by sorry
theorem DCF_notClosedUnderRightQuotient :
    ¬ ClosedUnderRightQuotient (alpha := Bool) is_DCF := by sorry
theorem DCF_closedUnderRightQuotientWithRegular {T : Type} [Fintype T] :
    ClosedUnderRightQuotientWithRegular (alpha := T) is_DCF := by sorry

/-! ### Context-free languages -/
theorem CF_closedUnderUnion {T : Type} : ClosedUnderUnion (@is_CF T) := by sorry
theorem CF_notClosedUnderIntersection : ¬ ClosedUnderIntersection (@is_CF (Fin 3)) := by sorry
theorem CF_notClosedUnderComplement : ¬ ClosedUnderComplement (@is_CF (Fin 3)) := by sorry
theorem CF_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation (@is_CF T) := by sorry
theorem CF_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar (@is_CF T) := by sorry
theorem CF_closedUnderHomomorphism : ClosedUnderHomomorphism is_CF := by sorry
theorem CF_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism is_CF := by sorry
theorem CF_closedUnderSubstitution {alpha : Type} [Fintype alpha] : ClosedUnderSubstitution is_CF := by sorry
theorem CF_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_CF := by sorry
theorem CF_closedUnderReverse {T : Type} : ClosedUnderReverse (@is_CF T) := by sorry
theorem CF_closedUnderIntersectionWithRegular {T : Type} : ClosedUnderIntersectionWithRegular (@is_CF T) := by sorry
theorem CF_notClosedUnderRightQuotient :
    ¬ ClosedUnderRightQuotient (alpha := Bool) is_CF := by sorry
theorem CF_closedUnderRightQuotientWithRegular {T : Type} : ClosedUnderRightQuotientWithRegular (@is_CF T) := by sorry

/-! ### Indexed languages -/

/-- Three-letter alphabet used by the indexed right-quotient counterexample. -/
inductive CopyLetter where
  | a | b | separator
deriving DecidableEq, Inhabited

instance : Fintype CopyLetter where
  elems := {CopyLetter.a, CopyLetter.b, CopyLetter.separator}
  complete c := by cases c <;> simp

theorem Indexed_closedUnderUnion {T : Type} : ClosedUnderUnion (@is_Indexed T) := by sorry
namespace IndexedIntersectionNonclosure
theorem Indexed_notClosedUnderIntersection :
    ¬ ClosedUnderIntersection (alpha := Bool) is_Indexed := by sorry
end IndexedIntersectionNonclosure
namespace IndexedComplementNonclosure
theorem Indexed_notClosedUnderComplement :
    ¬ ClosedUnderComplement (alpha := Bool) is_Indexed := by sorry
end IndexedComplementNonclosure
theorem Indexed_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation (@is_Indexed T) := by sorry
theorem Indexed_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar (@is_Indexed T) := by sorry
theorem Indexed_closedUnderHomomorphism : ClosedUnderHomomorphism is_Indexed := by sorry
theorem Indexed_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism is_Indexed := by sorry
theorem Indexed_closedUnderSubstitution : ClosedUnderSubstitution is_Indexed := by sorry
theorem Indexed_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_Indexed := by sorry
theorem Indexed_closedUnderReverse {T : Type} : ClosedUnderReverse (@is_Indexed T) := by sorry
theorem Indexed_closedUnderIntersectionWithRegular {T : Type} [Fintype T] : ClosedUnderIntersectionWithRegular (@is_Indexed T) := by sorry
theorem Indexed_notClosedUnderRightQuotient :
    ¬ ClosedUnderRightQuotient (alpha := CopyLetter) is_Indexed := by sorry
theorem Indexed_closedUnderRightQuotientWithRegular {T : Type} [Fintype T] : ClosedUnderRightQuotientWithRegular (@is_Indexed T) := by sorry

/-! ### Context-sensitive languages -/
theorem CS_closedUnderUnion {T : Type} : ClosedUnderUnion (@is_CS T) := by sorry
theorem CS_closedUnderIntersection {T : Type} [Fintype T] [DecidableEq T] : ClosedUnderIntersection (@is_CS T) := by sorry
theorem CS_closedUnderComplement {T : Type} [Fintype T] : ClosedUnderComplement (@is_CS T) := by sorry
theorem CS_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation (@is_CS T) := by sorry
theorem CS_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar (@is_CS T) := by sorry
theorem CS_notClosedUnderHomomorphism : ¬ ClosedUnderHomomorphism is_CS := by sorry
theorem CS_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism is_CS := by sorry
theorem CS_notClosedUnderSubstitution : ¬ ClosedUnderSubstitution is_CS := by sorry
theorem CS_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_CS := by sorry
theorem CS_closedUnderReverse {T : Type} : ClosedUnderReverse (@is_CS T) := by sorry
theorem CS_closedUnderIntersectionWithRegular {T : Type} [Fintype T] [DecidableEq T] : ClosedUnderIntersectionWithRegular (@is_CS T) := by sorry
theorem CS_notClosedUnderRightQuotient :
    ¬ ClosedUnderRightQuotient (alpha := Option Unit) is_CS := by sorry
theorem CS_notClosedUnderRightQuotientWithRegular :
    ¬ ClosedUnderRightQuotientWithRegular (alpha := Option Unit) is_CS := by sorry

/-! ### Recursive languages -/
theorem Recursive_closedUnderUnion {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderUnion (@is_Recursive T) := by sorry
theorem Recursive_closedUnderIntersection {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderIntersection (@is_Recursive T) := by sorry
theorem Recursive_closedUnderComplement {T : Type} : ClosedUnderComplement (@is_Recursive T) := by sorry
theorem Recursive_closedUnderConcatenation {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderConcatenation (@is_Recursive T) := by sorry
theorem Recursive_closedUnderKleeneStar {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderKleeneStar (@is_Recursive T) := by sorry
theorem Recursive_notClosedUnderHomomorphism : ¬ ClosedUnderHomomorphism is_Recursive := by sorry
theorem Recursive_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism is_Recursive := by sorry
theorem Recursive_notClosedUnderSubstitution : ¬ ClosedUnderSubstitution is_Recursive := by sorry
theorem Recursive_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_Recursive := by sorry
namespace RecursiveReverse
theorem Recursive_closedUnderReverse {T : Type} [DecidableEq T] [Fintype T] :
    ClosedUnderReverse (alpha := T) is_Recursive := by sorry
end RecursiveReverse
theorem Recursive_closedUnderIntersectionWithRegular {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderIntersectionWithRegular (@is_Recursive T) := by sorry
theorem Recursive_notClosedUnderRightQuotient :
    ¬ ClosedUnderRightQuotient (alpha := Bool) is_Recursive := by sorry
theorem Recursive_notClosedUnderRightQuotientWithRegular :
    ¬ ClosedUnderRightQuotientWithRegular (alpha := Bool) is_Recursive := by sorry

/-! ### Recursively enumerable languages -/
theorem RE_closedUnderUnion {T : Type} : ClosedUnderUnion (@is_RE T) := by sorry
theorem RE_closedUnderIntersection {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderIntersection (@is_RE T) := by sorry
theorem RE_notClosedUnderComplement : ¬ ClosedUnderComplement (@is_RE Unit) := by sorry
theorem RE_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation (@is_RE T) := by sorry
theorem RE_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar (@is_RE T) := by sorry
theorem RE_closedUnderHomomorphism : ClosedUnderHomomorphism is_RE := by sorry
theorem RE_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism is_RE := by sorry
theorem RE_closedUnderSubstitution : ClosedUnderSubstitution is_RE := by sorry
theorem RE_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism is_RE := by sorry
theorem RE_closedUnderReverse {T : Type} : ClosedUnderReverse (@is_RE T) := by sorry
theorem RE_closedUnderIntersectionWithRegular {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderIntersectionWithRegular (@is_RE T) := by sorry
theorem RE_closedUnderRightQuotient {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderRightQuotient (@is_RE T) := by sorry
theorem RE_closedUnderRightQuotientWithRegular {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderRightQuotientWithRegular (@is_RE T) := by sorry