@[instance_reducible]

instance String.Slice.Pattern.Model.Char.instPatternModelChar {c : Char} : PatternModel c

Equations

• String.Slice.Pattern.Model.Char.instPatternModelChar = { Matches := fun (s : String) => s = String.singleton c }

instance String.Slice.Pattern.Model.Char.instStrictPatternModelChar {c : Char} : StrictPatternModel c

instance String.Slice.Pattern.Model.Char.instNoPrefixPatternModelChar {c : Char} : NoPrefixPatternModel c

instance String.Slice.Pattern.Model.Char.instNoSuffixPatternModelChar {c : Char} : NoSuffixPatternModel c

theorem String.Slice.Pattern.Model.Char.isMatch_iff {c : Char} {s : Slice} {pos : s.Pos} : IsMatch c pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c

theorem String.Slice.Pattern.Model.Char.isRevMatch_iff {c : Char} {s : Slice} {pos : s.Pos} : IsRevMatch c pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c

theorem String.Slice.Pattern.Model.Char.isLongestMatch_iff {c : Char} {s : Slice} {pos : s.Pos} : IsLongestMatch c pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c

theorem String.Slice.Pattern.Model.Char.isLongestMatchAt_iff {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAt c pos pos' ↔ ∃ (h : pos ≠ s.endPos), pos' = pos.next h ∧ pos.get h = c

theorem String.Slice.Pattern.Model.Char.isLongestRevMatch_iff {c : Char} {s : Slice} {pos : s.Pos} : IsLongestRevMatch c pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAt_iff {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAt c pos pos' ↔ ∃ (h : pos' ≠ s.startPos), pos = pos'.prev h ∧ (pos'.prev h).get ⋯ = c

theorem String.Slice.Pattern.Model.Char.isLongestMatchAt_of_get_eq {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : pos.get h = c) : IsLongestMatchAt c pos (pos.next h)

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAt_of_get_eq {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos} (hc : (pos.prev h).get ⋯ = c) : IsLongestRevMatchAt c (pos.prev h) pos

instance String.Slice.Pattern.Model.Char.instLawfulForwardPatternModelChar {c : Char} : LawfulForwardPatternModel c

instance String.Slice.Pattern.Model.Char.instLawfulBackwardPatternModelChar {c : Char} : LawfulBackwardPatternModel c

theorem String.Slice.Pattern.Model.Char.toSearcher_eq {c : Char} {s : Slice} : ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (fun (x : Char) => x == c) s

theorem String.Slice.Pattern.Model.Char.toBackwardSearcher_eq {c : Char} {s : Slice} : ToBackwardSearcher.toSearcher c s = ToBackwardSearcher.toSearcher (fun (x : Char) => x == c) s

theorem String.Slice.Pattern.Model.Char.matchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} : MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c

theorem String.Slice.Pattern.Model.Char.revMatchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} : RevMatchesAt c pos ↔ ∃ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ = c

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

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

theorem String.Slice.Pattern.Model.Char.not_matchesAt_of_get_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : pos.get h ≠ c) : ¬MatchesAt c pos

theorem String.Slice.Pattern.Model.Char.not_revMatchesAt_of_get_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos} (hc : (pos.prev h).get ⋯ ≠ c) : ¬RevMatchesAt c pos

theorem String.Slice.Pattern.Model.Char.matchAt?_eq {s : Slice} {pos : s.Pos} {c : Char} : matchAt? c pos = if h₀ : ∃ (h : pos ≠ s.endPos), pos.get h = c then some (pos.next ⋯) else none

theorem String.Slice.Pattern.Model.Char.revMatchAt?_eq {s : Slice} {pos : s.Pos} {c : Char} : revMatchAt? c pos = if h₀ : ∃ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ = c then some (pos.prev ⋯) else none

