Theorem: DFA.toGrammar_lang_subs_lang (FormalSystems/Chomsky/Regular/DFA.lean)

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ Grammar.GeneratedLanguage (toGrammar M) ⊆ AcceptedLanguage M
Tactic:
intro _ h
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ a✝ ∈ AcceptedLanguage M

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ a✝ ∈ AcceptedLanguage M
Tactic:
apply Nonempty.elim h
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝) → a✝ ∈ AcceptedLanguage M

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝) → a✝ ∈ AcceptedLanguage M
Tactic:
intro d
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ a✝ ∈ AcceptedLanguage M

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ a✝ ∈ AcceptedLanguage M
Tactic:
constructor
State after:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ NFA.Run.last ?w ∈ M.F

case w
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Run M M.q₀ a✝

State before:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ NFA.Run.last ?w ∈ M.F

case w
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Run M M.q₀ a✝
Tactic:
apply Run.fromDerivation_result
State after:
case h.d
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ RegularGrammar.RegularDerivation (toGrammar M) M.q₀ a✝

State before:
case h.d
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ RegularGrammar.RegularDerivation (toGrammar M) M.q₀ a✝
Tactic:
apply RegularGrammar.RegularDerivation.fromDerivation
State after:
case h.d.derivation
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl M.q₀] ?h.d.w'

case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = ?h.d.w'

case h.d.w'
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Word ({ x // x ∈ (toGrammar M).V } ⊕ { x // x ∈ (toGrammar M).Z })

State before:
case h.d.derivation
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl M.q₀] ?h.d.w'

case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = ?h.d.w'

case h.d.w'
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Word ({ x // x ∈ (toGrammar M).V } ⊕ { x // x ∈ (toGrammar M).Z })
Tactic:
assumption
State after:
case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = Sum.inr <$> a✝

State before:
case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = Sum.inr <$> a✝
Tactic:
rfl
State after:
no goals