internlm/Lean-Github huggingface dataset:
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
apply Exists.intro
Proof state after:
case right.h
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
case right.h
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w
Tactic:
swap
Proof state after:
case right.w
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w

case right.h
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F
Theorem: DFA.fromNFA_run_imp_run
Proof state before:
case right.h
α 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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last (NFA.Run.step x right✝ r' h✝) ∈ M.F
Tactic:
assumption
Proof state after:
no goals
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ DFA.AcceptedLanguage (DFA.fromNFA M) ⊆ AcceptedLanguage M
Tactic:
intro w ⟨_, hr⟩
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
⊢ w ∈ AcceptedLanguage M
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
⊢ w ∈ AcceptedLanguage M
Tactic:
have ⟨q, hq, r, _⟩ := DFA.fromNFA_run_imp_run hr
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ w ∈ AcceptedLanguage M
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ w ∈ AcceptedLanguage M
Tactic:
exists q
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F
Tactic:
dsimp [DFA.fromNFA] at hq
Proof state after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ 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 ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ 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 ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F
Theorem: NFA.DFA_fromNFA_lang_subs_lang
Proof state before:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F
Tactic:
exists r
Proof state after:
no goals
Theorem: NFA.fromNFA_lang_eq_lang
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ DFA.AcceptedLanguage (DFA.fromNFA M) = AcceptedLanguage M
Tactic:
apply Set.ext
Proof state after:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ ∀ (x : Word { x // x ∈ (DFA.fromNFA M).Z }), x ∈ DFA.AcceptedLanguage (DFA.fromNFA M) ↔ x ∈ AcceptedLanguage M
Theorem: NFA.fromNFA_lang_eq_lang
Proof state before:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ ∀ (x : Word { x // x ∈ (DFA.fromNFA M).Z }), x ∈ DFA.AcceptedLanguage (DFA.fromNFA M) ↔ x ∈ AcceptedLanguage M
Tactic:
intros
Proof state after:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M) ↔ x✝ ∈ AcceptedLanguage M
Theorem: NFA.fromNFA_lang_eq_lang
Proof state before:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M) ↔ x✝ ∈ AcceptedLanguage M
Tactic:
constructor
Proof state after:
case h.mp
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Theorem: NFA.fromNFA_lang_eq_lang
Proof state before:
case h.mp
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Tactic:
apply DFA_fromNFA_lang_subs_lang
Proof state after:
case h.mpr
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Theorem: NFA.fromNFA_lang_eq_lang
Proof state before:
case h.mpr
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
x✝ : Word { x // x ∈ (DFA.fromNFA M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Tactic:
apply lang_subs_DFA_fromNFA_lang
Proof state after:
no goals
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
⊢ step.pre = Sum.inr a :: List.tail step.pre
Tactic:
have sound := step.sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound :
  let_fun x := Production.lhs ↑step.prod;
  lhs = step.pre * x * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound :
  let_fun x := Production.lhs ↑step.prod;
  lhs = step.pre * x * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre
Tactic:
simp_rw [Production.ContextFree.lhs_eq_lhs step.prod.val, h_lhs] at sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
⊢ step.pre = Sum.inr a :: List.tail step.pre
Tactic:
match hpre:step.pre with
| [] =>
  simp_rw [hpre, HMul.hMul, Mul.mul] at sound
  simp at sound
  rw [List.cons_eq_cons] at sound
  let ⟨_, _⟩ := sound
  contradiction
| x :: pres => 
  simp_rw [hpre, HMul.hMul, Mul.mul] at sound
  simp at sound; rw [List.cons_eq_cons] at sound
  simp [sound.left]
Proof state after:
no goals
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
hpre : step.pre = []
⊢ [] = Sum.inr a :: List.tail []
Tactic:
simp_rw [hpre, HMul.hMul, Mul.mul] at sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = List.append (List.append [] [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ [] = Sum.inr a :: List.tail []
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = List.append (List.append [] [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
simp at sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ [] = Sum.inr a :: List.tail []
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
rw [List.cons_eq_cons] at sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
⊢ [] = Sum.inr a :: List.tail []
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
let ⟨_, _⟩ := sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
left✝ : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod)
right✝ : xs = step.suf
⊢ [] = Sum.inr a :: List.tail []
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod) ∧ xs = step.suf
left✝ : Sum.inr a = Sum.inl (Production.ContextFree.lhs_var ↑step.prod)
right✝ : xs = step.suf
⊢ [] = Sum.inr a :: List.tail []
Tactic:
contradiction
Proof state after:
no goals
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Tactic:
simp_rw [hpre, HMul.hMul, Mul.mul] at sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound :
  Sum.inr a :: xs = List.append (List.append (x :: pres) [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Theorem: ContextFreeGrammar.derivation_step_prefix
Proof state before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound :
  Sum.inr a :: xs = List.append (List.append (x :: pres) [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
Tactic:
simp at sound
Proof state after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a :: xs = x :: (pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf)
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)