Theorem: Regex.NFA.pathToNext_of_compile_matches (RegexCorrectness/NFA/Transition/Path/Equivalence/PathOfMatch.lean)

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
unfold NFA.compile at eq
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs

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

State before:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
have := pathToNext_of_matches h.symm m
State after:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result).pathToNext (↑⟨0, ⋯⟩) done.nodes.size (↑(↑result).start) cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs

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

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

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
m : Data.Expr.matches cs r
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals