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

State before:
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] ↔ i' ∈ nfa.εClosure i
Tactic:
apply Iff.intro
State after:
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i

case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []

State before:
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i

case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Tactic:
. exact εClosure_of_pathIn
State after:
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []

State before:
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Tactic:
. intro h
  induction h with
  | base => exact .base (Nat.zero_le _)
  | @step i j k step _ ih =>
    cases Nat.decLt i nfa.nodes.size with
    | isTrue lt =>
      simp [εStep, lt] at step
      exact .step (.εStep (Nat.zero_le _) lt step) ih
    | isFalse nlt => simp [εStep, nlt] at step
State after:
no goals

State before:
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i
Tactic:
exact εClosure_of_pathIn
State after:
no goals

State before:
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Tactic:
intro h
State after:
case mpr
i i' : ℕ
nfa : NFA
h : i' ∈ nfa.εClosure i
⊢ nfa.pathIn 0 i i' []

State before:
case mpr
i i' : ℕ
nfa : NFA
h : i' ∈ nfa.εClosure i
⊢ nfa.pathIn 0 i i' []
Tactic:
induction h with
| base => exact .base (Nat.zero_le _)
| @step i j k step _ ih =>
  cases Nat.decLt i nfa.nodes.size with
  | isTrue lt =>
    simp [εStep, lt] at step
    exact .step (.εStep (Nat.zero_le _) lt step) ih
  | isFalse nlt => simp [εStep, nlt] at step
State after:
no goals

State before:
case mpr.base
i i' : ℕ
nfa : NFA
i✝ : ℕ
⊢ nfa.pathIn 0 i✝ i✝ []
Tactic:
exact .base (Nat.zero_le _)
State after:
no goals

State before:
case mpr.step
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
⊢ nfa.pathIn 0 i k []
Tactic:
cases Nat.decLt i nfa.nodes.size with
| isTrue lt =>
  simp [εStep, lt] at step
  exact .step (.εStep (Nat.zero_le _) lt step) ih
| isFalse nlt => simp [εStep, nlt] at step
State after:
no goals

State before:
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
⊢ nfa.pathIn 0 i k []
Tactic:
simp [εStep, lt] at step
State after:
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathIn 0 i k []

State before:
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathIn 0 i k []
Tactic:
exact .step (.εStep (Nat.zero_le _) lt step) ih
State after:
no goals

State before:
case mpr.step.isFalse
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
nlt : ¬i < nfa.nodes.size
⊢ nfa.pathIn 0 i k []
Tactic:
simp [εStep, nlt] at step
State after:
no goals