/-
Copyright (c) 2024 Tobias Leichtfried. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tobias Leichtfried
-/
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Tactic
import Mathlib.Util.Delaborators
import Mathlib.Computability.ContextFreeGrammar
import Mathlib.Computability.EpsilonNFA

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]

@[ext]
structure conf (p : PDA Q T S) where
  state : Q
  input : List T
  stack : List S

variable {pda : PDA Q T S}

namespace conf

abbrev appendInput (r : conf pda) (x : List T) : conf pda :=
  ⟨r.state, r.input++x, r.stack⟩

abbrev appendStack (r : conf pda) (β : List S) : conf pda :=
  ⟨r.state, r.input, r.stack++β⟩

abbrev stackPostfix (r : conf pda) (β : List S) : Prop :=
  ∃ α : List S, r.stack = α++β

abbrev stackPostfixNontriv (r : conf pda) (β : List S): Prop :=
  ∃ α : List S, α.length > 0 ∧ r.stack = α++β

end conf

def step (r₁ : conf pda) : Set (conf pda) :=
  match r₁ with
    | ⟨q, a::w, Z::α⟩ =>
        { r₂ : conf pda | ∃ (p : Q) (β : List S), (p,β) ∈ pda.transition_fun q a Z ∧
                          r₂ = ⟨p, w, (β ++ α)⟩ } ∪
        { r₂ : conf pda | ∃ (p : Q) (β : List S), (p,β) ∈ pda.transition_fun' q Z ∧
                          r₂ = ⟨p, a :: w, (β ++ α)⟩ }
    | ⟨q, [], Z::α⟩ => { r₂ : conf pda | ∃ (p : Q) (β : List S), (p,β) ∈ pda.transition_fun' q Z ∧
                                          r₂ = ⟨p, [], (β ++ α)⟩ }
    | ⟨_, _, []⟩ => ∅

def Reaches₁ (r₁ r₂ : conf pda) : Prop := r₂ ∈ step r₁
def Reaches : conf pda → conf pda → Prop := Relation.ReflTransGen Reaches₁

inductive ReachesIn : ℕ → conf pda → conf pda → Prop where
  | refl : (r₁ : conf pda)  → ReachesIn 0 r₁ r₁
  | step : {n: ℕ} → {r₁ r₂ r₃ : conf pda} → ReachesIn n r₁ r₂ → Reaches₁ r₂ r₃ → ReachesIn (n+1) r₁ r₃

def acceptsByEmptyStack (pda : PDA Q T S) : Language T :=
  { w : List T | ∃ q : Q,
      Reaches (⟨pda.initial_state, w, [pda.start_symbol]⟩ : conf pda) ⟨q, [], []⟩ }

def acceptsByFinalState (pda : PDA Q T S) : Language T :=
  { w : List T | ∃ q  ∈ pda.final_states, ∃ γ : List S,
      Reaches (⟨pda.initial_state, w, [pda.start_symbol]⟩ : conf pda) ⟨q, [], γ⟩ }

@[refl]
theorem Reaches.refl (r₁ : conf pda) : Reaches r₁ r₁ := Relation.ReflTransGen.refl

@[refl]
theorem reachesIn.refl (r₁ : conf pda) : ReachesIn 0 r₁ r₁ := ReachesIn.refl r₁

variable {r₁ r₂ : conf pda}

theorem reachesIn_zero (h: ReachesIn 0 r₁ r₂) : r₁ = r₂ := by
  rcases h with _|_
  · rfl

theorem reaches₁_iff_reachesIn_one : Reaches₁ r₁ r₂ ↔ ReachesIn 1 r₁ r₂ := by
  constructor
  · exact ReachesIn.step (by rfl)
  · intro h
    rcases h with _ | ⟨h₁,h₂⟩
    · apply reachesIn_zero at h₁
      simp_all

theorem reachesIn_of_n_one {r₃ : conf pda} {n : ℕ} (h₁ : ReachesIn n r₁ r₂) (h₂ : ReachesIn 1 r₂ r₃) :
    ReachesIn (n+1) r₁ r₃ :=  ReachesIn.step h₁ (reaches₁_iff_reachesIn_one.mpr h₂)


theorem reachesIn_one : ReachesIn 1 r₁ r₂ ↔ r₂ ∈ step r₁ := by
  rw [←reaches₁_iff_reachesIn_one,Reaches₁]

