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.

• Matches : String → Prop

  The predicate that says which strings match the pattern.

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

Type class for 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.

• not_matches_empty : ¬PatternModel.Matches pat ""

theorem String.Slice.Pattern.Model.not_matches_empty {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] : ¬PatternModel.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] [StrictPatternModel 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₁

@[simp]

theorem String.Slice.Pattern.Model.isMatch_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (h : s.copy = t.copy) {pos : s.Pos} : IsMatch pat (pos.cast h) ↔ IsMatch pat pos

@[simp]

theorem String.Slice.Pattern.Model.isMatch_sliceTo_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos p : s.Pos} {h : pos ≤ p} : IsMatch pat (p.sliceTo pos h) ↔ IsMatch pat pos

@[simp]

theorem String.Slice.Pattern.Model.isMatch_ofSliceTo_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceTo p).Pos} : IsMatch pat (Pos.ofSliceTo pos) ↔ IsMatch pat pos

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] [StrictPatternModel 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₂

@[simp]

theorem String.Slice.Pattern.Model.isRevMatch_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (h : s.copy = t.copy) {pos : s.Pos} : IsRevMatch pat (pos.cast h) ↔ IsRevMatch pat pos

@[simp]

theorem String.Slice.Pattern.Model.isRevMatch_sliceFrom_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos p : s.Pos} {h : p ≤ pos} : IsRevMatch pat (p.sliceFrom pos h) ↔ IsRevMatch pat pos

@[simp]

theorem String.Slice.Pattern.Model.isRevMatch_ofSliceFrom_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceFrom p).Pos} : IsRevMatch pat (Pos.ofSliceFrom pos) ↔ IsRevMatch pat pos

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_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ IsMatch pat pos ∧ ∀ (pos' : s.Pos), pos < pos' → ¬IsMatch pat pos'

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

@[simp]

theorem String.Slice.Pattern.Model.not_isLongestMatch_startPos {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} : ¬IsLongestMatch pat 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

@[simp]

theorem String.Slice.Pattern.Model.isLongestMatch_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : IsLongestMatch pat (pos.cast hst) ↔ IsLongestMatch pat pos

theorem String.Slice.Pattern.Model.IsLongestMatch.of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} {pos : s.Pos} {pos' : t.Pos} (h : IsLongestMatch pat pos) (h₁ : s.copy = t.copy) (h₂ : pos.cast h₁ = pos') : IsLongestMatch pat pos'

theorem String.Slice.Pattern.Model.IsLongestMatch.sliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} (h : IsLongestMatch pat pos) (p : s.Pos) (hp : pos ≤ p) : IsLongestMatch pat (p.sliceTo pos hp)

theorem String.Slice.Pattern.Model.isLongestMatch_of_ofSliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceTo p).Pos} (h : IsLongestMatch pat (Pos.ofSliceTo pos)) : IsLongestMatch pat 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_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ IsRevMatch pat pos ∧ ∀ (pos' : s.Pos), pos' < pos → ¬IsRevMatch pat pos'

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

@[simp]

theorem String.Slice.Pattern.Model.not_isLongestRevMatch_endPos {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} : ¬IsLongestRevMatch pat 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'

@[simp]

theorem String.Slice.Pattern.Model.isLongestRevMatch_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : IsLongestRevMatch pat (pos.cast hst) ↔ IsLongestRevMatch pat pos

theorem String.Slice.Pattern.Model.IsLongestRevMatch.of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} {pos : s.Pos} {pos' : t.Pos} (h : IsLongestRevMatch pat pos) (h₁ : s.copy = t.copy) (h₂ : pos.cast h₁ = pos') : IsLongestRevMatch pat pos'

theorem String.Slice.Pattern.Model.IsLongestRevMatch.sliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} (h : IsLongestRevMatch pat pos) (p : s.Pos) (hp : p ≤ pos) : IsLongestRevMatch pat (p.sliceFrom pos hp)

