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

State before:
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
h : nfa.pathIn 0 (↑nfa.start) (↑i) m
⊢ nfa.reaches i m
Tactic:
induction m using List.list_reverse_induction generalizing i with
| base => exact .nil (pathIn_iff_εClosure.mp h)
| ind m c ih =>
  have ⟨j, k, path, step, cls⟩ := pathIn.of_snoc_char h
  let j' : Fin nfa.nodes.size := ⟨j, path.lt_right nfa.start.isLt⟩
  have prev := ih (i := j') path
  exact .snoc prev step cls
State after:
no goals

State before:
case base
nfa : NFA
i : Fin nfa.nodes.size
h : nfa.pathIn 0 ↑nfa.start ↑i []
⊢ nfa.reaches i []
Tactic:
exact .nil (pathIn_iff_εClosure.mp h)
State after:
no goals

State before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
⊢ nfa.reaches i (m ++ [c])
Tactic:
have ⟨j, k, path, step, cls⟩ := pathIn.of_snoc_char h
State after:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
⊢ nfa.reaches i (m ++ [c])

State before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
⊢ nfa.reaches i (m ++ [c])
Tactic:
let j' : Fin nfa.nodes.size := ⟨j, path.lt_right nfa.start.isLt⟩
State after:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
⊢ nfa.reaches i (m ++ [c])

State before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
⊢ nfa.reaches i (m ++ [c])
Tactic:
have prev := ih (i := j') path
State after:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
prev : nfa.reaches j' m
⊢ nfa.reaches i (m ++ [c])

State before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
prev : nfa.reaches j' m
⊢ nfa.reaches i (m ++ [c])
Tactic:
exact .snoc prev step cls
State after:
no goals