theorem String.Slice.Pattern.Model.Char.isMatch_iff_isMatch_beq {c : Char} {s : Slice} {pos : s.Pos} : IsMatch c pos ↔ IsMatch (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.isRevMatch_iff_isRevMatch_beq {c : Char} {s : Slice} {pos : s.Pos} : IsRevMatch c pos ↔ IsRevMatch (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.isLongestMatch_iff_isLongestMatch_beq {c : Char} {s : Slice} {pos : s.Pos} : IsLongestMatch c pos ↔ IsLongestMatch (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.isLongestRevMatch_iff_isLongestRevMatch_beq {c : Char} {s : Slice} {pos : s.Pos} : IsLongestRevMatch c pos ↔ IsLongestRevMatch (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.isLongestMatchAt_iff_isLongestMatchAt_beq {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAt c pos pos' ↔ IsLongestMatchAt (fun (x : Char) => x == c) pos pos'

theorem String.Slice.Pattern.Model.Char.isLongestMatchAtChain_iff_isLongestMatchAtChain_beq {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAtChain c pos pos' ↔ IsLongestMatchAtChain (fun (x : Char) => x == c) pos pos'

theorem String.Slice.Pattern.Model.Char.isLongestMatchAtChain_iff {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAtChain c pos pos' ↔ pos ≤ pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h : pos'' < pos'), pos''.get ⋯ = c

theorem String.Slice.Pattern.Model.Char.isLongestMatchAtChain_iff_toList {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAtChain c pos pos' ↔ ∃ (h : pos ≤ pos'), (s.slice pos pos' h).copy.toList = List.replicate (s.slice pos pos' h).copy.toList.length c

theorem String.Slice.Pattern.Model.Char.isLongestMatchAtChain_startPos_endPos_iff_toList {c : Char} {s : Slice} : IsLongestMatchAtChain c s.startPos s.endPos ↔ s.copy.toList = List.replicate s.copy.toList.length c

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAt_iff_isLongestRevMatchAt_beq {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAt c pos pos' ↔ IsLongestRevMatchAt (fun (x : Char) => x == c) pos pos'

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_beq {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAtChain c pos pos' ↔ IsLongestRevMatchAtChain (fun (x : Char) => x == c) pos pos'

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_iff {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAtChain c pos pos' ↔ pos ≤ pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h : pos'' < pos'), pos''.get ⋯ = c

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_iff_toList {c : Char} {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAtChain c pos pos' ↔ ∃ (h : pos ≤ pos'), (s.slice pos pos' h).copy.toList = List.replicate (s.slice pos pos' h).copy.toList.length c

theorem String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_startPos_endPos_iff_toList {c : Char} {s : Slice} : IsLongestRevMatchAtChain c s.startPos s.endPos ↔ s.copy.toList = List.replicate s.copy.toList.length c

theorem String.Slice.Pattern.Model.Char.matchesAt_iff_matchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} : MatchesAt c pos ↔ MatchesAt (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.revMatchesAt_iff_revMatchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} : RevMatchesAt c pos ↔ RevMatchesAt (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.matchAt?_eq_matchAt?_beq {c : Char} {s : Slice} {pos : s.Pos} : matchAt? c pos = matchAt? (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.revMatchAt?_eq_revMatchAt?_beq {c : Char} {s : Slice} {pos : s.Pos} : revMatchAt? c pos = revMatchAt? (fun (x : Char) => x == c) pos

theorem String.Slice.Pattern.Model.Char.isValidSearchFrom_iff_isValidSearchFrom_beq {c : Char} {s : Slice} {p : s.Pos} {l : List (SearchStep s)} : IsValidSearchFrom c p l ↔ IsValidSearchFrom (fun (x : Char) => x == c) p l

theorem String.Slice.Pattern.Model.Char.isValidRevSearchFrom_iff_isValidRevSearchFrom_beq {c : Char} {s : Slice} {p : s.Pos} {l : List (SearchStep s)} : IsValidRevSearchFrom c p l ↔ IsValidRevSearchFrom (fun (x : Char) => x == c) p l

instance String.Slice.Pattern.Model.Char.instLawfulToForwardSearcherModelCharDefaultForwardSearcherForallBoolBeq {c : Char} : LawfulToForwardSearcherModel c

instance String.Slice.Pattern.Model.Char.instLawfulToBackwardSearcherModelCharDefaultBackwardSearcherForallBoolBeq {c : Char} : LawfulToBackwardSearcherModel c

theorem String.Slice.startsWith_char_eq_startsWith_beq {c : Char} {s : Slice} : s.startsWith c = s.startsWith fun (x : Char) => x == c

theorem String.Slice.dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} : s.dropPrefix? c = s.dropPrefix? fun (x : Char) => x == c

theorem String.Slice.dropPrefix_char_eq_dropPrefix_beq {c : Char} {s : Slice} : s.dropPrefix c = s.dropPrefix fun (x : Char) => x == c

theorem String.Slice.skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} : s.skipPrefix? c = s.skipPrefix? fun (x : Char) => x == c

theorem String.Slice.Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} : skipPrefix? c s = skipPrefix? (fun (x : Char) => x == c) s

theorem String.Slice.Pos.skip?_char_eq_skip?_beq {c : Char} {s : Slice} {pos : s.Pos} : pos.skip? c = pos.skip? fun (x : Char) => x == c

theorem String.Slice.Pos.skipWhile_char_eq_skipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) : curr.skipWhile c = curr.skipWhile fun (x : Char) => x == c

theorem String.Slice.skipPrefixWhile_char_eq_skipPrefixWhile_beq {c : Char} {s : Slice} : s.skipPrefixWhile c = s.skipPrefixWhile fun (x : Char) => x == c

theorem String.Slice.dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} : s.dropWhile c = s.dropWhile fun (x : Char) => x == c

theorem String.Slice.takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} : s.takeWhile c = s.takeWhile fun (x : Char) => x == c

theorem String.Slice.all_char_eq_all_beq {c : Char} {s : Slice} : s.all c = s.all fun (x : Char) => x == c

theorem String.Slice.find?_char_eq_find?_beq {c : Char} {s : Slice} : s.find? c = s.find? fun (x : Char) => x == c

theorem String.Slice.Pos.find?_char_eq_find?_beq {c : Char} {s : Slice} {p : s.Pos} : p.find? c = p.find? fun (x : Char) => x == c

theorem String.Slice.contains_char_eq_contains_beq {c : Char} {s : Slice} : s.contains c = s.contains fun (x : Char) => x == c

theorem String.Slice.endsWith_char_eq_endsWith_beq {c : Char} {s : Slice} : s.endsWith c = s.endsWith fun (x : Char) => x == c

theorem String.Slice.skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} : s.skipSuffix? c = s.skipSuffix? fun (x : Char) => x == c

theorem String.Slice.dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} : s.dropSuffix? c = s.dropSuffix? fun (x : Char) => x == c

theorem String.Slice.dropSuffix_char_eq_dropSuffix_beq {c : Char} {s : Slice} : s.dropSuffix c = s.dropSuffix fun (x : Char) => x == c

theorem String.Slice.Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} : skipSuffix? c s = skipSuffix? (fun (x : Char) => x == c) s