theorem String.Slice.Pattern.Model.isLongestRevMatch_of_ofSliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceFrom p).Pos} (h : IsLongestRevMatch pat (Pos.ofSliceFrom pos)) : IsLongestRevMatch pat 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_toList_eq {ρ : Type} {pat : ρ} [PatternModel pat] (h : ∀ (s t : String), PatternModel.Matches pat s → PatternModel.Matches pat t → s.toList.length = t.toList.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_toList_eq {ρ : Type} {pat : ρ} [PatternModel pat] (h : ∀ (s t : String), PatternModel.Matches pat s → PatternModel.Matches pat t → s.toList.length = t.toList.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] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) : startPos < endPos

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

@[simp]

theorem String.Slice.Pattern.Model.not_isLongestMatchAt_self {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos : s.Pos} : ¬IsLongestMatchAt pat startPos startPos

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

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

theorem String.Slice.Pattern.Model.IsLongestMatchAt.matches_slice {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) : PatternModel.Matches pat (s.slice startPos endPos ⋯).copy

@[simp]

theorem String.Slice.Pattern.Model.isLongestMatchAt_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {startPos endPos : s.Pos} : IsLongestMatchAt pat (startPos.cast hst) (endPos.cast hst) ↔ IsLongestMatchAt pat startPos endPos

theorem String.Slice.Pattern.Model.IsLongestMatchAt.of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} {s₁ e₁ : s.Pos} {s₂ e₂ : t.Pos} (h : IsLongestMatchAt pat s₁ e₁) (h₁ : s.copy = t.copy) (h₂ : s₁.cast h₁ = s₂) (h₃ : e₁.cast h₁ = e₂) : IsLongestMatchAt pat s₂ e₂

theorem String.Slice.Pattern.Model.IsLongestMatchAt.sliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) (p : s.Pos) (hp : endPos ≤ p) : IsLongestMatchAt pat (p.sliceTo startPos ⋯) (p.sliceTo endPos hp)

theorem String.Slice.Pattern.Model.isLongestMatchAt_of_ofSliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {startPos endPos : (s.sliceTo p).Pos} (h : IsLongestMatchAt pat (Pos.ofSliceTo startPos) (Pos.ofSliceTo endPos)) : IsLongestMatchAt pat startPos endPos

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

Predicate stating that the range between two positions of s can be covered by longest matches of the pattern within s.

• nil {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} (p : s.Pos) : IsLongestMatchAtChain pat p p
• cons {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} (startPos middlePos endPos : s.Pos) : IsLongestMatchAt pat startPos middlePos → IsLongestMatchAtChain pat middlePos endPos → IsLongestMatchAtChain pat startPos endPos

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

theorem String.Slice.Pattern.Model.IsLongestMatchAtChain.le {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAtChain pat startPos endPos) : startPos ≤ endPos

theorem String.Slice.Pattern.Model.IsLongestMatchAtChain.sliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAtChain pat startPos endPos) (p : s.Pos) (hp : endPos ≤ p) : IsLongestMatchAtChain pat (p.sliceTo startPos ⋯) (p.sliceTo endPos hp)

theorem String.Slice.Pattern.Model.isLongestMatchAtChain_of_ofSliceTo {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {startPos endPos : (s.sliceTo p).Pos} (h : IsLongestMatchAtChain pat (Pos.ofSliceTo startPos) (Pos.ofSliceTo endPos)) : IsLongestMatchAtChain pat startPos 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] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) : startPos < endPos

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

@[simp]

