class String.Slice.Pattern.Model.ForwardPatternModel {ρ : 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 ForwardPatternModel.Matches predicate that implementates 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 ForwardPatternModel.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 : ρ) [ForwardPatternModel 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 : ForwardPatternModel.Matches pat (s.sliceTo endPos).copy

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

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

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

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

Predicate stating that the region between the start of the slice s and the position endPos matches that 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.NoPrefixForwardPatternModel.

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

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

theorem String.Slice.Pattern.Model.IsLongestMatch.eq {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel pat] {s : Slice} {pos pos' : s.Pos} (h : IsLongestMatch pat pos) (h' : IsMatch pat pos') : pos' ≤ pos

class String.Slice.Pattern.Model.NoPrefixForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPatternModel 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) : ForwardPatternModel.Matches pat s → ForwardPatternModel.Matches pat (s ++ t) → t = ""

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

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

structure String.Slice.Pattern.Model.IsLongestMatchAt {ρ : Type} (pat : ρ) [ForwardPatternModel 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 starting at startPos.

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

theorem String.Slice.Pattern.Model.isLongestMatchAt_iff {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) : startPos < endPos

theorem String.Slice.Pattern.Model.IsLongestMatchAt.eq {ρ : Type} {pat : ρ} [ForwardPatternModel 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.IsLongestMatch.isLongestMatchAt_ofSliceFrom {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} (h : IsLongestMatch pat pos) : IsLongestMatchAt pat p₀ (Pos.ofSliceFrom pos)

structure String.Slice.Pattern.Model.MatchesAt {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ (h : pos ≤ endPos), IsMatch pat (pos.sliceFrom endPos h)

noncomputable def String.Slice.Pattern.Model.matchAt? {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel pat] {s : Slice} {startPos : s.Pos} : matchAt? pat startPos = none ↔ ¬MatchesAt pat startPos

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

Predicate stating compatibility between ForwardPatternModel 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 ForwardPatternModel instance.

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

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

inductive String.Slice.Pattern.Model.IsValidSearchFrom {ρ : Type} (pat : ρ) [ForwardPatternModel 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 : ρ} [ForwardPatternModel pat] {s : Slice} : IsValidSearchFrom pat s.endPos []
• matched {ρ : Type} {pat : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ} [ForwardPatternModel 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 : ρ) [ForwardPatternModel 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 ForwardPatternModel 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] [ForwardPatternModel pat] [LawfulForwardPatternModel pat] : LawfulToForwardSearcherModel pat