Research source · Plain text
Path.lean
site/public/formal/persistent-stacks/lean/FPRDTransfer/Theorem16/Invariants/Path.lean
766 lines. Source is displayed for inspection; it is not executed by this page.
File fingerprint
SHA-256: 0e9995447e0ee46541f20593199ee60a59c5d113044df303b25b455d7cf4d0ed
import FPRDTransfer.Theorem16.Invariants.StateLabel
namespace FPRD
namespace Theorem16
universe u
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 exact Task 5b result. Success names the scaffold endpoint `j ≤ i`
and leaves precisely the reversed prefix ending at `j`; failure means that the
bounded port word has no endpoint. -/
structure PathExact (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
(word : List Sym) (position : Nat) (hposition : position ≤ word.length)
(path : BoundedPath d k) : Prop where
ok_iff : ∀ rest,
Eval (rawGrammar A hdistance) (.nonterm (.path path))
(word.take position).reverse (.ok rest) ↔
∃ endpoint,
(A.run (word.take position)).2.follow
(A.run (word.take position)).2.top path.elems = some endpoint ∧
endpoint ≤ position ∧ rest = (word.take endpoint).reverse
err_iff :
Eval (rawGrammar A hdistance) (.nonterm (.path path))
(word.take position).reverse .err ↔
(A.run (word.take position)).2.follow
(A.run (word.take position)).2.top path.elems = none
/-- State and neighbourhood facts available strictly before `position`.
Task 5c supplies this context while closing the simultaneous induction. -/
structure EarlierGuardContext (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (word : List Sym) (position : Nat) : Prop where
guard : ∀ earlier, earlier < position →
PrefixGuardContext A hdistance (word.take earlier)
omit [DecidableEq Sym] in
theorem EarlierGuardContext.mono (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (word : List Sym) {earlier later : Nat}
(hcontext : EarlierGuardContext A hdistance word later)
(hle : earlier ≤ later) : EarlierGuardContext A hdistance word earlier where
guard index hindex := hcontext.guard index (Nat.lt_of_lt_of_le hindex hle)
def pathResult (A : Automaton Sym Q Gamma d k) (word : List Sym)
(position : Nat) (path : BoundedPath d k) : Result Sym :=
match (A.run (word.take position)).2.follow
(A.run (word.take position)).2.top path.elems with
| none => .err
| some endpoint => .ok (word.take endpoint).reverse
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem path_endpoint_le (A : Automaton Sym Q Gamma d k)
(word : List Sym) (position : Nat) (hposition : position ≤ word.length)
(path : BoundedPath d k) (endpoint : Nat)
(hfollow : (A.run (word.take position)).2.follow
(A.run (word.take position)).2.top path.elems = some endpoint) :
endpoint ≤ position := by
have hle := Scaffold.follow_le_nonforward (A.run (word.take position)).2
(Automaton.run_nonforward A (word.take position)) path.elems
(A.run (word.take position)).2.top endpoint hfollow
simpa [Automaton.run_top, List.length_take, Nat.min_eq_left hposition] using hle
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem foldl_step_edge_old (A : Automaton Sym Q Gamma d k) :
∀ (suffix : List Sym) (config : Q × Scaffold d Gamma)
(source : Nat) (port : Fin d), source ≤ config.2.top →
(suffix.foldl A.step config).2.edge source port = config.2.edge source port := by
intro suffix
induction suffix with
| nil => intro config source port _; rfl
| cons symbol suffix ih =>
intro config source port hsource
simp only [List.foldl_cons]
rw [ih (A.step config symbol) source port]
· unfold Automaton.step
apply Scaffold.append_edge_old
omega
· simp [Automaton.step]
omega
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem run_append_edge_old (A : Automaton Sym Q Gamma d k)
(initial suffix : List Sym) (source : Nat) (port : Fin d)
(hsource : source ≤ initial.length) :
(A.run (initial ++ suffix)).2.edge source port =
(A.run initial).2.edge source port := 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_edge_old A suffix _ source port htop
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem run_append_follow_old (A : Automaton Sym Q Gamma d k)
(initial suffix : List Sym) (ports : List (Fin d)) (source : Nat)
(hsource : source ≤ initial.length) :
(A.run (initial ++ suffix)).2.follow source ports =
(A.run initial).2.follow source ports := by
induction ports generalizing source with
| nil => rfl
| cons port ports ih =>
rw [Scaffold.follow_cons, Scaffold.follow_cons,
run_append_edge_old A initial suffix source port hsource]
cases hedge : (A.run initial).2.edge source port with
| none => rfl
| some next =>
apply ih next
exact Nat.le_trans
((Automaton.run_nonforward A initial) source port next hedge) hsource
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem run_take_follow_old (A : Automaton Sym Q Gamma d k)
(word : List Sym) {earlier later : Nat} (hearlier : earlier ≤ later)
(hlater : later ≤ word.length) (ports : List (Fin d)) :
(A.run (word.take later)).2.follow earlier ports =
(A.run (word.take earlier)).2.follow earlier ports := 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.follow earlier ports =
(A.run ((word.take later).take earlier ++
(word.take later).drop earlier)).2.follow earlier ports := by
rw [List.take_append_drop]
_ = (A.run ((word.take later).take earlier)).2.follow earlier ports :=
run_append_follow_old A _ _ ports earlier hlength
_ = (A.run (word.take earlier)).2.follow earlier ports := by rw [htake]
def currentTransitionInput (A : Automaton Sym Q Gamma d k)
(stem : List Sym) (symbol : Sym) : TransitionInput Sym Q Gamma d k :=
((A.run stem).1, symbol,
(A.run stem).2.viewAt k (A.run stem).2.top)
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem pathAlternative_eq_guard_seq (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (tail : BoundedPath d k) (port : Fin d)
(input : TransitionInput Sym Q Gamma d k) :
∃ body, pathAlternative A hdistance tail port input =
.seq (transitionExpr input.1 input.2.1 input.2.2) body := by
unfold pathAlternative
split <;> exact ⟨_, rfl⟩
theorem pathAlternative_nonactual_err (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(hcontext : PrefixGuardContext A hdistance stem)
(tail : BoundedPath d k) (port : Fin d)
(input : TransitionInput Sym Q Gamma d k)
(hne : input ≠ currentTransitionInput A stem symbol) :
Eval (rawGrammar A hdistance) (pathAlternative A hdistance tail port input)
(symbol :: stem.reverse) .err := by
have hguard := (transitionExpr_exact A hdistance stem symbol hcontext
input.1 input.2.1 input.2.2).err_iff.mpr
(by
intro hmatch
apply hne
apply Prod.ext
· exact hmatch.2.1.symm
· apply Prod.ext
· exact hmatch.1
· exact hmatch.2.2.symm)
obtain ⟨body, hbody⟩ := pathAlternative_eq_guard_seq A hdistance tail port input
rw [hbody]
exact Eval.seqErr hguard
theorem pathAlternatives_ok_of_actual (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(hcontext : PrefixGuardContext A hdistance stem)
(tail : BoundedPath d k) (port : Fin d) (rest : List Sym)
(hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port
(currentTransitionInput A stem symbol))
(symbol :: stem.reverse) (.ok rest)) :
Eval (rawGrammar A hdistance)
(Expr.altAll ((transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
(d := d) (k := k)).map (pathAlternative A hdistance tail port)))
(symbol :: stem.reverse) (.ok rest) := by
have hmember : currentTransitionInput A stem symbol ∈
transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
(d := d) (k := k) := FiniteEnum.complete _
generalize transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
(d := d) (k := k) = inputs at hmember ⊢
induction inputs with
| nil => simp at hmember
| cons input inputs ih =>
by_cases heq : input = currentTransitionInput A stem symbol
· subst input
exact Eval.altOk hactual
· apply Eval.altErr
· exact pathAlternative_nonactual_err A hdistance stem symbol hcontext
tail port input heq
· apply ih
exact (List.mem_cons.mp hmember).resolve_left (Ne.symm heq)
theorem pathAlternatives_err_of_actual (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(hcontext : PrefixGuardContext A hdistance stem)
(tail : BoundedPath d k) (port : Fin d)
(hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port
(currentTransitionInput A stem symbol))
(symbol :: stem.reverse) .err) :
Eval (rawGrammar A hdistance)
(Expr.altAll ((transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
(d := d) (k := k)).map (pathAlternative A hdistance tail port)))
(symbol :: stem.reverse) .err := by
apply altAll_err_of_all
intro expression hexpression
rcases List.mem_map.mp hexpression with ⟨input, _, rfl⟩
by_cases heq : input = currentTransitionInput A stem symbol
· subst input
exact hactual
· exact pathAlternative_nonactual_err A hdistance stem symbol hcontext
tail port input heq
theorem pathAlternatives_of_actual (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(hcontext : PrefixGuardContext A hdistance stem)
(tail : BoundedPath d k) (port : Fin d) (result : Result Sym)
(hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port
(currentTransitionInput A stem symbol))
(symbol :: stem.reverse) result) :
Eval (rawGrammar A hdistance)
(Expr.altAll ((transitionInputs (Sym := Sym) (Q := Q) (Gamma := Gamma)
(d := d) (k := k)).map (pathAlternative A hdistance tail port)))
(symbol :: stem.reverse) result := by
cases result with
| ok rest =>
exact pathAlternatives_ok_of_actual A hdistance stem symbol hcontext
tail port rest hactual
| err =>
exact pathAlternatives_err_of_actual A hdistance stem symbol hcontext
tail port hactual
theorem current_transition_ok (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(hcontext : PrefixGuardContext A hdistance stem) :
Eval (rawGrammar A hdistance)
(transitionExpr (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2)
(symbol :: stem.reverse) (.ok (symbol :: stem.reverse)) := by
exact (transitionExpr_exact A hdistance stem symbol hcontext
(currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2).ok_iff.mpr ⟨rfl, rfl, rfl⟩
omit [DecidableEq Sym] in
theorem path_zero_nonempty_eval (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (port : Fin d) (ports : List (Fin d))
(hports : (port :: ports).length ≤ k) :
Eval (rawGrammar A hdistance)
(.nonterm (.path (⟨port :: ports, hports⟩ : BoundedPath d k))) [] .err := by
apply Eval.nonterm
simp only [rawGrammar, pathRule]
apply altAll_err_of_all
intro expression hexpression
rcases List.mem_map.mp hexpression with ⟨input, _, rfl⟩
let tail : BoundedPath d k := ⟨ports, by
exact Nat.le_trans (by simp) hports⟩
obtain ⟨body, hbody⟩ := pathAlternative_eq_guard_seq A hdistance tail port input
rw [hbody]
exact Eval.seqErr (transitionExpr_nil_err input.1 input.2.1 input.2.2)
omit [DecidableEq Sym] in
theorem pathAlternative_missing_eval (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(tail : BoundedPath d k) (port : Fin d)
(htarget : (A.delta (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2).2.2 port = .missing)
(hguard : Eval (rawGrammar A hdistance)
(transitionExpr (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2)
(symbol :: stem.reverse) (.ok (symbol :: stem.reverse))) :
Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port (currentTransitionInput A stem symbol))
(symbol :: stem.reverse) .err := by
unfold pathAlternative
split <;> simp_all
exact Eval.seqOk hguard Eval.fail
omit [DecidableEq Sym] in
theorem pathAlternative_self_eval (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(tail : BoundedPath d k) (port : Fin d) (result : Result Sym)
(htarget : (A.delta (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2).2.2 port = .self)
(hguard : Eval (rawGrammar A hdistance)
(transitionExpr (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2)
(symbol :: stem.reverse) (.ok (symbol :: stem.reverse)))
(htail : Eval (rawGrammar A hdistance) (.nonterm (.path tail))
(symbol :: stem.reverse) result) :
Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port (currentTransitionInput A stem symbol))
(symbol :: stem.reverse) result := by
unfold pathAlternative
split <;> simp_all
exact Eval.seqOk hguard htail
omit [DecidableEq Sym] in
theorem pathAlternative_path_eval (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (stem : List Sym) (symbol : Sym)
(tail : BoundedPath d k) (port : Fin d) (oldPath : List (Fin d))
(result : Result Sym)
(htarget : (A.delta (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2).2.2 port = .path oldPath)
(hguard : Eval (rawGrammar A hdistance)
(transitionExpr (currentTransitionInput A stem symbol).1
(currentTransitionInput A stem symbol).2.1
(currentTransitionInput A stem symbol).2.2)
(symbol :: stem.reverse) (.ok (symbol :: stem.reverse)))
(hbody : Eval (rawGrammar A hdistance)
(.seq (.term symbol)
(.seq (.nonterm (.path (⟨oldPath, hdistance _ _ _ port oldPath htarget⟩ :
BoundedPath d k))) (.nonterm (.path tail))))
(symbol :: stem.reverse) result) :
Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port (currentTransitionInput A stem symbol))
(symbol :: stem.reverse) result := by
unfold pathAlternative
split
next generatedPath hgenerated =>
have hpaths : generatedPath = oldPath :=
Target.path.inj (hgenerated.symm.trans htarget)
subst generatedPath
exact Eval.seqOk hguard hbody
next hgenerated =>
cases hgenerated.symm.trans htarget
next hgenerated =>
cases hgenerated.symm.trans htarget
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem run_take_succ (A : Automaton Sym Q Gamma d k) (word : List Sym)
(position : Nat) (hposition : position < word.length) :
A.run (word.take (position + 1)) =
A.step (A.run (word.take position)) word[position] := by
rw [List.take_succ_eq_append_getElem hposition, Automaton.run_append]
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem reverse_take_succ (word : List Sym) (position : Nat)
(hposition : position < word.length) :
(word.take (position + 1)).reverse =
word[position] :: (word.take position).reverse := by
rw [List.take_succ_eq_append_getElem hposition]
simp
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem successor_follow_missing (A : Automaton Sym Q Gamma d k)
(word : List Sym) (position : Nat) (hposition : position < word.length)
(port : Fin d) (ports : List (Fin d))
(htarget : (A.delta (A.run (word.take position)).1 word[position]
((A.run (word.take position)).2.viewAt k
(A.run (word.take position)).2.top)).2.2 port = .missing) :
(A.run (word.take (position + 1))).2.follow
(A.run (word.take (position + 1))).2.top (port :: ports) = none := by
rw [Scaffold.follow_cons, run_take_succ A word position hposition]
simp [Automaton.step, Scaffold.resolve, htarget]
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem successor_follow_self (A : Automaton Sym Q Gamma d k)
(word : List Sym) (position : Nat) (hposition : position < word.length)
(port : Fin d) (ports : List (Fin d))
(htarget : (A.delta (A.run (word.take position)).1 word[position]
((A.run (word.take position)).2.viewAt k
(A.run (word.take position)).2.top)).2.2 port = .self) :
(A.run (word.take (position + 1))).2.follow
(A.run (word.take (position + 1))).2.top (port :: ports) =
(A.run (word.take (position + 1))).2.follow
(A.run (word.take (position + 1))).2.top ports := by
rw [Scaffold.follow_cons, run_take_succ A word position hposition]
simp [Automaton.step, Scaffold.resolve, htarget]
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem successor_follow_path_none (A : Automaton Sym Q Gamma d k)
(word : List Sym) (position : Nat) (hposition : position < word.length)
(port : Fin d) (ports oldPath : List (Fin d))
(htarget : (A.delta (A.run (word.take position)).1 word[position]
((A.run (word.take position)).2.viewAt k
(A.run (word.take position)).2.top)).2.2 port = .path oldPath)
(hold : (A.run (word.take position)).2.follow
(A.run (word.take position)).2.top oldPath = none) :
(A.run (word.take (position + 1))).2.follow
(A.run (word.take (position + 1))).2.top (port :: ports) = none := by
rw [Scaffold.follow_cons, run_take_succ A word position hposition]
simp [Automaton.step, Scaffold.resolve, htarget, hold]
omit [FiniteEnum Sym] [DecidableEq Sym] [FiniteEnum Q] [DecidableEq Q]
[FiniteEnum Gamma] [DecidableEq Gamma] in
theorem successor_follow_path_some (A : Automaton Sym Q Gamma d k)
(word : List Sym) (position endpoint : Nat)
(hposition : position < word.length) (hendpoint : endpoint ≤ position)
(port : Fin d) (ports oldPath : List (Fin d))
(htarget : (A.delta (A.run (word.take position)).1 word[position]
((A.run (word.take position)).2.viewAt k
(A.run (word.take position)).2.top)).2.2 port = .path oldPath)
(hold : (A.run (word.take position)).2.follow
(A.run (word.take position)).2.top oldPath = some endpoint) :
(A.run (word.take (position + 1))).2.follow
(A.run (word.take (position + 1))).2.top (port :: ports) =
(A.run (word.take endpoint)).2.follow endpoint ports := by
rw [Scaffold.follow_cons, run_take_succ A word position hposition]
simp only [Automaton.step, Scaffold.append_top, Scaffold.append_edge_new,
Scaffold.resolve, htarget, hold]
calc
(A.run (word.take position) |>.2.append
(A.delta (A.run (word.take position)).1 word[position]
((A.run (word.take position)).2.viewAt k
(A.run (word.take position)).2.top)).2.1
(A.delta (A.run (word.take position)).1 word[position]
((A.run (word.take position)).2.viewAt k
(A.run (word.take position)).2.top)).2.2).follow endpoint ports =
(A.run (word.take position)).2.follow endpoint ports := by
have hlength : endpoint ≤ (word.take position).length := by
simp [List.length_take, Nat.min_eq_left (Nat.le_of_lt hposition),
hendpoint]
simpa [List.take_succ_eq_append_getElem hposition,
Automaton.run_append] using
run_append_follow_old A (word.take position) [word[position]]
ports endpoint hlength
_ = (A.run (word.take endpoint)).2.follow endpoint ports :=
run_take_follow_old A word hendpoint (Nat.le_of_lt hposition) ports
theorem path_eval (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
(hposition : position ≤ word.length)
(hcontext : EarlierGuardContext A hdistance word position)
(path : BoundedPath d k) :
Eval (rawGrammar A hdistance) (.nonterm (.path path))
(word.take position).reverse (pathResult A word position path) := by
rcases path with ⟨ports, hports⟩
cases ports with
| nil =>
have heval : Eval (rawGrammar A hdistance)
(.nonterm (.path (⟨[], hports⟩ : BoundedPath d k)))
(word.take position).reverse (.ok (word.take position).reverse) := by
apply Eval.nonterm
simp only [rawGrammar, pathRule]
exact Eval.eps
simpa [pathResult, Scaffold.follow_nil, Automaton.run_top,
List.length_take, Nat.min_eq_left hposition] using heval
| cons port ports =>
cases position with
| zero =>
have heval := path_zero_nonempty_eval A hdistance port ports hports
simpa [pathResult, Automaton.run, Scaffold.base,
Scaffold.follow_cons] using heval
| succ predecessor =>
have hpredecessor : predecessor < word.length := by omega
let stem := word.take predecessor
let symbol := word[predecessor]
let tail : BoundedPath d k := ⟨ports, by
exact Nat.le_trans (by simp) hports⟩
let actual := currentTransitionInput A stem symbol
have hguardContext : PrefixGuardContext A hdistance stem := by
exact hcontext.guard predecessor (Nat.lt_succ_self predecessor)
have hguard : Eval (rawGrammar A hdistance)
(transitionExpr actual.1 actual.2.1 actual.2.2)
(symbol :: stem.reverse) (.ok (symbol :: stem.reverse)) := by
exact current_transition_ok A hdistance stem symbol hguardContext
cases hbranch : (A.delta actual.1 actual.2.1 actual.2.2).2.2 port with
| missing =>
have hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port actual)
(symbol :: stem.reverse) .err := by
simpa [actual] using pathAlternative_missing_eval A hdistance
stem symbol tail port (by simpa [actual] using hbranch)
(by simpa [actual] using hguard)
have hselected := pathAlternatives_of_actual A hdistance stem
symbol hguardContext tail port .err (by
simpa [actual] using hactual)
have heval : Eval (rawGrammar A hdistance)
(.nonterm (.path
(⟨port :: ports, hports⟩ : BoundedPath d k)))
(symbol :: stem.reverse) .err := by
apply Eval.nonterm
simpa only [rawGrammar, pathRule, tail] using hselected
have hfollow := successor_follow_missing A word predecessor
hpredecessor port ports (by
simpa [actual, currentTransitionInput, stem, symbol] using hbranch)
rw [reverse_take_succ word predecessor hpredecessor]
simpa [pathResult, hfollow] using heval
| self =>
have htail : Eval (rawGrammar A hdistance)
(.nonterm (.path tail)) (word.take (predecessor + 1)).reverse
(pathResult A word (predecessor + 1) tail) :=
path_eval A hdistance word (predecessor + 1) hposition hcontext tail
have htail' : Eval (rawGrammar A hdistance)
(.nonterm (.path tail)) (symbol :: stem.reverse)
(pathResult A word (predecessor + 1) tail) := by
simpa [stem, symbol,
reverse_take_succ word predecessor hpredecessor] using htail
have hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port actual)
(symbol :: stem.reverse)
(pathResult A word (predecessor + 1) tail) := by
simpa [actual] using pathAlternative_self_eval A hdistance
stem symbol tail port (pathResult A word (predecessor + 1) tail)
(by simpa [actual] using hbranch)
(by simpa [actual] using hguard) htail'
have hselected := pathAlternatives_of_actual A hdistance stem
symbol hguardContext tail port _ (by
simpa [actual] using hactual)
have heval : Eval (rawGrammar A hdistance)
(.nonterm (.path
(⟨port :: ports, hports⟩ : BoundedPath d k)))
(symbol :: stem.reverse)
(pathResult A word (predecessor + 1) tail) := by
apply Eval.nonterm
simpa only [rawGrammar, pathRule, tail] using hselected
have hfollow := successor_follow_self A word predecessor
hpredecessor port ports (by
simpa [actual, currentTransitionInput, stem, symbol] using hbranch)
rw [reverse_take_succ word predecessor hpredecessor]
simpa [pathResult, hfollow] using heval
| path oldPath =>
let oldBounded : BoundedPath d k := ⟨oldPath, by
exact hdistance actual.1 actual.2.1 actual.2.2 port oldPath hbranch⟩
have holdEval : Eval (rawGrammar A hdistance)
(.nonterm (.path oldBounded)) (word.take predecessor).reverse
(pathResult A word predecessor oldBounded) :=
path_eval A hdistance word predecessor (Nat.le_of_lt hpredecessor)
(hcontext.mono A hdistance word (Nat.le_succ predecessor)) oldBounded
cases hold : (A.run (word.take predecessor)).2.follow
(A.run (word.take predecessor)).2.top oldPath with
| none =>
have holdErr : Eval (rawGrammar A hdistance)
(.nonterm (.path oldBounded)) stem.reverse .err := by
simpa [pathResult, oldBounded, hold, stem] using holdEval
have hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port actual)
(symbol :: stem.reverse) .err := by
apply pathAlternative_path_eval A hdistance stem symbol tail
port oldPath .err (by simpa [actual] using hbranch)
(by simpa [actual] using hguard)
simpa [oldBounded, actual] using
(Eval.seqOk Eval.termOk (Eval.seqErr holdErr))
have hselected := pathAlternatives_of_actual A hdistance stem
symbol hguardContext tail port .err (by
simpa [actual] using hactual)
have heval : Eval (rawGrammar A hdistance)
(.nonterm (.path
(⟨port :: ports, hports⟩ : BoundedPath d k)))
(symbol :: stem.reverse) .err := by
apply Eval.nonterm
simpa only [rawGrammar, pathRule, tail] using hselected
have hfollow := successor_follow_path_none A word predecessor
hpredecessor port ports oldPath
(by simpa [actual, currentTransitionInput, stem, symbol] using hbranch)
hold
rw [reverse_take_succ word predecessor hpredecessor]
simpa [pathResult, hfollow] using heval
| some endpoint =>
have hendpoint : endpoint ≤ predecessor :=
path_endpoint_le A word predecessor
(Nat.le_of_lt hpredecessor) oldBounded endpoint (by
simpa [oldBounded] using hold)
have hendpointWord : endpoint ≤ word.length :=
Nat.le_trans hendpoint (Nat.le_of_lt hpredecessor)
have holdOk : Eval (rawGrammar A hdistance)
(.nonterm (.path oldBounded)) stem.reverse
(.ok (word.take endpoint).reverse) := by
simpa [pathResult, oldBounded, hold, stem] using holdEval
have htail : Eval (rawGrammar A hdistance)
(.nonterm (.path tail)) (word.take endpoint).reverse
(pathResult A word endpoint tail) :=
path_eval A hdistance word endpoint hendpointWord
(hcontext.mono A hdistance word
(Nat.le_trans hendpoint (Nat.le_succ predecessor))) tail
have hactual : Eval (rawGrammar A hdistance)
(pathAlternative A hdistance tail port actual)
(symbol :: stem.reverse) (pathResult A word endpoint tail) := by
apply pathAlternative_path_eval A hdistance stem symbol tail
port oldPath (pathResult A word endpoint tail)
(by simpa [actual] using hbranch)
(by simpa [actual] using hguard)
simpa [oldBounded, actual] using
(Eval.seqOk Eval.termOk (Eval.seqOk holdOk htail))
have hselected := pathAlternatives_of_actual A hdistance stem
symbol hguardContext tail port _ (by
simpa [actual] using hactual)
have heval : Eval (rawGrammar A hdistance)
(.nonterm (.path
(⟨port :: ports, hports⟩ : BoundedPath d k)))
(symbol :: stem.reverse) (pathResult A word endpoint tail) := by
apply Eval.nonterm
simpa only [rawGrammar, pathRule, tail] using hselected
have hfollow := successor_follow_path_some A word predecessor
endpoint hpredecessor hendpoint port ports oldPath
(by simpa [actual, currentTransitionInput, stem, symbol] using hbranch)
hold
have hresult : pathResult A word (predecessor + 1)
(⟨port :: ports, hports⟩ : BoundedPath d k) =
pathResult A word endpoint tail := by
unfold pathResult
rw [hfollow, Automaton.run_top]
simp [tail, List.length_take, Nat.min_eq_left hendpointWord]
rw [reverse_take_succ word predecessor hpredecessor]
rw [hresult]
exact heval
termination_by (position, path.elems.length)
decreasing_by all_goals simp_wf <;> simp_all <;> omega
omit [DecidableEq Sym] in
theorem pathExact_of_eval (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
(hposition : position ≤ word.length) (path : BoundedPath d k)
(heval : Eval (rawGrammar A hdistance) (.nonterm (.path path))
(word.take position).reverse (pathResult A word position path)) :
PathExact A hdistance word position hposition path := by
refine ⟨?_, ?_⟩
· intro rest
constructor
· intro hok
cases hfollow : (A.run (word.take position)).2.follow
(A.run (word.take position)).2.top path.elems with
| none =>
rw [pathResult, hfollow] at heval
have himpossible := eval_deterministic hok heval
cases himpossible
| some endpoint =>
rw [pathResult, hfollow] at heval
have hresult := eval_deterministic hok heval
cases hresult
exact ⟨endpoint, rfl,
path_endpoint_le A word position hposition path endpoint hfollow, rfl⟩
· rintro ⟨endpoint, hfollow, _, rfl⟩
simpa [pathResult, hfollow] using heval
· constructor
· intro herr
cases hfollow : (A.run (word.take position)).2.follow
(A.run (word.take position)).2.top path.elems with
| none => rfl
| some endpoint =>
rw [pathResult, hfollow] at heval
have himpossible := eval_deterministic herr heval
cases himpossible
· intro hfollow
simpa [pathResult, hfollow] using heval
omit [DecidableEq Sym] in
theorem path_nil_exact (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
(hposition : position ≤ word.length) :
PathExact A hdistance word position hposition (rootPath d k) := by
apply pathExact_of_eval
have heval : Eval (rawGrammar A hdistance)
(.nonterm (.path (rootPath d k))) (word.take position).reverse
(.ok (word.take position).reverse) := by
apply Eval.nonterm
simp only [rawGrammar, pathRule, rootPath]
exact Eval.eps
simpa [pathResult, rootPath, Scaffold.follow_nil, Automaton.run_top,
List.length_take, Nat.min_eq_left hposition] using heval
/-- I3 under the exact State/I4 facts at earlier positions. Position decreases
for old paths and path length decreases for `SELF`. -/
theorem path_exact (A : Automaton Sym Q Gamma d k)
(hdistance : A.DistanceOk) (word : List Sym) (position : Nat)
(hposition : position ≤ word.length)
(hcontext : EarlierGuardContext A hdistance word position)
(path : BoundedPath d k) :
PathExact A hdistance word position hposition path :=
pathExact_of_eval A hdistance word position hposition path
(path_eval A hdistance word position hposition hcontext path)
namespace PathRed
example (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
(word : List Sym) (position : Nat) (hposition : position ≤ word.length) :
PathExact A hdistance word position hposition (rootPath d k) :=
path_nil_exact A hdistance word position hposition
example (A : Automaton Sym Q Gamma d k) (hdistance : A.DistanceOk)
(word : List Sym) (position : Nat) (hposition : position ≤ word.length)
(hcontext : EarlierGuardContext A hdistance word position)
(path : BoundedPath d k) :
PathExact A hdistance word position hposition path :=
path_exact A hdistance word position hposition hcontext path
end PathRed
namespace PathExamples
def onePort : BoundedPath 1 1 := ⟨[0], by decide⟩
def oldPathMachine : Automaton Bool Unit Unit 1 1 where
delta _ _ _ := ((), (), fun _ => .path [])
init := ()
accept _ := true
def missingMachine : Automaton Bool Unit Unit 1 1 where
delta _ _ _ := ((), (), fun _ => .missing)
init := ()
accept _ := true
def selfMachine : Automaton Bool Unit Unit 1 1 where
delta _ _ _ := ((), (), fun _ => .self)
init := ()
accept _ := true
theorem oldPathMachine_distance : oldPathMachine.DistanceOk := by
intro control symbol neighbourhood port path hpath
simp [oldPathMachine] at hpath
subst path
simp
theorem missingMachine_distance : missingMachine.DistanceOk := by
intro control symbol neighbourhood port path hpath
simp [missingMachine] at hpath
theorem selfMachine_distance : selfMachine.DistanceOk := by
intro control symbol neighbourhood port path hpath
simp [selfMachine] at hpath
example (hcontext : EarlierGuardContext oldPathMachine
oldPathMachine_distance [true] 1) :
Eval (rawGrammar oldPathMachine oldPathMachine_distance)
(.nonterm (.path onePort)) [true] (.ok []) := by
apply ((path_exact oldPathMachine oldPathMachine_distance [true] 1
(by decide) hcontext onePort).ok_iff []).mpr
exact ⟨0, by decide, by decide, rfl⟩
example (hcontext : EarlierGuardContext missingMachine
missingMachine_distance [true] 1) :
Eval (rawGrammar missingMachine missingMachine_distance)
(.nonterm (.path onePort)) [true] .err := by
apply (path_exact missingMachine missingMachine_distance [true] 1
(by decide) hcontext onePort).err_iff.mpr
decide
/-- A nonempty `SELF` path succeeds at the same position and consumes nothing. -/
example (hcontext : EarlierGuardContext selfMachine
selfMachine_distance [true] 1) :
Eval (rawGrammar selfMachine selfMachine_distance)
(.nonterm (.path onePort)) [true] (.ok [true]) := by
apply ((path_exact selfMachine selfMachine_distance [true] 1
(by decide) hcontext onePort).ok_iff [true]).mpr
exact ⟨1, by decide, by decide, rfl⟩
end PathExamples
end Theorem16
end FPRD