Theorem: Regex.VM.captureNext_spec.go (RegexCorrectness/VM/Basic.lean)

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
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
  ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
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
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

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
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
State after:
no goals

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'
⊢ ∃ 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 ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
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''
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

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''
⊢ ∃ 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 ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
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 l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

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 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 ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current[i] (SparseSet.mem_get isLt)
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
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

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
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

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
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
Tactic:
subst hr
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 : List Char
prev : nfa.reaches current[i] m
r' : List Char
sv : Substring.ValidFor l m (it.curr :: r') s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) (it.curr :: r') it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

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 : List Char
prev : nfa.reaches current[i] m
r' : List Char
sv : Substring.ValidFor l m (it.curr :: r') s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) (it.curr :: r') it
⊢ ∃ 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:
exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
State after:
no goals

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 : List Char
prev : nfa.reaches current[i] m
r' : List Char
sv : Substring.ValidFor l m (it.curr :: r') s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) (it.curr :: r') it
⊢ String.Iterator.ValidFor ((m ++ [it.curr]).reverse ++ l.reverse) r' it.next
Tactic:
simp [iv.next]
State after:
no goals

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
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
h : (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
cases matched' with
| none =>
  simp at h
  exact eqs ▸ inv.acceptOfLastMatch h
| some =>
  have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
  have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
  have eqs' := iv.toString
  simp [String.Iterator.next, List.reverseAux_eq] at eqs'
  exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
State after:
no goals

State before:
case none
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (none, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse none fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse none fun x => lastMatch).isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp at h
State after:
case none
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (none, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse none fun x => lastMatch) =
    matched
h : lastMatch.isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case none
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (none, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse none fun x => lastMatch) =
    matched
h : lastMatch.isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact eqs ▸ inv.acceptOfLastMatch h
State after:
no goals

State before:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
State after:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
State after:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have eqs' := iv.toString
State after:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.next.s = { data := (m.reverse ++ l.reverse).reverseAux r }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.next.s = { data := (m.reverse ++ l.reverse).reverseAux r }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp [String.Iterator.next, List.reverseAux_eq] at eqs'
State after:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
State after:
no goals

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
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ haystack = { data := l ++ m ++ r }
Tactic:
simp [eqs, eqs']
State after:
no goals

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
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ haystack = it.next.toString
Tactic:
simp [eqs, String.Iterator.next]
State after:
no goals

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
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ current.clear.isEmpty = true
Tactic:
simp
State after:
no goals