StateLabel.lean

import FPRDTransfer.Theorem16.Grammar

namespace FPRD
namespace Theorem16

universe u uName uSymbol

/-- An expression has exactly one non-consuming Boolean outcome: success on
`condition`, and PEG failure on its negation. -/
structure ExactMatch {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 input) ↔ condition
  err_iff : Eval G expression input .err ↔ ¬condition

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]

/-- I1 at one automaton prefix, including the exact unchanged remainder and
the exact PEG failure result. -/
abbrev StateExact (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (stem : List Sym) (control : Q) : Prop :=
  ExactMatch (rawGrammar A hdistance) (.nonterm (.state control)) stem.reverse
    ((A.run stem).1 = control)

/-- I2 at one automaton prefix.  The new scaffold node has index `top`; a
successful label query is a zero-consumption lookahead. -/
abbrev LabelExact (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (stem : List Sym) (label : Gamma) : Prop :=
  ExactMatch (rawGrammar A hdistance) (.nonterm (.label label)) stem.reverse
    ((A.run stem).2.label (A.run stem).2.top = some label)

/-- I4's exact statement is named here because the State/Label successor step
uses it at the predecessor prefix.  Task 5c proves it unconditionally. -/
abbrev NeighbourhoodExact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym)
    (neighbourhood : Unfold d Gamma k) : Prop :=
  ExactMatch (rawGrammar A hdistance) (.nonterm (.neighbourhood neighbourhood))
    stem.reverse
    ((A.run stem).2.viewAt k (A.run stem).2.top = neighbourhood)

/-- Exactly the predecessor facts used by a transition guard. -/
structure PrefixGuardContext (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) : Prop where
  state : ∀ control, StateExact A hdistance stem control
  neighbourhood : ∀ shape, NeighbourhoodExact A hdistance stem shape

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem pos_ok_of_ok {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol}
    {expression : Expr Name Symbol} {input rest : List Symbol}
    (h : Eval G expression input (.ok rest)) :
    Eval G (Expr.pos expression) input (.ok input) :=
  Eval.notErr (Eval.notOk h)

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem pos_err_of_err {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol}
    {expression : Expr Name Symbol} {input : List Symbol}
    (h : Eval G expression input .err) :
    Eval G (Expr.pos expression) input .err :=
  Eval.notOk (Eval.notErr h)

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem exactMatch_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 input))
    (herr : ¬condition → Eval G expression input .err) :
    ExactMatch 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

/-- The source transition lookahead recognizes exactly the actual input symbol,
predecessor control, and predecessor neighbourhood. -/
theorem transitionExpr_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem)
    (control : Q) (expectedSymbol : Sym)
    (neighbourhood : Unfold d Gamma k) :
    ExactMatch (rawGrammar A hdistance)
      (transitionExpr control expectedSymbol neighbourhood)
      (actualSymbol :: stem.reverse)
      (expectedSymbol = actualSymbol ∧
        (A.run stem).1 = control ∧
        (A.run stem).2.viewAt k (A.run stem).2.top = neighbourhood) := by
  apply exactMatch_of_cases
  · rintro ⟨rfl, hcontrol, hneighbourhood⟩
    exact Eval.seqOk
      (pos_ok_of_ok (Eval.seqOk Eval.termOk
        ((hcontext.state control).ok_iff.mpr hcontrol)))
      (pos_ok_of_ok (Eval.seqOk Eval.termOk
        ((hcontext.neighbourhood neighbourhood).ok_iff.mpr hneighbourhood)))
  · intro hcondition
    by_cases hsymbol : expectedSymbol = actualSymbol
    · subst expectedSymbol
      by_cases hcontrol : (A.run stem).1 = control
      · exact Eval.seqOk
          (pos_ok_of_ok (Eval.seqOk Eval.termOk
            ((hcontext.state control).ok_iff.mpr hcontrol)))
          (pos_err_of_err (Eval.seqOk Eval.termOk
            ((hcontext.neighbourhood neighbourhood).err_iff.mpr (by
              intro hneighbourhood
              exact hcondition ⟨rfl, hcontrol, hneighbourhood⟩))))
      · exact Eval.seqErr
          (pos_err_of_err (Eval.seqOk Eval.termOk
            ((hcontext.state control).err_iff.mpr hcontrol)))
    · exact Eval.seqErr (pos_err_of_err (Eval.seqErr (Eval.termNe hsymbol)))

