/- 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