theorem
Regex.VM.eachStepChar.go.induct'
{s : String}
(σ : Strategy s)
(nfa : NFA)
(wf : nfa.WellFormed)
(pos : s.ValidPos)
(ne : pos ≠ s.endValidPos)
(current : SearchState σ nfa)
(motive : (i : ℕ) → i ≤ current.states.count → SearchState σ nfa → Prop)
(base : ∀ (next : SearchState σ nfa), motive current.states.count ⋯ next)
(done :
∀ (i : ℕ) (hlt : i < current.states.count) (next : SearchState σ nfa),
nfa[current.states[i]] = NFA.Node.done → motive i ⋯ next)
(found :
∀ (i : ℕ) (hlt : i < current.states.count) (next : SearchState σ nfa),
nfa[current.states[i]] ≠ NFA.Node.done →
∀ (matched : Option σ.Update) (next' : SearchState σ nfa),
stepChar σ nfa wf pos ne current.updates next current.states[i] = (matched, next') →
matched.isSome = true → motive i ⋯ next)
(not_found :
∀ (i : ℕ) (hlt : i < current.states.count) (next : SearchState σ nfa),
nfa[current.states[i]] ≠ NFA.Node.done →
∀ (matched : Option σ.Update) (next' : SearchState σ nfa),
stepChar σ nfa wf pos ne current.updates next current.states[i] = (matched, next') →
¬matched.isSome = true → motive (i + 1) ⋯ next' → motive i ⋯ next)
(i : ℕ)
(hle : i ≤ current.states.count)
(next : SearchState σ nfa)
:
motive i hle next
@[simp]
theorem
Regex.VM.eachStepChar.go_base
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{ne : pos ≠ s.endValidPos}
{current next : SearchState σ nfa}
:
@[simp]
theorem
Regex.VM.eachStepChar.go_done
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{ne : pos ≠ s.endValidPos}
{current : SearchState σ nfa}
{i : ℕ}
{next : SearchState σ nfa}
(hlt : i < current.states.count)
(hn : nfa[current.states[i]] = NFA.Node.done)
:
@[simp]
theorem
Regex.VM.eachStepChar.go_found
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{ne : pos ≠ s.endValidPos}
{current : SearchState σ nfa}
{i : ℕ}
{next next' : SearchState σ nfa}
{matched : Option σ.Update}
(hlt : i < current.states.count)
(hn : nfa[current.states[i]] ≠ NFA.Node.done)
(h : stepChar σ nfa wf pos ne current.updates next current.states[i] = (matched, next'))
(found : matched.isSome = true)
:
@[simp]
theorem
Regex.VM.eachStepChar.go_not_found
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{ne : pos ≠ s.endValidPos}
{current : SearchState σ nfa}
{i : ℕ}
{next next' : SearchState σ nfa}
{matched : Option σ.Update}
(hlt : i < current.states.count)
(hn : nfa[current.states[i]] ≠ NFA.Node.done)
(h : stepChar σ nfa wf pos ne current.updates next current.states[i] = (matched, next'))
(not_found : ¬matched.isSome = true)
: