Neighbourhood.lean

import FPRDTransfer.Theorem16.Invariants.Path

namespace FPRD
namespace Theorem16

universe u uName uSymbol uItem

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]

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem exactMatch_seq {Name : Type uName} {Symbol : Type uSymbol}
    {G : Grammar Name Symbol} {left right : Expr Name Symbol}
    {input : List Symbol} {leftCondition rightCondition : Prop}
    (hleft : ExactMatch G left input leftCondition)
    (hright : ExactMatch G right input rightCondition) :
    ExactMatch G (.seq left right) input (leftCondition ∧ rightCondition) := by
  apply exactMatch_of_cases
  · rintro ⟨hleftCondition, hrightCondition⟩
    exact Eval.seqOk (hleft.ok_iff.mpr hleftCondition)
      (hright.ok_iff.mpr hrightCondition)
  · intro hcondition
    by_cases hleftCondition : leftCondition
    · exact Eval.seqOk (hleft.ok_iff.mpr hleftCondition)
        (hright.err_iff.mpr (by
          intro hrightCondition
          exact hcondition ⟨hleftCondition, hrightCondition⟩))
    · exact Eval.seqErr (hleft.err_iff.mpr hleftCondition)

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem seqAll_map_exact {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 →
      ExactMatch G (expression item) input (predicate item)) :
    ExactMatch G (Expr.seqAll (items.map expression)) input
      (∀ item, item ∈ items → predicate item) := by
  induction items with
  | nil =>
      apply exactMatch_of_cases
      · intro _
        exact Eval.eps
      · simp
  | cons item items ih =>
      change ExactMatch G
        (.seq (expression item) (Expr.seqAll (items.map expression))) input _
      have hhead := hall item (by simp)
      have htail := ih (fun other hother => hall other (by simp [hother]))
      have hseq := exactMatch_seq hhead htail
      refine ⟨hseq.ok_iff.trans ?_, hseq.err_iff.trans (not_congr ?_)⟩
      · simp
      · simp

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem observeAt_viewAt (S : Scaffold d Gamma) (depth vertex : Nat)
    (ports : List (Fin d)) (hlength : ports.length ≤ depth) :
    observeAt depth (S.viewAt depth vertex) ports hlength =
      match S.follow vertex ports with
      | none => none
      | some endpoint => some (S.label endpoint) := by
  induction depth generalizing vertex ports with
  | zero =>
      cases ports with
      | nil => rfl
      | cons port ports => simp at hlength
  | succ depth ih =>
      cases ports with
      | nil => rfl
      | cons port ports =>
          simp only [Scaffold.follow_cons]
          cases hedge : S.edge vertex port with
          | none => simp [Scaffold.viewAt, observeAt, hedge]
          | some endpoint =>
              simpa [Scaffold.viewAt, observeAt, hedge] using
                ih endpoint ports (Nat.le_of_succ_le_succ hlength)

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem observe_viewAt (S : Scaffold d Gamma) (vertex : Nat)
    (path : BoundedPath d k) :
    observe (S.viewAt k vertex) path =
      match S.follow vertex path.elems with
      | none => none
      | some endpoint => some (S.label endpoint) := by
  exact observeAt_viewAt S k vertex path.elems path.length_le

def pathPresentAt (A : Automaton Sym Q Gamma d k) (word : List Sym)
    (position : Nat) (path : BoundedPath d k) : Prop :=
  ∃ endpoint, (A.run (word.take position)).2.follow
    (A.run (word.take position)).2.top path.elems = some endpoint

