Theorem: Regex.VM.matches_of_captureNext (RegexCorrectness/VM/Correctness.lean)

State before:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Tactic:
have ⟨s, l, m, r, sv, eqs, i, hr, hdone⟩ := captureNext_spec h v hsome
State after:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re

State before:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Tactic:
have ma := matches_of_reaches eq hr hdone
State after:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
ma : Data.Expr.matches m re
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re

State before:
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
ma : Data.Expr.matches m re
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
Tactic:
exact ⟨s, l, m, r, sv, eqs, ma⟩
State after:
no goals