theorem reachesIn_iff_split_last {n : ℕ} :
    (∃ c : conf pda, ReachesIn n r₁ c ∧ ReachesIn 1 c r₂) ↔ ReachesIn (n+1) r₁ r₂ := by
  constructor
  · intro ⟨c,h⟩
    exact reachesIn_of_n_one h.1 h.2
  · intro h
    rcases h with _ | @⟨n,_,c,_,h₀,h₁⟩
    use c
    exact ⟨h₀,reaches₁_iff_reachesIn_one.mp h₁⟩


theorem reachesIn_of_one_n {r₃ : conf pda} {n : ℕ} (h₁ : ReachesIn 1 r₁ r₂) (h₂ : ReachesIn n r₂ r₃) :
    ReachesIn (n+1) r₁ r₃ := by
  induction' n with n ih generalizing r₃
  · obtain ⟨rfl⟩ := reachesIn_zero h₂
    simp_all
  · obtain ⟨c,hc₁,hc₂⟩ := reachesIn_iff_split_last.mpr h₂
    apply ReachesIn.step
    exact ih hc₁
    exact reaches₁_iff_reachesIn_one.mpr hc₂

theorem reachesIn_iff_split_first {n : ℕ}:
    (∃ c : conf pda, ReachesIn 1 r₁ c ∧ ReachesIn n c r₂) ↔ ReachesIn (n+1) r₁ r₂ := by
  constructor
  · intro ⟨c,h₁,h₂⟩
    exact reachesIn_of_one_n h₁ h₂
  · intro h
    induction' n with n ih generalizing r₂
    · use r₂
    · rcases h with _|@⟨_,_,r₂',_,h₁,h₂⟩
      obtain ⟨c,hc₁,hc₂⟩ := ih h₁
      refine ⟨c,hc₁,?_⟩
      apply reachesIn_of_n_one
      exact hc₂
      exact reaches₁_iff_reachesIn_one.mp h₂


theorem ReachesIn.trans {r₃ : conf pda} {n m : ℕ} (h₁ : ReachesIn n r₁ r₂) (h₂ : ReachesIn m r₂ r₃) :
    ∃ k ≤ n+m, ReachesIn k r₁ r₃ := by
  induction' m with m ih generalizing r₃
  · use n
    apply reachesIn_zero at h₂
    simp_all
  · obtain ⟨c,hc₁,hc₂⟩:= reachesIn_iff_split_last.mpr h₂
    obtain ⟨k,ih⟩ := ih hc₁
    use k+1
    exact ⟨by linarith [ih.1],reachesIn_iff_split_last.mp ⟨c, ih.2, hc₂⟩⟩

theorem reaches_iff_reachesIn : Reaches r₁ r₂ ↔ ∃ n : ℕ, ReachesIn n r₁ r₂ := by
  constructor
  · intro h
    induction h with
    | refl => use 0
    | @tail c r₂ h₁ h₂ ih =>
      obtain ⟨n,hn⟩ := ih
      use n+1
      rw [←reachesIn_iff_split_last]
      exact ⟨c, hn, reaches₁_iff_reachesIn_one.mp h₂⟩
  · intro ⟨n,hn⟩
    induction' n with n ih generalizing r₂
    · apply reachesIn_zero at hn
      rw [hn]
    · obtain ⟨c,hc₁,hc₂⟩ :=  reachesIn_iff_split_last.mpr hn
      rw [←reaches₁_iff_reachesIn_one] at hc₂
      exact Relation.ReflTransGen.tail (ih hc₁) hc₂

theorem Reaches.trans {r₃ : conf pda} (h₁ : Reaches r₁ r₂) (h₂ : Reaches r₂ r₃) :
    Reaches r₁ r₃ := Relation.ReflTransGen.trans h₁ h₂


