@[implicit_reducible]

instance String.Slice.Pattern.Model.CharPred.instPatternModelForallCharBool {p : Char → Bool} : PatternModel p

Equations

• String.Slice.Pattern.Model.CharPred.instPatternModelForallCharBool = { Matches := fun (s : String) => ∃ (c : Char), s = String.singleton c ∧ p c = true, not_matches_empty := ⋯ }

instance String.Slice.Pattern.Model.CharPred.instNoPrefixPatternModelForallCharBool {p : Char → Bool} : NoPrefixPatternModel p

instance String.Slice.Pattern.Model.CharPred.instNoSuffixPatternModelForallCharBool {p : Char → Bool} : NoSuffixPatternModel p

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

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

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

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

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

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

theorem String.Slice.Pattern.Model.CharPred.isLongestMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : p (pos.get h) = true) : IsLongestMatchAt p pos (pos.next h)

theorem String.Slice.Pattern.Model.CharPred.isLongestRevMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos} (hc : p ((pos.prev h).get ⋯) = true) : IsLongestRevMatchAt p (pos.prev h) pos

instance String.Slice.Pattern.Model.CharPred.instLawfulForwardPatternModelForallCharBool {p : Char → Bool} : LawfulForwardPatternModel p

instance String.Slice.Pattern.Model.CharPred.instLawfulBackwardPatternModelForallCharBool {p : Char → Bool} : LawfulBackwardPatternModel p

instance String.Slice.Pattern.Model.CharPred.instLawfulToForwardSearcherModelForallCharBoolDefaultForwardSearcher {p : Char → Bool} : LawfulToForwardSearcherModel p

instance String.Slice.Pattern.Model.CharPred.instLawfulToBackwardSearcherModelForallCharBoolDefaultBackwardSearcher {p : Char → Bool} : LawfulToBackwardSearcherModel p

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

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

theorem String.Slice.Pattern.Model.CharPred.not_matchesAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : p (pos.get h) = false) : ¬MatchesAt p pos

theorem String.Slice.Pattern.Model.CharPred.not_revMatchesAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos} (hc : p ((pos.prev h).get ⋯) = false) : ¬RevMatchesAt p pos

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

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

@[implicit_reducible]

instance String.Slice.Pattern.Model.CharPred.Decidable.instPatternModelForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : PatternModel p

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.Pattern.Model.CharPred.Decidable.instNoPrefixPatternModelForallCharProp {p : Char → Prop} [DecidablePred p] : NoPrefixPatternModel p

instance String.Slice.Pattern.Model.CharPred.Decidable.instNoSuffixPatternModelForallCharProp {p : Char → Prop} [DecidablePred p] : NoSuffixPatternModel p

theorem String.Slice.Pattern.Model.CharPred.Decidable.isMatch_iff_isMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsMatch p pos ↔ IsMatch (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.isRevMatch_iff_isRevMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsRevMatch p pos ↔ IsRevMatch (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.isMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsMatch p pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isRevMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsRevMatch p pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsLongestMatch p pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsLongestRevMatch p pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatch_iff_isLongestMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsLongestMatch p pos ↔ IsLongestMatch (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatch_iff_isLongestRevMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsLongestRevMatch p pos ↔ IsLongestRevMatch (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAt_iff_isLongestMatchAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAt p pos pos' ↔ IsLongestMatchAt (fun (x : Char) => decide (p x)) pos pos'

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAt_iff_isLongestRevMatchAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAt p pos pos' ↔ IsLongestRevMatchAt (fun (x : Char) => decide (p x)) pos pos'

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos pos' : s.Pos} : IsLongestMatchAt p pos pos' ↔ ∃ (h : pos ≠ s.endPos), pos' = pos.next h ∧ p (pos.get h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos pos' : s.Pos} : IsLongestRevMatchAt p pos pos' ↔ ∃ (h : pos' ≠ s.startPos), pos = pos'.prev h ∧ p ((pos'.prev h).get ⋯)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : p (pos.get h)) : IsLongestMatchAt p pos (pos.next h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos} (hc : p ((pos.prev h).get ⋯)) : IsLongestRevMatchAt p (pos.prev h) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.matchesAt_iff_matchesAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : MatchesAt p pos ↔ MatchesAt (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.revMatchesAt_iff_revMatchesAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : RevMatchesAt p pos ↔ RevMatchesAt (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.matchAt?_eq_matchAt?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : matchAt? p pos = matchAt? (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.revMatchAt?_eq_revMatchAt?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : revMatchAt? p pos = revMatchAt? (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.skipPrefix?_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] : ForwardPattern.skipPrefix? p = ForwardPattern.skipPrefix? fun (x : Char) => decide (p x)

theorem String.Slice.Pattern.Model.CharPred.Decidable.skipSuffix?_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] : BackwardPattern.skipSuffix? p = BackwardPattern.skipSuffix? fun (x : Char) => decide (p x)

instance String.Slice.Pattern.Model.CharPred.Decidable.instLawfulForwardPatternModelForallCharProp {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p

instance String.Slice.Pattern.Model.CharPred.Decidable.instLawfulBackwardPatternModelForallCharProp {p : Char → Prop} [DecidablePred p] : LawfulBackwardPatternModel p

theorem String.Slice.Pattern.Model.CharPred.Decidable.toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} : ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (fun (x : Char) => decide (p x)) s

theorem String.Slice.Pattern.Model.CharPred.Decidable.toBackwardSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} : ToBackwardSearcher.toSearcher p s = ToBackwardSearcher.toSearcher (fun (x : Char) => decide (p x)) s

theorem String.Slice.Pattern.Model.CharPred.Decidable.isValidSearchFrom_iff_isValidSearchFrom_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} : IsValidSearchFrom p pos l ↔ IsValidSearchFrom (fun (x : Char) => decide (p x)) pos l

