theorem
Regex.NFA.captures_of_path.group
{s : String}
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
{tag : ℕ}
(eq : nfa.pushRegex next (Data.Expr.group tag e) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start pos next pos' update)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
nfa.pushRegex next e = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start pos next pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e)
:
∃ (groups : Data.CaptureGroups s),
EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups (Data.Expr.group tag e)
theorem
Regex.NFA.captures_of_path.alternate
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.alternate e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start pos next pos' update)
(ih₁ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
nfa.pushRegex next e₁ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start pos next pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e₁)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start pos next pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e₂)
:
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups (e₁.alternate e₂)
theorem
Regex.NFA.captures_of_path.concat
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.concat e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start pos next pos' update)
(ih₁ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
nfa.pushRegex next e₁ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start pos next pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e₁)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start pos next pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e₂)
:
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups (e₁.concat e₂)
theorem
Regex.NFA.captures_of_path.star_of_loop
{s : String}
{e : Data.Expr}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
[Compile.ProofData.Star]
{greedy : Bool}
(loop : Compile.ProofData.Star.Loop pos pos' update)
(ih :
∀ {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
Compile.ProofData.nfa'.Path Compile.ProofData.Star.nfaPlaceholder.nodes.size Compile.ProofData.Star.nfaExpr.start
pos Compile.ProofData.Star.nfaPlaceholder.start pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e)
:
∃ (groups : Data.CaptureGroups s),
EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups (Data.Expr.star greedy e)
theorem
Regex.NFA.captures_of_path.star
{s : String}
{nfa : NFA}
{next : ℕ}
{result : NFA}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
{greedy : Bool}
{e : Data.Expr}
(eq : nfa.pushRegex next (Data.Expr.star greedy e) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start pos next pos' update)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {pos pos' : s.ValidPos} {update : List (ℕ × s.ValidPos)},
nfa.pushRegex next e = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start pos next pos' update →
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e)
:
∃ (groups : Data.CaptureGroups s),
EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups (Data.Expr.star greedy e)
theorem
Regex.NFA.captures_of_path
{s : String}
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
(eq : nfa.pushRegex next e = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start pos next pos' update)
:
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e
theorem
Regex.NFA.captures_of_path_compile
{s : String}
{nfa : NFA}
{e : Data.Expr}
{pos pos' : s.ValidPos}
{update : List (ℕ × s.ValidPos)}
(eq : compile e = nfa)
(path : nfa.Path 1 nfa.start pos 0 pos' update)
:
∃ (groups : Data.CaptureGroups s), EquivUpdate groups update ∧ Data.Expr.Captures pos pos' groups e