class String.Slice.Pattern.Model.PatternModel {ρ : Type} (pat : ρ) : Type

This data-carrying typeclass is used to give semantics to a pattern type that implements ForwardPattern and/or ToForwardSearcher by providing an abstract, not necessarily decidable PatternModel.Matches predicate that implementations of ForwardPattern and ToForwardSearcher can be validated against.

Correctness results for generic functions relying on the pattern infrastructure, for example the correctness result for String.Slice.split, are then stated in terms of PatternModel.Matches, and can be specialized to specific patterns from there.

The corresponding compatibility typeclasses are String.Slice.Pattern.Model.LawfulForwardPatternModel and String.Slice.Pattern.Model.LawfulToForwardSearcherModel.

We include the condition that the empty string is not a match. This is necessary for the theory to work out as there is just no reasonable notion of searching that works for the empty string that is still specific enough to yield reasonably strong correctness results for operations based on searching.

This means that pattern types that allow searching for the empty string will have to special-case the empty string in their correctness statements.

• Matches : String → Prop

  The predicate that says which strings match the pattern.

• not_matches_empty : ¬Matches pat ""

structure String.Slice.Pattern.Model.IsMatch {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (endPos : s.Pos) : Prop

Predicate stating that the region between the start of the slice s and the position endPos matches the pattern pat. Note that there might be a longer match, see String.Slice.Pattern.IsLongestMatch.

• matches_copy : PatternModel.Matches pat (s.sliceTo endPos).copy

theorem String.Slice.Pattern.Model.IsMatch.ne_startPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} (h : IsMatch pat pos) : pos ≠ s.startPos

theorem String.Slice.Pattern.Model.isMatch_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsMatch pat pos ↔ PatternModel.Matches pat (s.sliceTo pos).copy

