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

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
⊢ Data.Expr.matches cs r
Tactic:
have hi : i.val = 0 := (done_iff_zero_compile eq i).mp h₂
State after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
⊢ Data.Expr.matches cs r

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
⊢ Data.Expr.matches cs r
Tactic:
have : nfa.pathIn 0 nfa.start i cs := pathIn_of_reaches h₁
State after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this : nfa.pathIn 0 (↑nfa.start) (↑i) cs
⊢ Data.Expr.matches cs r

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this : nfa.pathIn 0 (↑nfa.start) (↑i) cs
⊢ Data.Expr.matches cs r
Tactic:
have := pathToNext_of_compile_of_pathIn eq (hi ▸ this)
State after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this✝ : nfa.pathIn 0 (↑nfa.start) (↑i) cs
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Data.Expr.matches cs r

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this✝ : nfa.pathIn 0 (↑nfa.start) (↑i) cs
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Data.Expr.matches cs r
Tactic:
exact (matches_iff_pathToNext eq).mpr this
State after:
no goals