Theorem: Regex.NFA.matches_of_starLoop (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 }
cs : List Char
eq : nfa.pushRegex next r.star = result
mr : ∀ {cs : List Char}, (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs → Expr.matches cs r
loop : starLoop eq cs
⊢ Expr.matches cs r.star
Tactic:
induction loop with
| complete => exact .starEpsilon
| loop path _ m₂ => exact .starConcat _ _ _ (mr path) m₂
State after:
no goals

State before:
case complete
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
mr : ∀ {cs : List Char}, (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs → Expr.matches cs r
⊢ Expr.matches [] r.star
Tactic:
exact .starEpsilon
State after:
no goals

State before:
case loop
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
mr : ∀ {cs : List Char}, (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs → Expr.matches cs r
cs₁✝ cs₂✝ : List Char
path : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁✝
rest✝ : starLoop eq cs₂✝
m₂ : Expr.matches cs₂✝ r.star
⊢ Expr.matches (cs₁✝ ++ cs₂✝) r.star
Tactic:
exact .starConcat _ _ _ (mr path) m₂
State after:
no goals