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

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ Grammar.GeneratedLanguage G ⊆ NFA.AcceptedLanguage (toNFA G)
Tactic:
intro w ⟨d⟩
State after:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ w ∈ NFA.AcceptedLanguage (toNFA G)

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ w ∈ NFA.AcceptedLanguage (toNFA G)
Tactic:
constructor
State after:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ?w ∈ (toNFA G).Q₀ ∧ ∃ run, NFA.Run.last run ∈ (toNFA G).F

case w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ { x // x ∈ (toNFA G).Q }

State before:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ?w ∈ (toNFA G).Q₀ ∧ ∃ run, NFA.Run.last run ∈ (toNFA G).F

case w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ { x // x ∈ (toNFA G).Q }
Tactic:
constructor
State after:
case h.left
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ?w ∈ (toNFA G).Q₀

case h.right
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ∃ run, NFA.Run.last run ∈ (toNFA G).F

case w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ { x // x ∈ (toNFA G).Q }

State before:
case h.left
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ?w ∈ (toNFA G).Q₀

case h.right
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ∃ run, NFA.Run.last run ∈ (toNFA G).F

case w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ { x // x ∈ (toNFA G).Q }
Tactic:
simp [toNFA]
State after:
case h.left
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ?w = { val := Sum.inl G.start, property := ⋯ }

case h.right
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ∃ run, NFA.Run.last run ∈ (toNFA G).F

case w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ { x // x ∈ (toNFA G).Q }

State before:
case h.left
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ?w = { val := Sum.inl G.start, property := ⋯ }

case h.right
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ∃ run, NFA.Run.last run ∈ (toNFA G).F

case w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ { x // x ∈ (toNFA G).Q }
Tactic:
rfl
State after:
case h.right
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ∃ run, NFA.Run.last run ∈ (toNFA G).F

State before:
case h.right
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ ∃ run, NFA.Run.last run ∈ (toNFA G).F
Tactic:
constructor
State after:
case h.right.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ NFA.Run.last ?h.right.w ∈ (toNFA G).F

case h.right.w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ NFA.Run (toNFA G) { val := Sum.inl G.start, property := ⋯ } w

State before:
case h.right.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ NFA.Run.last ?h.right.w ∈ (toNFA G).F

case h.right.w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ NFA.Run (toNFA G) { val := Sum.inl G.start, property := ⋯ } w
Tactic:
apply NFA.Run.fromDerivation_last_in_final
State after:
case h.right.h.d
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ RegularDerivation G G.start w

State before:
case h.right.h.d
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ RegularDerivation G G.start w
Tactic:
apply RegularDerivation.fromDerivation
State after:
case h.right.h.d.derivation
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Grammar.Derivation G [Sum.inl G.start] ?h.right.h.d.w'

case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = ?h.right.h.d.w'

case h.right.h.d.w'
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })

State before:
case h.right.h.d.derivation
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Grammar.Derivation G [Sum.inl G.start] ?h.right.h.d.w'

case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = ?h.right.h.d.w'

case h.right.h.d.w'
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
Tactic:
assumption
State after:
case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = Sum.inr <$> w

State before:
case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = Sum.inr <$> w
Tactic:
rfl
State after:
no goals