internlm/Lean-Github huggingface dataset:
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Tactic:
dsimp [NFARunToRun, NFA.Run.last]
Proof state after:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFARunToRun r✝) ⋯) ∈ (fromNFA M).F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFARunToRun r✝) ⋯) ∈ (fromNFA M).F
Tactic:
apply RunFromRestricted_final
Proof state after:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun r✝) ∈ (fromNFA M).F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun r✝) ∈ (fromNFA M).F
Tactic:
apply NFARunToRun_final_imp_final
Proof state after:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F
Tactic:
dsimp [NFA.Run.last] at h
Proof state after:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F
Tactic:
assumption
Proof state after:
no goals
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ AcceptedLanguage M ⊆ DFA.AcceptedLanguage (DFA.fromNFA M)
Tactic:
intro w ⟨_, h_start, run, h_run⟩
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Tactic:
constructor
Proof state after:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F

case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F

case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
Tactic:
swap
Proof state after:
case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.RunFromRestricted
Proof state after:
case w.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) ?w.q w

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑?w.q ⊆ ↑(DFA.fromNFA M).q₀

case w.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ (DFA.toNFA (DFA.fromNFA M)).Q }

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted ?w.r ?w.h) ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case w.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) ?w.q w

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑?w.q ⊆ ↑(DFA.fromNFA M).q₀

case w.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ (DFA.toNFA (DFA.fromNFA M)).Q }

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted ?w.r ?w.h) ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.NFARunToRun
Proof state after:
case w.r.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run M ?w.r.q w

case w.r.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ M.Q }

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {?w.r.q}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun ?w.r.r) ?w.h) ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case w.r.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run M ?w.r.q w

case w.r.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ M.Q }

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {?w.r.q}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun ?w.r.r) ?w.h) ∈ (DFA.fromNFA M).F
Tactic:
assumption
Proof state after:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {w✝}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ?w.h) ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {w✝}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ?w.h) ∈ (DFA.fromNFA M).F
Tactic:
simp [DFA.fromNFA]
Proof state after:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w✝ ∈ M.Q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w✝ ∈ M.Q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F
Tactic:
assumption
Proof state after:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.RunFromRestricted_final
Proof state after:
case h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.NFARunToRun run) ∈ (DFA.fromNFA M).F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.NFARunToRun run) ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.NFARunToRun_final_imp_final
Proof state after:
case h.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last run ∈ M.F
Theorem: NFA.lang_subs_DFA_fromNFA_lang
Proof state before:
case h.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last run ∈ M.F
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h : NFA.Run.last r ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
match r with
| .final _ _ =>
  dsimp [NFA.Run.last, fromNFA] at h
  have ⟨_, qf, _, _⟩ := Finset.mem_filter.mp h
  exists qf; constructor; assumption
  apply Exists.intro; swap
  apply NFA.Run.final _
  assumption
  dsimp [NFA.Run.last]
  assumption
| .step _ h_step _ _ =>
  dsimp [NFA.Run.last] at h
  dsimp [fromNFA, toNFA] at h_step; simp at h_step
  have ⟨_, h_q₂, r', hr'⟩ := fromNFA_run_imp_run h
  rw [h_step, Finset.mem_fold_union_iff] at h_q₂
  have ⟨x, _, _⟩ := h_q₂
  exists x; constructor; assumption
  apply Exists.intro; swap
  apply NFA.Run.step
  repeat { assumption }
Proof state after:
no goals
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q₀ h✝) ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
dsimp [NFA.Run.last, fromNFA] at h
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
have ⟨_, qf, _, _⟩ := Finset.mem_filter.mp h
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
exists qf
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀ ∧ ∃ r', NFA.Run.last r' ∈ M.F
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀ ∧ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
constructor
Proof state after:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
assumption
Proof state after:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F