module

public import Langlib.Automata.Turing.Definition
public import Langlib.Classes.RecursivelyEnumerable.Definition
import Langlib.Automata.Turing.Equivalence.GrammarToTM
import Langlib.Automata.Turing.Equivalence.TMToGrammar
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.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



/-! # Turing-Recognizable Languages Are Exactly RE Languages

This module packages the two existing directions:

* `re_implies_tm`: unrestricted grammars are TM-recognizable.
* `TM_subset_RE`: TM-recognizable languages are generated by unrestricted grammars.

## Key results

- `TM_eq_RE`: equality of TM-recognizable and recursively enumerable languages.
- `is_TM_iff_is_RE`: pointwise membership equivalence.
-/

/-- The class of TM-recognizable languages is exactly the class of recursively
enumerable languages. -/
public theorem TM_eq_RE {T : Type} [DecidableEq T] [Fintype T] :
    (TM : Set (Language T)) = RE := by
  exact Set.Subset.antisymm TM_subset_RE RE_subset_TM

/-- Pointwise version of `TM_eq_RE`. -/
public theorem is_TM_iff_is_RE
    {T : Type} [DecidableEq T] [Fintype T]
    (L : Language T) :
    is_TM L ↔ is_RE L := by
  change L ∈ (TM : Set (Language T)) ↔ L ∈ RE
  rw [TM_eq_RE]