theorem String.Slice.Pattern.Model.isMatch_iff_exists_splits {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsMatch pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits t₁ t₂ ∧ PatternModel.Matches pat t₁

structure String.Slice.Pattern.Model.IsRevMatch {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (startPos : s.Pos) : Prop

Predicate stating that the region between the position startPos and the end of the slice s matches the pattern pat. Note that there might be a longer match.

• matches_copy : PatternModel.Matches pat (s.sliceFrom startPos).copy

theorem String.Slice.Pattern.Model.IsRevMatch.ne_endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} (h : IsRevMatch pat pos) : pos ≠ s.endPos

theorem String.Slice.Pattern.Model.isRevMatch_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsRevMatch pat pos ↔ PatternModel.Matches pat (s.sliceFrom pos).copy

theorem String.Slice.Pattern.Model.isRevMatch_iff_exists_splits {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsRevMatch pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits t₁ t₂ ∧ PatternModel.Matches pat t₂

structure String.Slice.Pattern.Model.IsLongestMatch {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop

Predicate stating that the region between the start of the slice s and the position pos matches the pattern pat, and that there is no longer match starting at the beginning of the slice. This is what a correct matcher should match.

In some cases, being a match and being a longest match will coincide, see String.Slice.Pattern.Model.NoPrefixPatternModel.

• isMatch : IsMatch pat pos
• not_isMatch (pos' : s.Pos) : pos < pos' → ¬IsMatch pat pos'

theorem String.Slice.Pattern.Model.IsLongestMatch.ne_startPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} (h : IsLongestMatch pat pos) : pos ≠ s.startPos

theorem String.Slice.Pattern.Model.IsLongestMatch.eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos} (h : IsLongestMatch pat pos) (h' : IsLongestMatch pat pos') : pos = pos'

theorem String.Slice.Pattern.Model.IsMatch.exists_isLongestMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsMatch pat pos → ∃ (pos' : s.Pos), IsLongestMatch pat pos'

theorem String.Slice.Pattern.Model.IsLongestMatch.le_of_isMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos} (h : IsLongestMatch pat pos) (h' : IsMatch pat pos') : pos' ≤ pos

structure String.Slice.Pattern.Model.IsLongestRevMatch {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop

Predicate stating that the region between the start of the slice s and the position pos matches the pattern pat, and that there is no longer match starting at the beginning of the slice. This is what a correct matcher should match.

In some cases, being a match and being a longest match will coincide, see String.Slice.Pattern.Model.NoPrefixPatternModel.

• isRevMatch : IsRevMatch pat pos
• not_isRevMatch (pos' : s.Pos) : pos' < pos → ¬IsRevMatch pat pos'

theorem String.Slice.Pattern.Model.IsLongestRevMatch.ne_endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} (h : IsLongestRevMatch pat pos) : pos ≠ s.endPos

theorem String.Slice.Pattern.Model.IsLongestRevMatch.eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos} (h : IsLongestRevMatch pat pos) (h' : IsLongestRevMatch pat pos') : pos = pos'

theorem String.Slice.Pattern.Model.IsRevMatch.exists_isLongestRevMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsRevMatch pat pos → ∃ (pos' : s.Pos), IsLongestRevMatch pat pos'

theorem String.Slice.Pattern.Model.IsLongestRevMatch.le_of_isRevMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos} (h : IsLongestRevMatch pat pos) (h' : IsRevMatch pat pos') : pos ≤ pos'

class String.Slice.Pattern.Model.NoPrefixPatternModel {ρ : Type} (pat : ρ) [PatternModel pat] : Prop

Predicate stating that a match for a given pattern is never a proper prefix of another match.

This implies that the notion of match and longest match coincide.

• eq_empty (s t : String) : PatternModel.Matches pat s → PatternModel.Matches pat (s ++ t) → t = ""

theorem String.Slice.Pattern.Model.NoPrefixPatternModel.of_length_eq {ρ : Type} {pat : ρ} [PatternModel pat] (h : ∀ (s t : String), PatternModel.Matches pat s → PatternModel.Matches pat t → s.length = t.length) : NoPrefixPatternModel pat

theorem String.Slice.Pattern.Model.isLongestMatch_iff_isMatch {ρ : Type} (pat : ρ) [PatternModel pat] [NoPrefixPatternModel pat] {s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ IsMatch pat pos

class String.Slice.Pattern.Model.NoSuffixPatternModel {ρ : Type} (pat : ρ) [PatternModel pat] : Prop

Predicate stating that a match for a given pattern is never a proper suffix of another match.

This implies that the notion of reverse match and longest reverse match coincide.

• eq_empty (s t : String) : PatternModel.Matches pat t → PatternModel.Matches pat (s ++ t) → s = ""

theorem String.Slice.Pattern.Model.NoSuffixPatternModel.of_length_eq {ρ : Type} {pat : ρ} [PatternModel pat] (h : ∀ (s t : String), PatternModel.Matches pat s → PatternModel.Matches pat t → s.length = t.length) : NoSuffixPatternModel pat

theorem String.Slice.Pattern.Model.isLongestRevMatch_iff_isRevMatch {ρ : Type} (pat : ρ) [PatternModel pat] [NoSuffixPatternModel pat] {s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ IsRevMatch pat pos

structure String.Slice.Pattern.Model.IsLongestMatchAt {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop

Predicate stating that the slice formed by startPos and endPos contains a match of pat in s and it is longest among matches starting at startPos.

• le : startPos ≤ endPos
• isLongestMatch_sliceFrom : IsLongestMatch pat (startPos.sliceFrom endPos ⋯)

theorem String.Slice.Pattern.Model.isLongestMatchAt_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), IsLongestMatch pat (pos₁.sliceFrom pos₂ h)

theorem String.Slice.Pattern.Model.IsLongestMatchAt.lt {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) : startPos < endPos

theorem String.Slice.Pattern.Model.IsLongestMatchAt.eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos} (h : IsLongestMatchAt pat startPos endPos) (h' : IsLongestMatchAt pat startPos endPos') : endPos = endPos'

theorem String.Slice.Pattern.Model.isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos} {startPos endPos : (s.sliceFrom base).Pos} : IsLongestMatchAt pat startPos endPos ↔ IsLongestMatchAt pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos)

theorem String.Slice.Pattern.Model.IsLongestMatch.isLongestMatchAt_ofSliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} (h : IsLongestMatch pat pos) : IsLongestMatchAt pat p₀ (Pos.ofSliceFrom pos)

@[simp]

theorem String.Slice.Pattern.Model.isLongestMatchAt_startPos_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {endPos : s.Pos} : IsLongestMatchAt pat s.startPos endPos ↔ IsLongestMatch pat endPos

structure String.Slice.Pattern.Model.IsLongestRevMatchAt {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop

Predicate stating that the slice formed by startPos and endPos contains is a match of pat in s and it is longest among matches ending at endPos.

• le : startPos ≤ endPos
• isLongestRevMatch_sliceTo : IsLongestRevMatch pat (endPos.sliceTo startPos ⋯)

theorem String.Slice.Pattern.Model.isLongestRevMatchAt_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), IsLongestRevMatch pat (pos₂.sliceTo pos₁ h)

theorem String.Slice.Pattern.Model.IsLongestRevMatchAt.lt {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) : startPos < endPos

