[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
s : σ
S : Set σ
a : α
⊢ s ∈ stepSet M S a ↔ ∃ t, t ∈ S ∧ s ∈ step M t a
[PROOFSTEP]
simp [stepSet]
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
a : α
⊢ stepSet M ∅ a = ∅
[PROOFSTEP]
simp [stepSet]
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
S : Set σ
x : List α
a : α
⊢ evalFrom M S (x ++ [a]) = stepSet M (evalFrom M S x) a
[PROOFSTEP]
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ x ∈ accepts M ↔ ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
⊢ DFA.accepts (toDFA M) = accepts M
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ x ∈ DFA.accepts (toDFA M) ↔ x ∈ accepts M
[PROOFSTEP]
rw [mem_accepts, DFA.mem_accepts]
[GOAL]
case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept ↔ ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept → ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
[PROOFSTEP]
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩
[GOAL]
case h.mpr
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ (∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x) → DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept
[PROOFSTEP]
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ accepts M
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
rw [← toDFA_correct] at hx ⊢
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ DFA.accepts (toDFA M)
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ DFA.accepts (toDFA M)
[PROOFSTEP]
exact M.toDFA.pumping_lemma hx hlen
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ NFA.evalFrom (toNFA M) {start} s = {evalFrom M start s}
[PROOFSTEP]
change List.foldl M.toNFA.stepSet { start } s = {List.foldl M.step start s}
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
[PROOFSTEP]
induction' s with a s ih generalizing start
[GOAL]
case nil
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} [] = {List.foldl M.step start []}
[PROOFSTEP]
tauto
[GOAL]
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} (a :: s) = {List.foldl M.step start (a :: s)}
[PROOFSTEP]
rw [List.foldl, List.foldl, show M.toNFA.stepSet { start } a = {M.step start a} by simp [NFA.stepSet]]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ NFA.stepSet (toNFA M) {start} a = {step M start a}
[PROOFSTEP]
simp [NFA.stepSet]
[GOAL]
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {step M start a} s = {List.foldl M.step (step M start a) s}
[PROOFSTEP]
tauto
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
⊢ NFA.accepts (toNFA M) = accepts M
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ NFA.accepts (toNFA M) ↔ x ∈ accepts M
[PROOFSTEP]
rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) ↔ x ∈ accepts M
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) → x ∈ accepts M
[PROOFSTEP]
rintro ⟨S, hS₁, hS₂⟩
[GOAL]
case h.mp.intro.intro
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ (toNFA M).accept
hS₂ : S ∈ {evalFrom M M.start x}
⊢ x ∈ accepts M
[PROOFSTEP]
rwa [Set.mem_singleton_iff.mp hS₂] at hS₁ 
[GOAL]
case h.mpr
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ accepts M → ∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}
[PROOFSTEP]
exact fun h => ⟨M.eval x, h, rfl⟩