/-- Two transition guards cannot both match the same prefix unless their
source triples are identical. -/
theorem transition_guard_unique (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem)
    {leftControl rightControl : Q} {leftSymbol rightSymbol : Sym}
    {leftNeighbourhood rightNeighbourhood : Unfold d Gamma k}
    (hleft : Eval (rawGrammar A hdistance)
      (transitionExpr leftControl leftSymbol leftNeighbourhood)
      (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse)))
    (hright : Eval (rawGrammar A hdistance)
      (transitionExpr rightControl rightSymbol rightNeighbourhood)
      (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse))) :
    (leftControl, leftSymbol, leftNeighbourhood) =
      (rightControl, rightSymbol, rightNeighbourhood) := by
  have hl := (transitionExpr_exact A hdistance stem actualSymbol hcontext
    leftControl leftSymbol leftNeighbourhood).ok_iff.mp hleft
  have hr := (transitionExpr_exact A hdistance stem actualSymbol hcontext
    rightControl rightSymbol rightNeighbourhood).ok_iff.mp hright
  rcases hl with ⟨rfl, hlControl, hlNeighbourhood⟩
  rcases hr with ⟨rfl, hrControl, hrNeighbourhood⟩
  have hcontrol : leftControl = rightControl := hlControl.symm.trans hrControl
  have hneighbourhood : leftNeighbourhood = rightNeighbourhood :=
    hlNeighbourhood.symm.trans hrNeighbourhood
  simp [hcontrol, hneighbourhood]

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem altAll_err_of_all {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol}
    (expressions : List (Expr Name Symbol)) (input : List Symbol)
    (hall : ∀ expression, expression ∈ expressions →
      Eval G expression input .err) :
    Eval G (Expr.altAll expressions) input .err := by
  induction expressions with
  | nil => exact Eval.fail
  | cons expression expressions ih =>
      exact Eval.altErr (hall expression (by simp))
        (ih (fun item hitem => hall item (by simp [hitem])))

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem exactMatch_self {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol} {expression : Expr Name Symbol}
    {input : List Symbol} {condition : Prop}
    (hexact : ExactMatch G expression input condition) :
    ExactMatch G expression input (Eval G expression input (.ok input)) := by
  apply exactMatch_of_cases
  · exact id
  · intro hnot
    by_cases hcondition : condition
    · exact (hnot (hexact.ok_iff.mpr hcondition)).elim
    · exact hexact.err_iff.mpr hcondition

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem altAll_exact {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol} (expressions : List (Expr Name Symbol))
    (input : List Symbol) (predicate : Expr Name Symbol → Prop)
    (hall : ∀ expression, expression ∈ expressions →
      ExactMatch G expression input (predicate expression)) :
    ExactMatch G (Expr.altAll expressions) input
      (∃ expression, expression ∈ expressions ∧ predicate expression) := by
  induction expressions with
  | nil =>
      apply exactMatch_of_cases
      · simp
      · intro _
        exact Eval.fail
  | cons expression expressions ih =>
      have hhead := hall expression (by simp)
      have htail := ih (fun item hitem => hall item (by simp [hitem]))
      apply exactMatch_of_cases
      · rintro ⟨item, hitem, hpredicate⟩
        by_cases hfirst : predicate expression
        · exact Eval.altOk (hhead.ok_iff.mpr hfirst)
        · have hrest : ∃ item, item ∈ expressions ∧ predicate item := by
            rcases List.mem_cons.mp hitem with rfl | hitem
            · exact (hfirst hpredicate).elim
            · exact ⟨item, hitem, 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 ⟨expression, by simp, hfirst⟩
        · apply htail.err_iff.mpr
          rintro ⟨item, hitem, hpredicate⟩
          exact hnone ⟨item, by simp [hitem], hpredicate⟩