def pathLabelledAt (A : Automaton Sym Q Gamma d k) (word : List Sym)
    (position : Nat) (path : BoundedPath d k) (label : Gamma) : Prop :=
  ∃ endpoint, (A.run (word.take position)).2.follow
      (A.run (word.take position)).2.top path.elems = some endpoint ∧
    (A.run (word.take position)).2.label endpoint = some label

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem foldl_step_label_old (A : Automaton Sym Q Gamma d k) :
    ∀ (suffix : List Sym) (config : Q × Scaffold d Gamma) (source : Nat),
      source ≤ config.2.top →
      (suffix.foldl A.step config).2.label source = config.2.label source := by
  intro suffix
  induction suffix with
  | nil => intro config source _; rfl
  | cons symbol suffix ih =>
      intro config source hsource
      simp only [List.foldl_cons]
      rw [ih (A.step config symbol) source]
      · unfold Automaton.step
        apply Scaffold.append_label_old
        omega
      · simp [Automaton.step]
        omega

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem run_append_label_old (A : Automaton Sym Q Gamma d k)
    (initial suffix : List Sym) (source : Nat) (hsource : source ≤ initial.length) :
    (A.run (initial ++ suffix)).2.label source =
      (A.run initial).2.label source := by
  have htop : source ≤ (A.run initial).2.top := by
    rw [Automaton.run_top]
    exact hsource
  unfold Automaton.run
  rw [List.foldl_append]
  exact foldl_step_label_old A suffix _ source htop

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem run_take_label_old (A : Automaton Sym Q Gamma d k)
    (word : List Sym) {earlier later : Nat} (hearlier : earlier ≤ later)
    (hlater : later ≤ word.length) :
    (A.run (word.take later)).2.label earlier =
      (A.run (word.take earlier)).2.label earlier := by
  have htake : (word.take later).take earlier = word.take earlier := by
    simp [List.take_take, Nat.min_eq_left hearlier]
  have hlength : earlier ≤ ((word.take later).take earlier).length := by
    rw [List.length_take, List.length_take]
    apply (Nat.le_min).2
    exact ⟨Nat.le_refl _, (Nat.le_min).2
      ⟨hearlier, Nat.le_trans hearlier hlater⟩⟩
  calc
    (A.run (word.take later)).2.label earlier =
        (A.run ((word.take later).take earlier ++
          (word.take later).drop earlier)).2.label earlier := by
            rw [List.take_append_drop]
    _ = (A.run ((word.take later).take earlier)).2.label earlier :=
      run_append_label_old A _ _ earlier hlength
    _ = (A.run (word.take earlier)).2.label earlier := by rw [htake]

/-- I4 needs path exactness at the current prefix and label exactness at every
possible endpoint, including the current endpoint reached through `SELF`. -/
structure NeighbourhoodContext (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length) : Prop where
  path : ∀ bounded, PathExact A hdistance word position hposition bounded
  label : ∀ endpoint, endpoint ≤ position → ∀ target,
    LabelExact A hdistance (word.take endpoint) target

omit [DecidableEq Sym] in
theorem path_pos_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) :
    ExactMatch (rawGrammar A hdistance) (.pos (.nonterm (.path path)))
      (word.take position).reverse (pathPresentAt A word position path) := by
  let S := (A.run (word.take position)).2
  have hpath := hcontext.path path
  apply exactMatch_of_cases
  · rintro ⟨endpoint, hfollow⟩
    apply pos_ok_of_ok
    apply (hpath.ok_iff (word.take endpoint).reverse).mpr
    exact ⟨endpoint, hfollow,
      path_endpoint_le A word position hposition path endpoint hfollow, rfl⟩
  · intro hmissing
    apply pos_err_of_err
    apply hpath.err_iff.mpr
    cases hfollow : S.follow S.top path.elems with
    | none => rfl
    | some endpoint =>
        exact (hmissing ⟨endpoint, by simpa [S] using hfollow⟩).elim

