theorem
Regex.NFA.path_of_captures.group
{s : String}
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{pos pos' : s.ValidPos}
{groups : Data.CaptureGroups s}
{tag : ℕ}
(eq : nfa.pushRegex next (Data.Expr.group tag 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 (ℕ × s.ValidPos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start pos next pos' update)
:
theorem
Regex.NFA.path_of_captures.alternateLeft
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' : s.ValidPos}
{groups : Data.CaptureGroups s}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.alternate 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 (ℕ × s.ValidPos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start pos next pos' update)
:
theorem
Regex.NFA.path_of_captures.alternateRight
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' : s.ValidPos}
{groups : Data.CaptureGroups s}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.alternate 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 (ℕ × s.ValidPos)),
EquivUpdate groups update ∧ result.Path nfa.nodes.size result.start pos next pos' update)
:
theorem
Regex.NFA.path_of_captures.concat
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' pos'' : s.ValidPos}
{e₁ e₂ : Data.Expr}
{groups₁ groups₂ : Data.CaptureGroups s}
(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 (ℕ × s.ValidPos)),
EquivUpdate groups₁ update ∧ result.Path nfa.nodes.size result.start pos next pos' update)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × s.ValidPos)),
EquivUpdate groups₂ update ∧ result.Path nfa.nodes.size result.start pos' next pos'' update)
:
theorem
Regex.NFA.path_of_captures.starConcat
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' pos'' : s.ValidPos}
{greedy : Bool}
{e : Data.Expr}
{groups₁ groups₂ : Data.CaptureGroups s}
(eq : nfa.pushRegex next (Data.Expr.star greedy 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 (ℕ × s.ValidPos)),
EquivUpdate groups₁ update ∧ result.Path nfa.nodes.size result.start pos next pos' update)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA},
nfa.pushRegex next (Data.Expr.star greedy e) = result →
nfa.WellFormed →
next < nfa.nodes.size →
∃ (update : List (ℕ × s.ValidPos)),
EquivUpdate groups₂ update ∧ result.Path nfa.nodes.size result.start pos' next pos'' update)
:
theorem
Regex.NFA.path_of_captures
{s : String}
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{pos pos' : s.ValidPos}
{groups : Data.CaptureGroups s}
(eq : nfa.pushRegex next e = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(c : Data.Expr.Captures pos pos' groups e)
:
theorem
Regex.NFA.path_of_captures_compile
{s : String}
{nfa : NFA}
{e : Data.Expr}
{pos pos' : s.ValidPos}
{groups : Data.CaptureGroups s}
(eq : compile e = nfa)
(c : Data.Expr.Captures pos pos' groups e)
: