Theorem: Regex.NFA.εClosure_of_pathIn (RegexCorrectness/NFA/Transition/Closure/Equivalence.lean)

State before:
i i' : ℕ
nfa : NFA
start : ℕ
path : nfa.pathIn start i i' []
⊢ i' ∈ nfa.εClosure i
Tactic:
generalize h : [] = cs at path
State after:
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
h : [] = cs
path : nfa.pathIn start i i' cs
⊢ i' ∈ nfa.εClosure i

State before:
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
h : [] = cs
path : nfa.pathIn start i i' cs
⊢ i' ∈ nfa.εClosure i
Tactic:
induction path with
| base _ => exact .base
| @step i j k cs cs' step _ ih =>
  simp at h
  simp [h] at *
  cases step with
  | εStep _ _ step =>
    exact εClosure.step (εStep_of_εStep step) ih
State after:
no goals

State before:
case base
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
i✝ : ℕ
h✝ : start ≤ i✝
h : [] = []
⊢ i✝ ∈ nfa.εClosure i✝
Tactic:
exact .base
State after:
no goals

State before:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest✝ : nfa.pathIn start j k cs'
ih : [] = cs' → k ∈ nfa.εClosure j
h : [] = cs ++ cs'
⊢ k ∈ nfa.εClosure i
Tactic:
simp at h
State after:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest✝ : nfa.pathIn start j k cs'
ih : [] = cs' → k ∈ nfa.εClosure j
h : cs = [] ∧ cs' = []
⊢ k ∈ nfa.εClosure i

State before:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest✝ : nfa.pathIn start j k cs'
ih : [] = cs' → k ∈ nfa.εClosure j
h : cs = [] ∧ cs' = []
⊢ k ∈ nfa.εClosure i
Tactic:
simp [h] at *
State after:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j []
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
⊢ k ∈ nfa.εClosure i

State before:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j []
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
⊢ k ∈ nfa.εClosure i
Tactic:
cases step with
| εStep _ _ step =>
  exact εClosure.step (εStep_of_εStep step) ih
State after:
no goals

State before:
case step.εStep
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ k ∈ nfa.εClosure i
Tactic:
exact εClosure.step (εStep_of_εStep step) ih
State after:
no goals