omit [DecidableEq Sym] [DecidableEq Gamma] in
theorem mem_stateAlternatives_iff (A : Automaton Sym Q Gamma d k)
    (target : Q) (expression : Expr (NT Q Gamma d k) Sym) :
    expression ∈ stateAlternatives A target ↔
      ∃ input ∈ transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
          (d := d) (k := k),
        (A.delta input.1 input.2.1 input.2.2).1 = target ∧
          transitionExpr input.1 input.2.1 input.2.2 = expression := by
  simp [stateAlternatives]

omit [DecidableEq Sym] [DecidableEq Q] in
theorem mem_labelAlternatives_iff (A : Automaton Sym Q Gamma d k)
    (target : Gamma) (expression : Expr (NT Q Gamma d k) Sym) :
    expression ∈ labelAlternatives A target ↔
      ∃ input ∈ transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
          (d := d) (k := k),
        (A.delta input.1 input.2.1 input.2.2).2.1 = target ∧
          transitionExpr input.1 input.2.1 input.2.2 = expression := by
  simp [labelAlternatives]

theorem stateAlternative_self_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Q)
    (expression : Expr (NT Q Gamma d k) Sym)
    (hexpression : expression ∈ stateAlternatives A target) :
    ExactMatch (rawGrammar A hdistance) expression
      (actualSymbol :: stem.reverse)
      (Eval (rawGrammar A hdistance) expression
        (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse))) := by
  rcases (mem_stateAlternatives_iff A target expression).mp hexpression with
    ⟨input, _, _, hexpression⟩
  rw [← hexpression]
  exact exactMatch_self (transitionExpr_exact A hdistance stem actualSymbol
    hcontext input.1 input.2.1 input.2.2)

theorem labelAlternative_self_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Gamma)
    (expression : Expr (NT Q Gamma d k) Sym)
    (hexpression : expression ∈ labelAlternatives A target) :
    ExactMatch (rawGrammar A hdistance) expression
      (actualSymbol :: stem.reverse)
      (Eval (rawGrammar A hdistance) expression
        (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse))) := by
  rcases (mem_labelAlternatives_iff A target expression).mp hexpression with
    ⟨input, _, _, hexpression⟩
  rw [← hexpression]
  exact exactMatch_self (transitionExpr_exact A hdistance stem actualSymbol
    hcontext input.1 input.2.1 input.2.2)

theorem stateAlternatives_success_iff (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Q) :
    (∃ expression, expression ∈ stateAlternatives A target ∧
      Eval (rawGrammar A hdistance) expression
        (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse))) ↔
      (A.delta (A.run stem).1 actualSymbol
        ((A.run stem).2.viewAt k (A.run stem).2.top)).1 = target := by
  constructor
  · rintro ⟨expression, hexpression, heval⟩
    rcases (mem_stateAlternatives_iff A target expression).mp hexpression with
      ⟨⟨control, expectedSymbol, neighbourhood⟩, _, htarget, hshape⟩
    rw [← hshape] at heval
    have hcondition := (transitionExpr_exact A hdistance stem actualSymbol
      hcontext control expectedSymbol neighbourhood).ok_iff.mp heval
    rw [hcondition.2.1, ← hcondition.1, hcondition.2.2]
    exact htarget
  · intro htarget
    let actualInput : TransitionInput Sym Q Gamma d k :=
      ((A.run stem).1, actualSymbol,
        (A.run stem).2.viewAt k (A.run stem).2.top)
    refine ⟨transitionExpr actualInput.1 actualInput.2.1 actualInput.2.2, ?_, ?_⟩
    · apply (mem_stateAlternatives_iff A target _).mpr
      exact ⟨actualInput, FiniteEnum.complete actualInput, htarget, rfl⟩
    · exact (transitionExpr_exact A hdistance stem actualSymbol hcontext
        actualInput.1 actualInput.2.1 actualInput.2.2).ok_iff.mpr
          ⟨rfl, rfl, rfl⟩

