internlm/Lean-Github huggingface dataset:
Theorem: Grammar.ExampleGrammar.productions_eq_ex_productions
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
p : GenericProduction ExampleGrammar.Z ExampleGrammar.V
⊢ p ∈ ExampleGrammar.productions ↔ p ∈ ExampleProductions
Tactic:
simp [ExampleGrammar]
Proof state after:
no goals
Theorem: NFA.Run.fromDerivation_last_in_final
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
⊢ last (fromDerivation G d) ∈ (toNFA G).F
Tactic:
match d with
| .eps (v:=v) _ _ =>
  simp [last, toNFA]
  exists .eps v
| .alpha _ _ _ =>
  simp [last, fromDerivation, Fintype.wrap, toNFA]
| .step _ _ _ _ _ =>
  simp [last]
  apply fromDerivation_last_in_final
Proof state after:
no goals
Theorem: NFA.Run.fromDerivation_last_in_final
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
v : { x // x ∈ G.V }
h_v✝ : RegularProduction.eps v ∈ G.productions
h_w✝ : w✝ = ε
⊢ last (fromDerivation G (RegularDerivation.eps v h_v✝ h_w✝)) ∈ (toNFA G).F
Tactic:
simp [last, toNFA]
Proof state after:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
v : { x // x ∈ G.V }
h_v✝ : RegularProduction.eps v ∈ G.productions
h_w✝ : w✝ = ε
⊢ ∃ a,
    (a ∈ G.productions ∧ RegularProduction.isEps a) ∧
      Fintype.wrap (Sum.inl (RegularProduction.lhs a)) = { val := Sum.inl v, property := ⋯ }
Theorem: NFA.Run.fromDerivation_last_in_final
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
v : { x // x ∈ G.V }
h_v✝ : RegularProduction.eps v ∈ G.productions
h_w✝ : w✝ = ε
⊢ ∃ a,
    (a ∈ G.productions ∧ RegularProduction.isEps a) ∧
      Fintype.wrap (Sum.inl (RegularProduction.lhs a)) = { val := Sum.inl v, property := ⋯ }
Tactic:
exists .eps v
Proof state after:
no goals
Theorem: NFA.Run.fromDerivation_last_in_final
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝ : { x // x ∈ G.Z }
h_v✝ : RegularProduction.alpha x✝ a✝ ∈ G.productions
h_w✝ : w✝ = [a✝]
⊢ last (fromDerivation G (RegularDerivation.alpha x✝ h_v✝ h_w✝)) ∈ (toNFA G).F
Tactic:
simp [last, fromDerivation, Fintype.wrap, toNFA]
Proof state after:
no goals
Theorem: NFA.Run.fromDerivation_last_in_final
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G (RegularDerivation.step x✝ v'✝ h✝ h_w✝ a✝)) ∈ (toNFA G).F
Tactic:
simp [last]
Proof state after:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G a✝) ∈ (toNFA G).F
Theorem: NFA.Run.fromDerivation_last_in_final
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G a✝) ∈ (toNFA G).F
Tactic:
apply fromDerivation_last_in_final
Proof state after:
no goals
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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⟩
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof 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)
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof state after:
no goals
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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₀
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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₀
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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₀
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof 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
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof state after:
no goals
Theorem: RegularGrammar.toNFA_lang_subs_lang
Proof 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
Proof state after:
no goals
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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⟩
Proof 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)
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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
Proof 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 }
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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
Proof 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 }
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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]
Proof 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 }
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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
Proof 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
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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
Proof 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
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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
Proof 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
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof 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
Proof 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 })