omit [DecidableEq Sym] in
theorem path_label_body_ok (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) (label : Gamma)
    (hlabelled : pathLabelledAt A word position path label) :
    ∃ rest, Eval (rawGrammar A hdistance)
      (.seq (.nonterm (.path path)) (.nonterm (.label label)))
      (word.take position).reverse (.ok rest) := by
  rcases hlabelled with ⟨endpoint, hfollow, hlabel⟩
  have hle := path_endpoint_le A word position hposition path endpoint hfollow
  have hendpointWord : endpoint ≤ word.length := Nat.le_trans hle hposition
  have hlabel' : (A.run (word.take endpoint)).2.label
      (A.run (word.take endpoint)).2.top = some label := by
    rw [Automaton.run_top, List.length_take,
      Nat.min_eq_left hendpointWord, ← run_take_label_old A word hle hposition]
    exact hlabel
  refine ⟨(word.take endpoint).reverse, ?_⟩
  exact Eval.seqOk (middle := (word.take endpoint).reverse)
    (((hcontext.path path).ok_iff _).mpr ⟨endpoint, hfollow, hle, rfl⟩)
    (((hcontext.label endpoint hle label).ok_iff).mpr hlabel')

omit [DecidableEq Sym] in
theorem path_label_body_err (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) (label : Gamma)
    (hnot : ¬pathLabelledAt A word position path label) :
    Eval (rawGrammar A hdistance)
      (.seq (.nonterm (.path path)) (.nonterm (.label label)))
      (word.take position).reverse .err := by
  let S := (A.run (word.take position)).2
  cases hfollow : S.follow S.top path.elems with
  | none =>
      apply Eval.seqErr
      apply (hcontext.path path).err_iff.mpr
      simpa [S] using hfollow
  | some endpoint =>
      have hfollow' : (A.run (word.take position)).2.follow
          (A.run (word.take position)).2.top path.elems = some endpoint := by
        simpa [S] using hfollow
      have hle := path_endpoint_le A word position hposition path endpoint hfollow'
      apply Eval.seqOk
      · exact ((hcontext.path path).ok_iff _).mpr
          ⟨endpoint, hfollow', hle, rfl⟩
      · apply (hcontext.label endpoint hle label).err_iff.mpr
        intro hlabel
        have hendpointWord : endpoint ≤ word.length := Nat.le_trans hle hposition
        have hlabelEarly : (A.run (word.take endpoint)).2.label endpoint =
            some label := by
          simpa [Automaton.run_top, List.length_take,
            Nat.min_eq_left hendpointWord] using hlabel
        have hlabel' : (A.run (word.take position)).2.label endpoint =
            some label := by
          rw [run_take_label_old A word hle hposition]
          exact hlabelEarly
        exact hnot ⟨endpoint, hfollow', hlabel'⟩

omit [DecidableEq Sym] in
theorem path_label_pos_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) (label : Gamma) :
    ExactMatch (rawGrammar A hdistance)
      (.pos (.seq (.nonterm (.path path)) (.nonterm (.label label))))
      (word.take position).reverse (pathLabelledAt A word position path label) := by
  apply exactMatch_of_cases
  · intro hlabelled
    rcases path_label_body_ok A hdistance word position hposition hcontext path
      label hlabelled with ⟨rest, heval⟩
    exact pos_ok_of_ok heval
  · intro hnot
    exact pos_err_of_err
      (path_label_body_err A hdistance word position hposition hcontext path label hnot)

omit [DecidableEq Sym] in
theorem path_label_not_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) (label : Gamma) :
    ExactMatch (rawGrammar A hdistance)
      (.notP (.seq (.nonterm (.path path)) (.nonterm (.label label))))
      (word.take position).reverse
      (¬pathLabelledAt A word position path label) := by
  classical
  apply exactMatch_of_cases
  · intro hnot
    exact Eval.notErr
      (path_label_body_err A hdistance word position hposition hcontext path label hnot)
  · intro hnnot
    by_cases hlabelled : pathLabelledAt A word position path label
    · rcases path_label_body_ok A hdistance word position hposition hcontext path
        label hlabelled with ⟨rest, heval⟩
      exact Eval.notOk heval
    · exact (hnnot hlabelled).elim

omit [DecidableEq Sym] in
theorem path_not_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) :
    ExactMatch (rawGrammar A hdistance) (.notP (.nonterm (.path path)))
      (word.take position).reverse (¬pathPresentAt A word position path) := by
  classical
  apply exactMatch_of_cases
  · intro hnot
    apply Eval.notErr
    apply (hcontext.path path).err_iff.mpr
    let S := (A.run (word.take position)).2
    cases hfollow : S.follow S.top path.elems with
    | none => rfl
    | some endpoint =>
        exact (hnot ⟨endpoint, by simpa [S] using hfollow⟩).elim
  · intro hnnot
    by_cases hpresent : pathPresentAt A word position path
    · rcases hpresent with ⟨endpoint, hfollow⟩
      apply Eval.notOk
      exact ((hcontext.path path).ok_iff _).mpr
        ⟨endpoint, hfollow,
          path_endpoint_le A word position hposition path endpoint hfollow, rfl⟩
    · exact (hnnot hpresent).elim