theorem labelAlternatives_success_iff (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Gamma) :
    (∃ expression, expression ∈ labelAlternatives A target ∧
      Eval (rawGrammar A hdistance) expression
        (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse))) ↔
      (A.delta (A.run stem).1 actualSymbol
        ((A.run stem).2.viewAt k (A.run stem).2.top)).2.1 = target := by
  constructor
  · rintro ⟨expression, hexpression, heval⟩
    rcases (mem_labelAlternatives_iff A target expression).mp hexpression with
      ⟨⟨control, expectedSymbol, neighbourhood⟩, _, htarget, hshape⟩
    rw [← hshape] at heval
    have hcondition := (transitionExpr_exact A hdistance stem actualSymbol
      hcontext control expectedSymbol neighbourhood).ok_iff.mp heval
    rw [hcondition.2.1, ← hcondition.1, hcondition.2.2]
    exact htarget
  · intro htarget
    let actualInput : TransitionInput Sym Q Gamma d k :=
      ((A.run stem).1, actualSymbol,
        (A.run stem).2.viewAt k (A.run stem).2.top)
    refine ⟨transitionExpr actualInput.1 actualInput.2.1 actualInput.2.2, ?_, ?_⟩
    · apply (mem_labelAlternatives_iff A target _).mpr
      exact ⟨actualInput, FiniteEnum.complete actualInput, htarget, rfl⟩
    · exact (transitionExpr_exact A hdistance stem actualSymbol hcontext
        actualInput.1 actualInput.2.1 actualInput.2.2).ok_iff.mpr
          ⟨rfl, rfl, rfl⟩

theorem stateAlternatives_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Q) :
    ExactMatch (rawGrammar A hdistance) (Expr.altAll (stateAlternatives A target))
      (actualSymbol :: stem.reverse)
      ((A.delta (A.run stem).1 actualSymbol
        ((A.run stem).2.viewAt k (A.run stem).2.top)).1 = target) := by
  have hordered := altAll_exact (stateAlternatives A target)
    (actualSymbol :: stem.reverse)
    (fun expression => Eval (rawGrammar A hdistance) expression
      (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse)))
    (stateAlternative_self_exact A hdistance stem actualSymbol hcontext target)
  have hcondition := stateAlternatives_success_iff A hdistance stem
    actualSymbol hcontext target
  exact ⟨hordered.ok_iff.trans hcondition,
    hordered.err_iff.trans (not_congr hcondition)⟩

theorem labelAlternatives_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (actualSymbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Gamma) :
    ExactMatch (rawGrammar A hdistance) (Expr.altAll (labelAlternatives A target))
      (actualSymbol :: stem.reverse)
      ((A.delta (A.run stem).1 actualSymbol
        ((A.run stem).2.viewAt k (A.run stem).2.top)).2.1 = target) := by
  have hordered := altAll_exact (labelAlternatives A target)
    (actualSymbol :: stem.reverse)
    (fun expression => Eval (rawGrammar A hdistance) expression
      (actualSymbol :: stem.reverse) (.ok (actualSymbol :: stem.reverse)))
    (labelAlternative_self_exact A hdistance stem actualSymbol hcontext target)
  have hcondition := labelAlternatives_success_iff A hdistance stem
    actualSymbol hcontext target
  exact ⟨hordered.ok_iff.trans hcondition,
    hordered.err_iff.trans (not_congr hcondition)⟩