theorem String.Slice.Pattern.Model.not_isLongestRevMatchAt_self {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {endPos : s.Pos} : ¬IsLongestRevMatchAt pat endPos 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

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

theorem String.Slice.Pattern.Model.IsLongestRevMatchAt.matches_slice {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) : PatternModel.Matches pat (s.slice startPos endPos ⋯).copy

@[simp]

theorem String.Slice.Pattern.Model.isLongestRevMatchAt_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {startPos endPos : s.Pos} : IsLongestRevMatchAt pat (startPos.cast hst) (endPos.cast hst) ↔ IsLongestRevMatchAt pat startPos endPos

theorem String.Slice.Pattern.Model.IsLongestRevMatchAt.of_eq {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} {s₁ e₁ : s.Pos} {s₂ e₂ : t.Pos} (h : IsLongestRevMatchAt pat s₁ e₁) (h₁ : s.copy = t.copy) (h₂ : s₁.cast h₁ = s₂) (h₃ : e₁.cast h₁ = e₂) : IsLongestRevMatchAt pat s₂ e₂

theorem String.Slice.Pattern.Model.IsLongestRevMatchAt.sliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) (p : s.Pos) (hp : p ≤ startPos) : IsLongestRevMatchAt pat (p.sliceFrom startPos hp) (p.sliceFrom endPos ⋯)

theorem String.Slice.Pattern.Model.isLongestRevMatchAt_of_ofSliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {startPos endPos : (s.sliceFrom p).Pos} (h : IsLongestRevMatchAt pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos)) : IsLongestRevMatchAt pat startPos endPos

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

Predicate stating that the range between two positions of s can be covered by longest reverse matches of the pattern within s.

• nil {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} (p : s.Pos) : IsLongestRevMatchAtChain pat p p
• cons {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} (startPos middlePos endPos : s.Pos) : IsLongestRevMatchAtChain pat startPos middlePos → IsLongestRevMatchAt pat middlePos endPos → IsLongestRevMatchAtChain pat startPos endPos

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

theorem String.Slice.Pattern.Model.IsLongestRevMatchAtChain.le {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAtChain pat startPos endPos) : startPos ≤ endPos

theorem String.Slice.Pattern.Model.IsLongestRevMatchAtChain.sliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAtChain pat startPos endPos) (p : s.Pos) (hp : p ≤ startPos) : IsLongestRevMatchAtChain pat (p.sliceFrom startPos hp) (p.sliceFrom endPos ⋯)

theorem String.Slice.Pattern.Model.isLongestRevMatchAtChain_of_ofSliceFrom {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {startPos endPos : (s.sliceFrom p).Pos} (h : IsLongestRevMatchAtChain pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos)) : IsLongestRevMatchAtChain pat startPos endPos

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] [StrictPatternModel 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

@[simp]

theorem String.Slice.Pattern.Model.matchesAt_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : MatchesAt pat (pos.cast hst) ↔ MatchesAt pat pos

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] [StrictPatternModel 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

@[simp]

theorem String.Slice.Pattern.Model.revMatchesAt_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : RevMatchesAt pat (pos.cast hst) ↔ RevMatchesAt pat pos

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

theorem String.Slice.Pattern.Model.lt_of_matchAt?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : matchAt? pat startPos = some endPos) : startPos < endPos

@[simp]

theorem String.Slice.Pattern.Model.matchAt?_cast {ρ : Type} (pat : ρ) [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {startPos : s.Pos} : matchAt? pat (startPos.cast hst) = Option.map (fun (x : s.Pos) => x.cast hst) (matchAt? 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

theorem String.Slice.Pattern.Model.lt_of_revMatchAt?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : revMatchAt? pat endPos = some startPos) : startPos < endPos

@[simp]

theorem String.Slice.Pattern.Model.revMatchAt?_cast {ρ : Type} (pat : ρ) [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {startPos : s.Pos} : revMatchAt? pat (startPos.cast hst) = Option.map (fun (x : s.Pos) => x.cast hst) (revMatchAt? pat startPos)

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

theorem String.Slice.Pattern.Model.isValidSearchFrom_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} {l : List (SearchStep t)} : IsValidSearchFrom pat (pos.cast hst) l ↔ IsValidSearchFrom pat pos (List.map (fun (x : SearchStep t) => SearchStep.cast ⋯ x) 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

theorem String.Slice.Pattern.Model.isValidRevSearchFrom_cast_iff {ρ : Type} {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} {l : List (SearchStep t)} : IsValidRevSearchFrom pat (pos.cast hst) l ↔ IsValidRevSearchFrom pat pos (List.map (fun (x : SearchStep t) => SearchStep.cast ⋯ x) 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