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))
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 j : Fin nfa.nodes.size), i ∈ SparseSet.empty → ↑j ∈ nfa.εStep ↑i → j ∈ SparseSet.empty
Tactic:
simp only [hnotMem]
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
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → 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
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → False
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
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
Tactic:
intro i hi
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 : Fin nfa.nodes.size
hi : 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
Theorem: Regex.VM.captureNext_spec
Proof state before:
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 : Fin nfa.nodes.size
hi : 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
Tactic:
have ⟨l, r, v'⟩ := v.validFor
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 : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it ∧ nfa.reaches i m
Theorem: Regex.VM.captureNext_spec
Proof state before:
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 : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it ∧ nfa.reaches i m
Tactic:
let pos : String.Pos := ⟨String.utf8Len l⟩
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 : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it ∧ nfa.reaches i m
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Tactic:
. 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
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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ String.Iterator.ValidFor ([].reverse ++ l.reverse.reverse) r it
Tactic:
simp [v']
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_1.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 : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ Substring.ValidFor l.reverse [] r { str := it.toString, startPos := pos, stopPos := pos }
Tactic:
apply Substring.ValidFor.of_eq <;> simp [v'.toString, List.reverseAux_eq]
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Tactic:
have := (exploreεClosure_spec.mem_next_iff he (by simp only [hnotMem]; simp) i).mp hi
Proof state after:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
this : i ∈ SparseSet.empty ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
this : i ∈ SparseSet.empty ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Tactic:
simp only [hnotMem] at this
Proof state after:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
this : False ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
this : False ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Tactic:
simp at this
Proof state after:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
this : ↑i ∈ nfa.εClosure ↑nfa.start
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Theorem: Regex.VM.captureNext_spec
Proof state before:
case refine_1.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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
this : ↑i ∈ nfa.εClosure ↑nfa.start
⊢ ↑i ∈ nfa.εClosure ↑nfa.start
Tactic:
exact this
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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ SparseSet.empty → ↑j ∈ nfa.εStep ↑i → j ∈ SparseSet.empty
Tactic:
simp only [hnotMem]
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
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → 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
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
i : Fin nfa.nodes.size
hi : i ∈ init'
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → False
Tactic:
simp
Proof state after:
no goals