theorem
Regex.NFA.path_of_captures.group
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{it it' : String.Iterator}
{groups : Data.CaptureGroups}
{tag : ℕ}
(eq : nfa.pushRegex next (Data.Expr.group tag e) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(v : it.Valid)
(v' : it'.Valid)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start it next it' update)
:
∃ (update : List (ℕ × String.Pos)),
EquivUpdate (Data.CaptureGroups.group tag it.pos it'.pos groups) update ∧ result.Path nfa.nodes.size result.start it next it' update
theorem
Regex.NFA.path_of_captures.alternateLeft
{nfa : NFA}
{next : ℕ}
{result : NFA}
{it it' : String.Iterator}
{groups : Data.CaptureGroups}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.alternate e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(v : it.Valid)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e₁ = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start it next it' update)
:
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start it next it' update
theorem
Regex.NFA.path_of_captures.alternateRight
{nfa : NFA}
{next : ℕ}
{result : NFA}
{it it' : String.Iterator}
{groups : Data.CaptureGroups}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.alternate e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(v : it.Valid)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start it next it' update)
:
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start it next it' update
theorem
Regex.NFA.path_of_captures.concat
{nfa : NFA}
{next : ℕ}
{result : NFA}
{e₁ e₂ : Data.Expr}
{it it' it'' : String.Iterator}
{groups₁ groups₂ : Data.CaptureGroups}
(eq : nfa.pushRegex next (e₁.concat e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(ih₁ :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e₁ = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups₁ update ∧ result.Path nfa.nodes.size result.start it next it' update)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups₂ update ∧ result.Path nfa.nodes.size result.start it' next it'' update)
:
theorem
Regex.NFA.path_of_captures.starConcat
{nfa : NFA}
{next : ℕ}
{result : NFA}
{e : Data.Expr}
{it it' it'' : String.Iterator}
{groups₁ groups₂ : Data.CaptureGroups}
(eq : nfa.pushRegex next e.star = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(v : it.Valid)
(ih₁ :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups₁ update ∧ result.Path nfa.nodes.size result.start it next it' update)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e.star = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups₂ update ∧ result.Path nfa.nodes.size result.start it' next it'' update)
:
theorem
Regex.NFA.path_of_captures
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{it it' : String.Iterator}
{groups : Data.CaptureGroups}
(eq : nfa.pushRegex next e = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(c : Data.Expr.Captures it it' groups e)
:
∃ (update : List (ℕ × String.Pos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start it next it' update
theorem
Regex.NFA.path_of_captures_compile
{nfa : NFA}
{e : Data.Expr}
{it it' : String.Iterator}
{groups : Data.CaptureGroups}
(eq : compile e = nfa)
(c : Data.Expr.Captures it it' groups e)
:
∃ (update : List (ℕ × String.Pos)), EquivUpdate groups update ∧ nfa.Path 1 nfa.start it 0 it' update