Reachability.lean

import FPRDTransfer.Theorem16.Normalize

namespace FPRD

namespace Scaffold

variable {d : Nat} {Gamma : Type u}

/-- Generated scaffold edges never point above their source.  Unlike strict
`Backward`, this includes the self-loop created by `Target.self`. -/
def NonForward (S : Scaffold d Gamma) : Prop :=
  ∀ v port target, S.edge v port = some target → target ≤ v

theorem base_nonforward (d : Nat) (Gamma : Type u) :
    (Scaffold.base d Gamma).NonForward := by
  intro v port target h
  simp [Scaffold.base] at h

theorem follow_le_nonforward (S : Scaffold d Gamma) (hnf : S.NonForward) :
    ∀ (path : List (Fin d)) (source target : Nat),
      S.follow source path = some target → target ≤ source := by
  intro path
  induction path with
  | nil =>
      intro source target h
      simp [Scaffold.follow_nil] at h
      omega
  | cons port path ih =>
      intro source target h
      rw [Scaffold.follow_cons] at h
      cases hedge : S.edge source port with
      | none => rw [hedge] at h; simp at h
      | some middle =>
          rw [hedge] at h
          exact Nat.le_trans (ih middle target h) (hnf source port middle hedge)

/-- Appending preserves non-forwardness for old paths, missing targets, and
`SELF`; no self-free side condition is needed. -/
theorem append_nonforward (S : Scaffold d Gamma) (hnf : S.NonForward)
    (label : Gamma) (targets : Fin d → Target d) :
    (S.append label targets).NonForward := by
  intro source port target hedge
  by_cases hnew : source = S.top + 1
  · subst source
    rw [Scaffold.append_edge_new] at hedge
    cases htarget : targets port with
    | path path =>
        rw [htarget] at hedge
        simp only [Scaffold.resolve] at hedge
        exact Nat.le_trans (follow_le_nonforward S hnf path S.top target hedge)
          (Nat.le_succ S.top)
    | self =>
        rw [htarget] at hedge
        simp [Scaffold.resolve] at hedge
        omega
    | missing =>
        rw [htarget] at hedge
        simp [Scaffold.resolve] at hedge
  · rw [Scaffold.append_edge_old S label targets hnew port] at hedge
    exact hnf source port target hedge

end Scaffold

namespace Automaton

/-- Every generated run scaffold is non-forward, including runs whose
transitions emit `SELF`. -/
theorem run_nonforward (A : Automaton Sym Q Gamma d k) (word : List Sym) :
    (A.run word).2.NonForward := by
  have fold_nonforward : ∀ (suffix : List Sym)
      (config : Q × Scaffold d Gamma), config.2.NonForward →
      (suffix.foldl A.step config).2.NonForward := by
    intro suffix
    induction suffix with
    | nil => intro config hconfig; exact hconfig
    | cons symbol rest ih =>
        intro config hconfig
        apply ih (A.step config symbol)
        unfold Automaton.step
        exact Scaffold.append_nonforward _ hconfig _ _
  exact fold_nonforward word (A.init, Scaffold.base d Gamma)
    (Scaffold.base_nonforward d Gamma)

end Automaton

namespace Theorem16
namespace ReachabilityExamples

def oldPathScaffold : Scaffold 1 Unit :=
  (Scaffold.base 1 Unit).append () (fun _ => .path [])

def missingScaffold : Scaffold 1 Unit :=
  (Scaffold.base 1 Unit).append () (fun _ => .missing)

def selfScaffold : Scaffold 1 Unit :=
  (Scaffold.base 1 Unit).append () (fun _ => .self)

example : oldPathScaffold.edge oldPathScaffold.top 0 = some 0 := by decide

example : missingScaffold.edge missingScaffold.top 0 = none := by decide

example : selfScaffold.edge selfScaffold.top 0 = some selfScaffold.top := by decide

example : oldPathScaffold.NonForward := by
  exact Scaffold.append_nonforward _ (Scaffold.base_nonforward 1 Unit) _ _

example : missingScaffold.NonForward := by
  exact Scaffold.append_nonforward _ (Scaffold.base_nonforward 1 Unit) _ _

example : selfScaffold.NonForward := by
  exact Scaffold.append_nonforward _ (Scaffold.base_nonforward 1 Unit) _ _

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

example (word : List Bool) : (selfMachine.run word).2.NonForward :=
  Automaton.run_nonforward selfMachine word

end ReachabilityExamples
end Theorem16
end FPRD