Normalize.lean

import FPRDTransfer.PEG.TableEval

namespace FPRD
namespace Theorem16

universe u

/-- Duplicate the old control carrier under `some` and reserve `none` as a
fresh initial state.  The fresh state behaves like the old initial state on
the first symbol and has the same empty-word acceptance bit. -/
def normalize (A : Automaton Sym Q Gamma d k) :
    Automaton Sym (Option Q) Gamma d k where
  delta state symbol neighbourhood :=
    let result := A.delta (state.getD A.init) symbol neighbourhood
    (some result.1, result.2.1, result.2.2)
  init := none
  accept
    | none => A.accept A.init
    | some state => A.accept state

@[simp] theorem normalize_accept_none (A : Automaton Sym Q Gamma d k) :
    (normalize A).accept none = A.accept A.init := rfl

@[simp] theorem normalize_accept_some (A : Automaton Sym Q Gamma d k)
    (state : Q) : (normalize A).accept (some state) = A.accept state := rfl

theorem normalize_step_none (A : Automaton Sym Q Gamma d k)
    (scaffold : Scaffold d Gamma) (symbol : Sym) :
    (normalize A).step (none, scaffold) symbol =
      let result := A.step (A.init, scaffold) symbol
      (some result.1, result.2) := by
  rfl

theorem normalize_step_some (A : Automaton Sym Q Gamma d k)
    (state : Q) (scaffold : Scaffold d Gamma) (symbol : Sym) :
    (normalize A).step (some state, scaffold) symbol =
      let result := A.step (state, scaffold) symbol
      (some result.1, result.2) := by
  rfl

theorem normalize_foldl_some (A : Automaton Sym Q Gamma d k) :
    ∀ (word : List Sym) (config : Q × Scaffold d Gamma),
      word.foldl (normalize A).step (some config.1, config.2) =
        let result := word.foldl A.step config
        (some result.1, result.2) := by
  intro word
  induction word with
  | nil => intro config; rfl
  | cons symbol rest ih =>
      intro config
      simp only [List.foldl_cons]
      rw [normalize_step_some]
      exact ih (A.step config symbol)

theorem normalize_run_cons (A : Automaton Sym Q Gamma d k)
    (symbol : Sym) (rest : List Sym) :
    (normalize A).run (symbol :: rest) =
      let result := A.run (symbol :: rest)
      (some result.1, result.2) := by
  simp only [Automaton.run, List.foldl_cons]
  change rest.foldl (normalize A).step
      ((normalize A).step (none, Scaffold.base d Gamma) symbol) = _
  rw [normalize_step_none]
  exact normalize_foldl_some A rest
    (A.step (A.init, Scaffold.base d Gamma) symbol)

/-- Fresh-state duplication preserves the language, including the empty word
and computations which later re-enter the old initial control. -/
theorem normalize_decides (A : Automaton Sym Q Gamma d k) (word : List Sym) :
    (normalize A).decides word = A.decides word := by
  cases word with
  | nil => rfl
  | cons symbol rest =>
      simp only [Automaton.decides, normalize_run_cons]
      exact normalize_accept_some A (A.run (symbol :: rest)).1

/-- Normalization changes only the control tag, so the distance constraint is
preserved verbatim. -/
theorem normalize_distanceOk (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) : (normalize A).DistanceOk := by
  intro state symbol neighbourhood port path hpath
  cases state with
  | none =>
      exact hdistance A.init symbol neighbourhood port path (by
        simpa [normalize] using hpath)
  | some state =>
      exact hdistance state symbol neighbourhood port path (by
        simpa [normalize] using hpath)

namespace NormalizeExamples

def reentering : Automaton Bool Bool Unit 1 0 where
  delta _ _ _ := (false, (), fun _ => .missing)
  init := false
  accept q := !q

example : reentering.decides [] = true := by decide

example : (normalize reentering).decides [] = reentering.decides [] := by
  exact normalize_decides reentering []

example : ((normalize reentering).run [true]).1 = some false := by decide

example : (normalize reentering).decides [true] = reentering.decides [true] := by
  exact normalize_decides reentering [true]

example : (normalize reentering).DistanceOk :=
  normalize_distanceOk reentering (by
    intro q x neighbourhood port path h
    simp [reentering] at h)

end NormalizeExamples
end Theorem16
end FPRD