@[instance_reducible]

instance String.Slice.Pattern.Model.ForwardSliceSearcher.instPatternModel {pat : Slice} : PatternModel pat

Equations

• String.Slice.Pattern.Model.ForwardSliceSearcher.instPatternModel = { Matches := fun (s : String) => s = pat.copy }

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.strictPatternModel {pat : Slice} (hpat : pat.isEmpty = false) : StrictPatternModel pat

instance String.Slice.Pattern.Model.ForwardSliceSearcher.instNoPrefixPatternModel {pat : Slice} : NoPrefixPatternModel pat

instance String.Slice.Pattern.Model.ForwardSliceSearcher.instNoSuffixPatternModel {pat : Slice} : NoSuffixPatternModel pat

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isMatch_iff {pat s : Slice} {pos : s.Pos} : IsMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isRevMatch_iff {pat s : Slice} {pos : s.Pos} : IsRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatch_iff {pat s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatch_iff {pat s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAtChain_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAtChain pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), ∃ (n : Nat), (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAtChain_startPos_endPos_iff {pat s : Slice} : IsLongestMatchAtChain pat s.startPos s.endPos ↔ ∃ (n : Nat), s.copy = String.join (List.replicate n pat.copy)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAtChain_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAtChain pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), ∃ (n : Nat), (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAtChain_startPos_endPos_iff {pat s : Slice} : IsLongestRevMatchAtChain pat s.startPos s.endPos ↔ ∃ (n : Nat), s.copy = String.join (List.replicate n pat.copy)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (pat.copy ++ t₂) ∧ pos₂.Splits (t₁ ++ pat.copy) t₂

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (pat.copy ++ t₂) ∧ pos₂.Splits (t₁ ++ pat.copy) t₂

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatch_iff_splits {pat s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ ∃ (t : String), pos.Splits pat.copy t

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatch_iff_splits {pat s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ ∃ (t : String), pos.Splits t pat.copy

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) : IsLongestMatchAt pat pos₁ pos₂ ↔ s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) : IsLongestRevMatchAt pat pos₁ pos₂ ↔ s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.offset_of_isLongestMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) (h' : IsLongestMatchAt pat pos₁ pos₂) : pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.offset_of_isLongestRevMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) (h' : IsLongestRevMatchAt pat pos₁ pos₂) : pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_splits {pat s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits t₁ (pat.copy ++ t₂)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.revMatchesAt_iff_splits {pat s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits (t₁ ++ pat.copy) t₂

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.exists_matchesAt_iff_eq_append {pat s : Slice} : (∃ (pos : s.Pos), MatchesAt pat pos) ↔ ∃ (t₁ : String), ∃ (t₂ : String), s.copy = t₁ ++ pat.copy ++ t₂

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.exists_revMatchesAt_iff_eq_append {pat s : Slice} : (∃ (pos : s.Pos), RevMatchesAt pat pos) ↔ ∃ (t₁ : String), ∃ (t₂ : String), s.copy = t₁ ++ pat.copy ++ t₂

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_isLongestMatchAt {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : MatchesAt pat pos ↔ ∃ (h : Pos.Raw.IsValidForSlice s (pos.offset.increaseBy pat.utf8ByteSize)), IsLongestMatchAt pat pos (s.pos (pos.offset.increaseBy pat.utf8ByteSize) h)

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.revMatchesAt_iff_isLongestRevMatchAt {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : RevMatchesAt pat pos ↔ ∃ (h : Pos.Raw.IsValidForSlice s (pos.offset.decreaseBy pat.utf8ByteSize)), IsLongestRevMatchAt pat (s.pos (pos.offset.decreaseBy pat.utf8ByteSize) h) pos

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_getElem {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) : MatchesAt pat pos ↔ ∃ (h : pos.offset.byteIdx + pat.copy.toByteArray.size ≤ s.copy.toByteArray.size), ∀ (j : Nat) (hj : j < pat.copy.toByteArray.size), pat.copy.toByteArray[j] = s.copy.toByteArray[pos.offset.byteIdx + j]

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.le_of_matchesAt {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) (h' : MatchesAt pat pos) : pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos

@[instance_reducible]

instance String.Slice.Pattern.Model.ForwardStringSearcher.instPatternModel {pat : String} : PatternModel pat

Equations

• String.Slice.Pattern.Model.ForwardStringSearcher.instPatternModel = { Matches := fun (s : String) => s = pat }

theorem String.Slice.Pattern.Model.ForwardStringSearcher.strictPatternModel {pat : String} (h : pat ≠ "") : StrictPatternModel pat

instance String.Slice.Pattern.Model.ForwardStringSearcher.instNoPrefixPatternModel {pat : String} : NoPrefixPatternModel pat

instance String.Slice.Pattern.Model.ForwardStringSearcher.instNoSuffixPatternModel {pat : String} : NoSuffixPatternModel pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} : IsMatch pat pos ↔ IsMatch pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isRevMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} : IsRevMatch pat pos ↔ IsRevMatch pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatch_iff_isLongestMatch_toSlice {pat : String} {s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ IsLongestMatch pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatch_iff_isLongestRevMatch_toSlice {pat : String} {s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ IsLongestRevMatch pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff_isLongestMatchAt_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt pat pos₁ pos₂ ↔ IsLongestMatchAt pat.toSlice pos₁ pos₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAtChain_iff_isLongestMatchAtChain_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAtChain pat pos₁ pos₂ ↔ IsLongestMatchAtChain pat.toSlice pos₁ pos₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAtChain_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAtChain pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), ∃ (n : Nat), (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat)

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAtChain_startPos_endPos_iff {pat : String} {s : Slice} : IsLongestMatchAtChain pat s.startPos s.endPos ↔ ∃ (n : Nat), s.copy = String.join (List.replicate n pat)

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAt pat pos₁ pos₂ ↔ IsLongestRevMatchAt pat.toSlice pos₁ pos₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAtChain pat pos₁ pos₂ ↔ IsLongestRevMatchAtChain pat.toSlice pos₁ pos₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAtChain_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAtChain pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), ∃ (n : Nat), (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat)

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAtChain_startPos_endPos_iff {pat : String} {s : Slice} : IsLongestRevMatchAtChain pat s.startPos s.endPos ↔ ∃ (n : Nat), s.copy = String.join (List.replicate n pat)

theorem String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ MatchesAt pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isMatch_iff {pat : String} {s : Slice} {pos : s.Pos} : IsMatch pat pos ↔ (s.sliceTo pos).copy = pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} : IsRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatch_iff {pat : String} {s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} : IsLongestRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") : IsLongestMatchAt pat pos₁ pos₂ ↔ s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") : IsLongestRevMatchAt pat pos₁ pos₂ ↔ s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray

theorem String.Slice.Pattern.Model.ForwardStringSearcher.offset_of_isLongestMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") (h' : IsLongestMatchAt pat pos₁ pos₂) : pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize

theorem String.Slice.Pattern.Model.ForwardStringSearcher.offset_of_isLongestRevMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") (h' : IsLongestRevMatchAt pat pos₁ pos₂) : pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize

theorem String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits t₁ (pat ++ t₂)

theorem String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos.Splits (t₁ ++ pat) t₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.exists_matchesAt_iff_eq_append {pat : String} {s : Slice} : (∃ (pos : s.Pos), MatchesAt pat pos) ↔ ∃ (t₁ : String), ∃ (t₂ : String), s.copy = t₁ ++ pat ++ t₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.exists_revMatchesAt_iff_eq_append {pat : String} {s : Slice} : (∃ (pos : s.Pos), RevMatchesAt pat pos) ↔ ∃ (t₁ : String), ∃ (t₂ : String), s.copy = t₁ ++ pat ++ t₂

theorem String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") : MatchesAt pat pos ↔ ∃ (h : Pos.Raw.IsValidForSlice s (pos.offset.increaseBy pat.utf8ByteSize)), IsLongestMatchAt pat pos (s.pos (pos.offset.increaseBy pat.utf8ByteSize) h)

theorem String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_isLongestRevMatchAt {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") : RevMatchesAt pat pos ↔ ∃ (h : Pos.Raw.IsValidForSlice s (pos.offset.decreaseBy pat.utf8ByteSize)), IsLongestRevMatchAt pat (s.pos (pos.offset.decreaseBy pat.utf8ByteSize) h) pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") : MatchesAt pat pos ↔ ∃ (h : pos.offset.byteIdx + pat.toByteArray.size ≤ s.copy.toByteArray.size), ∀ (j : Nat) (hj : j < pat.toByteArray.size), pat.toByteArray[j] = s.copy.toByteArray[pos.offset.byteIdx + j]

theorem String.Slice.Pattern.Model.ForwardStringSearcher.le_of_matchesAt {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") (h' : MatchesAt pat pos) : pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_matchesAt_toSlice {pat : String} {s : Slice} {pos : s.Pos} : MatchesAt pat pos ↔ MatchesAt pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_revMatchesAt_toSlice {pat : String} {s : Slice} {pos : s.Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat.toSlice pos

theorem String.Slice.Pattern.Model.ForwardStringSearcher.toSearcher_eq {pat : String} {s : Slice} : ToForwardSearcher.toSearcher pat s = ToForwardSearcher.toSearcher pat.toSlice s

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isValidSearchFrom_iff_isValidSearchFrom_toSlice {pat : String} {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} : IsValidSearchFrom pat pos l ↔ IsValidSearchFrom pat.toSlice pos l

theorem String.Slice.Pattern.Model.ForwardStringSearcher.isValidRevSearchFrom_iff_isValidRevSearchFrom_toSlice {pat : String} {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} : IsValidRevSearchFrom pat pos l ↔ IsValidRevSearchFrom pat.toSlice pos l