Grammar.lean

import FPRDTransfer.Theorem16.Reachability

namespace FPRD
namespace Theorem16

universe u v w

/-- Observe the root reached by a path whose length is bounded by the unfolding
depth.  `none`, `some none`, and `some (some label)` remain distinct. -/
def observeAt {Gamma : Type u} {d : Nat} :
    (depth : Nat) → Unfold d Gamma depth →
      (path : List (Fin d)) → path.length ≤ depth → Option (Option Gamma)
  | _, .missing, _, _ => none
  | 0, .leaf label, [], _ => some label
  | 0, .leaf _, _ :: _, hlength =>
      False.elim (Nat.not_succ_le_zero _ hlength)
  | _depth + 1, .node label _, [], _ => some label
  | depth + 1, .node _ children, port :: rest, hlength =>
      observeAt depth (children port) rest (Nat.le_of_succ_le_succ hlength)

def observe {Gamma : Type u} {d k : Nat}
    (neighbourhood : Unfold d Gamma k) (path : BoundedPath d k) :
    Option (Option Gamma) :=
  observeAt k neighbourhood path.elems path.length_le

/-- The empty bounded path, used to observe the root at every depth. -/
def rootPath (d k : Nat) : BoundedPath d k := ⟨[], by simp⟩

theorem boundedPath_elems_starts_root (d k : Nat) :
    ∃ rest, FiniteEnum.elems (α := BoundedPath d k) = rootPath d k :: rest := by
  cases k with
  | zero => exact ⟨[], rfl⟩
  | succ k => exact ⟨_, rfl⟩

/-- Bounded observations separate exact-depth unfoldings. -/
theorem unfold_eq_iff_observe_all {Gamma : Type u} {d k : Nat}
    (left right : Unfold d Gamma k) :
    left = right ↔ ∀ path : BoundedPath d k,
      observe left path = observe right path := by
  constructor
  · intro heq path
    cases heq
    rfl
  · intro hall
    induction k with
    | zero =>
        cases left with
        | missing =>
            cases right with
            | missing => rfl
            | leaf label =>
                have h := hall (⟨[], by simp⟩ : BoundedPath d 0)
                simp [observe, observeAt] at h
        | leaf leftLabel =>
            cases right with
            | missing =>
                have h := hall (⟨[], by simp⟩ : BoundedPath d 0)
                simp [observe, observeAt] at h
            | leaf rightLabel =>
                have h := hall (⟨[], by simp⟩ : BoundedPath d 0)
                simp [observe, observeAt] at h
                cases h
                rfl
    | succ depth ih =>
        cases left with
        | missing =>
            cases right with
            | missing => rfl
            | node label children =>
                have h := hall (⟨[], by simp⟩ : BoundedPath d (depth + 1))
                simp [observe, observeAt] at h
        | node leftLabel leftChildren =>
            cases right with
            | missing =>
                have h := hall (⟨[], by simp⟩ : BoundedPath d (depth + 1))
                simp [observe, observeAt] at h
            | node rightLabel rightChildren =>
                have hlabel := hall
                  (⟨[], by simp⟩ : BoundedPath d (depth + 1))
                simp [observe, observeAt] at hlabel
                cases hlabel
                have hchildren : leftChildren = rightChildren := by
                  funext port
                  apply ih (leftChildren port) (rightChildren port)
                  intro path
                  have hchild := hall
                    (⟨port :: path.elems,
                      Nat.succ_le_succ path.length_le⟩ :
                      BoundedPath d (depth + 1))
                  simpa [observe, observeAt] using hchild
                cases hchildren
                rfl

/-- The raw source nonterminal carrier is finite by construction; path names
carry the distance bound rather than an unrestricted list. -/
inductive NT (Q : Type) (Gamma : Type u) (d k : Nat) where
  | state (control : Q)
  | label (symbol : Gamma)
  | neighbourhood (shape : Unfold d Gamma k)
  | path (ports : BoundedPath d k)
  | anyStar
  | accepts
  deriving DecidableEq

instance [FiniteEnum Q] [FiniteEnum Gamma] :
    FiniteEnum (NT Q Gamma d k) where
  elems :=
    (FiniteEnum.elems (α := Q)).map NT.state ++
    (FiniteEnum.elems (α := Gamma)).map NT.label ++
    (FiniteEnum.elems (α := Unfold d Gamma k)).map NT.neighbourhood ++
    (FiniteEnum.elems (α := BoundedPath d k)).map NT.path ++
    [.anyStar, .accepts]
  complete name := by
    cases name <;> simp [FiniteEnum.complete]

section Grammar

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]

abbrev TransitionInput (Sym Q : Type) (Gamma : Type u) (d k : Nat) :=
  Q × (Sym × Unfold d Gamma k)

def transitionInputs : List (TransitionInput Sym Q Gamma d k) :=
  FiniteEnum.elems

/-- The source abbreviation `&(sigma State(q)) &(sigma Neighbourhood(N))`. -/
def transitionExpr (control : Q) (symbol : Sym)
    (neighbourhood : Unfold d Gamma k) : Expr (NT Q Gamma d k) Sym :=
  .seq
    (.pos (.seq (.term symbol) (.nonterm (.state control))))
    (.pos (.seq (.term symbol) (.nonterm (.neighbourhood neighbourhood))))