omit [DecidableEq Sym] in
theorem path_unlabelled_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (path : BoundedPath d k) :
    ExactMatch (rawGrammar A hdistance)
      (.seq (.pos (.nonterm (.path path)))
        (Expr.seqAll ((FiniteEnum.elems (α := Gamma)).map fun label =>
          .notP (.seq (.nonterm (.path path)) (.nonterm (.label label))))))
      (word.take position).reverse
      (pathPresentAt A word position path ∧
        ∀ label, ¬pathLabelledAt A word position path label) := by
  have hpresent := path_pos_exact A hdistance word position hposition hcontext path
  have hlabels := seqAll_map_exact (FiniteEnum.elems (α := Gamma))
    (fun label => Expr.notP
      (.seq (.nonterm (NT.path path)) (.nonterm (.label label))))
    (word.take position).reverse
    (fun label => ¬pathLabelledAt A word position path label)
    (fun label _ => path_label_not_exact A hdistance word position hposition
      hcontext path label)
  have hseq := exactMatch_seq hpresent hlabels
  refine ⟨hseq.ok_iff.trans ?_, hseq.err_iff.trans (not_congr ?_)⟩
  · constructor
    · rintro ⟨hpath, hall⟩
      exact ⟨hpath, fun label => hall label (FiniteEnum.complete label)⟩
    · rintro ⟨hpath, hall⟩
      exact ⟨hpath, fun label _ => hall label⟩
  · constructor
    · rintro ⟨hpath, hall⟩
      exact ⟨hpath, fun label => hall label (FiniteEnum.complete label)⟩
    · rintro ⟨hpath, hall⟩
      exact ⟨hpath, fun label _ => hall label⟩

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem path_unlabelled_iff_observe (A : Automaton Sym Q Gamma d k)
    (word : List Sym) (position : Nat) (path : BoundedPath d k) :
    (pathPresentAt A word position path ∧
      ∀ label, ¬pathLabelledAt A word position path label) ↔
    observe ((A.run (word.take position)).2.viewAt k
      (A.run (word.take position)).2.top) path = some none := by
  let S := (A.run (word.take position)).2
  rw [observe_viewAt]
  cases hfollow : S.follow S.top path.elems with
  | none => simp [pathPresentAt, pathLabelledAt, S, hfollow]
  | some endpoint =>
      cases hlabel : S.label endpoint with
      | none => simp [pathPresentAt, pathLabelledAt, S, hfollow, hlabel]
      | some label =>
          constructor
          · rintro ⟨_, hall⟩
            exact (hall label ⟨endpoint, by simpa [S] using hfollow,
              by simpa [S] using hlabel⟩).elim
          · intro himpossible
            simp only [Option.some.injEq] at himpossible
            have hlabel' : (A.run (word.take position)).2.label endpoint =
                some label := by simpa [S] using hlabel
            rw [hlabel'] at himpossible
            contradiction

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem path_labelled_iff_observe (A : Automaton Sym Q Gamma d k)
    (word : List Sym) (position : Nat) (path : BoundedPath d k)
    (label : Gamma) :
    pathLabelledAt A word position path label ↔
      observe ((A.run (word.take position)).2.viewAt k
        (A.run (word.take position)).2.top) path = some (some label) := by
  let S := (A.run (word.take position)).2
  rw [observe_viewAt]
  cases hfollow : S.follow S.top path.elems with
  | none => simp [pathLabelledAt, S, hfollow]
  | some endpoint =>
      simp [pathLabelledAt, S, hfollow]

omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
  [FiniteEnum Gamma] [DecidableEq Gamma] in
theorem path_absent_iff_observe (A : Automaton Sym Q Gamma d k)
    (word : List Sym) (position : Nat) (path : BoundedPath d k) :
    (¬pathPresentAt A word position path) ↔
      observe ((A.run (word.take position)).2.viewAt k
        (A.run (word.take position)).2.top) path = none := by
  let S := (A.run (word.take position)).2
  rw [observe_viewAt]
  cases hfollow : S.follow S.top path.elems with
  | none => simp [pathPresentAt, S, hfollow]
  | some endpoint => simp [pathPresentAt, S, hfollow]

omit [DecidableEq Sym] in
theorem observationFact_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (neighbourhood : Unfold d Gamma k) (path : BoundedPath d k) :
    ExactMatch (rawGrammar A hdistance)
      (observationFact (Q := Q) (Sym := Sym) neighbourhood path)
      (word.take position).reverse
      (observe neighbourhood path =
        observe ((A.run (word.take position)).2.viewAt k
          (A.run (word.take position)).2.top) path) := by
  unfold observationFact
  cases hobs : observe neighbourhood path with
  | none =>
      have hexact := path_not_exact A hdistance word position hposition hcontext path
      refine ⟨hexact.ok_iff.trans ?_, hexact.err_iff.trans (not_congr ?_)⟩
      · simpa [hobs, eq_comm] using
          (path_absent_iff_observe A word position path)
      · simpa [hobs, eq_comm] using
          (path_absent_iff_observe A word position path)
  | some observation =>
      cases observation with
      | none =>
          have hexact := path_unlabelled_exact A hdistance word position hposition
            hcontext path
          refine ⟨hexact.ok_iff.trans ?_, hexact.err_iff.trans (not_congr ?_)⟩
          · simpa [hobs, eq_comm] using
              (path_unlabelled_iff_observe A word position path)
          · simpa [hobs, eq_comm] using
              (path_unlabelled_iff_observe A word position path)
      | some label =>
          have hexact := path_label_pos_exact A hdistance word position hposition
            hcontext path label
          refine ⟨hexact.ok_iff.trans ?_, hexact.err_iff.trans (not_congr ?_)⟩
          · simpa [hobs, eq_comm] using
              (path_labelled_iff_observe A word position path label)
          · simpa [hobs, eq_comm] using
              (path_labelled_iff_observe A word position path label)

omit [DecidableEq Sym] in
/-- Conditional I4: exact paths at the current prefix plus exact labels at all
reachable endpoints make the finite observation conjunction extensional. -/
theorem neighbourhood_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length)
    (hcontext : NeighbourhoodContext A hdistance word position hposition)
    (neighbourhood : Unfold d Gamma k) :
    NeighbourhoodExact A hdistance (word.take position) neighbourhood := by
  let actual := (A.run (word.take position)).2.viewAt k
    (A.run (word.take position)).2.top
  have hsequence := seqAll_map_exact
    (FiniteEnum.elems (α := BoundedPath d k))
    (observationFact (Q := Q) (Sym := Sym) neighbourhood)
    (word.take position).reverse
    (fun path => observe neighbourhood path = observe actual path)
    (fun path _ => observationFact_exact A hdistance word position hposition
      hcontext neighbourhood path)
  have hcondition :
      (∀ path, path ∈ FiniteEnum.elems (α := BoundedPath d k) →
        observe neighbourhood path = observe actual path) ↔
      actual = neighbourhood := by
    constructor
    · intro hall
      symm
      apply (unfold_eq_iff_observe_all neighbourhood actual).2
      intro path
      exact hall path (FiniteEnum.complete path)
    · intro heq path _
      rw [heq]
  have hnontermOk := eval_nonterm_iff (rawGrammar A hdistance)
    (NT.neighbourhood neighbourhood) (word.take position).reverse
    (.ok (word.take position).reverse)
  have hnontermErr := eval_nonterm_iff (rawGrammar A hdistance)
    (NT.neighbourhood neighbourhood) (word.take position).reverse .err
  refine ⟨?_, ?_⟩
  · simpa [rawGrammar, neighbourhoodRule, actual] using
      hnontermOk.trans (hsequence.ok_iff.trans hcondition)
  · simpa [rawGrammar, neighbourhoodRule, actual] using
      hnontermErr.trans (hsequence.err_iff.trans (not_congr hcondition))

