Theorem: Regex.NFA.eq_next_of_pathToNext (RegexCorrectness/NFA/Transition/Path/Equivalence/MatchOfPath.lean)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
path : (↑result).pathToNext next' nfa.nodes.size i cs
⊢ next' = ↑next
Tactic:
obtain ⟨i', pcs, scs, _, path, step⟩ := path
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
⊢ next' = ↑next

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
⊢ next' = ↑next
Tactic:
have := eq_or_ge_of_step_pushRegex eq (le_of_pathIn_right path) step.h₂ step.step
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
this : next' = ↑next ∨ nfa.nodes.size ≤ next'
⊢ next' = ↑next

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
this : next' = ↑next ∨ nfa.nodes.size ≤ next'
⊢ next' = ↑next
Tactic:
cases this with
| inl eq => exact eq
| inr ge => exfalso; exact Nat.not_le_of_lt assm ge
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq✝ : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
eq : next' = ↑next
⊢ next' = ↑next
Tactic:
exact eq
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
ge : nfa.nodes.size ≤ next'
⊢ next' = ↑next
Tactic:
exfalso
State after:
case intro.intro.intro.intro.intro.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
ge : nfa.nodes.size ≤ next'
⊢ False

State before:
case intro.intro.intro.intro.intro.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
ge : nfa.nodes.size ≤ next'
⊢ False
Tactic:
exact Nat.not_le_of_lt assm ge
State after:
no goals