Corollaries.lean

import FPRDTransfer.Theorem16.Main
import FPRDTransfer.RealtimeTransfer

namespace FPRD
namespace Theorem16

/-- T89 composed with the generic sufficient direction. -/
theorem revRT_multitape_subset_PEG
    {Sym Q T : Type} {m : Nat}
    [DecidableEq Sym] [DecidableEq Q] [DecidableEq T]
    (fs : FiniteEnum Sym) (fq : FiniteEnum Q) (ft : FiniteEnum T)
    (machine : MultiTapeMachine Sym Q T m) :
    InPEG (fun word => machine.decides word.reverse = true) := by
  letI : FiniteEnum Sym := fs
  letI : FiniteEnum Q := fq
  letI : FiniteEnum T := ft
  have hcompiled := scaffold_to_peg
    (inferInstance : FiniteEnum Sym)
    (inferInstance : FiniteEnum (Q × (Fin m → T)))
    (inferInstance : FiniteEnum (Tuple (2 * m) T))
    (compile machine.toStack) (compile_distanceOk machine.toStack)
  have hlanguage :
      (fun word : List Sym =>
        (compile machine.toStack).decides word.reverse = true) =
      (fun word : List Sym => machine.decides word.reverse = true) := by
    funext word
    apply propext
    rw [MultiTapeMachine.realtime_transfer_decides]
  rw [← hlanguage]
  exact hcompiled

/-- Even-length palindromes over the binary alphabet. -/
def EPAL₂ (word : List Bool) : Prop :=
  word = word.reverse ∧ word.length % 2 = 0

theorem epal₂_reverse (word : List Bool) :
    EPAL₂ word.reverse ↔ EPAL₂ word := by
  simp [EPAL₂, eq_comm]

/-- If a strict real-time multitape recognizer for `EPAL₂` is supplied, the
checked T89 composition places `EPAL₂` in PEG.  This theorem introduces no
recognizer constant or extra assumption. -/
theorem epal₂_inPEG_of_multitape_recognizer
    {Q T : Type} {m : Nat}
    [DecidableEq Q] [DecidableEq T]
    (fq : FiniteEnum Q) (ft : FiniteEnum T)
    (machine : MultiTapeMachine Bool Q T m)
    (hmachine : ∀ word, machine.decides word = true ↔ EPAL₂ word) :
    InPEG EPAL₂ := by
  have hreverse := revRT_multitape_subset_PEG
    (inferInstance : FiniteEnum Bool) fq ft machine
  have hlanguage :
      (fun word => machine.decides word.reverse = true) = EPAL₂ := by
    funext word
    apply propext
    exact (hmachine word.reverse).trans (epal₂_reverse word)
  rw [← hlanguage]
  exact hreverse

end Theorem16
end FPRD