theorem String.Slice.Pattern.Model.CharPred.Decidable.isValidRevSearchFrom_iff_isValidRevSearchFrom_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} : IsValidRevSearchFrom p pos l ↔ IsValidRevSearchFrom (fun (x : Char) => decide (p x)) pos l

instance String.Slice.Pattern.Model.CharPred.Decidable.instLawfulToForwardSearcherModelForallCharPropDefaultForwardSearcherForallBoolDecide {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p

instance String.Slice.Pattern.Model.CharPred.Decidable.instLawfulToBackwardSearcherModelForallCharPropDefaultBackwardSearcherForallBoolDecide {p : Char → Prop} [DecidablePred p] : LawfulToBackwardSearcherModel p

theorem String.Slice.Pattern.Model.CharPred.Decidable.matchesAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.revMatchesAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : RevMatchesAt p pos ↔ ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯)

theorem String.Slice.Pattern.Model.CharPred.Decidable.not_matchesAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : ¬p (pos.get h)) : ¬MatchesAt p pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.not_revMatchesAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {h : pos ≠ s.startPos} (hc : ¬p ((pos.prev h).get ⋯)) : ¬RevMatchesAt p pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.matchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Prop} [DecidablePred p] : matchAt? p pos = if h₀ : ∃ (h : pos ≠ s.endPos), p (pos.get h) then some (pos.next ⋯) else none

theorem String.Slice.Pattern.Model.CharPred.Decidable.revMatchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Prop} [DecidablePred p] : revMatchAt? p pos = if h₀ : ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) then some (pos.prev ⋯) else none

theorem String.Slice.startsWith_prop_eq_startsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.startsWith p = s.startsWith fun (x : Char) => decide (p x)

theorem String.Slice.dropPrefix?_prop_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropPrefix? p = s.dropPrefix? fun (x : Char) => decide (p x)

theorem String.Slice.dropPrefix_prop_eq_dropPrefix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropPrefix p = s.dropPrefix fun (x : Char) => decide (p x)

theorem String.Slice.skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.skipPrefix? p = s.skipPrefix? fun (x : Char) => decide (p x)

theorem String.Slice.Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : skipPrefix? p s = skipPrefix? (fun (x : Char) => decide (p x)) s

theorem String.Slice.Pos.skipWhile_prop_eq_skipWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) : curr.skipWhile p = curr.skipWhile fun (x : Char) => decide (p x)

theorem String.Slice.skipPrefixWhile_prop_eq_skipPrefixWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.skipPrefixWhile p = s.skipPrefixWhile fun (x : Char) => decide (p x)

theorem String.Slice.dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropWhile p = s.dropWhile fun (x : Char) => decide (p x)

theorem String.Slice.takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.takeWhile p = s.takeWhile fun (x : Char) => decide (p x)

theorem String.Slice.all_prop_eq_all_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.all p = s.all fun (x : Char) => decide (p x)

theorem String.Slice.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.find? p = s.find? fun (x : Char) => decide (p x)

theorem String.Slice.Pos.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : pos.find? p = pos.find? fun (x : Char) => decide (p x)

theorem String.Slice.contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.contains p = s.contains fun (x : Char) => decide (p x)

theorem String.Slice.endsWith_prop_eq_endsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.endsWith p = s.endsWith fun (x : Char) => decide (p x)

theorem String.Slice.skipSuffix?_prop_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.skipSuffix? p = s.skipSuffix? fun (x : Char) => decide (p x)

theorem String.Slice.dropSuffix?_prop_eq_dropSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropSuffix? p = s.dropSuffix? fun (x : Char) => decide (p x)

theorem String.Slice.dropSuffix_prop_eq_dropSuffix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropSuffix p = s.dropSuffix fun (x : Char) => decide (p x)

theorem String.Slice.Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : skipSuffix? p s = skipSuffix? (fun (x : Char) => decide (p x)) s

theorem String.Slice.Pos.revSkipWhile_prop_eq_revSkipWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) : curr.revSkipWhile p = curr.revSkipWhile fun (x : Char) => decide (p x)

theorem String.Slice.skipSuffixWhile_prop_eq_skipSuffixWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.skipSuffixWhile p = s.skipSuffixWhile fun (x : Char) => decide (p x)

theorem String.Slice.dropEndWhile_prop_eq_dropEndWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropEndWhile p = s.dropEndWhile fun (x : Char) => decide (p x)

theorem String.Slice.takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.takeEndWhile p = s.takeEndWhile fun (x : Char) => decide (p x)