theorem decreasing_input_one' (h : ReachesIn 1 r₁ r₂) :
    ∃ w : List T, r₁.input = w ++ r₂.input := by
  apply reachesIn_one.mp at h           -- Apply characterization of ReachesIn 1
  rcases r₁ with ⟨q, w,  _ | ⟨Z, β⟩⟩      -- To simplify step we have to split cases
  · simp [step] at h                    -- If the stack is empty no computation can happen
  · rcases w with  _ | ⟨a, w⟩            -- Again case split if a read is possilbe
    · dsimp [step] at h
      obtain ⟨_,_,h⟩ := h                -- If tape is empty no read can happen
      use []
      simp [h.2]                        -- Closes the goal
    · dsimp [step] at h
      rw [Set.mem_union] at h           -- Convert membership of union to or
      rcases h with h|h                 -- Split cases on wether a read is happening
      · rw [Set.mem_setOf] at h         -- Convert membeship of set builder to predicate
        obtain ⟨p,β,h⟩ := h              -- We know that a is beeing read
        use [a]
        simp [h.2]                      -- Closes the goal
      · obtain ⟨_,_,h⟩ := h              -- No read is happening, so as before
        use []
        simp [h.2]

theorem decreasing_input_one (h : ReachesIn 1 r₁ r₂) :
    ∃ w : List T, r₁.input = w ++ r₂.input := by
  apply reachesIn_one.mp at h
  rcases r₁ with ⟨q,_|⟨a,w⟩,_|⟨Z,β⟩⟩
  · simp [step] at h
  · obtain ⟨_,_,h⟩ := h
    use []
    simp [h.2]
  · simp [step] at h
  · rcases h with h|h
    · obtain ⟨p,β,h⟩ := h
      rw [h.2]
      use [a]
      simp
    · obtain ⟨p,β,h⟩ := h
      rw [h.2]
      simp

theorem decreasing_input (h : Reaches r₁ r₂) :
    ∃ w : List T, r₁.input = w ++ r₂.input := by
  rw [reaches_iff_reachesIn] at h
  obtain ⟨n,h'⟩ := h
  induction' n with n ih generalizing r₂
  · apply reachesIn_zero at h'
    use []
    simp_all
  · apply reachesIn_iff_split_last.mpr at h'
    obtain ⟨c,h',h''⟩ := h'
    apply ih at h'
    apply decreasing_input_one at h''
    obtain ⟨w₁,hw₁⟩ :=  h'
    obtain ⟨w₂,hw₂⟩ :=  h''
    use w₁++w₂
    simp [hw₁,hw₂]

theorem unconsumed_input_one (x : List T) :
    ReachesIn 1 r₁ r₂ ↔ ReachesIn 1 (r₁.appendInput x) (r₂.appendInput x) := by
  constructor
  · intro h
    rcases r₂ with ⟨p,v,α⟩
    rcases r₁ with ⟨q,_|⟨a,w⟩,_|⟨Z,β⟩⟩ <;>
    simp [reachesIn_one,step,conf.appendInput] at *
    · rcases x with _|⟨a,w⟩ <;> simp_all
    · rw [←List.cons_append]
      rw [List.append_left_inj]
      exact h
  · intro h
    rcases r₂ with ⟨p,v,α⟩
    rcases r₁ with ⟨q,_|⟨a,w⟩,_|⟨Z,β⟩⟩ <;>
    simp [reachesIn_one,step,conf.appendInput] at *
    · rcases x with _|⟨a,w⟩
      · simp at h; assumption
      · simp at h
        rcases h with h|h
        · obtain ⟨p,β,h⟩ := h
          have : (v ++ a :: w).length = w.length := by rw [h.1]
          rw [List.length_append,List.length_cons] at this
          linarith
        · assumption
    · rwa [←List.cons_append, List.append_left_inj] at h

theorem unconsumed_input_N {n : ℕ} (x : List T) :
    ReachesIn n r₁ r₂ ↔ ReachesIn n (r₁.appendInput x) (r₂.appendInput x) := by
  constructor
  · induction' n with n ih generalizing r₁ r₂
    case zero =>
      intro h
      apply reachesIn_zero at h
      rw [h]
    case succ =>
      intro h
      apply reachesIn_iff_split_last.mpr at h
      obtain ⟨c,h'⟩ := h
      have : ReachesIn n (r₁.appendInput x) (c.appendInput x) := ih h'.1
      apply And.right at h'
      rw [unconsumed_input_one x] at h'
      rw [←reachesIn_iff_split_last]
      use c.appendInput x
  · induction' n with n ih generalizing r₁ r₂
    · intro h
      apply reachesIn_zero at h
      simp only [conf.appendInput,conf.mk.injEq] at h
      obtain rfl : r₁ = r₂ := by ext <;> simp_all
      rfl
    · intro h
      rw [←reachesIn_iff_split_last] at *
      obtain ⟨c,h⟩ := h
      have := decreasing_input_one h.2
      obtain ⟨w,h'⟩ := this
      set c' : conf pda := ⟨c.state,w++r₂.input,c.stack⟩ with def_c'
      have : c'.appendInput x = c := by
        rcases c with ⟨q,l,β⟩
        simp [def_c',h',conf.appendInput,conf] at *
        exact h'.symm
      rw [←this] at h
      use c'
      constructor
      · apply ih
        exact h.1
      · apply (unconsumed_input_one x).mpr
        exact h.2