theorem state_rule_step_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Q) :
    ExactMatch (rawGrammar A hdistance) (.nonterm (.state target))
      (symbol :: stem.reverse)
      ((A.delta (A.run stem).1 symbol
        ((A.run stem).2.viewAt k (A.run stem).2.top)).1 = target) := by
  have halternatives := stateAlternatives_exact A hdistance stem symbol hcontext target
  apply exactMatch_of_cases
  · intro htarget
    apply Eval.nonterm
    by_cases hinitial : target = A.init
    · simp only [rawGrammar, if_pos hinitial, List.singleton_append, Expr.altAll,
        List.foldr_cons]
      exact Eval.altErr (Eval.notOk Eval.anyOk)
        (halternatives.ok_iff.mpr htarget)
    · simp only [rawGrammar, if_neg hinitial, List.nil_append]
      exact halternatives.ok_iff.mpr htarget
  · intro htarget
    apply Eval.nonterm
    by_cases hinitial : target = A.init
    · simp only [rawGrammar, if_pos hinitial, List.singleton_append, Expr.altAll,
        List.foldr_cons]
      exact Eval.altErr (Eval.notOk Eval.anyOk)
        (halternatives.err_iff.mpr htarget)
    · simp only [rawGrammar, if_neg hinitial, List.nil_append]
      exact halternatives.err_iff.mpr htarget

theorem label_rule_step_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Gamma) :
    ExactMatch (rawGrammar A hdistance) (.nonterm (.label target))
      (symbol :: stem.reverse)
      ((A.delta (A.run stem).1 symbol
        ((A.run stem).2.viewAt k (A.run stem).2.top)).2.1 = target) := by
  have halternatives := labelAlternatives_exact A hdistance stem symbol hcontext target
  refine ⟨?_, ?_⟩
  · simpa [rawGrammar] using
      (eval_nonterm_iff (rawGrammar A hdistance) (.label target)
        (symbol :: stem.reverse) (.ok (symbol :: stem.reverse))).trans
          halternatives.ok_iff
  · simpa [rawGrammar] using
      (eval_nonterm_iff (rawGrammar A hdistance) (.label target)
        (symbol :: stem.reverse) .err).trans halternatives.err_iff

/-- Conditional successor form of I1.  Task 5c supplies the predecessor
context by simultaneous induction. -/
theorem state_step_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Q) :
    StateExact A hdistance (stem ++ [symbol]) target := by
  change ExactMatch (rawGrammar A hdistance) (.nonterm (.state target))
    (stem ++ [symbol]).reverse ((A.run (stem ++ [symbol])).1 = target)
  simpa [List.reverse_append, Automaton.run_append, Automaton.step] using
    state_rule_step_exact A hdistance stem symbol hcontext target

/-- Conditional successor form of I2.  The newly appended node's label is the
label emitted by the actual transition. -/
theorem label_step_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Gamma) :
    LabelExact A hdistance (stem ++ [symbol]) target := by
  change ExactMatch (rawGrammar A hdistance) (.nonterm (.label target))
    (stem ++ [symbol]).reverse
    ((A.run (stem ++ [symbol])).2.label (A.run (stem ++ [symbol])).2.top =
      some target)
  simpa [List.reverse_append, Automaton.run_append, Automaton.step] using
    label_rule_step_exact A hdistance stem symbol hcontext target

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem transitionExpr_nil_err (control : Q) (symbol : Sym)
    (neighbourhood : Unfold d Gamma k) {G : Grammar (NT Q Gamma d k) Sym} :
    Eval G (transitionExpr control symbol neighbourhood) [] .err := by
  apply Eval.seqErr
  apply pos_err_of_err
  exact Eval.seqErr Eval.termNil

