module

public import Langlib.Automata.LinearBounded.Definition
public import Langlib.Automata.LinearBounded.Equivalence.EndmarkerTape
import Mathlib.Algebra.Order.Floor.Extended
import Mathlib.Algebra.Order.Floor.Semifield
import Mathlib.Algebra.Order.Interval.Basic
import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
import Mathlib.Analysis.SpecialFunctions.Bernstein
import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
import Mathlib.CategoryTheory.Category.Init
import Mathlib.Combinatorics.Enumerative.DyckWord
import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
import Mathlib.Data.NNRat.Floor
import Mathlib.Data.Nat.Factorial.DoubleFactorial
import Mathlib.Geometry.Euclidean.Altitude
import Mathlib.NumberTheory.Height.Basic
import Mathlib.NumberTheory.LucasLehmer
import Mathlib.NumberTheory.SelbergSieve
import Mathlib.Tactic.Cases
import Mathlib.Tactic.ENatToNat
import Mathlib.Tactic.NormNum.BigOperators
import Mathlib.Tactic.NormNum.Irrational
import Mathlib.Tactic.NormNum.IsCoprime
import Mathlib.Tactic.NormNum.IsSquare
import Mathlib.Tactic.NormNum.LegendreSymbol
import Mathlib.Tactic.NormNum.ModEq
import Mathlib.Tactic.NormNum.NatFactorial
import Mathlib.Tactic.NormNum.NatFib
import Mathlib.Tactic.NormNum.NatLog
import Mathlib.Tactic.NormNum.NatSqrt
import Mathlib.Tactic.NormNum.Ordinal
import Mathlib.Tactic.NormNum.Parity
import Mathlib.Tactic.NormNum.Prime
import Mathlib.Tactic.NormNum.RealSqrt
import Mathlib.Topology.Sheaves.Init
@[expose]
public section



/-!
# Deterministic LBA Languages ⊆ LBA Languages

We show that every language recognized by a deterministic linearly bounded automaton (DLBA)
is also recognized by a nondeterministic linearly bounded automaton (LBA).

## Strategy

The conversion uses `Option Λ` as the LBA state space:
- `some q` simulates LBA state `q` (always non-accepting in the NLBA)
- `none` is a special accepting halt state

When the DLBA halts (`transition` returns `none`) in an accepting state, the LBA
transitions to `none`. This ensures the LBA accepts (reaches an accepting state)
if and only if the DLBA accepts (halts in an accepting state).

## Main Results

* `is_DLBA_subset_is_LBA` — Every DLBA language is an (endmarker) LBA language
-/

namespace DLBA

open LBA

/-! ### Conversion from DLBA to LBA -/

/-- Convert a deterministic DLBA to an LBA using `Option Λ` states.
- `some q` simulates DLBA state `q` (non-accepting)
- `none` is the accepting halt state
When the DLBA halts in an accepting state, we transition to `none`. -/
def toLBA' {Γ : Type*} {Λ : Type*} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) : LBA.Machine Γ (Option Λ) where
  transition := fun q a =>
    match q with
    | none => ∅
    | some q =>
      match M.transition q a with
      | some (q', a', d) => {(some q', a', d)}
      | none => if M.accept q then {(none, a, DLBA.Dir.stay)} else ∅
  accept := fun q =>
    match q with
    | none => true
    | some _ => false
  initial := some M.initial

/-! ### Step Correspondence -/

