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

State before:
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
h : nfa.reaches i m
⊢ nfa.pathIn 0 (↑nfa.start) (↑i) m
Tactic:
induction h with
| nil cls => simp [pathIn_iff_εClosure.mpr cls]
| @snoc i j k c m _ step cls ih =>
  simp [charStep] at step
  have ih' : nfa.pathIn (min 0 j) nfa.start j (m ++ [c]) :=
    ih.snoc_char i.isLt step
  simp at ih'
  have := ih'.trans (pathIn_iff_εClosure.mpr cls)
  simp at this
  exact this
State after:
no goals

State before:
case nil
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
i✝ : Fin nfa.nodes.size
cls : ↑i✝ ∈ nfa.εClosure ↑nfa.start
⊢ nfa.pathIn 0 ↑nfa.start ↑i✝ []
Tactic:
simp [pathIn_iff_εClosure.mpr cls]
State after:
no goals

State before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
step : j ∈ nfa.charStep (↑i) c
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
simp [charStep] at step
State after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])

State before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
have ih' : nfa.pathIn (min 0 j) nfa.start j (m ++ [c]) :=
  ih.snoc_char i.isLt step
State after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn (min 0 j) (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])

State before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn (min 0 j) (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
simp at ih'
State after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])

State before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
have := ih'.trans (pathIn_iff_εClosure.mpr cls)
State after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c] ++ [])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])

State before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c] ++ [])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
simp at this
State after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])

State before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
exact this
State after:
no goals