@[simp]

theorem Regex.Strategy.materializeRegexGroups_empty {s : String} : materializeRegexGroups Data.CaptureGroups.empty = fun (x : ℕ) => none

@[simp]

theorem Regex.Strategy.materializeRegexGroups_group {s : String} {tag : ℕ} {first last : s.ValidPos} {groups : Data.CaptureGroups s} : materializeRegexGroups (Data.CaptureGroups.group tag first last groups) = fun (tag' : ℕ) => if tag = tag' then some (first, last) else materializeRegexGroups groups tag'

@[simp]

theorem Regex.Strategy.materializeRegexGroups_concat {s : String} {g₁ g₂ : Data.CaptureGroups s} : materializeRegexGroups (g₁.concat g₂) = fun (tag : ℕ) => materializeRegexGroups g₂ tag <|> materializeRegexGroups g₁ tag

theorem Regex.Strategy.mem_tags_of_materializeRegexGroups_some {s : String} {e : Data.Expr} {pos pos' : s.ValidPos} {groups : Data.CaptureGroups s} {tag : ℕ} (c : Data.Expr.Captures pos pos' groups e) (isSome : (materializeRegexGroups groups tag).isSome = true) : tag ∈ e.tags

@[simp]

theorem Regex.Strategy.materializeUpdatesAux_snoc {s : String} {n : ℕ} {accum : Vector s.ValidPosPlusOne n} {updates : List (ℕ × s.ValidPos)} {offset : ℕ} {pos : s.ValidPos} : materializeUpdatesAux n accum (updates ++ [(offset, pos)]) = (materializeUpdatesAux n accum updates).setIfInBounds offset (String.ValidPosPlusOne.validPos pos)

theorem Regex.Strategy.materializeUpdatesAux_swap {s : String} {n : ℕ} {accum : Vector s.ValidPosPlusOne n} {updates : List (ℕ × s.ValidPos)} {offset₁ : ℕ} {pos₁ : s.ValidPos} {offset₂ : ℕ} {pos₂ : s.ValidPos} (ne : offset₁ ≠ offset₂) : materializeUpdatesAux n accum ((offset₁, pos₁) :: (offset₂, pos₂) :: updates) = materializeUpdatesAux n accum ((offset₂, pos₂) :: (offset₁, pos₁) :: updates)

theorem Regex.Strategy.materializeUpdatesAux_cons_of_not_in {s : String} {n : ℕ} {accum : Vector s.ValidPosPlusOne n} {updates : List (ℕ × s.ValidPos)} {offset : ℕ} {pos : s.ValidPos} (h : ∀ (offset' : ℕ) (pos' : s.ValidPos), (offset', pos') ∈ updates → offset ≠ offset') : materializeUpdatesAux n accum ((offset, pos) :: updates) = (materializeUpdatesAux n accum updates).setIfInBounds offset (String.ValidPosPlusOne.validPos pos)

@[simp]

theorem Regex.Strategy.materializeUpdatesAux_nil {s : String} {n : ℕ} {accum : Vector s.ValidPosPlusOne n} : materializeUpdatesAux n accum [] = accum

theorem Regex.Strategy.materializeUpdatesAux_append {s : String} {n : ℕ} {accum : Vector s.ValidPosPlusOne n} {updates₁ updates₂ : List (ℕ × s.ValidPos)} : materializeUpdatesAux n accum (updates₁ ++ updates₂) = materializeUpdatesAux n (materializeUpdatesAux n accum updates₁) updates₂

theorem Regex.Strategy.materializeUpdatesAux_getElem {s : String} {n : ℕ} {accum : Vector s.ValidPosPlusOne n} {updates : List (ℕ × s.ValidPos)} {offset : ℕ} (h : offset < n) : (materializeUpdatesAux n accum updates)[offset] = ((materializeUpdatesAux n (Vector.replicate n (String.ValidPosPlusOne.sentinel s)) updates)[offset] <|> accum[offset])

@[simp]

theorem Regex.Strategy.materializeUpdates_empty {s : String} {n : ℕ} : materializeUpdates n [] = Vector.replicate n (String.ValidPosPlusOne.sentinel s)

@[simp]

theorem Regex.Strategy.materializeUpdates_snoc {s : String} {n : ℕ} {updates : List (ℕ × s.ValidPos)} {offset : ℕ} {pos : s.ValidPos} : materializeUpdates n (updates ++ [(offset, pos)]) = (materializeUpdates n updates).setIfInBounds offset (String.ValidPosPlusOne.validPos pos)

theorem Regex.Strategy.materializeUpdates_append_getElem {s : String} {n : ℕ} {updates₁ updates₂ : List (ℕ × s.ValidPos)} {offset : ℕ} (h : offset < n) : (materializeUpdates n (updates₁ ++ updates₂))[offset] = ((materializeUpdates n updates₂)[offset] <|> (materializeUpdates n updates₁)[offset])