Theorem: RegularGrammar.toNFA_lang_subs_lang (FormalSystems/Chomsky/Regular/NFA.lean)

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ NFA.AcceptedLanguage (toNFA G) ⊆ Grammar.GeneratedLanguage G
Tactic:
intro w ⟨q₀, h_q₀, r, hr⟩
State after:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ w ∈ Grammar.GeneratedLanguage G

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ w ∈ Grammar.GeneratedLanguage G
Tactic:
constructor
State after:
case val
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)

State before:
case val
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
Tactic:
apply RegularDerivation.toDerivation
State after:
case val.d
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ RegularDerivation G G.start w

State before:
case val.d
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ RegularDerivation G G.start w
Tactic:
apply NFA.Run.toDerivation
State after:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ ↑?val.d.q = Sum.inl G.start

case val.d.hlast
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ { x // x ∈ (toNFA G).Q }

case val.d.run
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) ?val.d.q w

State before:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ ↑?val.d.q = Sum.inl G.start

case val.d.hlast
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ { x // x ∈ (toNFA G).Q }

case val.d.run
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) ?val.d.q w
Tactic:
. dsimp [toNFA] at h_q₀
  simp at h_q₀
  have := congrArg Subtype.val h_q₀
  simp at this
  assumption
State after:
case val.d.hlast
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.run
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) q₀ w

State before:
case val.d.hlast
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.run
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) q₀ w
Tactic:
. assumption
State after:
no goals

State before:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ ↑?val.d.q = Sum.inl G.start
Tactic:
dsimp [toNFA] at h_q₀
State after:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ ↑?val.d.q = Sum.inl G.start

State before:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ ↑?val.d.q = Sum.inl G.start
Tactic:
simp at h_q₀
State after:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
⊢ ↑?val.d.q = Sum.inl G.start

State before:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
⊢ ↑?val.d.q = Sum.inl G.start
Tactic:
have := congrArg Subtype.val h_q₀
State after:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
this : ↑q₀ = ↑{ val := Sum.inl G.start, property := ⋯ }
⊢ ↑?val.d.q = Sum.inl G.start

State before:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
this : ↑q₀ = ↑{ val := Sum.inl G.start, property := ⋯ }
⊢ ↑?val.d.q = Sum.inl G.start
Tactic:
simp at this
State after:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
this : ↑q₀ = Sum.inl G.start
⊢ ↑?val.d.q = Sum.inl G.start

State before:
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
this : ↑q₀ = Sum.inl G.start
⊢ ↑?val.d.q = Sum.inl G.start
Tactic:
assumption
State after:
no goals

State before:
case val.d.hlast
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F
Tactic:
assumption
State after:
no goals