/-
If the DLBA takes a step from state q, the converted LBA takes the corresponding step.
-/
theorem dlba_step_implies_lba_step {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (cfg : Cfg Γ Λ n) (cfg' : Cfg Γ Λ n)
    (h : DLBA.step M cfg = some cfg') :
    LBA.Step (toLBA' M)
      ⟨some cfg.state, cfg.tape⟩
      ⟨some cfg'.state, cfg'.tape⟩ := by
  unfold step at h;
  rcases h' : M.transition cfg.state cfg.tape.read with ( _ | ⟨ q', a, d ⟩ ) <;> simp_all +decide;
  exact ⟨ q', a, d, by unfold toLBA'; aesop ⟩

/-
If the DLBA halts in an accepting state, the LBA can transition to the accepting
halt state `none`.
-/
theorem dlba_halt_accept_implies_lba_step {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (cfg : Cfg Γ Λ n)
    (h_halt : DLBA.step M cfg = none)
    (h_acc : M.accept cfg.state = true) :
    LBA.Step (toLBA' M)
      ⟨some cfg.state, cfg.tape⟩
      ⟨none, cfg.tape⟩ := by
  use none, cfg.tape.read, DLBA.Dir.stay;
  simp_all +decide [ BoundedTape.write, BoundedTape.moveHead ];
  unfold toLBA';
  unfold step at h_halt; aesop;

/-! ### Multi-step Correspondence -/

/-- Lift a single DLBA configuration to the LBA state space. -/
def liftCfg {Γ : Type*} {Λ : Type*} {n : ℕ}
    (cfg : Cfg Γ Λ n) : DLBA.Cfg Γ (Option Λ) n :=
  ⟨some cfg.state, cfg.tape⟩

/-
If `iterateStep M cfg k = some cfg'`, then the converted LBA can reach
`liftCfg cfg'` from `liftCfg cfg`.
-/
theorem iterateStep_implies_lba_reaches {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (cfg cfg' : Cfg Γ Λ n) {k : ℕ}
    (hk : iterateStep M cfg k = some cfg') :
    LBA.Reaches (toLBA' M) (liftCfg cfg) (liftCfg cfg') := by
  induction' k with k ih generalizing cfg cfg';
  · cases cfg' ; cases cfg ; cases hk ; tauto;
  · obtain ⟨cfg'', hk''⟩ : ∃ cfg'', iterateStep M cfg k = some cfg'' ∧ DLBA.step M cfg'' = some cfg' := by
      exact Option.bind_eq_some_iff.mp hk;
    exact Relation.ReflTransGen.trans ( ih cfg cfg'' hk''.1 ) ( Relation.ReflTransGen.single ( dlba_step_implies_lba_step M cfg'' cfg' hk''.2 ) )

/-! ### Acceptance Correspondence -/

/-
If the deterministic DLBA accepts, the converted LBA also accepts (from the
lifted initial configuration).
-/
theorem dlba_accepts_implies_lba_accepts' {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (cfg : Cfg Γ Λ n)
    (h : DLBA.Accepts M cfg) :
    LBA.Accepts (toLBA' M) (liftCfg cfg) := by
  obtain ⟨ k, hk₁, cfg', hk₂, hk₃ ⟩ := h;
  -- Use `dlba_halt_accept_implies_lba_step` to get the step from `liftCfg cfg'` to `⟨none, cfg'.tape⟩`.
  have h_step : LBA.Step (toLBA' M) ⟨some cfg'.state, cfg'.tape⟩ ⟨none, cfg'.tape⟩ := by
    apply dlba_halt_accept_implies_lba_step;
    · rw [ iterateStep_succ, hk₂ ] at hk₁ ; aesop;
    · exact hk₃;
  refine' ⟨ _, _, _ ⟩;
  exact ⟨ none, cfg'.tape ⟩;
  · exact Relation.ReflTransGen.tail ( iterateStep_implies_lba_reaches M cfg cfg' hk₂ ) h_step;
  · rfl

/-
Conversely, if the converted LBA accepts from a lifted configuration, then the
original DLBA also accepts.

For a step from `some q` in the converted LBA, the result is either `some q'`
(simulating a DLBA step) or `none` (DLBA halts in accepting state).
-/
theorem toLBA'_step_cases {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (q : Λ) (tape : BoundedTape Γ n)
    (cfg' : Cfg Γ (Option Λ) n)
    (h : LBA.Step (toLBA' M) ⟨some q, tape⟩ cfg') :
    (∃ q' tape', cfg' = ⟨some q', tape'⟩ ∧ DLBA.step M ⟨q, tape⟩ = some ⟨q', tape'⟩) ∨
    (cfg' = ⟨none, tape⟩ ∧ DLBA.step M ⟨q, tape⟩ = none ∧ M.accept q = true) := by
  cases cfg' ; simp_all +decide [ Step ];
  rcases h with ⟨ a, d, h, rfl ⟩;
  unfold toLBA' at h;
  unfold step; simp +decide;
  cases h' : M.transition q ( tape.contents tape.head ) <;> simp +decide [ h' ] at h ⊢;
  · unfold BoundedTape.write BoundedTape.moveHead; aesop;
  · grind +splitImp

/-
If the converted LBA reaches a configuration from `liftCfg cfg`, then either
the state is `some q` with a corresponding DLBA iterateStep, or the DLBA accepts.
-/
theorem toLBA'_reaches_inv {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (cfg : Cfg Γ Λ n)
    (cfg' : Cfg Γ (Option Λ) n)
    (h : LBA.Reaches (toLBA' M) (liftCfg cfg) cfg') :
    (∃ cfg_lba : Cfg Γ Λ n, cfg'.state = some cfg_lba.state ∧ cfg'.tape = cfg_lba.tape ∧
      ∃ k, iterateStep M cfg k = some cfg_lba) ∨
    (cfg'.state = none ∧ DLBA.Accepts M cfg) := by
  induction' h with cfg'' cfg''' h;
  · exact Or.inl ⟨ cfg, rfl, rfl, 0, rfl ⟩;
  · rename_i h₁ h₂;
    rcases h₂ with ( ⟨ cfg_lba, h₂, h₃, k, hk ⟩ | ⟨ h₂, h₃ ⟩ ) <;> simp_all +decide [ Step ];
    · rcases h₁ with ⟨ q', a, d, h₁, rfl ⟩;
      unfold toLBA' at h₁; simp_all +decide;
      rcases h : M.transition cfg_lba.state ( cfg_lba.tape.contents cfg_lba.tape.head ) with ( _ | ⟨ q', a', d' ⟩ ) <;> simp_all +decide;
      · use k;
        simp_all +decide [ iterateStep_succ ];
        unfold step; aesop;
      · refine' ⟨ ⟨ q', ( cfg_lba.tape.write a' ).moveHead d' ⟩, _, _, k + 1, _ ⟩ <;> simp_all +decide [ iterateStep_succ ];
        unfold step; aesop;
    · unfold toLBA' at h₁; aesop;

theorem lba_accepts_implies_dlba_accepts' {Γ : Type*} {Λ : Type*} {n : ℕ} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (cfg : Cfg Γ Λ n)
    (h : LBA.Accepts (toLBA' M) (liftCfg cfg)) :
    DLBA.Accepts M cfg := by
  obtain ⟨ cfg', hcfg', hcfg'' ⟩ := h;
  obtain ⟨ cfg_lba, hcfg_lba₁, hcfg_lba₂, k, hk ⟩ | hcfg_lba₃ := toLBA'_reaches_inv M cfg cfg' hcfg';
  · unfold toLBA' at hcfg''; aesop;
  · exact hcfg_lba₃.2

/-! ### Language Definitions For DLBAs -/

/-- Load a non-empty list onto a bounded tape for a deterministic DLBA. -/
noncomputable def loadListDLBA {Γ : Type*} (w : List Γ) (hw : w ≠ []) :
    BoundedTape Γ (w.length - 1) :=
  ⟨fun i => w.get ⟨i.val, by have := i.isLt; have := List.length_pos_of_ne_nil hw; omega⟩,
   ⟨0, by have := List.length_pos_of_ne_nil hw; omega⟩⟩

/-- Initial configuration for a non-empty list input on a deterministic DLBA. -/
noncomputable def initCfgListDLBA {Γ : Type*} {Λ : Type*}
    (M : DLBA.Machine Γ Λ) (w : List Γ) (hw : w ≠ []) :
    Cfg Γ Λ (w.length - 1) :=
  ⟨M.initial, loadListDLBA w hw⟩

/-- Recognition via an embedding from the input alphabet into the tape alphabet,
for a deterministic DLBA. -/
noncomputable def LanguageViaEmbedDLBA {T Γ : Type*} {Λ : Type*}
    (M : DLBA.Machine Γ Λ) (embed : T → Γ) : _root_.Language T :=
  fun w => ∃ (hw : w.map embed ≠ []),
    DLBA.Accepts M (initCfgListDLBA M (w.map embed) hw)

/-! ### Initial Configuration Correspondence -/

/-
The lifted DLBA initial configuration equals the LBA initial configuration.
-/
theorem initCfg_lift_eq {Γ : Type*} {Λ : Type*} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (w : List Γ) (hw : w ≠ []) :
    liftCfg (initCfgListDLBA M w hw) =
    LBA.initCfgList (toLBA' M) w hw := by
  rfl

end DLBA

/-! ### Main Theorem -/

/-
The language via embedding for the DLBA equals that of the converted LBA.
-/
theorem dlba_language_eq_lba_language {T Γ : Type*} {Λ : Type*} [DecidableEq Γ]
    (M : DLBA.Machine Γ Λ) (embed : T → Γ) :
    DLBA.LanguageViaEmbedDLBA M embed = LBA.LanguageViaEmbed (DLBA.toLBA' M) embed := by
  funext w
  simp [DLBA.LanguageViaEmbedDLBA, LBA.LanguageViaEmbed];
  grind +suggestions

/-
**Main theorem**: Every deterministic LBA language is also an LBA language.
-/
theorem is_DLBA_subset_is_LBA {T : Type} [Fintype T] [DecidableEq T] {L : _root_.Language T}
    (h : is_DLBA L) : is_LBA L := by
  obtain ⟨ Γ, Λ, hΓ, hΛ, hdecΓ, hdecΛ, acceptEmpty, M, hM ⟩ := h
  haveI := hΓ; haveI := hΛ; haveI := hdecΓ; haveI := hdecΛ
  -- Convert the DLBA to a bounded-tape LBA `toLBA' M`, then run it on `⊢ w ⊣` via `simMachine`,
  -- carrying the DLBA's empty-word decision into the simulator's `ε`-bit.
  refine ⟨ Γ, LBA.SimState (Option Λ), hΓ, inferInstance, hdecΓ, inferInstance,
    LBA.simMachine (DLBA.toLBA' M) acceptEmpty, ?_ ⟩
  rw [LBA.language_simMachine_eq, ← hM]
  have key : DLBA.LanguageViaEmbed M (fun t => some (Sum.inl t))
      = LBA.LanguageViaEmbed (DLBA.toLBA' M) (fun t => some (Sum.inl t)) :=
    dlba_language_eq_lba_language M (fun t => some (Sum.inl t))
  funext w
  simp only [DLBA.LanguageRecognized, LBA.LanguageRecognized, key]

theorem DLBA_subset_LBA {T : Type} [Fintype T] [DecidableEq T] :
    (DLBA : Set (Language T)) ⊆ LBA := by
  intro L hL
  simp [DLBA] at hL
  exact is_DLBA_subset_is_LBA hL
