PEGCorollary.lean

import FPRDTransfer.Theorem16.Corollaries
import FrontierDerivative.RootSharingMachine

/-!
# PEG corollaries for source-selecting stack machines

This module composes the existing T101 compiler with the sufficient direction
of LMR Theorem 16. It does not construct a machine recognizing `EPAL₂`.
-/

namespace FrontierDerivative.RootSharingMachine

open FPRD
open RootSharing

universe u

/-- The T101 cell carrier is finite whenever its symbol carrier is finite. -/
def cellFiniteEquiv {A : Type u} {s : Nat} :
    FiniteEquiv (A × Fin s) (Cell s A) where
  toFun value := ⟨value.1, value.2⟩
  invFun cell := (cell.symbol, cell.next)
  left_inv value := by cases value; rfl
  right_inv cell := by cases cell; rfl

/-- T101 composed with the generic sufficient direction. -/
theorem revRootSharing_subset_PEG
    {Sym Q : Type} {A : Type u} {s : Nat}
    [DecidableEq Sym] [DecidableEq Q] [DecidableEq A]
    (fs : FiniteEnum Sym) (fq : FiniteEnum Q) (fa : FiniteEnum A)
    (machine : Machine Sym Q A s) :
    InPEG (fun word => machine.decides word.reverse = true) := by
  letI : FiniteEnum Sym := fs
  letI : FiniteEnum Q := fq
  letI : FiniteEnum A := fa
  letI : FiniteEnum (Cell s A) := FiniteEnum.ofEquiv
    (inferInstance : FiniteEnum (A × Fin s)) cellFiniteEquiv
  have hcompiled := Theorem16.scaffold_to_peg
    (inferInstance : FiniteEnum Sym)
    (inferInstance : FiniteEnum Q)
    (inferInstance : FiniteEnum (RootLabel s A))
    (compile machine) (compile_distanceOk machine)
  have hlanguage :
      (fun word : List Sym =>
        (compile machine).decides word.reverse = true) =
      (fun word : List Sym => machine.decides word.reverse = true) := by
    funext word
    apply propext
    rw [compile_decides]
  rw [← hlanguage]
  exact hcompiled

/-- A supplied T101 recognizer for `EPAL₂` yields the corresponding PEG
membership theorem without introducing a recognizer witness. -/
theorem epal₂_inPEG_of_rootSharing_recognizer
    {Q : Type} {A : Type u} {s : Nat}
    [DecidableEq Q] [DecidableEq A]
    (fq : FiniteEnum Q) (fa : FiniteEnum A)
    (machine : Machine Bool Q A s)
    (hmachine : ∀ word, machine.decides word = true ↔ Theorem16.EPAL₂ word) :
    InPEG Theorem16.EPAL₂ := by
  have hreverse := revRootSharing_subset_PEG
    (inferInstance : FiniteEnum Bool) fq fa machine
  have hlanguage :
      (fun word => machine.decides word.reverse = true) = Theorem16.EPAL₂ := by
    funext word
    apply propext
    exact (hmachine word.reverse).trans (Theorem16.epal₂_reverse word)
  rw [← hlanguage]
  exact hreverse

end FrontierDerivative.RootSharingMachine