/-- The four exact invariants at one prefix of one ambient word. -/
structure PrefixExactAt (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length) : Prop where
  state : ∀ control, StateExact A hdistance (word.take position) control
  label : ∀ target, LabelExact A hdistance (word.take position) target
  neighbourhood : ∀ shape,
    NeighbourhoodExact A hdistance (word.take position) shape
  path : ∀ bounded, PathExact A hdistance word position hposition bounded

/-- Simultaneous strong-prefix closure in dependency order: state and label at
the current position, path using strictly earlier guards, then neighbourhood
using current paths and labels at every endpoint. -/
theorem prefix_exact_at (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
    (hposition : position ≤ word.length) :
    PrefixExactAt A hdistance word position hposition := by
  cases position with
  | zero =>
      have hstate : ∀ control, StateExact A hdistance (word.take 0) control := by
        intro control
        simpa using state_nil_exact A hdistance control
      have hlabel : ∀ target, LabelExact A hdistance (word.take 0) target := by
        intro target
        simpa using label_nil_exact A hdistance target
      have hearlier : EarlierGuardContext A hdistance word 0 := by
        refine ⟨?_⟩
        intro earlier hearlier
        omega
      have hpath : ∀ bounded,
          PathExact A hdistance word 0 hposition bounded := by
        intro bounded
        exact path_exact A hdistance word 0 hposition hearlier bounded
      have hneighbourhoodContext :
          NeighbourhoodContext A hdistance word 0 hposition := by
        refine ⟨hpath, ?_⟩
        intro endpoint hendpoint target
        ·
          have : endpoint = 0 := Nat.eq_zero_of_le_zero hendpoint
          subst endpoint
          exact hlabel target
      have hneighbourhood : ∀ shape,
          NeighbourhoodExact A hdistance (word.take 0) shape := by
        intro shape
        exact neighbourhood_exact A hdistance word 0 hposition
          hneighbourhoodContext shape
      exact ⟨hstate, hlabel, hneighbourhood, hpath⟩
  | succ predecessor =>
      have hpredecessor : predecessor < word.length := by omega
      have hpast := prefix_exact_at A hdistance word predecessor
        (Nat.le_of_lt hpredecessor)
      have hguard : PrefixGuardContext A hdistance
          (word.take predecessor) := ⟨hpast.state, hpast.neighbourhood⟩
      have hprefix : word.take (predecessor + 1) =
          word.take predecessor ++ [word[predecessor]] :=
        List.take_succ_eq_append_getElem hpredecessor
      have hstate : ∀ control,
          StateExact A hdistance (word.take (predecessor + 1)) control := by
        intro control
        rw [hprefix]
        exact state_step_exact A hdistance (word.take predecessor)
          word[predecessor] hguard control
      have hlabel : ∀ target,
          LabelExact A hdistance (word.take (predecessor + 1)) target := by
        intro target
        rw [hprefix]
        exact label_step_exact A hdistance (word.take predecessor)
          word[predecessor] hguard target
      have hearlier : EarlierGuardContext A hdistance word
          (predecessor + 1) := by
        refine ⟨?_⟩
        intro earlier hearlier
        ·
          have hearlierWord : earlier ≤ word.length :=
            Nat.le_trans (Nat.le_of_lt hearlier) hposition
          have hexact := prefix_exact_at A hdistance word earlier hearlierWord
          exact ⟨hexact.state, hexact.neighbourhood⟩
      have hpath : ∀ bounded,
          PathExact A hdistance word (predecessor + 1) hposition bounded := by
        intro bounded
        exact path_exact A hdistance word (predecessor + 1) hposition
          hearlier bounded
      have hneighbourhoodContext : NeighbourhoodContext A hdistance word
          (predecessor + 1) hposition := by
        refine ⟨hpath, ?_⟩
        intro endpoint hendpoint target
        ·
          by_cases hcurrent : endpoint = predecessor + 1
          · subst endpoint
            exact hlabel target
          · have hearlier : endpoint < predecessor + 1 :=
              Nat.lt_of_le_of_ne hendpoint hcurrent
            have hendpointWord : endpoint ≤ word.length :=
              Nat.le_trans hendpoint hposition
            exact (prefix_exact_at A hdistance word endpoint hendpointWord).label target
      have hneighbourhood : ∀ shape,
          NeighbourhoodExact A hdistance (word.take (predecessor + 1)) shape := by
        intro shape
        exact neighbourhood_exact A hdistance word (predecessor + 1) hposition
          hneighbourhoodContext shape
      exact ⟨hstate, hlabel, hneighbourhood, hpath⟩
termination_by position

/-- Unconditional all-prefix I1--I4 package at a complete word. -/
theorem prefix_exact (A : Automaton Sym Q Gamma d k)
    (hdistance : A.DistanceOk) (word : List Sym) :
    PrefixExactAt A hdistance word word.length (Nat.le_refl _) :=
  prefix_exact_at A hdistance word word.length (Nat.le_refl _)

omit [DecidableEq Sym] in
/-- Named Task-5c fixture: the impossible top-level missing neighbourhood still
rejects because the exhaustive conjunction starts with `!Path([])`. -/
theorem top_missing_neighbourhood_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 :=
  neighbourhood_missing_err A hdistance input

end Theorem16
end FPRD