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

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Expr.matches cs r
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r
State after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ Expr.matches cs r

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ Expr.matches cs r
Tactic:
have : nfa = result.val := by
  rw [←eq]
  rfl
State after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
this : nfa = ↑result
⊢ Expr.matches cs r

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
this : nfa = ↑result
⊢ Expr.matches cs r
Tactic:
rw [this] at path
State after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
path : (↑result).pathToNext 0 1 (↑(↑result).start) cs
this : nfa = ↑result
⊢ Expr.matches cs r

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
path : (↑result).pathToNext 0 1 (↑(↑result).start) cs
this : nfa = ↑result
⊢ Expr.matches cs r
Tactic:
exact matches_of_pathToNext_pushRegex rfl path
State after:
no goals

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa = ↑result
Tactic:
rw [←eq]
State after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ compile r = ↑result

State before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ compile r = ↑result
Tactic:
rfl
State after:
no goals