theorem unconsumed_input (x : List T) :
    Reaches r₁ r₂ ↔ Reaches (r₁.appendInput x) (r₂.appendInput x) := by
  rw [reaches_iff_reachesIn,reaches_iff_reachesIn]
  constructor <;> intro ⟨n,h'⟩ <;> use n
  · exact (unconsumed_input_N x).mp h'
  · exact (unconsumed_input_N x).mpr h'


theorem reachesIn_pos_of_not_self {n : ℕ} (h : r₁ ≠ r₂) :
    ReachesIn n r₁ r₂ → n > 0 := by
  rcases n with _ | ⟨n⟩
  · intro h
    apply reachesIn_zero at h
    contradiction
  · intro _
    apply Nat.zero_lt_succ

theorem reachesIn_one_on_empty_stack {q p: Q}{w w': List T}{α : List S}:
    ¬pda.ReachesIn 1 ⟨q, w, []⟩ ⟨p, w', α⟩ := by
  intro h
  rw [reachesIn_one] at h
  simp [step] at h

theorem reaches_on_empty_stack {q p: Q}{w w': List T}{α : List S}:
    pda.Reaches ⟨q, w, []⟩ ⟨p, w', α⟩ → w=w' ∧ α = [] ∧ q = p := by
  intro h
  rw [reaches_iff_reachesIn] at h
  obtain ⟨n,hr⟩ := h
  induction' n with n ih
  · apply reachesIn_zero at hr
    rw [conf.mk.injEq] at hr
    simp [hr]
  · rw [←reachesIn_iff_split_first] at hr
    obtain ⟨⟨q',v,α'⟩,h₁,h₂⟩ := hr
    apply reachesIn_one_on_empty_stack at h₁
    contradiction

theorem reaches_of_reachesIn  {n: ℕ}(h: pda.ReachesIn n r₁ r₂) : pda.Reaches r₁ r₂ :=
  reaches_iff_reachesIn.mpr ⟨n, h⟩

theorem reaches₁_push {q : Q}{x : List T}{Z : S}{γ : List S}{c : pda.conf}
    (h : pda.Reaches₁ ⟨q, x, Z::γ⟩ c) :
    (∃(a : T)(y : List T)(p : Q)(α : List S), x = a::y ∧ c = ⟨p, y, α ++ γ⟩ ∧
    (p, α) ∈ pda.transition_fun q a Z) ∨
    (∃(p : Q)(α : List S), c = ⟨p, x, α ++ γ⟩ ∧  (p, α) ∈ pda.transition_fun' q Z) := by
  rcases x with _ | ⟨a, y⟩
  · right
    simp only [Reaches₁, step] at h
    obtain ⟨p, β, _, h⟩ := Set.mem_setOf.mp h
    use p, β
  · simp only [Reaches₁, step] at h
    rw [Set.mem_union] at h
    rcases h with h|h
    · obtain ⟨p, β, _, h⟩ := Set.mem_setOf.mp h
      left
      use a, y, p, β
    · obtain ⟨p, β, _, h⟩ := Set.mem_setOf.mp h
      right
      use p, β


theorem split_stack {n : ℕ}{q p : Q}{x : List T}{α β : List S}
    (h : pda.ReachesIn n ⟨q, x, α ++ β⟩ ⟨p, [], []⟩):
    ∃(q₁ : Q)(m₁ m₂ : ℕ)(y₁ y₂ : List T), x=y₁++y₂ ∧ m₁ ≤ n ∧ m₂ ≤ n ∧
    pda.ReachesIn m₁ ⟨q, y₁, α⟩ ⟨q₁, [], []⟩ ∧ pda.ReachesIn m₂ ⟨q₁, y₂, β⟩ ⟨p, [], []⟩ := by
  induction' n with n ih generalizing q x α β
  · apply reachesIn_zero at h
    obtain ⟨rfl, rfl, h'⟩ := conf.mk.inj h
    obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.mp h'
    use q, 0, 0, [], []
    simp [ReachesIn.refl]
  · rcases α with _ | ⟨Z, α'⟩
    · use q, 0, n+1, [], x
      simpa [ReachesIn.refl] using h
    · rw [List.cons_append] at h
      rw [←reachesIn_iff_split_first] at h
      obtain ⟨c, hc₁, hc₂⟩ := h
      rw [←reaches₁_iff_reachesIn_one] at hc₁
      obtain ⟨a, y, p, γ, hx, rfl, ht⟩ | ⟨p, γ, rfl, ht⟩ := reaches₁_push hc₁
      · rw [←List.append_assoc] at hc₂
        obtain ⟨q₁, m₁, m₂, y₁, y₂, hy, hm₁, hm₂, hr₁, hr₂⟩ := ih hc₂
        use q₁, m₁ + 1, m₂, a::y₁, y₂
        refine ⟨by simp [hy, hx], by linarith [hm₁], by linarith [hm₁], ?_, hr₂⟩
        rw [←reachesIn_iff_split_first]
        use ⟨p, y₁, γ ++ α'⟩
        simp [hr₁, reachesIn_one, step, ht]
      · rw [←List.append_assoc] at hc₂
        obtain ⟨q₁, m₁, m₂, y₁, y₂, hy, hm₁, hm₂, hr₁, hr₂⟩ := ih hc₂
        use q₁, m₁ + 1, m₂, y₁, y₂
        refine ⟨hy, by linarith  [hm₁], by linarith [hm₂], ?_, hr₂⟩
        rw [←reachesIn_iff_split_first]
        use ⟨p, y₁, γ ++ α'⟩
        cases y₁ <;>
        simp [hr₁, reachesIn_one, step, ht]

theorem Reaches₁.append_stack {x y : List T}{α β : List S}{q p : Q}(γ : List S)
    (h : pda.Reaches₁ ⟨q, x, α⟩ ⟨p, y, β⟩):
    pda.Reaches ⟨q, x, α ++ γ⟩ ⟨p, y, β ++ γ⟩ := by
  rw [Reaches₁] at *
  rw [reaches_iff_reachesIn]
  rcases α  with _ | ⟨Z, α'⟩
  · use 0
    obtain ⟨rfl, rfl, rfl⟩ : p = q ∧ y = x ∧ β = [] :=  by simpa [step] using h
    rfl
  · rcases x with _ | ⟨a, x'⟩
    · use 1
      rw [←reaches₁_iff_reachesIn_one, Reaches₁]
      simp only [step, Set.mem_setOf_eq, conf.mk.injEq, List.cons_append]  at *
      obtain ⟨p', β', h⟩ := h
      use p', β'
      use h.1, h.2.1, h.2.2.1
      simp [h]
    · use 1
      rw [←reaches₁_iff_reachesIn_one, Reaches₁]
      simp only [step, Set.mem_setOf_eq, conf.mk.injEq, List.cons_append, Set.mem_union]  at *
      rcases h with h|h
      case' h.inl => left
      case' h.inr => right
      all_goals obtain ⟨p', β', h⟩ := h <;>
      use p', β' <;>
      use h.1, h.2.1, h.2.2.1 <;>
      simp [h]

theorem Reaches.append_stack {x y : List T}{α β: List S}{q p : Q}
    (h : pda.Reaches ⟨q, x, α⟩ ⟨p, y, β⟩)(γ : List S):
    pda.Reaches ⟨q, x, α ++ γ⟩ ⟨p, y, β ++ γ⟩ := by
  rw [reaches_iff_reachesIn] at h
  obtain ⟨n, h⟩ := h
  induction' n with n ih generalizing q x α
  · obtain ⟨rfl, rfl, rfl⟩:= conf.mk.inj (reachesIn_zero h)
    rfl
  · rw [←reachesIn_iff_split_first] at h
    obtain ⟨⟨q₀, x', α'⟩, h₁, h₂⟩ := h
    have h₂ := ih h₂
    rw [←reaches₁_iff_reachesIn_one] at h₁
    have h₁ := h₁.append_stack γ
    exact Reaches.trans h₁ h₂

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

section SameTransitions

/-- Two PDAs with the same transition functions have the same single-step relation. -/
lemma reaches1_of_same_transitions (P₁ P₂ : PDA Q T S)
    (ht : P₁.transition_fun = P₂.transition_fun)
    (ht' : P₁.transition_fun' = P₂.transition_fun')
    (q q' : Q) (w w' : List T) (γ γ' : List S) :
    @PDA.Reaches₁ _ _ _ _ _ _ P₁ ⟨q, w, γ⟩ ⟨q', w', γ'⟩ ↔
    @PDA.Reaches₁ _ _ _ _ _ _ P₂ ⟨q, w, γ⟩ ⟨q', w', γ'⟩ := by
  unfold Reaches₁ step
  cases w with
  | nil =>
    cases γ with
    | nil => simp
    | cons Z α =>
      simp only [Set.mem_setOf_eq, conf.mk.injEq]
      constructor <;> intro ⟨p, β, h1, h2⟩
      · exact ⟨p, β, ht' ▸ h1, h2⟩
      · exact ⟨p, β, ht'.symm ▸ h1, h2⟩
  | cons a w =>
    cases γ with
    | nil => simp
    | cons Z α =>
      simp only [Set.mem_union, Set.mem_setOf_eq, conf.mk.injEq]
      constructor <;> intro h
      · rcases h with ⟨p, β, h1, h2⟩ | ⟨p, β, h1, h2⟩
        · left; exact ⟨p, β, ht ▸ h1, h2⟩
        · right; exact ⟨p, β, ht' ▸ h1, h2⟩
      · rcases h with ⟨p, β, h1, h2⟩ | ⟨p, β, h1, h2⟩
        · left; exact ⟨p, β, ht.symm ▸ h1, h2⟩
        · right; exact ⟨p, β, ht'.symm ▸ h1, h2⟩

/-- Two PDAs with the same transition functions have the same multi-step relation. -/
lemma reaches_of_same_transitions (P₁ P₂ : PDA Q T S)
    (ht : P₁.transition_fun = P₂.transition_fun)
    (ht' : P₁.transition_fun' = P₂.transition_fun')
    (c₁ c₂ : PDA.conf P₁)
    (h : @PDA.Reaches _ _ _ _ _ _ P₁ c₁ c₂) :
    @PDA.Reaches _ _ _ _ _ _ P₂
      ⟨c₁.state, c₁.input, c₁.stack⟩ ⟨c₂.state, c₂.input, c₂.stack⟩ := by
  induction h with
  | refl => exact Relation.ReflTransGen.refl
  | @tail c₂ c₃ _ h₂ ih =>
    exact ih.tail ((PDA.reaches1_of_same_transitions P₁ P₂ ht ht'
      c₂.state c₃.state c₂.input c₃.input c₂.stack c₃.stack).mp h₂)

end SameTransitions

variable {T : Type} [Fintype T]

def is_PDA_emptyStack (L : Language T) : Prop :=
  ∃ (Q S : Type) (_ : Fintype Q) (_ : Fintype S), ∃ M : PDA Q T S, M.acceptsByEmptyStack = L

/-- A language over a finite terminal alphabet is accepted by some PDA via empty-stack
acceptance. -/
alias is_PDA := is_PDA_emptyStack

@[simp]
theorem is_PDA_emptyStack_iff_is_PDA {L : Language T} :
    is_PDA_emptyStack L  ↔ is_PDA L := by
  rw [is_PDA]

/-- A language over a finite terminal alphabet is accepted by some PDA via final-state
acceptance. -/
def is_PDA_finalState (L : Language T) : Prop :=
  ∃ (Q S : Type) (_ : Fintype Q) (_ : Fintype S), ∃ M : PDA Q T S, M.acceptsByFinalState = L

/-- The class of languages recognized by PDAs via empty-stack acceptance. -/
def EmptyStackClass : Set (Language T) :=
  setOf is_PDA

/-- The class of PDA-recognizable languages.

This lives under `PDA.Class` because the top-level name `PDA` is already used by the
automaton structure. -/
alias Class := PDA.EmptyStackClass

/-- The class of languages recognized by PDAs via final-state acceptance. -/
def FinalStateClass : Set (Language T) :=
  setOf is_PDA_finalState
