internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
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 } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
unfold captureNext at h
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
h :
  (let saveSlots := Vec.ofFn fun x => captureNext.initSave saveSize;
    match exploreεClosure nfa it.pos SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] with
    | (matched, init, saveSlots) => captureNext.go nfa saveSize it init SparseSet.empty saveSlots matched) =
    matched
v : it.Valid
hsome : matched.isSome = true
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
h :
  (let saveSlots := Vec.ofFn fun x => captureNext.initSave saveSize;
    match exploreεClosure nfa it.pos SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] with
    | (matched, init, saveSlots) => captureNext.go nfa saveSize it init SparseSet.empty saveSlots matched) =
    matched
v : it.Valid
hsome : matched.isSome = true
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
generalize _hs : Vec.ofFn (fun _ => captureNext.initSave saveSize) = saveSlots at h
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
h :
  (let saveSlots := saveSlots;
    match exploreεClosure nfa it.pos SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] with
    | (matched, init, saveSlots) => captureNext.go nfa saveSize it init SparseSet.empty saveSlots matched) =
    matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
h :
  (let saveSlots := saveSlots;
    match exploreεClosure nfa it.pos SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] with
    | (matched, init, saveSlots) => captureNext.go nfa saveSize it init SparseSet.empty saveSlots matched) =
    matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp at h
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
h :
  captureNext.go nfa saveSize it
      (exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[]).2.1
      SparseSet.empty
      (exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[]).2.2
      (exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[]).1 =
    matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
h :
  captureNext.go nfa saveSize it
      (exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[]).2.1
      SparseSet.empty
      (exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[]).2.2
      (exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[]).1 =
    matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
generalize he : exploreεClosure nfa it.i .empty (captureNext.initSave saveSize) .none saveSlots nfa.start #[] = init at h
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] = init
h : captureNext.go nfa saveSize it init.2.1 SparseSet.empty init.2.2 init.1 = matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] = init
h : captureNext.go nfa saveSize it init.2.1 SparseSet.empty init.2.2 init.1 = matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
let (matched', init', saveSlots) := init
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h :
  captureNext.go nfa saveSize it (matched', init', saveSlots).2.1 SparseSet.empty (matched', init', saveSlots).2.2
      (matched', init', saveSlots).1 =
    matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h :
  captureNext.go nfa saveSize it (matched', init', saveSlots).2.1 SparseSet.empty (matched', init', saveSlots).2.2
      (matched', init', saveSlots).1 =
    matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp at h
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have hnotMem (i : Fin nfa.nodes.size) : ¬i ∈ SparseSet.empty := by
  simp only [SparseSet.not_mem_of_isEmpty SparseSet.isEmpty_empty]
  simp
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have inv : captureNext.go.Inv nfa it it.toString init' matched' := by
  refine ⟨exploreεClosure_spec.preserve_cls he (by simp only [hnotMem]; simp), ?_, ?_⟩
  . intro i hi
    have ⟨l, r, v'⟩ := v.validFor
    let pos : String.Pos := ⟨String.utf8Len l⟩
    refine ⟨⟨it.toString, pos, pos⟩, l.reverse, [], r, ?_, by simp [v'], .nil ?_⟩
    . apply Substring.ValidFor.of_eq <;> simp [v'.toString, List.reverseAux_eq]
    . have := (exploreεClosure_spec.mem_next_iff he (by simp only [hnotMem]; simp) i).mp hi
      simp only [hnotMem] at this
      simp at this
      exact this
  . intro hsome
    have ⟨i, hi, hdone⟩ := (exploreεClosure_mem_done_iff he (by simp only [hnotMem]; simp)).mpr hsome
    have cls := (exploreεClosure_spec.mem_next_iff he (by simp only [hnotMem]; simp) i).mp hi
    simp only [hnotMem] at cls
    simp at cls
    have ⟨l, r, v'⟩ := v.validFor
    let pos : String.Pos := ⟨String.utf8Len l⟩
    refine ⟨⟨it.toString, pos, pos⟩, l.reverse, [], r, ?_, by simp [v'.toString, List.reverseAux_eq], ⟨i, .nil cls, hdone⟩⟩
    apply Substring.ValidFor.of_eq <;> simp [v'.toString, List.reverseAux_eq]
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
inv : captureNext.go.Inv nfa it it.toString init' matched'
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
inv : captureNext.go.Inv nfa it it.toString init' matched'
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact captureNext_spec.go h inv v rfl (by simp) hsome
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
i : Fin nfa.nodes.size
⊢ i ∉ SparseSet.empty
Tactic:
simp only [SparseSet.not_mem_of_isEmpty SparseSet.isEmpty_empty]
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
i : Fin nfa.nodes.size
⊢ ¬False
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
i : Fin nfa.nodes.size
⊢ ¬False
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ captureNext.go.Inv nfa it it.toString init' matched'
Tactic:
refine ⟨exploreεClosure_spec.preserve_cls he (by simp only [hnotMem]; simp), ?_, ?_⟩
Proof state after:
case refine_1
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ ∀ i ∈ init',
    ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it ∧ nfa.reaches i m

case refine_2
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ matched'.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_2
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ matched'.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
. intro hsome
  have ⟨i, hi, hdone⟩ := (exploreεClosure_mem_done_iff he (by simp only [hnotMem]; simp)).mpr hsome
  have cls := (exploreεClosure_spec.mem_next_iff he (by simp only [hnotMem]; simp) i).mp hi
  simp only [hnotMem] at cls
  simp at cls
  have ⟨l, r, v'⟩ := v.validFor
  let pos : String.Pos := ⟨String.utf8Len l⟩
  refine ⟨⟨it.toString, pos, pos⟩, l.reverse, [], r, ?_, by simp [v'.toString, List.reverseAux_eq], ⟨i, .nil cls, hdone⟩⟩
  apply Substring.ValidFor.of_eq <;> simp [v'.toString, List.reverseAux_eq]
Proof state after:
no goals