def stateAlternatives (A : Automaton Sym Q Gamma d k) (target : Q) :
    List (Expr (NT Q Gamma d k) Sym) :=
  (transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma) (d := d) (k := k)).filterMap
    fun input =>
      if (A.delta input.1 input.2.1 input.2.2).1 = target then
        some (transitionExpr input.1 input.2.1 input.2.2)
      else none

def labelAlternatives (A : Automaton Sym Q Gamma d k) (target : Gamma) :
    List (Expr (NT Q Gamma d k) Sym) :=
  (transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma) (d := d) (k := k)).filterMap
    fun input =>
      if (A.delta input.1 input.2.1 input.2.2).2.1 = target then
        some (transitionExpr input.1 input.2.1 input.2.2)
      else none

def pathAlternative (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (tail : BoundedPath d k) (port : Fin d)
    (input : TransitionInput Sym Q Gamma d k) :
    Expr (NT Q Gamma d k) Sym :=
  let guard := transitionExpr input.1 input.2.1 input.2.2
  match htarget : (A.delta input.1 input.2.1 input.2.2).2.2 port with
  | .path oldPath =>
      let boundedOld : BoundedPath d k :=
        ⟨oldPath, hdistance input.1 input.2.1 input.2.2 port oldPath htarget⟩
      .seq guard
        (.seq (.term input.2.1)
          (.seq (.nonterm (.path boundedOld)) (.nonterm (.path tail))))
  | .missing => .seq guard .fail
  | .self => .seq guard (.nonterm (.path tail))

def pathRule (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
    (path : BoundedPath d k) : Expr (NT Q Gamma d k) Sym :=
  match hpath : path.elems with
  | [] => .eps
  | port :: tail =>
      let boundedTail : BoundedPath d k := ⟨tail, by
        have := path.length_le
        simp only [hpath, List.length_cons] at this
        omega⟩
      Expr.altAll
        ((transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma) (d := d) (k := k)).map
          (pathAlternative A hdistance boundedTail port))

def observationFact (neighbourhood : Unfold d Gamma k)
    (path : BoundedPath d k) : Expr (NT Q Gamma d k) Sym :=
  let pathExpr : Expr (NT Q Gamma d k) Sym := .nonterm (.path path)
  match observe neighbourhood path with
  | none => .notP pathExpr
  | some none =>
      .seq (.pos pathExpr)
        (Expr.seqAll ((FiniteEnum.elems (α := Gamma)).map fun label =>
          .notP (.seq pathExpr (.nonterm (.label label)))))
  | some (some label) =>
      .pos (.seq pathExpr (.nonterm (.label label)))

def neighbourhoodRule (neighbourhood : Unfold d Gamma k) :
    Expr (NT Q Gamma d k) Sym :=
  Expr.seqAll ((FiniteEnum.elems (α := BoundedPath d k)).map
    (observationFact (Q := Q) (Sym := Sym) neighbourhood))

def acceptsRule (A : Automaton Sym Q Gamma d k) :
    Expr (NT Q Gamma d k) Sym :=
  Expr.altAll (((FiniteEnum.elems (α := Q)).filter fun control =>
    A.accept control = true).map fun control =>
      .seq (.nonterm (.state control)) (.nonterm .anyStar))

/-- The exact finite raw grammar from the source construction.  Empty
alternative families use `fail`; `Path([])` is explicitly `eps`. -/
def rawGrammar (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk) :
    Grammar (NT Q Gamma d k) Sym where
  start := .accepts
  rule
    | .state control =>
        Expr.altAll
          ((if control = A.init then [.notP .any] else []) ++
            stateAlternatives A control)
    | .label label => Expr.altAll (labelAlternatives A label)
    | .neighbourhood neighbourhood => neighbourhoodRule (Q := Q) (Sym := Sym) neighbourhood
    | .path path => pathRule A hdistance path
    | .anyStar => .alt (.seq .any (.nonterm .anyStar)) .eps
    | .accepts => acceptsRule A

def rawFiniteGrammar (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk) :
    FiniteGrammar Sym (NT Q Gamma d k) where
  alphabet := inferInstance
  nonterminals := inferInstance
  grammar := rawGrammar A hdistance

def canonicalEquiv :
    FiniteEquiv (NT Q Gamma d k) (Fin (FiniteEnum.card (NT Q Gamma d k))) :=
  FiniteEnum.equivFin (NT Q Gamma d k)

def canonicalGrammar (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk) :
    Grammar (Fin (FiniteEnum.card (NT Q Gamma d k))) Sym :=
  transportGrammar canonicalEquiv (rawGrammar A hdistance)

def canonicalFiniteGrammar (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) :
    FiniteGrammar Sym (Fin (FiniteEnum.card (NT Q Gamma d k))) :=
  transportFiniteGrammar canonicalEquiv (rawFiniteGrammar A hdistance)

def ntRank : NT Q Gamma d k → Nat
  | .state _ | .label _ | .anyStar => 0
  | .path path => path.elems.length
  | .neighbourhood _ => k + 1
  | .accepts => k + 2

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
@[simp] theorem transitionExpr_samePositionCalls (control : Q) (symbol : Sym)
    (neighbourhood : Unfold d Gamma k) :
    Expr.samePositionCalls (transitionExpr control symbol neighbourhood) = [] := by
  simp [transitionExpr, Expr.pos, Expr.samePositionCalls,
    Expr.guaranteedConsumes]

omit [FiniteEnum Sym] [DecidableEq Sym] in
theorem samePositionCalls_altAll {Name : Type v}
    (expressions : List (Expr Name Sym)) :
    Expr.samePositionCalls (Expr.altAll expressions) =
      expressions.flatMap Expr.samePositionCalls := by
  induction expressions with
  | nil => rfl
  | cons expression expressions ih =>
      change Expr.samePositionCalls (.alt expression (Expr.altAll expressions)) = _
      simp [Expr.samePositionCalls, ih]

omit [FiniteEnum Sym] [DecidableEq Sym] in
theorem samePositionCalls_seqAll {Name : Type v}
    (expressions : List (Expr Name Sym))
    (hzero : ∀ expression, expression ∈ expressions →
      Expr.guaranteedConsumes expression = false) :
    Expr.samePositionCalls (Expr.seqAll expressions) =
      expressions.flatMap Expr.samePositionCalls := by
  induction expressions with
  | nil => rfl
  | cons expression expressions ih =>
      change Expr.samePositionCalls (.seq expression (Expr.seqAll expressions)) = _
      rw [Expr.samePositionCalls]
      simp [hzero expression (by simp), ih (fun item hitem =>
        hzero item (by simp [hitem]))]

omit [FiniteEnum Sym] [DecidableEq Sym] in
theorem guaranteedConsumes_seqAll_false {Name : Type v}
    (expressions : List (Expr Name Sym))
    (hzero : ∀ expression, expression ∈ expressions →
      Expr.guaranteedConsumes expression = false) :
    Expr.guaranteedConsumes (Expr.seqAll expressions) = false := by
  induction expressions with
  | nil => rfl
  | cons expression expressions ih =>
      change Expr.guaranteedConsumes
        (.seq expression (Expr.seqAll expressions)) = false
      rw [Expr.guaranteedConsumes, hzero expression (by simp)]
      simp only [Bool.false_or]
      exact ih (fun item hitem => hzero item (by simp [hitem]))

omit [FiniteEnum Sym] [DecidableEq Sym] in
theorem guaranteedConsumes_transport {Name : Type v} {Name' : Type w}
    (equiv : FiniteEquiv Name Name')
    (expression : Expr Name Sym) :
    Expr.guaranteedConsumes (transportExpr equiv expression) =
      Expr.guaranteedConsumes expression := by
  induction expression <;> simp_all [transportExpr, Expr.guaranteedConsumes]

omit [FiniteEnum Sym] [DecidableEq Sym] in
theorem samePositionCalls_transport {Name : Type v} {Name' : Type w}
    (equiv : FiniteEquiv Name Name')
    (expression : Expr Name Sym) :
    Expr.samePositionCalls (transportExpr equiv expression) =
      (Expr.samePositionCalls expression).map equiv := by
  induction expression with
  | eps | fail | any | term | nonterm => simp [transportExpr, Expr.samePositionCalls]
  | alt left right ihLeft ihRight =>
      simp [transportExpr, Expr.samePositionCalls, ihLeft, ihRight]
  | notP body ih => simp [transportExpr, Expr.samePositionCalls, ih]
  | seq left right ihLeft ihRight =>
      simp only [transportExpr, Expr.samePositionCalls, ihLeft, ihRight,
        List.map_append]
      rw [guaranteedConsumes_transport]
      split <;> simp

omit [DecidableEq Sym] [DecidableEq Gamma] in
theorem stateAlternatives_calls_empty (A : Automaton Sym Q Gamma d k)
    (target : Q) :
    (stateAlternatives A target).flatMap Expr.samePositionCalls = [] := by
  unfold stateAlternatives
  generalize (transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
    (d := d) (k := k)) = inputs
  induction inputs with
  | nil => rfl
  | cons input inputs ih =>
      by_cases htarget : (A.delta input.1 input.2.1 input.2.2).1 = target
      · simp [htarget, ih]
      · simp [htarget, ih]

omit [DecidableEq Sym] [DecidableEq Q] in
theorem labelAlternatives_calls_empty (A : Automaton Sym Q Gamma d k)
    (target : Gamma) :
    (labelAlternatives A target).flatMap Expr.samePositionCalls = [] := by
  unfold labelAlternatives
  generalize (transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
    (d := d) (k := k)) = inputs
  induction inputs with
  | nil => rfl
  | cons input inputs ih =>
      by_cases htarget : (A.delta input.1 input.2.1 input.2.2).2.1 = target
      · simp [htarget, ih]
      · simp [htarget, ih]

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem pathAlternative_call (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (tail : BoundedPath d k) (port : Fin d)
    (input : TransitionInput Sym Q Gamma d k) {callee}
    (hcall : callee ∈ Expr.samePositionCalls
      (pathAlternative A hdistance tail port input)) :
    callee = NT.path tail := by
  unfold pathAlternative at hcall
  split at hcall <;>
    simp [Expr.samePositionCalls, Expr.guaranteedConsumes] at hcall
  exact hcall.2

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [DecidableEq Gamma] in
theorem observationFact_call (neighbourhood : Unfold d Gamma k)
    (path : BoundedPath d k) {callee}
    (hcall : callee ∈ Expr.samePositionCalls
      (observationFact (Q := Q) (Sym := Sym) neighbourhood path)) :
    callee = NT.path path ∨ ∃ label, callee = NT.label label := by
  unfold observationFact at hcall
  cases hobs : observe neighbourhood path with
  | none =>
      rw [hobs] at hcall
      exact Or.inl (by simpa [Expr.samePositionCalls] using hcall)
  | some observation =>
      cases observation with
      | none =>
          rw [hobs] at hcall
          let facts : List (Expr (NT Q Gamma d k) Sym) :=
            (FiniteEnum.elems (α := Gamma)).map fun label =>
            Expr.notP (.seq (.nonterm (NT.path path)) (.nonterm (.label label)))
          have hzero : ∀ expression, expression ∈ facts →
              Expr.guaranteedConsumes expression = false := by
            intro expression hexpression
            simp [facts] at hexpression
            obtain ⟨label, hlabel, rfl⟩ := hexpression
            rfl
          change callee ∈ [NT.path path] ++
            Expr.samePositionCalls (Expr.seqAll facts) at hcall
          rw [samePositionCalls_seqAll facts hzero] at hcall
          rcases List.mem_append.mp hcall with hpath | hfact
          · exact Or.inl (by simpa using hpath)
          · rw [List.mem_flatMap] at hfact
            obtain ⟨expression, hexpression, hcallee⟩ := hfact
            simp [facts] at hexpression
            obtain ⟨label, hlabel, rfl⟩ := hexpression
            simp [Expr.samePositionCalls, Expr.guaranteedConsumes] at hcallee
            rcases hcallee with hpath | hlabel
            · exact Or.inl hpath
            · exact Or.inr ⟨label, hlabel⟩
      | some label =>
          rw [hobs] at hcall
          simp [Expr.pos, Expr.samePositionCalls, Expr.guaranteedConsumes] at hcall
          rcases hcall with hpath | hlabel
          · exact Or.inl hpath
          · exact Or.inr ⟨label, hlabel⟩

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [DecidableEq Gamma] in
theorem observationFact_notGuaranteed (neighbourhood : Unfold d Gamma k)
    (path : BoundedPath d k) :
    Expr.guaranteedConsumes
      (observationFact (Q := Q) (Sym := Sym) neighbourhood path) = false := by
  unfold observationFact
  cases hobs : observe neighbourhood path with
  | none => rfl
  | some observation =>
    cases observation with
    | none =>
      let facts : List (Expr (NT Q Gamma d k) Sym) :=
        (FiniteEnum.elems (α := Gamma)).map fun label =>
          Expr.notP (.seq (.nonterm (NT.path path)) (.nonterm (.label label)))
      have hzero : ∀ expression, expression ∈ facts →
          Expr.guaranteedConsumes expression = false := by
        intro expression hexpression
        simp [facts] at hexpression
        obtain ⟨label, hlabel, rfl⟩ := hexpression
        rfl
      have hseq := guaranteedConsumes_seqAll_false facts hzero
      change Expr.guaranteedConsumes
        (.seq (.pos (.nonterm (NT.path path))) (Expr.seqAll facts)) = false
      simp [Expr.pos, Expr.guaranteedConsumes, hseq]
    | some label =>
      rfl

omit [DecidableEq Sym] in
theorem rawGrammar_call_rank_lt (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) {caller callee : NT Q Gamma d k}
    (hcall : callee ∈ Expr.samePositionCalls
      ((rawGrammar A hdistance).rule caller)) :
    ntRank callee < ntRank caller := by
  cases caller with
  | state control =>
      change callee ∈ Expr.samePositionCalls
        (Expr.altAll ((if control = A.init then [.notP .any] else []) ++
          stateAlternatives A control)) at hcall
      rw [samePositionCalls_altAll, List.flatMap_append,
        stateAlternatives_calls_empty] at hcall
      split at hcall <;> simp [Expr.samePositionCalls] at hcall
  | label label =>
      change callee ∈ Expr.samePositionCalls
        (Expr.altAll (labelAlternatives A label)) at hcall
      rw [samePositionCalls_altAll, labelAlternatives_calls_empty] at hcall
      simp at hcall
  | anyStar =>
      simp [rawGrammar, Expr.samePositionCalls, Expr.guaranteedConsumes] at hcall
  | path path =>
      change callee ∈ Expr.samePositionCalls (pathRule A hdistance path) at hcall
      unfold pathRule at hcall
      split at hcall
      · simp [Expr.samePositionCalls] at hcall
      · rename_i hpath
        rw [samePositionCalls_altAll] at hcall
        simp only [List.mem_flatMap, List.mem_map] at hcall
        obtain ⟨expression, ⟨input, hinput, rfl⟩, hcall⟩ := hcall
        have hcallee := pathAlternative_call A hdistance _ _ input hcall
        subst callee
        dsimp [ntRank]
        rw [hpath]
        simp
  | neighbourhood neighbourhood =>
      change callee ∈ Expr.samePositionCalls
        (neighbourhoodRule (Q := Q) (Sym := Sym) neighbourhood) at hcall
      unfold neighbourhoodRule at hcall
      rw [samePositionCalls_seqAll _ (by
        intro expression hexpression
        simp at hexpression
        obtain ⟨path, hpath, rfl⟩ := hexpression
        exact observationFact_notGuaranteed (Q := Q) (Sym := Sym) neighbourhood path)] at hcall
      simp only [List.mem_flatMap, List.mem_map] at hcall
      obtain ⟨fact, ⟨path, hpath, rfl⟩, hcall⟩ := hcall
      rcases observationFact_call (Q := Q) (Sym := Sym) neighbourhood path hcall with
        hpathCall | ⟨label, hlabelCall⟩
      · subst callee
        simp [ntRank]
        exact Nat.lt_succ_of_le path.length_le
      · subst callee
        simp [ntRank]
  | accepts =>
      change callee ∈ Expr.samePositionCalls (acceptsRule A) at hcall
      unfold acceptsRule at hcall
      rw [samePositionCalls_altAll] at hcall
      simp only [List.mem_flatMap, List.mem_map] at hcall
      obtain ⟨expression, ⟨control, hcontrol, rfl⟩, hcall⟩ := hcall
      simp [Expr.samePositionCalls, Expr.guaranteedConsumes] at hcall
      rcases hcall with rfl | rfl <;> simp [ntRank]

end Grammar

section RelationalTotality

variable {Sym : Type} {n : Nat} [DecidableEq Sym]

def HasResult (G : Grammar (Fin n) Sym) (expr : Expr (Fin n) Sym)
    (input : List Sym) : Prop :=
  ∃ result, Eval G expr input result

/-- Relational evaluation exists when proper-suffix calls and the explicitly
same-position calls already have results.  This proof does not invoke the
executable table evaluator. -/
theorem expr_hasResult_of_calls (G : Grammar (Fin n) Sym)
    {expr : Expr (Fin n) Sym} {input : List Sym}
    (shorter : ∀ suffix, suffix <:+ input → suffix.length < input.length →
      ∀ name, HasResult G (.nonterm name) suffix)
    (same : ∀ name, name ∈ Expr.samePositionCalls expr →
      HasResult G (.nonterm name) input) :
    HasResult G expr input := by
  induction expr generalizing input with
  | eps => exact ⟨.ok input, .eps⟩
  | fail => exact ⟨.err, .fail⟩
  | any =>
      cases input with
      | nil => exact ⟨.err, .anyNil⟩
      | cons symbol rest => exact ⟨.ok rest, .anyOk⟩
  | term expected =>
      cases input with
      | nil => exact ⟨.err, .termNil⟩
      | cons actual rest =>
          by_cases hsame : expected = actual
          · subst actual
            exact ⟨.ok rest, .termOk⟩
          · exact ⟨.err, .termNe hsame⟩
  | nonterm name => exact same name (by simp [Expr.samePositionCalls])
  | seq left right ihLeft ihRight =>
      obtain ⟨leftResult, hleft⟩ := ihLeft shorter (fun name hname =>
        same name (by simp [Expr.samePositionCalls, hname]))
      cases leftResult with
      | err => exact ⟨.err, .seqErr hleft⟩
      | ok middle =>
          have hmiddleSuffix : middle <:+ input := eval_remainder_suffix hleft
          have hrightShorter : ∀ suffix, suffix <:+ middle →
              suffix.length < middle.length →
              ∀ name, HasResult G (.nonterm name) suffix := by
            intro suffix hsuffix hlength name
            exact shorter suffix (hsuffix.trans hmiddleSuffix)
              (Nat.lt_of_lt_of_le hlength hmiddleSuffix.length_le) name
          have hrightSame : ∀ name,
              name ∈ Expr.samePositionCalls right →
              HasResult G (.nonterm name) middle := by
            intro name hname
            rcases Nat.lt_or_eq_of_le hmiddleSuffix.length_le with hlt | heq
            · exact shorter middle hmiddleSuffix hlt name
            · have hm : middle = input := hmiddleSuffix.eq_of_length heq
              subst middle
              by_cases hconsumes : Expr.guaranteedConsumes left = true
              · exact (Nat.ne_of_lt
                  (guaranteedConsumes_sound hleft hconsumes) rfl).elim
              · exact same name (by
                  simp [Expr.samePositionCalls, hconsumes, hname])
          obtain ⟨rightResult, hright⟩ :=
            ihRight hrightShorter hrightSame
          exact ⟨rightResult, .seqOk hleft hright⟩
  | alt left right ihLeft ihRight =>
      obtain ⟨leftResult, hleft⟩ := ihLeft shorter (fun name hname =>
        same name (by simp [Expr.samePositionCalls, hname]))
      cases leftResult with
      | ok rest => exact ⟨.ok rest, .altOk hleft⟩
      | err =>
          obtain ⟨rightResult, hright⟩ := ihRight shorter (fun name hname =>
            same name (by simp [Expr.samePositionCalls, hname]))
          exact ⟨rightResult, .altErr hleft hright⟩
  | notP body ih =>
      obtain ⟨bodyResult, hbody⟩ := ih shorter (fun name hname =>
        same name (by simpa [Expr.samePositionCalls] using hname))
      cases bodyResult with
      | ok rest => exact ⟨.err, .notOk hbody⟩
      | err => exact ⟨.ok input, .notErr hbody⟩

theorem ordered_nonterm_hasResult (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (input : List Sym)
    (shorter : ∀ suffix, suffix <:+ input → suffix.length < input.length →
      ∀ name, HasResult G (.nonterm name) suffix)
    (before after : List (Fin n))
    (horder : schedule.order = before ++ after)
    (hbefore : ∀ name, name ∈ before → HasResult G (.nonterm name) input) :
    ∀ name, name ∈ before ++ after → HasResult G (.nonterm name) input := by
  induction after generalizing before with
  | nil =>
      intro name hname
      exact hbefore name (by simpa using hname)
  | cons caller after ih =>
      have hrule : HasResult G (G.rule caller) input :=
        expr_hasResult_of_calls G shorter (fun callee hcall =>
          hbefore callee (schedule.earlier horder hcall))
      have hcaller : HasResult G (.nonterm caller) input := by
        obtain ⟨result, hresult⟩ := hrule
        exact ⟨result, .nonterm hresult⟩
      have hnewBefore : ∀ name, name ∈ before ++ [caller] →
          HasResult G (.nonterm name) input := by
        intro name hname
        rcases List.mem_append.mp hname with hold | hnew
        · exact hbefore name hold
        · have : name = caller := by simpa using hnew
          subst name
          exact hcaller
      have hnewOrder : schedule.order = (before ++ [caller]) ++ after := by
        simpa [List.append_assoc] using horder
      have hrec := ih (before := before ++ [caller]) hnewOrder hnewBefore
      intro name hname
      exact hrec name (by simpa [List.append_assoc] using hname)

theorem scheduled_suffix_nonterm_hasResult (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (input : List Sym) :
    ∀ suffix, suffix <:+ input → ∀ name,
      HasResult G (.nonterm name) suffix := by
  induction input with
  | nil =>
      have hcurrent := ordered_nonterm_hasResult G schedule []
        (fun suffix _ hlength => by simp at hlength) [] schedule.order
        (by simp) (by simp)
      intro suffix hsuffix name
      have hsuffixNil : suffix = [] := hsuffix.eq_of_length
        (Nat.eq_zero_of_le_zero hsuffix.length_le)
      subst suffix
      exact hcurrent name (by simp [schedule.complete name])
  | cons symbol rest ih =>
      have hshorter : ∀ suffix, suffix <:+ symbol :: rest →
          suffix.length < (symbol :: rest).length →
          ∀ name, HasResult G (.nonterm name) suffix := by
        intro suffix hsuffix hlength name
        exact ih suffix (TableEval.suffix_of_proper_suffix_cons hsuffix hlength) name
      have hcurrent := ordered_nonterm_hasResult G schedule (symbol :: rest)
        hshorter [] schedule.order (by simp) (by simp)
      intro suffix hsuffix name
      by_cases heq : suffix = symbol :: rest
      · subst suffix
        exact hcurrent name (by simp [schedule.complete name])
      · have hlength : suffix.length < (symbol :: rest).length :=
          Nat.lt_of_le_of_ne hsuffix.length_le (fun hlen =>
            heq (hsuffix.eq_of_length hlen))
        exact ih suffix (TableEval.suffix_of_proper_suffix_cons hsuffix hlength) name

/-- Every rank-scheduled finite grammar is relationally total by an induction
independent of `evalTable`. -/
theorem total_of_rankSchedule (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) : Total G := by
  intro expr input
  apply expr_hasResult_of_calls G
  · intro suffix hsuffix hlength name
    exact scheduled_suffix_nonterm_hasResult G schedule input suffix hsuffix name
  · intro name hname
    exact scheduled_suffix_nonterm_hasResult G schedule input input (by simp) name

end RelationalTotality

section RankOrder

def rankBucket (rank : Fin n → Nat) (level : Nat) : List (Fin n) :=
  (FiniteEnum.dedup (List.finRange n)).filter fun name => rank name = level

def rankOrder (rank : Fin n → Nat) : Nat → List (Fin n)
  | 0 => rankBucket rank 0
  | bound + 1 => rankOrder rank bound ++ rankBucket rank (bound + 1)

@[simp] theorem mem_rankBucket (rank : Fin n → Nat) (level : Nat)
    (name : Fin n) : name ∈ rankBucket rank level ↔ rank name = level := by
  simp [rankBucket]

@[simp] theorem mem_rankOrder (rank : Fin n → Nat) (bound : Nat)
    (name : Fin n) : name ∈ rankOrder rank bound ↔ rank name ≤ bound := by
  induction bound with
  | zero => simp [rankOrder]
  | succ bound ih =>
      simp only [rankOrder, List.mem_append, ih, mem_rankBucket]
      omega

theorem rankBucket_nodup (rank : Fin n → Nat) (level : Nat) :
    (rankBucket rank level).Nodup := by
  exact (FiniteEnum.nodup_dedup (List.finRange n)).filter _

theorem rankOrder_nodup (rank : Fin n → Nat) (bound : Nat) :
    (rankOrder rank bound).Nodup := by
  induction bound with
  | zero => exact rankBucket_nodup rank 0
  | succ bound ih =>
      rw [rankOrder, List.nodup_append]
      refine ⟨ih, rankBucket_nodup rank (bound + 1), ?_⟩
      intro left hleft right hright heq
      have hle : rank left ≤ bound := (mem_rankOrder rank bound left).mp hleft
      have hrightRank : rank right = bound + 1 :=
        (mem_rankBucket rank (bound + 1) right).mp hright
      subst right
      omega

theorem pairwise_of_all {α : Type} (relation : α → α → Prop)
    (items : List α)
    (hall : ∀ left, left ∈ items → ∀ right, right ∈ items →
      relation left right) : items.Pairwise relation := by
  induction items with
  | nil => simp
  | cons head tail ih =>
      rw [List.pairwise_cons]
      constructor
      · intro item hitem
        exact hall head (by simp) item (by simp [hitem])
      · exact ih (fun left hleft right hright =>
          hall left (by simp [hleft]) right (by simp [hright]))

theorem rankBucket_pairwise (rank : Fin n → Nat) (level : Nat) :
    (rankBucket rank level).Pairwise fun left right => rank left ≤ rank right := by
  apply pairwise_of_all
  intro left hleft right hright
  rw [(mem_rankBucket rank level left).mp hleft,
    (mem_rankBucket rank level right).mp hright]
  omega

theorem rankOrder_pairwise (rank : Fin n → Nat) (bound : Nat) :
    (rankOrder rank bound).Pairwise fun left right => rank left ≤ rank right := by
  induction bound with
  | zero => exact rankBucket_pairwise rank 0
  | succ bound ih =>
      rw [rankOrder, List.pairwise_append]
      refine ⟨ih, rankBucket_pairwise rank (bound + 1), ?_⟩
      intro left hleft right hright
      have hle : rank left ≤ bound := (mem_rankOrder rank bound left).mp hleft
      have hrightRank : rank right = bound + 1 :=
        (mem_rankBucket rank (bound + 1) right).mp hright
      omega

theorem earlier_of_rankOrder (rank : Fin n → Nat) (bound : Nat)
    {before after : List (Fin n)} {caller callee : Fin n}
    (horder : rankOrder rank bound = before ++ caller :: after)
    (hcallee : rank callee < rank caller)
    (hcomplete : rank callee ≤ bound) : callee ∈ before := by
  have hmem : callee ∈ before ++ caller :: after := by
    rw [← horder]
    exact (mem_rankOrder rank bound callee).2 hcomplete
  rcases List.mem_append.mp hmem with hbefore | hsuffix
  · exact hbefore
  · rcases List.mem_cons.mp hsuffix with heq | hafter
    · subst callee
      omega
    · have hsorted : (before ++ caller :: after).Pairwise
          (fun left right => rank left ≤ rank right) := by
        rw [← horder]
        exact rankOrder_pairwise rank bound
      have hsuffixSorted : (caller :: after).Pairwise
          (fun left right => rank left ≤ rank right) :=
        (List.pairwise_append.mp hsorted).2.1
      have hcallerLe : rank caller ≤ rank callee :=
        (List.pairwise_cons.mp hsuffixSorted).1 callee hafter
      omega

end RankOrder

section GeneratedSchedule

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]

/-- The source rank transported to the canonical finite nonterminal carrier. -/
def canonicalRank
    (name : Fin (FiniteEnum.card (NT Q Gamma d k))) : Nat :=
  ntRank ((canonicalEquiv (Q := Q) (Gamma := Gamma) (d := d) (k := k)).symm name)

omit [FiniteEnum Q] [DecidableEq Q] [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem ntRank_le (name : NT Q Gamma d k) : ntRank name ≤ k + 2 := by
  cases name with
  | state _ | label _ | anyStar => simp [ntRank]
  | path path =>
      dsimp [ntRank]
      have := path.length_le
      omega
  | neighbourhood _ | accepts => simp [ntRank]

omit [DecidableEq Sym] in
theorem canonicalGrammar_call_rank_lt (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk)
    {caller callee : Fin (FiniteEnum.card (NT Q Gamma d k))}
    (hcall : callee ∈ Expr.samePositionCalls
      ((canonicalGrammar A hdistance).rule caller)) :
    canonicalRank callee < canonicalRank caller := by
  change callee ∈ Expr.samePositionCalls
    (transportExpr canonicalEquiv
      ((rawGrammar A hdistance).rule (canonicalEquiv.symm caller))) at hcall
  rw [samePositionCalls_transport] at hcall
  obtain ⟨rawCallee, hrawCall, rfl⟩ := List.mem_map.mp hcall
  simpa [canonicalRank] using
    (rawGrammar_call_rank_lt A hdistance hrawCall)

/-- The generated canonical grammar is ordered by increasing same-position
rank.  The certificate includes `SELF`, whose recursive path call has the
strictly shorter tail rank. -/
def canonicalGrammar_rankSchedule (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) : RankSchedule (canonicalGrammar A hdistance) where
  order := rankOrder canonicalRank (k + 2)
  nodup := rankOrder_nodup canonicalRank (k + 2)
  complete name := (mem_rankOrder canonicalRank (k + 2) name).2 (by
    exact ntRank_le (canonicalEquiv.symm name))
  earlier horder hcall :=
    earlier_of_rankOrder canonicalRank (k + 2) horder
      (canonicalGrammar_call_rank_lt A hdistance hcall)
      (ntRank_le (canonicalEquiv.symm _))

/-- Relational totality is proved by the structural existence induction above;
the executable table evaluator is not used. -/
theorem canonicalGrammar_total (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) : Total (canonicalGrammar A hdistance) :=
  total_of_rankSchedule _ (canonicalGrammar_rankSchedule A hdistance)

theorem rawGrammar_total (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) : Total (rawGrammar A hdistance) :=
  (total_transport_iff canonicalEquiv (rawGrammar A hdistance)).mp
    (canonicalGrammar_total A hdistance)

omit [DecidableEq Sym] in
/-- `Path([])` always succeeds without consuming input. -/
theorem rootPath_ok (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (input : List Sym) :
    Eval (rawGrammar A hdistance) (.nonterm (.path (rootPath d k))) input
      (.ok input) := by
  apply Eval.nonterm
  simpa [rawGrammar, pathRule, rootPath] using
    (Eval.eps : Eval (rawGrammar A hdistance) .eps input (.ok input))

omit [DecidableEq Sym] in
/-- The root fact of a missing neighbourhood rejects because it is the
negative lookahead `!Path([])`, while `Path([])` is epsilon. -/
theorem missing_root_fact_err (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (input : List Sym) :
    Eval (rawGrammar A hdistance)
      (observationFact (Q := Q) (Sym := Sym) (.missing : Unfold d Gamma k)
        (rootPath d k)) input .err := by
  simpa [observationFact, observe, observeAt, rootPath] using
    (Eval.notOk (rootPath_ok A hdistance input))

omit [DecidableEq Sym] in
/-- A top-level missing unfolding can never be the neighbourhood of a run
scaffold.  Its rule starts with the failing root fact above. -/
theorem neighbourhood_missing_err (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (input : List Sym) :
    Eval (rawGrammar A hdistance)
      (.nonterm (.neighbourhood (.missing : Unfold d Gamma k))) input .err := by
  apply Eval.nonterm
  change Eval (rawGrammar A hdistance)
    (neighbourhoodRule (Q := Q) (Sym := Sym) (.missing : Unfold d Gamma k))
    input .err
  unfold neighbourhoodRule
  obtain ⟨rest, hrest⟩ := boundedPath_elems_starts_root d k
  rw [hrest]
  exact Eval.seqErr (missing_root_fact_err A hdistance input)

end GeneratedSchedule

namespace GrammarExamples

def emptyPath : BoundedPath 1 1 := ⟨[], by simp⟩
def childPath : BoundedPath 1 1 := ⟨[0], by simp⟩

def unlabelledRoot : Unfold 1 Bool 1 :=
  .node none (fun _ => .missing)

def labelledRoot : Unfold 1 Bool 1 :=
  .node (some true) (fun _ => .leaf none)

example : observe unlabelledRoot emptyPath = some none := by decide
example : observe unlabelledRoot childPath = none := by decide
example : observe labelledRoot emptyPath = some (some true) := by decide
example : observe labelledRoot childPath = some none := by decide

example (left right : Unfold 1 Bool 1) :
    left = right ↔ ∀ path : BoundedPath 1 1,
      observe left path = observe right path :=
  unfold_eq_iff_observe_all left right

example : NT Unit Bool 1 1 := .accepts

example : (FiniteEnum.elems (α := NT Unit Bool 1 1)).length > 0 := by decide

def selfGrammarMachine : Automaton Bool Unit Unit 1 1 where
  delta _ _ _ := ((), (), fun _ => .self)
  init := ()
  accept _ := true

theorem selfGrammarDistance : selfGrammarMachine.DistanceOk := by
  intro control symbol neighbourhood port path hpath
  simp [selfGrammarMachine] at hpath

example :
    (rawGrammar selfGrammarMachine selfGrammarDistance).rule (.path emptyPath) =
      .eps := by rfl

example : Total (rawGrammar selfGrammarMachine selfGrammarDistance) :=
  rawGrammar_total selfGrammarMachine selfGrammarDistance

example : RankSchedule (canonicalGrammar selfGrammarMachine selfGrammarDistance) :=
  canonicalGrammar_rankSchedule selfGrammarMachine selfGrammarDistance

end GrammarExamples
end Theorem16
end FPRD