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