theorem String.Slice.Pos.revSkip?_char_eq_revSkip?_beq {c : Char} {s : Slice} {pos : s.Pos} : pos.revSkip? c = pos.revSkip? fun (x : Char) => x == c

theorem String.Slice.Pos.revSkipWhile_char_eq_revSkipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) : curr.revSkipWhile c = curr.revSkipWhile fun (x : Char) => x == c

theorem String.Slice.skipSuffixWhile_char_eq_skipSuffixWhile_beq {c : Char} {s : Slice} : s.skipSuffixWhile c = s.skipSuffixWhile fun (x : Char) => x == c

theorem String.Slice.dropEndWhile_char_eq_dropEndWhile_beq {c : Char} {s : Slice} : s.dropEndWhile c = s.dropEndWhile fun (x : Char) => x == c

theorem String.Slice.takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} : s.takeEndWhile c = s.takeEndWhile fun (x : Char) => x == c

theorem String.Slice.revFind?_char_eq_revFind?_beq {c : Char} {s : Slice} : s.revFind? c = s.revFind? fun (x : Char) => x == c

theorem String.Slice.Pos.revFind?_char_eq_revFind?_beq {c : Char} {s : Slice} {p : s.Pos} : p.revFind? c = p.revFind? fun (x : Char) => x == c

theorem String.Slice.revAll_char_eq_revAll_beq {c : Char} {s : Slice} : s.revAll c = s.revAll fun (x : Char) => x == c