omit [DecidableEq Sym] in
theorem stateAlternatives_nil_err (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (target : Q) :
    ∀ expression, expression ∈ stateAlternatives A target →
      Eval (rawGrammar A hdistance) expression [] .err := by
  intro expression hexpression
  unfold stateAlternatives at hexpression
  generalize (transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
    (d := d) (k := k)) = inputs at hexpression
  induction inputs with
  | nil => simp at hexpression
  | cons input inputs ih =>
      by_cases htarget : (A.delta input.1 input.2.1 input.2.2).1 = target
      · simp only [List.filterMap_cons, if_pos htarget,
          List.mem_cons] at hexpression
        rcases hexpression with rfl | hexpression
        · exact transitionExpr_nil_err _ _ _
        · exact ih hexpression
      · simp only [List.filterMap_cons, if_neg htarget] at hexpression
        exact ih hexpression

omit [DecidableEq Sym] in
theorem labelAlternatives_nil_err (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (target : Gamma) :
    ∀ expression, expression ∈ labelAlternatives A target →
      Eval (rawGrammar A hdistance) expression [] .err := by
  intro expression hexpression
  unfold labelAlternatives at hexpression
  generalize (transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
    (d := d) (k := k)) = inputs at hexpression
  induction inputs with
  | nil => simp at hexpression
  | cons input inputs ih =>
      by_cases htarget : (A.delta input.1 input.2.1 input.2.2).2.1 = target
      · simp only [List.filterMap_cons, if_pos htarget,
          List.mem_cons] at hexpression
        rcases hexpression with rfl | hexpression
        · exact transitionExpr_nil_err _ _ _
        · exact ih hexpression
      · simp only [List.filterMap_cons, if_neg htarget] at hexpression
        exact ih hexpression

omit [DecidableEq Sym] in
theorem state_nil_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (control : Q) :
    StateExact A hdistance [] control := by
  by_cases hcontrol : control = A.init
  · subst control
    have hok : Eval (rawGrammar A hdistance) (.nonterm (.state A.init)) []
        (.ok []) := by
      apply Eval.nonterm
      simp only [rawGrammar]
      exact Eval.altOk (Eval.notErr Eval.anyNil)
    refine ⟨?_, ?_⟩
    · constructor
      · intro _
        rfl
      · intro _
        exact hok
    · constructor
      · intro herr heq
        have himpossible := eval_deterministic herr hok
        cases himpossible
      · intro hne
        exact (hne rfl).elim
  · have herr : Eval (rawGrammar A hdistance) (.nonterm (.state control)) []
        .err := by
      apply Eval.nonterm
      simp only [rawGrammar, if_neg hcontrol, List.nil_append]
      exact altAll_err_of_all _ _
        (stateAlternatives_nil_err A hdistance control)
    refine ⟨?_, ?_⟩
    · constructor
      · intro hok
        have himpossible := eval_deterministic hok herr
        cases himpossible
      · intro heq
        exact (hcontrol (by simpa using heq.symm)).elim
    · constructor
      · intro _ heq
        exact hcontrol (by simpa using heq.symm)
      · intro _
        exact herr

omit [DecidableEq Sym] in
theorem label_nil_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (label : Gamma) :
    LabelExact A hdistance [] label := by
  have herr : Eval (rawGrammar A hdistance) (.nonterm (.label label)) [] .err := by
    apply Eval.nonterm
    simp only [rawGrammar]
    exact altAll_err_of_all _ _ (labelAlternatives_nil_err A hdistance label)
  refine ⟨?_, ?_⟩
  · constructor
    · intro hok
      have himpossible := eval_deterministic hok herr
      cases himpossible
    · intro heq
      simp [Automaton.run, Scaffold.base] at heq
  · constructor
    · intro _ heq
      simp [Automaton.run, Scaffold.base] at heq
    · intro _
      exact herr

namespace StateLabelRed

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]

example (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (control : Q) :
    StateExact A hdistance [] control :=
  state_nil_exact A hdistance control

example (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (label : Gamma) :
    LabelExact A hdistance [] label :=
  label_nil_exact A hdistance label

example (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (stem : List Sym) (symbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Q) :
    StateExact A hdistance (stem ++ [symbol]) target :=
  state_step_exact A hdistance stem symbol hcontext target

example (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (stem : List Sym) (symbol : Sym)
    (hcontext : PrefixGuardContext A hdistance stem) (target : Gamma) :
    LabelExact A hdistance (stem ++ [symbol]) target :=
  label_step_exact A hdistance stem symbol hcontext target

end StateLabelRed
end Theorem16
end FPRD