Theorem: Regex.VM.captureNext_spec.go
Proof state before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it
prev : nfa.reaches current[i] m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
Proof state after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it
prev : nfa.reaches current[i] m
r' : List Char
hr : r = it.curr :: r'
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m