theorem String.Slice.Pattern.Model.IsLongestRevMatchAt.eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos startPos' endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) (h' : IsLongestRevMatchAt pat startPos' endPos) : startPos = startPos'

theorem String.Slice.Pattern.Model.isLongestRevMatchAt_iff_isLongestRevMatchAt_ofSliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos} {startPos endPos : (s.sliceTo base).Pos} : IsLongestRevMatchAt pat startPos endPos ↔ IsLongestRevMatchAt pat (Pos.ofSliceTo startPos) (Pos.ofSliceTo endPos)

theorem String.Slice.Pattern.Model.IsLongestRevMatch.isLongestRevMatchAt_ofSliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} (h : IsLongestRevMatch pat pos) : IsLongestRevMatchAt pat (Pos.ofSliceTo pos) p₀

@[simp]

theorem String.Slice.Pattern.Model.isLongestRevMatchAt_endPos_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos : s.Pos} : IsLongestRevMatchAt pat startPos s.endPos ↔ IsLongestRevMatch pat startPos

structure String.Slice.Pattern.Model.MatchesAt {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop

Predicate stating that there is a (longest) match starting at the given position.

• exists_isLongestMatchAt : ∃ (endPos : s.Pos), IsLongestMatchAt pat pos endPos

theorem String.Slice.Pattern.Model.matchesAt_iff_exists_isLongestMatchAt {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ ∃ (endPos : s.Pos), IsLongestMatchAt pat pos endPos

theorem String.Slice.Pattern.Model.matchesAt_iff_exists_isLongestMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ (h : pos ≤ endPos), IsLongestMatch pat (pos.sliceFrom endPos h)

theorem String.Slice.Pattern.Model.matchesAt_iff_exists_isMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ (h : pos ≤ endPos), IsMatch pat (pos.sliceFrom endPos h)

@[simp]

theorem String.Slice.Pattern.Model.not_matchesAt_endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} : ¬MatchesAt pat s.endPos

theorem String.Slice.Pattern.Model.matchesAt_iff_matchesAt_ofSliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos} {pos : (s.sliceFrom base).Pos} : MatchesAt pat pos ↔ MatchesAt pat (Pos.ofSliceFrom pos)

theorem String.Slice.Pattern.Model.IsLongestMatchAt.matchesAt {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) : MatchesAt pat startPos

structure String.Slice.Pattern.Model.RevMatchesAt {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos) : Prop

Predicate stating that there is a (longest) match ending at the given position.

• exists_isLongestRevMatchAt : ∃ (startPos : s.Pos), IsLongestRevMatchAt pat startPos pos

theorem String.Slice.Pattern.Model.revMatchesAt_iff_exists_isLongestRevMatchAt {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ ∃ (startPos : s.Pos), IsLongestRevMatchAt pat startPos pos

theorem String.Slice.Pattern.Model.revMatchesAt_iff_exists_isLongestRevMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ ∃ (startPos : s.Pos), ∃ (h : startPos ≤ pos), IsLongestRevMatch pat (pos.sliceTo startPos h)

theorem String.Slice.Pattern.Model.revMatchesAt_iff_exists_isRevMatch {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ ∃ (startPos : s.Pos), ∃ (h : startPos ≤ pos), IsRevMatch pat (pos.sliceTo startPos h)

@[simp]

theorem String.Slice.Pattern.Model.not_revMatchesAt_startPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} : ¬RevMatchesAt pat s.startPos

theorem String.Slice.Pattern.Model.revMatchesAt_iff_revMatchesAt_ofSliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos} {pos : (s.sliceTo base).Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat (Pos.ofSliceTo pos)

theorem String.Slice.Pattern.Model.IsLongestRevMatchAt.revMatchesAt {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) : RevMatchesAt pat endPos

noncomputable def String.Slice.Pattern.Model.matchAt? {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (startPos : s.Pos) : Option s.Pos

Noncomputable model function returning the end point of the longest match starting at the given position, or none if there is no match.

Equations

• String.Slice.Pattern.Model.matchAt? pat startPos = if h : ∃ (endPos : s.Pos), String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos then some h.choose else none

@[simp]

theorem String.Slice.Pattern.Model.matchAt?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} : matchAt? pat startPos = some endPos ↔ IsLongestMatchAt pat startPos endPos

@[simp]

theorem String.Slice.Pattern.Model.matchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos : s.Pos} : matchAt? pat startPos = none ↔ ¬MatchesAt pat startPos

noncomputable def String.Slice.Pattern.Model.revMatchAt? {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} (endPos : s.Pos) : Option s.Pos

