Main.lean

import FPRDTransfer.Theorem16.Invariants.Neighbourhood

namespace FPRD
namespace Theorem16

universe u uName uSymbol uItem

/-- An expression either completes the whole input under `condition` or
returns PEG failure under its negation. -/
structure ExactComplete {Name : Type uName} {Symbol : Type uSymbol}
    (G : Grammar Name Symbol) (expression : Expr Name Symbol)
    (input : List Symbol) (condition : Prop) : Prop where
  ok_iff : Eval G expression input (.ok []) ↔ condition
  err_iff : Eval G expression input .err ↔ ¬condition

theorem exactComplete_of_cases {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol} {expression : Expr Name Symbol}
    {input : List Symbol} {condition : Prop}
    (hok : condition → Eval G expression input (.ok []))
    (herr : ¬condition → Eval G expression input .err) :
    ExactComplete G expression input condition := by
  classical
  refine ⟨?_, ?_⟩
  · constructor
    · intro heval
      by_cases hcondition : condition
      · exact hcondition
      · have himpossible := eval_deterministic heval (herr hcondition)
        cases himpossible
    · exact hok
  · constructor
    · intro heval hcondition
      have himpossible := eval_deterministic heval (hok hcondition)
      cases himpossible
    · exact herr

theorem altAll_map_complete {Name : Type uName} {Symbol : Type uSymbol}
    {Item : Type uItem} {G : Grammar Name Symbol} (items : List Item)
    (expression : Item → Expr Name Symbol) (input : List Symbol)
    (predicate : Item → Prop)
    (hall : ∀ item, item ∈ items →
      ExactComplete G (expression item) input (predicate item)) :
    ExactComplete G (Expr.altAll (items.map expression)) input
      (∃ item, item ∈ items ∧ predicate item) := by
  induction items with
  | nil =>
      apply exactComplete_of_cases
      · simp
      · intro _
        exact Eval.fail
  | cons item items ih =>
      change ExactComplete G
        (.alt (expression item) (Expr.altAll (items.map expression))) input _
      have hhead := hall item (by simp)
      have htail := ih (fun other hother => hall other (by simp [hother]))
      apply exactComplete_of_cases
      · rintro ⟨chosen, hchosen, hpredicate⟩
        by_cases hfirst : predicate item
        · exact Eval.altOk (hhead.ok_iff.mpr hfirst)
        · have hrest : ∃ other, other ∈ items ∧ predicate other := by
            rcases List.mem_cons.mp hchosen with rfl | hchosen
            · exact (hfirst hpredicate).elim
            · exact ⟨chosen, hchosen, hpredicate⟩
          exact Eval.altErr (hhead.err_iff.mpr hfirst)
            (htail.ok_iff.mpr hrest)
      · intro hnone
        apply Eval.altErr
        · apply hhead.err_iff.mpr
          intro hfirst
          exact hnone ⟨item, by simp, hfirst⟩
        · apply htail.err_iff.mpr
          rintro ⟨other, hother, hpredicate⟩
          exact hnone ⟨other, by simp [hother], hpredicate⟩

variable {Sym Q : Type} {Gamma : Type u} {d k : Nat}
variable [FiniteEnum Sym] [DecidableEq Sym]
variable [FiniteEnum Q] [DecidableEq Q]
variable [FiniteEnum Gamma] [DecidableEq Gamma]

def acceptingControls (A : Automaton Sym Q Gamma d k) : List Q :=
  (FiniteEnum.elems (α := Q)).filter fun control => A.accept control = true

theorem acceptAlternative_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (control : Q) :
    ExactComplete (rawGrammar A hdistance)
      (.seq (.nonterm (.state control)) (.nonterm .anyStar)) word.reverse
      ((A.run word).1 = control) := by
  have hinvariants := prefix_exact A hdistance word
  have hstate : StateExact A hdistance word control := by
    simpa using hinvariants.state control
  apply exactComplete_of_cases
  · intro hcontrol
    exact Eval.seqOk (hstate.ok_iff.mpr hcontrol)
      (anyStar_ok (rawGrammar A hdistance) NT.anyStar rfl word.reverse)
  · intro hcontrol
    exact Eval.seqErr (hstate.err_iff.mpr hcontrol)

