theorem
Regex.VM.captureNext.go.induct'
(σ : Strategy)
(nfa : NFA)
(wf : nfa.WellFormed)
(motive : String.Iterator → Option σ.Update → SearchState σ nfa → SearchState σ nfa → Prop)
(not_found :
∀ (it : String.Iterator) (matched : Option σ.Update) (current next : SearchState σ nfa),
it.atEnd = true → motive it matched current next)
(found :
∀ (it : String.Iterator) (matched : Option σ.Update) (current next : SearchState σ nfa),
¬it.atEnd = true → current.states.isEmpty = true → matched.isSome = true → motive it matched current next)
(ind_not_found :
∀ (it : String.Iterator) (matched : Option σ.Update) (current next : SearchState σ nfa),
let stepped := eachStepChar σ nfa wf it current next;
let expanded := εClosure σ nfa wf it.next none stepped.2 [(σ.empty, ⟨nfa.start, ⋯⟩)];
¬it.atEnd = true →
matched = none →
stepped.1 = none →
motive it.next expanded.1 expanded.2 { states := current.states.clear, updates := current.updates } →
motive it matched current next)
(ind_found :
∀ (it : String.Iterator) (matched : Option σ.Update) (current next : SearchState σ nfa),
let stepped := eachStepChar σ nfa wf it current next;
¬it.atEnd = true →
(matched.isSome = true → ¬current.states.isEmpty = true) →
matched.isSome = true ∨ stepped.1.isSome = true →
motive it.next (stepped.1 <|> matched) stepped.2
{ states := current.states.clear, updates := current.updates } →
motive it matched current next)
(it : String.Iterator)
(matched : Option σ.Update)
(current next : SearchState σ nfa)
:
motive it matched current next
@[simp]
theorem
Regex.VM.captureNext.go_not_found
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{current next : SearchState σ nfa}
(atEnd : it.atEnd = true)
:
@[simp]
theorem
Regex.VM.captureNext.go_found
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{current next : SearchState σ nfa}
(atEnd : ¬it.atEnd = true)
(isEmpty : current.states.isEmpty = true)
(isSome : matched.isSome = true)
:
@[simp]
theorem
Regex.VM.captureNext.go_ind_not_found
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{current next : SearchState σ nfa}
(stepped expanded : Option σ.Update × SearchState σ nfa)
(eq₁ : stepped = eachStepChar σ nfa wf it current next)
(eq₂ : expanded = εClosure σ nfa wf it.next none stepped.2 [(σ.empty, ⟨nfa.start, ⋯⟩)])
(atEnd : ¬it.atEnd = true)
(isNone₁ : matched = none)
(isNone₂ : stepped.1 = none)
:
@[simp]
theorem
Regex.VM.captureNext.go_ind_found
{σ : Strategy}
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option σ.Update}
{current next : SearchState σ nfa}
(stepped : Option σ.Update × SearchState σ nfa)
(eq : stepped = eachStepChar σ nfa wf it current next)
(atEnd : ¬it.atEnd = true)
(hemp : matched.isSome = true → ¬current.states.isEmpty = true)
(isSome : matched.isSome = true ∨ stepped.1.isSome = true)
: