internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.captureNext_spec.go
Proof state before:
case inl
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
h : lastMatch = matched
⊢ 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

case inr
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
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ 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:
next h' =>
  subst h
  exact eqs ▸ inv.acceptOfLastMatch
Proof state after:
case inr
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
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ 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
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
h : lastMatch = matched
⊢ 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:
subst h
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 : 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
⊢ 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
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 : 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
⊢ 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
Proof state after:
no goals
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
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
hm : lastMatch.isNone = true
⊢ 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:
generalize he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored at h
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := explored;
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ 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
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := explored;
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ 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:
let (_, current', saveSlots') := explored
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := (fst✝, current', saveSlots');
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ 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
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := (fst✝, current', saveSlots');
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ 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:
simp [hm] at h
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
⊢ 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
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
⊢ 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 mem_current'_iff := exploreεClosure_spec.mem_next_iff he inv.currentClosure
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ 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
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ 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:
generalize hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped at h
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped
h :
  captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch) =
    matched
⊢ 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
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
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)
Proof state after:
no goals
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
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
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:
cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
| inl mem_current =>
  have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
  have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
  subst hr
  exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
| inr cls' =>
  have ⟨l, r, iv⟩ := v.validFor
  have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
  subst hr
  let startPos : String.Pos := ⟨String.utf8Len l⟩
  refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
  . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
  . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
  . have prev : nfa.reaches current'[i] [] := .nil cls'
    exact prev.snoc step cls
Proof state after:
no goals