[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s✝ : σ
a : α
s : σ
hs : s ∈ εClosure M ∅
⊢ False
[PROOFSTEP]
induction hs
[GOAL]
case base
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s✝¹ : σ
a : α
s s✝ : σ
a✝ : s✝ ∈ ∅
⊢ False
[PROOFSTEP]
assumption
[GOAL]
case step
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s✝¹ : σ
a : α
s s✝ t✝ : σ
a✝¹ : t✝ ∈ step M s✝ none
a✝ : εClosure M ∅ s✝
a_ih✝ : False
⊢ False
[PROOFSTEP]
assumption
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
⊢ s ∈ stepSet M S a ↔ ∃ t, t ∈ S ∧ s ∈ εClosure M (step M t (some a))
[PROOFSTEP]
simp_rw [stepSet, mem_iUnion₂, exists_prop]
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a✝ a : α
⊢ stepSet M ∅ a = ∅
[PROOFSTEP]
simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S✝ : Set σ
x✝ : List α
s : σ
a✝ : α
S : Set σ
x : List α
a : α
⊢ evalFrom M S (x ++ [a]) = stepSet M (evalFrom M S x) a
[PROOFSTEP]
rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a : α
x : List α
⊢ evalFrom M ∅ x = ∅
[PROOFSTEP]
induction' x using List.reverseRecOn with x a ih
[GOAL]
case H0
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
⊢ evalFrom M ∅ [] = ∅
[PROOFSTEP]
rw [evalFrom_nil, εClosure_empty]
[GOAL]
case H1
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a✝ : α
x : List α
a : α
ih : evalFrom M ∅ x = ∅
⊢ evalFrom M ∅ (x ++ [a]) = ∅
[PROOFSTEP]
rw [evalFrom_append_singleton, ih, stepSet_empty]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a : α
M : NFA α σ
S : Set σ
⊢ εNFA.εClosure (toεNFA M) S = S
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S ↔ a ∈ S
[PROOFSTEP]
refine' ⟨_, εNFA.εClosure.base _⟩
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S → a ∈ S
[PROOFSTEP]
rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)
[GOAL]
case h.base
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S
[PROOFSTEP]
exact h
[GOAL]
case h.step
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝¹ : α
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : εNFA.εClosure (toεNFA M) S s✝
h : a ∈ εNFA.step (toεNFA M) s✝ none
⊢ a ∈ S
[PROOFSTEP]
cases h
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.evalFrom (toεNFA M) start = evalFrom M start
[PROOFSTEP]
rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
[PROOFSTEP]
suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
this : εNFA.stepSet (toεNFA M) = stepSet M
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.stepSet (toεNFA M) = stepSet M
[PROOFSTEP]
ext S s
[GOAL]
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ εNFA.stepSet (toεNFA M) S s ↔ x✝ ∈ stepSet M S s
[PROOFSTEP]
simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]
[GOAL]
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i, i ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) i (some s))) ↔ ∃ i, i ∈ S ∧ x✝ ∈ step M i s
[PROOFSTEP]
apply exists_congr
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ a ∈ S ∧ x✝ ∈ step M a s
[PROOFSTEP]
simp only [and_congr_right_iff]
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S → (x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ x✝ ∈ step M a s)
[PROOFSTEP]
intro _ _
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a✝¹ (some s)) ↔ x✝ ∈ step M a✝¹ s
[PROOFSTEP]
rw [M.toεNFA_εClosure]
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.step (toεNFA M) a✝¹ (some s) ↔ x✝ ∈ step M a✝¹ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ εNFA.accepts (toεNFA M) = accepts M
[PROOFSTEP]
rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ {x | ∃ S, S ∈ (toεNFA M).accept ∧ S ∈ evalFrom M (toεNFA M).start x} = accepts M
[PROOFSTEP]
rfl