theorem accepts_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) :
    ExactComplete (rawGrammar A hdistance) (.nonterm .accepts) word.reverse
      (A.decides word = true) := by
  have halternatives := altAll_map_complete (acceptingControls A)
    (fun control => Expr.seq (.nonterm (NT.state control)) (.nonterm .anyStar))
    word.reverse (fun control => (A.run word).1 = control)
    (fun control _ => acceptAlternative_exact A hdistance word control)
  have hcondition :
      (∃ control, control ∈ acceptingControls A ∧ (A.run word).1 = control) ↔
      A.decides word = true := by
    constructor
    · rintro ⟨control, hcontrol, hfinal⟩
      unfold acceptingControls at hcontrol
      simp only [List.mem_filter] at hcontrol
      rw [Automaton.decides, hfinal]
      exact of_decide_eq_true hcontrol.2
    · intro haccept
      refine ⟨(A.run word).1, ?_, rfl⟩
      unfold acceptingControls
      simp only [List.mem_filter]
      exact ⟨FiniteEnum.complete _, decide_eq_true (by
        simpa [Automaton.decides] using haccept)⟩
  have hnontermOk := eval_nonterm_iff (rawGrammar A hdistance) NT.accepts
    word.reverse (.ok [])
  have hnontermErr := eval_nonterm_iff (rawGrammar A hdistance) NT.accepts
    word.reverse .err
  refine ⟨?_, ?_⟩
  · simpa [rawGrammar, acceptsRule, acceptingControls] using
      hnontermOk.trans (halternatives.ok_iff.trans hcondition)
  · simpa [rawGrammar, acceptsRule, acceptingControls] using
      hnontermErr.trans (halternatives.err_iff.trans (not_congr hcondition))

/-- The raw grammar recognizes the reversed language of the automaton by
complete match. -/
theorem rawGrammar_recognizes (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) :
    Recognizes (rawGrammar A hdistance)
      (fun input => A.decides input.reverse = true) := by
  intro input
  have hexact := accepts_exact A hdistance input.reverse
  simpa [Automaton.decides, rawGrammar] using hexact.ok_iff.symm

/-- LMR Theorem 16, sufficient direction. -/
theorem scaffold_to_peg
    {Sym Q : Type} {Gamma : Type u} {d k : Nat}
    [DecidableEq Sym] [DecidableEq Q] [DecidableEq Gamma]
    (fs : FiniteEnum Sym) (fq : FiniteEnum Q) (fg : FiniteEnum Gamma)
    (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk) :
    InPEG (fun word => A.decides word.reverse = true) := by
  letI : FiniteEnum Sym := fs
  letI : FiniteEnum Q := fq
  letI : FiniteEnum Gamma := fg
  let normalized := normalize A
  have hnormalized : normalized.DistanceOk :=
    normalize_distanceOk A hdistance
  refine ⟨FiniteEnum.card (NT (Option Q) Gamma d k),
    canonicalFiniteGrammar normalized hnormalized,
    canonicalGrammar_total normalized hnormalized, ?_⟩
  have hraw := rawGrammar_recognizes normalized hnormalized
  have hcanonical : Recognizes (canonicalGrammar normalized hnormalized)
      (fun word => normalized.decides word.reverse = true) :=
    (recognizes_transport_iff
      (canonicalEquiv (Q := Option Q) (Gamma := Gamma) (d := d) (k := k))
      (rawGrammar normalized hnormalized) _).2 hraw
  simpa [canonicalFiniteGrammar, canonicalGrammar, normalized,
    normalize_decides] using hcanonical

end Theorem16
end FPRD