Noncomputable model function returning the start point of the longest match ending at the given position, or none if there is no match.

Equations

• String.Slice.Pattern.Model.revMatchAt? pat endPos = if h : ∃ (startPos : s.Pos), String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos then some h.choose else none

@[simp]

theorem String.Slice.Pattern.Model.revMatchAt?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} : revMatchAt? pat endPos = some startPos ↔ IsLongestRevMatchAt pat startPos endPos

@[simp]

theorem String.Slice.Pattern.Model.revMatchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {endPos : s.Pos} : revMatchAt? pat endPos = none ↔ ¬RevMatchesAt pat endPos

class String.Slice.Pattern.Model.LawfulForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPattern pat] [PatternModel pat] extends String.Slice.Pattern.LawfulForwardPattern pat : Prop

Predicate stating compatibility between PatternModel and ForwardPattern.

This extends LawfulForwardPattern, but it is much stronger because it forces the ForwardPattern to match the longest prefix of the given slice that matches the property supplied by the PatternModel instance.

• skipPrefixOfNonempty?_eq {s : Slice} (h : s.isEmpty = false) : ForwardPattern.skipPrefixOfNonempty? pat s h = ForwardPattern.skipPrefix? pat s
• startsWith_eq (s : Slice) : ForwardPattern.startsWith pat s = (ForwardPattern.skipPrefix? pat s).isSome
• skipPrefix?_eq_some_iff {s : Slice} (pos : s.Pos) : ForwardPattern.skipPrefix? pat s = some pos ↔ IsLongestMatch pat pos

theorem String.Slice.Pattern.Model.LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat] [LawfulForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} : ForwardPattern.skipPrefix? pat (s.sliceFrom p₀) = none ↔ ¬MatchesAt pat p₀

theorem String.Slice.Pattern.Model.LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat] [LawfulForwardPatternModel pat] {s : Slice} : ForwardPattern.skipPrefix? pat s = none ↔ ¬MatchesAt pat s.startPos

class String.Slice.Pattern.Model.LawfulBackwardPatternModel {ρ : Type} (pat : ρ) [BackwardPattern pat] [PatternModel pat] extends String.Slice.Pattern.LawfulBackwardPattern pat : Prop

Predicate stating compatibility between PatternModel and BackwardPattern.

This extends LawfulBackwardPattern, but it is much stronger because it forces the BackwardPattern to match the longest prefix of the given slice that matches the property supplied by the PatternModel instance.

• skipSuffixOfNonempty?_eq {s : Slice} (h : s.isEmpty = false) : BackwardPattern.skipSuffixOfNonempty? pat s h = BackwardPattern.skipSuffix? pat s
• endsWith_eq (s : Slice) : BackwardPattern.endsWith pat s = (BackwardPattern.skipSuffix? pat s).isSome
• skipSuffix?_eq_some_iff {s : Slice} (pos : s.Pos) : BackwardPattern.skipSuffix? pat s = some pos ↔ IsLongestRevMatch pat pos

theorem String.Slice.Pattern.Model.LawfulBackwardPatternModel.skipSuffix?_sliceTo_eq_none_iff {ρ : Type} {pat : ρ} [BackwardPattern pat] [PatternModel pat] [LawfulBackwardPatternModel pat] {s : Slice} {p₀ : s.Pos} : BackwardPattern.skipSuffix? pat (s.sliceTo p₀) = none ↔ ¬RevMatchesAt pat p₀

theorem String.Slice.Pattern.Model.LawfulBackwardPatternModel.skipSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [BackwardPattern pat] [PatternModel pat] [LawfulBackwardPatternModel pat] {s : Slice} : BackwardPattern.skipSuffix? pat s = none ↔ ¬RevMatchesAt pat s.endPos

inductive String.Slice.Pattern.Model.IsValidSearchFrom {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} : s.Pos → List (SearchStep s) → Prop

Inductive predicate stating that a list of search steps represents a valid search from a given position in a slice.

"Searching" here means always taking the longest match at the first position where the pattern matches.

Hence, this predicate determines the list of search steps up to grouping of rejections.

• endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} : IsValidSearchFrom pat s.endPos []
• matched {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {l : List (SearchStep s)} {startPos endPos : s.Pos} : IsLongestMatchAt pat startPos endPos → IsValidSearchFrom pat endPos l → IsValidSearchFrom pat startPos (SearchStep.matched startPos endPos :: l)
• mismatched {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {l : List (SearchStep s)} {startPos endPos : s.Pos} : startPos < endPos → (∀ (pos : s.Pos), startPos ≤ pos → pos < endPos → ¬MatchesAt pat pos) → IsValidSearchFrom pat endPos l → IsValidSearchFrom pat startPos (SearchStep.rejected startPos endPos :: l)

theorem String.Slice.Pattern.Model.IsValidSearchFrom.matched_of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos startPos' endPos : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidSearchFrom pat endPos l) (h₂ : IsLongestMatchAt pat startPos' endPos) (h₃ : startPos = startPos') : IsValidSearchFrom pat startPos' (SearchStep.matched startPos endPos :: l)

theorem String.Slice.Pattern.Model.IsValidSearchFrom.mismatched_of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos startPos' endPos : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidSearchFrom pat endPos l) (h₀ : startPos' < endPos) (h₂ : ∀ (pos : s.Pos), startPos' ≤ pos → pos < endPos → ¬MatchesAt pat pos) (h₃ : startPos = startPos') : IsValidSearchFrom pat startPos' (SearchStep.rejected startPos endPos :: l)

theorem String.Slice.Pattern.Model.IsValidSearchFrom.endPos_of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {l : List (SearchStep s)} (hp : p = s.endPos) (hl : l = []) : IsValidSearchFrom pat p l

class String.Slice.Pattern.Model.LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type} [ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] : Prop

Predicate stating compatibility between PatternModel and ToForwardSearcher.

We require the searcher to always match the longest match at the first position where the pattern matches; see IsValidSearchFrom.

• isValidSearchFrom_toList (s : Slice) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList

theorem String.Slice.Pattern.Model.LawfulToForwardSearcherModel.defaultImplementation {ρ : Type} {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat] [PatternModel pat] [LawfulForwardPatternModel pat] : LawfulToForwardSearcherModel pat

inductive String.Slice.Pattern.Model.IsValidRevSearchFrom {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice} : s.Pos → List (SearchStep s) → Prop

Inductive predicate stating that a list of search steps represents a valid backwards search from a given position in a slice.

"Searching" here means always taking the longest match at the first position where the pattern matches.

Hence, this predicate determines the list of search steps up to grouping of rejections.

• startPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} : IsValidRevSearchFrom pat s.startPos []
• matched {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {l : List (SearchStep s)} {startPos endPos : s.Pos} : IsLongestRevMatchAt pat startPos endPos → IsValidRevSearchFrom pat startPos l → IsValidRevSearchFrom pat endPos (SearchStep.matched startPos endPos :: l)
• mismatched {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {l : List (SearchStep s)} {startPos endPos : s.Pos} : startPos < endPos → (∀ (pos : s.Pos), startPos < pos → pos ≤ endPos → ¬RevMatchesAt pat pos) → IsValidRevSearchFrom pat startPos l → IsValidRevSearchFrom pat endPos (SearchStep.rejected startPos endPos :: l)

theorem String.Slice.Pattern.Model.IsValidRevSearchFrom.matched_of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidRevSearchFrom pat startPos l) (h₂ : IsLongestRevMatchAt pat startPos endPos') (h₃ : endPos = endPos') : IsValidRevSearchFrom pat endPos' (SearchStep.matched startPos endPos :: l)

theorem String.Slice.Pattern.Model.IsValidRevSearchFrom.mismatched_of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidRevSearchFrom pat startPos l) (h₀ : startPos < endPos') (h₂ : ∀ (pos : s.Pos), startPos < pos → pos ≤ endPos' → ¬RevMatchesAt pat pos) (h₃ : endPos = endPos') : IsValidRevSearchFrom pat endPos' (SearchStep.rejected startPos endPos :: l)

theorem String.Slice.Pattern.Model.IsValidRevSearchFrom.startPos_of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {l : List (SearchStep s)} (hp : p = s.startPos) (hl : l = []) : IsValidRevSearchFrom pat p l

class String.Slice.Pattern.Model.LawfulToBackwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type} [ToBackwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] : Prop

Predicate stating compatibility between PatternModel and ToBackwardSearcher.

We require the searcher to always match the longest match at the first position where the pattern matches; see IsValidRevSearchFrom.

• isValidRevSearchFrom_toList (s : Slice) : IsValidRevSearchFrom pat s.endPos (ToBackwardSearcher.toSearcher pat s).toList

theorem String.Slice.Pattern.Model.LawfulToBackwardSearcherModel.defaultImplementation {ρ : Type} {pat : ρ} [BackwardPattern pat] [StrictBackwardPattern pat] [PatternModel pat] [LawfulBackwardPatternModel pat] : LawfulToBackwardSearcherModel pat