From 10ece4e082ac78e3ded5ad855c3c8fb10073b241 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 4 Mar 2026 18:50:32 +0100 Subject: [PATCH] refactor: reduce duplication in string pattern lemmas (#12793) This PR takes a more principled approach in deriving `String` pattern lemmas by reducing to simpler cases similar to how the instances are defined. This reduces duplication of complex arguments (at the expense of having to state more simple lemmas; however these lemmas are useful to users as well). --- src/Init/Data/String/Lemmas/Pattern/Char.lean | 161 +++++++++++++++++- .../Data/String/Lemmas/Pattern/Find/Char.lean | 12 ++ .../Data/String/Lemmas/Pattern/Find/Pred.lean | 149 +++++----------- .../String/Lemmas/Pattern/Find/String.lean | 7 +- src/Init/Data/String/Lemmas/Pattern/Pred.lean | 155 ++++++++++++++++- .../String/Lemmas/Pattern/Split/Char.lean | 40 ++--- .../String/Lemmas/Pattern/Split/Pred.lean | 40 ++--- .../String/Lemmas/Pattern/String/Basic.lean | 49 ++++-- .../Lemmas/Pattern/String/ForwardPattern.lean | 105 +++++++++++- .../Pattern/String/ForwardSearcher.lean | 46 +++-- src/Init/Data/String/Pattern/Char.lean | 79 ++------- src/Init/Data/String/Pattern/Pred.lean | 4 +- 12 files changed, 587 insertions(+), 260 deletions(-) diff --git a/src/Init/Data/String/Lemmas/Pattern/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Char.lean index 6bb7a39cc1..605b4e08ad 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Char.lean @@ -8,6 +8,12 @@ module prelude public import Init.Data.String.Pattern.Char public import Init.Data.String.Lemmas.Pattern.Basic +public import Init.Data.String.Slice +public import Init.Data.String.Lemmas.Pattern.Pred +public import Init.Data.String.Search +import all Init.Data.String.Slice +import all Init.Data.String.Pattern.Char +import all Init.Data.String.Search import Init.Data.Option.Lemmas import Init.Data.String.Lemmas.Basic import Init.Data.String.Lemmas.Order @@ -54,8 +60,8 @@ instance {c : Char} : LawfulForwardPatternModel c where dropPrefix?_eq_some_iff {s} pos := by simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)] -instance {c : Char} : LawfulToForwardSearcherModel c := - .defaultImplementation +theorem toSearcher_eq {c : Char} {s : Slice} : + ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (· == c) s := (rfl) theorem matchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} : MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c := by @@ -80,4 +86,153 @@ theorem matchAt?_eq {s : Slice} {pos : s.Pos} {c : Char} : if h₀ : ∃ (h : pos ≠ s.endPos), pos.get h = c then some (pos.next h₀.1) else none := by split <;> simp_all [isLongestMatchAt_iff, matchesAt_iff] -end String.Slice.Pattern.Model.Char +theorem isMatch_iff_isMatch_beq {c : Char} {s : Slice} {pos : s.Pos} : + IsMatch c pos ↔ IsMatch (· == c) pos := by + simp [isMatch_iff, CharPred.isMatch_iff, beq_iff_eq] + +theorem isLongestMatch_iff_isLongestMatch_beq {c : Char} {s : Slice} {pos : s.Pos} : + IsLongestMatch c pos ↔ IsLongestMatch (· == c) pos := by + simp [isLongestMatch_iff_isMatch, isMatch_iff_isMatch_beq] + +theorem isLongestMatchAt_iff_isLongestMatchAt_beq {c : Char} {s : Slice} + {pos pos' : s.Pos} : + IsLongestMatchAt c pos pos' ↔ IsLongestMatchAt (· == c) pos pos' := by + simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_beq] + +theorem matchesAt_iff_matchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} : + MatchesAt c pos ↔ MatchesAt (· == c) pos := by + simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_beq] + +theorem matchAt?_eq_matchAt?_beq {c : Char} {s : Slice} {pos : s.Pos} : + matchAt? c pos = matchAt? (· == c) pos := by + refine Option.ext (fun pos' => ?_) + simp [matchAt?_eq_some_iff, isLongestMatchAt_iff_isLongestMatchAt_beq] + +theorem isValidSearchFrom_iff_isValidSearchFrom_beq {c : Char} {s : Slice} {p : s.Pos} + {l : List (SearchStep s)} : IsValidSearchFrom c p l ↔ IsValidSearchFrom (· == c) p l := by + refine ⟨fun h => ?_, fun h => ?_⟩ + · induction h with + | endPos => simpa using IsValidSearchFrom.endPos + | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_beq] + | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_beq] + · induction h with + | endPos => simpa using IsValidSearchFrom.endPos + | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_beq] + | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_beq] + +instance {c : Char} : LawfulToForwardSearcherModel c where + isValidSearchFrom_toList s := by + simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_beq] using + LawfulToForwardSearcherModel.isValidSearchFrom_toList (pat := (· == c)) (s := s) + +end Pattern.Model.Char + +theorem startsWith_char_eq_startsWith_beq {c : Char} {s : Slice} : + s.startsWith c = s.startsWith (· == c) := (rfl) + +theorem dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} : + s.dropPrefix? c = s.dropPrefix? (· == c) := (rfl) + +theorem dropPrefix_char_eq_dropPrefix_beq {c : Char} {s : Slice} : + s.dropPrefix c = s.dropPrefix (· == c) := (rfl) + +theorem Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} : + dropPrefix? c s = dropPrefix? (· == c) s := (rfl) + +private theorem dropWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : + dropWhile.go s c curr = dropWhile.go s (· == c) curr := by + fun_induction dropWhile.go s c curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih] + | case3 pos h => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq] + +theorem dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} : + s.dropWhile c = s.dropWhile (· == c) := by + simpa only [dropWhile] using dropWhileGo_eq s.startPos + +private theorem takeWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : + takeWhile.go s c curr = takeWhile.go s (· == c) curr := by + fun_induction takeWhile.go s c curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih] + | case3 pos h => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq] + +theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} : + s.takeWhile c = s.takeWhile (· == c) := by + simp only [takeWhile]; exact takeWhileGo_eq s.startPos + +theorem all_char_eq_all_beq {c : Char} {s : Slice} : + s.all c = s.all (· == c) := by + simp only [all, dropWhile_char_eq_dropWhile_beq] + +theorem find?_char_eq_find?_beq {c : Char} {s : Slice} : + s.find? c = s.find? (· == c) := + (rfl) + +theorem Pos.find?_char_eq_find?_beq {c : Char} {s : Slice} {p : s.Pos} : + p.find? c = p.find? (· == c) := + (rfl) + +theorem contains_char_eq_contains_beq {c : Char} {s : Slice} : + s.contains c = s.contains (· == c) := + (rfl) + +theorem endsWith_char_eq_endsWith_beq {c : Char} {s : Slice} : + s.endsWith c = s.endsWith (· == c) := (rfl) + +theorem dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} : + s.dropSuffix? c = s.dropSuffix? (· == c) := (rfl) + +theorem dropSuffix_char_eq_dropSuffix_beq {c : Char} {s : Slice} : + s.dropSuffix c = s.dropSuffix (· == c) := (rfl) + +theorem Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} : + dropSuffix? c s = dropSuffix? (· == c) s := (rfl) + +private theorem dropEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : + dropEndWhile.go s c curr = dropEndWhile.go s (· == c) curr := by + fun_induction dropEndWhile.go s c curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih] + | case3 pos h => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq] + +theorem dropEndWhile_char_eq_dropEndWhile_beq {c : Char} {s : Slice} : + s.dropEndWhile c = s.dropEndWhile (· == c) := by + simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos + +private theorem takeEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : + takeEndWhile.go s c curr = takeEndWhile.go s (· == c) curr := by + fun_induction takeEndWhile.go s c curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih] + | case3 pos h => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq] + +theorem takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} : + s.takeEndWhile c = s.takeEndWhile (· == c) := by + simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos + +end String.Slice diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean index 9e80ce4992..11ab2c2ddf 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean @@ -143,6 +143,18 @@ theorem Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : String} {po rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff] exact Slice.Pos.find?_char_eq_none_iff_not_mem_of_splits (Pos.splits_toSlice_iff.mpr hs) +theorem Pos.find?_char_eq_find?_beq {c : Char} {s : String} {pos : s.Pos} : + pos.find? c = pos.find? (· == c) := by + simp only [Pos.find?_eq_find?_toSlice, Slice.Pos.find?_char_eq_find?_beq] + +theorem find?_char_eq_find?_beq {c : Char} {s : String} : + s.find? c = s.find? (· == c) := by + simp only [find?_eq_find?_toSlice, Slice.find?_char_eq_find?_beq] + +theorem contains_char_eq_contains_beq {c : Char} {s : String} : + s.contains c = s.contains (· == c) := by + simp only [contains_eq_contains_toSlice, Slice.contains_char_eq_contains_beq] + theorem find?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} : s.find? c = some pos ↔ ∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (Pos.ne_endPos_of_lt h') ≠ c := by diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean index d766da2f4f..e8a52711bc 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean @@ -7,6 +7,8 @@ module prelude public import Init.Data.String.Slice +import all Init.Data.String.Slice +import all Init.Data.String.Search import Init.Data.String.Lemmas.Pattern.Find.Basic import Init.Data.String.Lemmas.Pattern.Pred import Init.Data.String.Lemmas.Basic @@ -27,7 +29,8 @@ theorem find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : s.find? p = some pos ↔ ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by - grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff] + simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff, decide_eq_true_eq, + decide_eq_false_iff_not] theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} : s.find? p = some pos ↔ @@ -48,17 +51,8 @@ theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : {pos : s.Pos} : s.find? p = some pos ↔ ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬ p d := by - rw [find?_prop_eq_some_iff] - refine ⟨?_, ?_⟩ - · rintro ⟨h, hp, hmin⟩ - exact ⟨_, _, _, pos.splits_next_right h, hp, fun d hd => by - obtain ⟨pos', hlt, hpget⟩ := (pos.splits_next_right h).mem_toList_left_iff.mp hd - subst hpget; exact hmin _ hlt⟩ - · rintro ⟨t, c, u, hs, hpc, hmin⟩ - have hne := hs.ne_endPos_of_singleton - refine ⟨hne, ?_, fun pos' hlt => hmin _ (hs.mem_toList_left_iff.mpr ⟨pos', hlt, rfl⟩)⟩ - rw [(singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm] - exact hpc + simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff_splits, decide_eq_true_eq, + decide_eq_false_iff_not] @[simp] theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy.toList.any p := by @@ -70,10 +64,7 @@ theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy @[simp] theorem contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : Slice} : s.contains p = s.copy.toList.any p := by - rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff] - simp only [Pattern.Model.CharPred.Decidable.matchesAt_iff, ne_eq, List.any_eq_true, - mem_toList_copy_iff_exists_get, decide_eq_true_eq] - exact ⟨fun ⟨pos, h, hp⟩ => ⟨_, ⟨_, _, rfl⟩, hp⟩, fun ⟨_, ⟨p, h, h'⟩, hp⟩ => ⟨p, h, h' ▸ hp⟩⟩ + rw [contains_prop_eq_contains_decide, contains_bool_eq] theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} : pos.find? p = some pos' ↔ @@ -141,64 +132,48 @@ theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Sl pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧ ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → ¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by - grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff] + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff, decide_eq_true_eq, + decide_eq_false_iff_not] theorem Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? p = some pos' ↔ ∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬ p d := by - rw [Pos.find?_prop_eq_some_iff] - refine ⟨?_, ?_⟩ - · rintro ⟨hle, ⟨hne, hp⟩, hmin⟩ - have hsplit := pos'.splits_next_right hne - obtain ⟨v, hv1, hv2⟩ := (hs.le_iff_exists_eq_append hsplit).mp hle - refine ⟨v, pos'.get hne, _, hsplit.of_eq hv1 rfl, hp, fun d hd => ?_⟩ - obtain ⟨_, hcopy⟩ := - Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hv2, hsplit.of_eq hv1 rfl⟩ - rw [← hcopy] at hd - obtain ⟨q, hq, hqget⟩ := mem_toList_copy_iff_exists_get.mp hd - have hlt : Pos.ofSlice q < pos' := by - simpa [← Slice.Pos.lt_endPos_iff, ← Pos.ofSlice_lt_ofSlice_iff] using hq - subst hqget; rw [Slice.Pos.get_eq_get_ofSlice]; exact hmin _ Pos.le_ofSlice hlt - · rintro ⟨v, c, w, hsplit, hpc, hmin⟩ - have hne := hsplit.ne_endPos_of_singleton - have hu : u = v ++ (singleton c ++ w) := - append_right_inj t |>.mp (hs.eq_append.symm.trans (by rw [hsplit.eq_append, append_assoc])) - have hle : pos ≤ pos' := (hs.le_iff_exists_eq_append hsplit).mpr ⟨v, rfl, hu⟩ - refine ⟨hle, ⟨hne, ?_⟩, fun pos'' hle' hlt => hmin _ ?_⟩ - · rw [(singleton_append_inj.mp (hsplit.eq_right (pos'.splits_next_right hne))).1.symm] - exact hpc - · obtain ⟨_, hcopy⟩ := - Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hu, hsplit⟩ - rw [← hcopy] - exact mem_toList_copy_iff_exists_get.mpr - ⟨pos''.slice pos pos' hle' (Std.le_of_lt hlt), - fun h => Std.ne_of_lt hlt - (by rw [← Slice.Pos.ofSlice_slice (h₁ := hle') (h₂ := Std.le_of_lt hlt), h, - Slice.Pos.ofSlice_endPos]), - by rw [Slice.Pos.get_eq_get_ofSlice] - simp [Slice.Pos.ofSlice_slice]⟩ + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff_splits hs, decide_eq_true_eq, + decide_eq_false_iff_not] theorem Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : pos.find? p = none ↔ ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → ¬ p (pos'.get h) := by - grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff] + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff, decide_eq_false_iff_not] theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? p = none ↔ ∀ c ∈ u.toList, ¬ p c := by - rw [Pos.find?_prop_eq_none_iff] - constructor - · intro h c hc - obtain ⟨pos', hle, hne, hget⟩ := hs.mem_toList_right_iff.mp hc - subst hget; exact h pos' hle hne - · intro h pos' hle hne - exact h _ (hs.mem_toList_right_iff.mpr ⟨pos', hle, hne, rfl⟩) + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff_of_splits hs, + decide_eq_false_iff_not] end String.Slice namespace String +theorem Pos.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : String} + {pos : s.Pos} : pos.find? p = pos.find? (decide <| p ·) := by + show (pos.toSlice.find? p).map Pos.ofToSlice = (pos.toSlice.find? (decide <| p ·)).map Pos.ofToSlice + simp only [show pos.toSlice.find? p = pos.toSlice.find? (decide <| p ·) from + Slice.Pos.find?_prop_eq_find?_decide] + +theorem find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : String} : + s.find? p = s.find? (decide <| p ·) := by + show (s.toSlice.find? p).map Pos.ofToSlice = (s.toSlice.find? (decide <| p ·)).map Pos.ofToSlice + simp only [show s.toSlice.find? p = s.toSlice.find? (decide <| p ·) from + Slice.find?_prop_eq_find?_decide] + +theorem contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {s : String} : + s.contains p = s.contains (decide <| p ·) := by + show s.toSlice.contains p = s.toSlice.contains (decide <| p ·) + exact Slice.contains_prop_eq_contains_decide + theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos pos' : s.Pos} : pos.find? p = some pos' ↔ pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧ @@ -257,52 +232,27 @@ theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : St pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧ ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → ¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by - simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff, - Slice.Pos.find?_prop_eq_some_iff, endPos_toSlice] - refine ⟨?_, ?_⟩ - · rintro ⟨pos', ⟨h₁, ⟨h₂, hp⟩, h₃⟩, rfl⟩ - refine ⟨by simpa [Pos.ofToSlice_le_iff] using h₁, - ⟨by simpa [← Pos.ofToSlice_inj] using h₂, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩ - intro pos'' h₄ h₅ - simpa using h₃ pos''.toSlice (by simpa [Pos.toSlice_le] using h₄) (by simpa using h₅) - · rintro ⟨h₁, ⟨h₂, hp⟩, h₃⟩ - refine ⟨pos'.toSlice, ⟨by simpa [Pos.toSlice_le] using h₁, - ⟨by simpa [← Pos.toSlice_inj] using h₂, by simpa using hp⟩, fun p hp₁ hp₂ => ?_⟩, - by simp⟩ - simpa using h₃ (Pos.ofToSlice p) - (by simpa [Pos.ofToSlice_le_iff] using hp₁) (by simpa using hp₂) + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff, decide_eq_true_eq, + decide_eq_false_iff_not] theorem Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? p = some pos' ↔ ∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬ p d := by - simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff, - Slice.Pos.find?_prop_eq_some_iff_splits (Pos.splits_toSlice_iff.mpr hs)] - constructor - · rintro ⟨q, ⟨v, c, w, hsplit, hpc, hmin⟩, rfl⟩ - exact ⟨v, c, w, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩ - · rintro ⟨v, c, w, hsplit, hpc, hmin⟩ - exact ⟨pos'.toSlice, ⟨v, c, w, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩ + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff_splits hs, decide_eq_true_eq, + decide_eq_false_iff_not] theorem Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : pos.find? p = none ↔ ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → ¬ p (pos'.get h) := by - simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff, - Slice.Pos.find?_prop_eq_none_iff, endPos_toSlice] - refine ⟨?_, ?_⟩ - · intro h pos' h₁ h₂ - simpa [Pos.get_ofToSlice] using - h pos'.toSlice (by simpa [Pos.toSlice_le] using h₁) (by simpa [← Pos.toSlice_inj] using h₂) - · intro h pos' h₁ h₂ - simpa using h (Pos.ofToSlice pos') - (by simpa [Pos.ofToSlice_le_iff] using h₁) (by simpa [← Pos.ofToSlice_inj] using h₂) + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff, decide_eq_false_iff_not] theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? p = none ↔ ∀ c ∈ u.toList, ¬ p c := by - rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff] - exact Slice.Pos.find?_prop_eq_none_iff_of_splits (Pos.splits_toSlice_iff.mpr hs) + simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff_of_splits hs, + decide_eq_false_iff_not] theorem find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} : s.find? p = some pos ↔ @@ -332,28 +282,15 @@ theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s. theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : s.find? p = some pos ↔ ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by - simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_prop_eq_some_iff, - endPos_toSlice, exists_and_right] - refine ⟨?_, ?_⟩ - · rintro ⟨pos, ⟨⟨h, hp⟩, h'⟩, rfl⟩ - refine ⟨⟨by simpa [← Pos.ofToSlice_inj] using h, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩ - intro pos' hp - simpa using h' pos'.toSlice hp - · rintro ⟨⟨h, hp⟩, hmin⟩ - exact ⟨pos.toSlice, ⟨⟨by simpa [← Pos.toSlice_inj] using h, by simpa using hp⟩, - fun pos' hp => by simpa using hmin (Pos.ofToSlice pos') hp⟩, by simp⟩ + simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff, decide_eq_true_eq, + decide_eq_false_iff_not] theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : s.find? p = some pos ↔ ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬ p d := by - simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, - Slice.find?_prop_eq_some_iff_splits] - constructor - · rintro ⟨q, ⟨t, c, u, hsplit, hpc, hmin⟩, rfl⟩ - exact ⟨t, c, u, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩ - · rintro ⟨t, c, u, hsplit, hpc, hmin⟩ - exact ⟨pos.toSlice, ⟨t, c, u, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩ + simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff_splits, decide_eq_true_eq, + decide_eq_false_iff_not] @[simp] theorem contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toList.any p := by @@ -362,6 +299,6 @@ theorem contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toL @[simp] theorem contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : String} : s.contains p = s.toList.any p := by - simp [contains_eq_contains_toSlice, Slice.contains_prop_eq, copy_toSlice] + rw [contains_prop_eq_contains_decide, contains_bool_eq] end String diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/String.lean b/src/Init/Data/String/Lemmas/Pattern/Find/String.lean index 7fd16dd248..b966ffed15 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Find/String.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Find/String.lean @@ -8,6 +8,7 @@ module prelude public import Init.Data.String.Search import all Init.Data.String.Slice +import all Init.Data.String.Pattern.String import Init.ByCases import Init.Data.String.Lemmas.Pattern.Find.Basic import Init.Data.String.Lemmas.Pattern.String.ForwardSearcher @@ -55,11 +56,7 @@ theorem contains_slice_iff {t s : Slice} : @[simp] theorem contains_string_iff {t : String} {s : Slice} : s.contains t ↔ t.toList <:+: s.copy.toList := by - by_cases ht : t = "" - · simp [contains_string_eq_true_of_empty ht s, ht] - · have := Pattern.Model.ForwardStringSearcher.lawfulToForwardSearcherModel (pat := t) ht - simp only [Pattern.Model.contains_eq_true_iff, - Pattern.Model.ForwardStringSearcher.exists_matchesAt_iff_eq_append ht, isInfix_toList_iff] + simp [contains_string_eq_contains_toSlice, contains_slice_iff, copy_toSlice] @[simp] theorem contains_slice_eq_false_iff {t s : Slice} : diff --git a/src/Init/Data/String/Lemmas/Pattern/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Pred.lean index 3357f5acd8..4492f6f077 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Pred.lean @@ -8,6 +8,11 @@ module prelude public import Init.Data.String.Pattern.Pred public import Init.Data.String.Lemmas.Pattern.Basic +public import Init.Data.String.Slice +public import Init.Data.String.Search +import all Init.Data.String.Slice +import all Init.Data.String.Pattern.Pred +import all Init.Data.String.Search import Init.Data.Option.Lemmas import Init.Data.String.Lemmas.Basic import Init.Data.String.Lemmas.Order @@ -112,6 +117,15 @@ theorem isLongestMatchAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice {h : pos ≠ s.endPos} (hc : p (pos.get h)) : IsLongestMatchAt p pos (pos.next h) := isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩ +theorem matchesAt_iff_matchesAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice} + {pos : s.Pos} : MatchesAt p pos ↔ MatchesAt (decide <| p ·) pos := by + simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_decide] + +theorem matchAt?_eq_matchAt?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} + {pos : s.Pos} : matchAt? p pos = matchAt? (decide <| p ·) pos := by + ext endPos + simp [isLongestMatchAt_iff_isLongestMatchAt_decide] + theorem dropPrefix?_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] : ForwardPattern.dropPrefix? p = ForwardPattern.dropPrefix? (decide <| p ·) := rfl @@ -120,8 +134,26 @@ instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p whe rw [dropPrefix?_eq_dropPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide] exact LawfulForwardPatternModel.dropPrefix?_eq_some_iff .. -instance {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p := - .defaultImplementation +theorem toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} : + ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (decide <| p ·) s := (rfl) + +theorem isValidSearchFrom_iff_isValidSearchFrom_decide {p : Char → Prop} [DecidablePred p] + {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} : + IsValidSearchFrom p pos l ↔ IsValidSearchFrom (decide <| p ·) pos l := by + refine ⟨fun h => ?_, fun h => ?_⟩ + · induction h with + | endPos => simpa using IsValidSearchFrom.endPos + | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_decide] + | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_decide] + · induction h with + | endPos => simpa using IsValidSearchFrom.endPos + | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_decide] + | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_decide] + +instance {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p where + isValidSearchFrom_toList s := by + simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_decide] using + LawfulToForwardSearcherModel.isValidSearchFrom_toList (pat := (decide <| p ·)) (s := s) theorem matchesAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) := by @@ -138,4 +170,121 @@ theorem matchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Prop} [DecidablePred end Decidable -end String.Slice.Pattern.Model.CharPred +end Pattern.Model.CharPred + +theorem startsWith_prop_eq_startsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.startsWith p = s.startsWith (decide <| p ·) := (rfl) + +theorem dropPrefix?_prop_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.dropPrefix? p = s.dropPrefix? (decide <| p ·) := (rfl) + +theorem dropPrefix_prop_eq_dropPrefix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.dropPrefix p = s.dropPrefix (decide <| p ·) := (rfl) + +theorem Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide + {p : Char → Prop} [DecidablePred p] {s : Slice} : + dropPrefix? p s = dropPrefix? (decide <| p ·) s := (rfl) + +private theorem dropWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) : + dropWhile.go s p curr = dropWhile.go s (decide <| p ·) curr := by + fun_induction dropWhile.go s p curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih] + | case3 pos h => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide] + +theorem dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.dropWhile p = s.dropWhile (decide <| p ·) := by + simpa only [dropWhile] using dropWhileGo_eq s.startPos + +private theorem takeWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) : + takeWhile.go s p curr = takeWhile.go s (decide <| p ·) curr := by + fun_induction takeWhile.go s p curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih] + | case3 pos h => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide] + +theorem takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.takeWhile p = s.takeWhile (decide <| p ·) := by + simp only [takeWhile]; exact takeWhileGo_eq s.startPos + +theorem all_prop_eq_all_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.all p = s.all (decide <| p ·) := by + simp only [all, dropWhile_prop_eq_dropWhile_decide] + +theorem find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.find? p = s.find? (decide <| p ·) := + (rfl) + +theorem Pos.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} + {pos : s.Pos} : + pos.find? p = pos.find? (decide <| p ·) := + (rfl) + +theorem contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.contains p = s.contains (decide <| p ·) := + (rfl) + +theorem endsWith_prop_eq_endsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.endsWith p = s.endsWith (decide <| p ·) := (rfl) + +theorem dropSuffix?_prop_eq_dropSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.dropSuffix? p = s.dropSuffix? (decide <| p ·) := (rfl) + +theorem dropSuffix_prop_eq_dropSuffix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : + s.dropSuffix p = s.dropSuffix (decide <| p ·) := (rfl) + +theorem Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide + {p : Char → Prop} [DecidablePred p] {s : Slice} : + dropSuffix? p s = dropSuffix? (decide <| p ·) s := (rfl) + +private theorem dropEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} + (curr : s.Pos) : + dropEndWhile.go s p curr = dropEndWhile.go s (decide <| p ·) curr := by + fun_induction dropEndWhile.go s p curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih] + | case3 pos h => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide] + +theorem dropEndWhile_prop_eq_dropEndWhile_decide {p : Char → Prop} [DecidablePred p] + {s : Slice} : + s.dropEndWhile p = s.dropEndWhile (decide <| p ·) := by + simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos + +private theorem takeEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} + (curr : s.Pos) : + takeEndWhile.go s p curr = takeEndWhile.go s (decide <| p ·) curr := by + fun_induction takeEndWhile.go s p curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih] + | case3 pos h => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide] + +theorem takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidablePred p] + {s : Slice} : + s.takeEndWhile p = s.takeEndWhile (decide <| p ·) := by + simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos + +end String.Slice diff --git a/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean index 54e46035b5..3e6da1cafb 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split/Char.lean @@ -9,10 +9,14 @@ prelude public import Init.Data.String.Slice public import Init.Data.String.Search public import Init.Data.List.SplitOn.Basic +public import Init.Data.String.Lemmas.Pattern.Split.Basic +public import Init.Data.String.Lemmas.Pattern.Char +import all Init.Data.String.Lemmas.Pattern.Split.Basic import Init.Data.String.Termination import Init.Data.Order.Lemmas import Init.Data.Iterators.Lemmas.Combinators.FilterMap import Init.Data.String.Lemmas.Pattern.Split.Basic +import Init.Data.String.Lemmas.Pattern.Split.Pred import Init.Data.String.Lemmas.Pattern.Char import Init.ByCases import Init.Data.String.OrderInstances @@ -26,28 +30,26 @@ namespace String.Slice open Pattern.Model Pattern.Model.Char +theorem Pattern.Model.split_char_eq_split_beq {c : Char} {s : Slice} + (f curr : s.Pos) (hle : f ≤ curr) : + Model.split c f curr hle = Model.split (· == c) f curr hle := by + fun_induction Model.split c f curr hle with + | case1 fr h => simp + | case2 fr curr hle h pos h₁ h₂ ih => + conv => rhs; rw [Model.split] + simp only [h, ↓reduceDIte] + split <;> simp_all [matchAt?_eq_matchAt?_beq] + | case3 fr curr hle h pos ih => + conv => rhs; rw [Model.split] + simp only [h, ↓reduceDIte] + split <;> simp_all [matchAt?_eq_matchAt?_beq] + theorem toList_splitToSubslice_char {s : Slice} {c : Char} : (s.splitToSubslice c).toList.map (Slice.copy ∘ Subslice.toSlice) = (s.copy.toList.splitOn c).map String.ofList := by - simp only [Pattern.toList_splitToSubslice_eq_modelSplit] - suffices ∀ (f p : s.Pos) (hle : f ≤ p) (t₁ t₂ : String), - p.Splits t₁ t₂ → (Pattern.Model.split c f p hle).map (copy ∘ Subslice.toSlice) = - (t₂.toList.splitOnPPrepend (· == c) (s.subslice f p hle).copy.toList.reverse).map String.ofList by - simpa [List.splitOn_eq_splitOnP] using this s.startPos s.startPos (Std.le_refl _) "" s.copy - intro f p hle t₁ t₂ hp - induction p using Pos.next_induction generalizing f t₁ t₂ with - | next p h ih => - obtain ⟨t₂, rfl⟩ := hp.exists_eq_singleton_append h - by_cases hpc : p.get h = c - · simp [split_eq_of_isLongestMatchAt (isLongestMatchAt_of_get_eq hpc), - ih _ (Std.le_refl _) _ _ hp.next, - List.splitOnPPrepend_cons_pos (p := (· == c)) (beq_iff_eq.2 hpc)] - · rw [split_eq_next_of_not_matchesAt h (not_matchesAt_of_get_ne hpc)] - simp only [toList_append, toList_singleton, List.cons_append, List.nil_append, Subslice.copy_eq] - rw [ih _ _ _ _ hp.next, List.splitOnPPrepend_cons_neg (by simpa)] - have := (splits_slice (Std.le_trans hle (by simp)) (p.slice f (p.next h) hle (by simp))).eq_append - simp_all - | endPos => simp_all + have : (s.splitToSubslice c).toList = (s.splitToSubslice (· == c)).toList := by + simp only [Pattern.toList_splitToSubslice_eq_modelSplit, Pattern.Model.split_char_eq_split_beq] + simp only [this, List.splitOn_eq_splitOnP, toList_splitToSubslice_bool] theorem toList_split_char {s : Slice} {c : Char} : (s.split c).toList.map Slice.copy = (s.copy.toList.splitOn c).map String.ofList := by diff --git a/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean index ae579318f2..da26eb0099 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split/Pred.lean @@ -9,7 +9,10 @@ prelude public import Init.Data.String.Slice public import Init.Data.String.Search public import Init.Data.List.SplitOn.Basic +public import Init.Data.String.Lemmas.Pattern.Split.Basic +public import Init.Data.String.Lemmas.Pattern.Pred import Init.Data.String.Termination +import all Init.Data.String.Lemmas.Pattern.Split.Basic import Init.Data.Order.Lemmas import Init.Data.Iterators.Lemmas.Combinators.FilterMap import Init.Data.String.Lemmas.Pattern.Split.Basic @@ -61,28 +64,27 @@ section open Pattern.Model Pattern.Model.CharPred.Decidable +theorem Pattern.Model.split_eq_split_decide {p : Char → Prop} [DecidablePred p] {s : Slice} + (f curr : s.Pos) (hle : f ≤ curr) : + Model.split p f curr hle = Model.split (decide <| p ·) f curr hle := by + fun_induction Model.split p f curr hle with + | case1 fr h => simp + | case2 fr curr hle h pos h₁ h₂ ih => + conv => rhs; rw [Model.split] + simp only [h, ↓reduceDIte] + split <;> simp_all [matchAt?_eq_matchAt?_decide] + | case3 fr curr hle h pos ih => + conv => rhs; rw [Model.split] + simp only [h, ↓reduceDIte] + split <;> simp_all [matchAt?_eq_matchAt?_decide] + theorem toList_splitToSubslice_prop {s : Slice} {p : Char → Prop} [DecidablePred p] : (s.splitToSubslice p).toList.map (Slice.copy ∘ Subslice.toSlice) = (s.copy.toList.splitOnP p).map String.ofList := by - simp only [Pattern.toList_splitToSubslice_eq_modelSplit] - suffices ∀ (f pos : s.Pos) (hle : f ≤ pos) (t₁ t₂ : String), - pos.Splits t₁ t₂ → (Pattern.Model.split p f pos hle).map (copy ∘ Subslice.toSlice) = - (t₂.toList.splitOnPPrepend p (s.subslice f pos hle).copy.toList.reverse).map String.ofList by - simpa using this s.startPos s.startPos (Std.le_refl _) "" s.copy - intro f pos hle t₁ t₂ hp - induction pos using Pos.next_induction generalizing f t₁ t₂ with - | next pos h ih => - obtain ⟨t₂, rfl⟩ := hp.exists_eq_singleton_append h - by_cases hpc : p (pos.get h) - · simp [split_eq_of_isLongestMatchAt (isLongestMatchAt_of_get hpc), - ih _ (Std.le_refl _) _ _ hp.next, - List.splitOnPPrepend_cons_pos (p := (decide <| p ·)) (by simpa using hpc)] - · rw [split_eq_next_of_not_matchesAt h (not_matchesAt_of_get hpc)] - simp only [toList_append, toList_singleton, List.cons_append, List.nil_append, Subslice.copy_eq] - rw [ih _ _ _ _ hp.next, List.splitOnPPrepend_cons_neg (by simpa)] - have := (splits_slice (Std.le_trans hle (by simp)) (pos.slice f (pos.next h) hle (by simp))).eq_append - simp_all - | endPos => simp_all + have : (s.splitToSubslice p).toList = (s.splitToSubslice (decide <| p ·)).toList := by + simp only [Pattern.toList_splitToSubslice_eq_modelSplit, split_eq_split_decide] + rw [this] + exact toList_splitToSubslice_bool theorem toList_split_prop {s : Slice} {p : Char → Prop} [DecidablePred p] : (s.split p).toList.map Slice.copy = (s.copy.toList.splitOnP p).map String.ofList := by diff --git a/src/Init/Data/String/Lemmas/Pattern/String/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/String/Basic.lean index 6d4a73ea7f..727cc661fc 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/Basic.lean @@ -6,6 +6,7 @@ Author: Markus Himmel module prelude +public import Init.Data.String.Pattern.String public import Init.Data.String.Lemmas.Pattern.Basic import Init.Data.String.Lemmas.IsEmpty import Init.Data.String.Lemmas.Basic @@ -150,19 +151,19 @@ theorem isMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} : IsMatch (ρ := String) pat pos ↔ IsMatch (ρ := Slice) pat.toSlice pos := by simp only [Model.isMatch_iff, ForwardPatternModel.Matches, copy_toSlice] -theorem isLongestMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} : +theorem isLongestMatch_iff_isLongestMatch_toSlice {pat : String} {s : Slice} {pos : s.Pos} : IsLongestMatch (ρ := String) pat pos ↔ IsLongestMatch (ρ := Slice) pat.toSlice pos where mp h := ⟨isMatch_iff_slice.1 h.isMatch, fun p hp hm => h.not_isMatch p hp (isMatch_iff_slice.2 hm)⟩ mpr h := ⟨isMatch_iff_slice.2 h.isMatch, fun p hp hm => h.not_isMatch p hp (isMatch_iff_slice.1 hm)⟩ -theorem isLongestMatchAt_iff_slice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : +theorem isLongestMatchAt_iff_isLongestMatchAt_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} : IsLongestMatchAt (ρ := String) pat pos₁ pos₂ ↔ IsLongestMatchAt (ρ := Slice) pat.toSlice pos₁ pos₂ := by - simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_slice] + simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_toSlice] -theorem matchesAt_iff_slice {pat : String} {s : Slice} {pos : s.Pos} : +theorem matchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} : MatchesAt (ρ := String) pat pos ↔ MatchesAt (ρ := Slice) pat.toSlice pos := by - simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_slice] + simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice] private theorem toSlice_isEmpty (h : pat ≠ "") : pat.toSlice.isEmpty = false := by rwa [isEmpty_toSlice, isEmpty_eq_false_iff] @@ -178,7 +179,7 @@ theorem isLongestMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ theorem isLongestMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ h, (s.slice pos₁ pos₂ h).copy = pat := by - rw [isLongestMatchAt_iff_slice, + rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice, ForwardSliceSearcher.isLongestMatchAt_iff (toSlice_isEmpty h)] simp @@ -186,7 +187,7 @@ theorem isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : (h : pat ≠ "") : IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂ := by - rw [isLongestMatchAt_iff_slice, + rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice, ForwardSliceSearcher.isLongestMatchAt_iff_splits (toSlice_isEmpty h)] simp @@ -194,7 +195,7 @@ theorem isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : (h : pat ≠ "") : IsLongestMatchAt pat pos₁ pos₂ ↔ s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray := by - rw [isLongestMatchAt_iff_slice, + rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice, ForwardSliceSearcher.isLongestMatchAt_iff_extract (toSlice_isEmpty h)] simp @@ -203,11 +204,11 @@ theorem offset_of_isLongestMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm] exact ForwardSliceSearcher.offset_of_isLongestMatchAt (toSlice_isEmpty h) - (isLongestMatchAt_iff_slice.1 h') + (isLongestMatchAt_iff_isLongestMatchAt_toSlice.1 h') theorem matchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") : MatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ (pat ++ t₂) := by - rw [matchesAt_iff_slice, + rw [matchesAt_iff_toSlice, ForwardSliceSearcher.matchesAt_iff_splits (toSlice_isEmpty h)] simp @@ -229,8 +230,8 @@ theorem matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos} IsLongestMatchAt pat pos (s.pos _ h) := by have key := ForwardSliceSearcher.matchesAt_iff_isLongestMatchAt (pat := pat.toSlice) (toSlice_isEmpty h) (pos := pos) - simp only [utf8ByteSize_toSlice, ← isLongestMatchAt_iff_slice] at key - rwa [matchesAt_iff_slice] + simp only [utf8ByteSize_toSlice, ← isLongestMatchAt_iff_isLongestMatchAt_toSlice] at key + rwa [matchesAt_iff_toSlice] theorem matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") : MatchesAt pat pos ↔ @@ -240,13 +241,33 @@ theorem matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat have key := ForwardSliceSearcher.matchesAt_iff_getElem (pat := pat.toSlice) (toSlice_isEmpty h) (pos := pos) simp only [copy_toSlice] at key - rwa [matchesAt_iff_slice] + rwa [matchesAt_iff_toSlice] theorem le_of_matchesAt {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") (h' : MatchesAt pat pos) : pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos := by rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm] exact ForwardSliceSearcher.le_of_matchesAt (toSlice_isEmpty h) - (matchesAt_iff_slice.1 h') + (matchesAt_iff_toSlice.1 h') + +theorem matchesAt_iff_matchesAt_toSlice {pat : String} {s : Slice} + {pos : s.Pos} : MatchesAt pat pos ↔ MatchesAt pat.toSlice pos := by + simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice] + +theorem toSearcher_eq {pat : String} {s : Slice} : + ToForwardSearcher.toSearcher pat s = ToForwardSearcher.toSearcher pat.toSlice s := (rfl) + +theorem isValidSearchFrom_iff_isValidSearchFrom_toSlice {pat : String} + {s : Slice} {pos : s.Pos} {l : List (SearchStep s)} : + IsValidSearchFrom pat pos l ↔ IsValidSearchFrom pat.toSlice pos l := by + refine ⟨fun h => ?_, fun h => ?_⟩ + · induction h with + | endPos => simpa using IsValidSearchFrom.endPos + | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_toSlice] + | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_toSlice] + · induction h with + | endPos => simpa using IsValidSearchFrom.endPos + | matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_toSlice] + | mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_toSlice] end ForwardStringSearcher diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean index a335b13a2c..4aea20d8c9 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean @@ -8,7 +8,10 @@ module prelude public import Init.Data.String.Lemmas.Pattern.String.Basic public import Init.Data.String.Pattern.String +public import Init.Data.String.Slice import all Init.Data.String.Pattern.String +import all Init.Data.String.Slice +import Init.Data.String.Lemmas.Pattern.Pred import Init.Data.String.Lemmas.Pattern.Memcmp import Init.Data.String.Lemmas.Basic import Init.Data.ByteArray.Lemmas @@ -86,4 +89,104 @@ public theorem lawfulForwardPatternModel {pat : String} (hpat : pat ≠ "") : end Model.ForwardStringSearcher -end String.Slice.Pattern +end Pattern + +public theorem startsWith_string_eq_startsWith_toSlice {pat : String} {s : Slice} : + s.startsWith pat = s.startsWith pat.toSlice := (rfl) + +public theorem dropPrefix?_string_eq_dropPrefix?_toSlice {pat : String} {s : Slice} : + s.dropPrefix? pat = s.dropPrefix? pat.toSlice := (rfl) + +public theorem dropPrefix_string_eq_dropPrefix_toSlice {pat : String} {s : Slice} : + s.dropPrefix pat = s.dropPrefix pat.toSlice := (rfl) + +public theorem Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice + {pat : String} {s : Slice} : + dropPrefix? pat s = dropPrefix? pat.toSlice s := (rfl) + +private theorem dropWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : + dropWhile.go s pat curr = dropWhile.go s pat.toSlice curr := by + fun_induction dropWhile.go s pat curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih] + | case3 pos h => + conv => rhs; rw [dropWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice] + +public theorem dropWhile_string_eq_dropWhile_toSlice {pat : String} {s : Slice} : + s.dropWhile pat = s.dropWhile pat.toSlice := by + simpa only [dropWhile] using dropWhileGo_string_eq s.startPos + +private theorem takeWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : + takeWhile.go s pat curr = takeWhile.go s pat.toSlice curr := by + fun_induction takeWhile.go s pat curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih] + | case3 pos h => + conv => rhs; rw [takeWhile.go] + simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice] + +public theorem takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice} : + s.takeWhile pat = s.takeWhile pat.toSlice := by + simp only [takeWhile]; exact takeWhileGo_string_eq s.startPos + +public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} : + s.all pat = s.all pat.toSlice := by + simp only [all, dropWhile_string_eq_dropWhile_toSlice] + +public theorem endsWith_string_eq_endsWith_toSlice {pat : String} {s : Slice} : + s.endsWith pat = s.endsWith pat.toSlice := (rfl) + +public theorem dropSuffix?_string_eq_dropSuffix?_toSlice {pat : String} {s : Slice} : + s.dropSuffix? pat = s.dropSuffix? pat.toSlice := (rfl) + +public theorem dropSuffix_string_eq_dropSuffix_toSlice {pat : String} {s : Slice} : + s.dropSuffix pat = s.dropSuffix pat.toSlice := (rfl) + +public theorem Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice + {pat : String} {s : Slice} : + dropSuffix? pat s = dropSuffix? pat.toSlice s := (rfl) + +private theorem dropEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : + dropEndWhile.go s pat curr = dropEndWhile.go s pat.toSlice curr := by + fun_induction dropEndWhile.go s pat curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih] + | case3 pos h => + conv => rhs; rw [dropEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice] + +public theorem dropEndWhile_string_eq_dropEndWhile_toSlice {pat : String} {s : Slice} : + s.dropEndWhile pat = s.dropEndWhile pat.toSlice := by + simpa only [dropEndWhile] using dropEndWhileGo_string_eq s.endPos + +private theorem takeEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) : + takeEndWhile.go s pat curr = takeEndWhile.go s pat.toSlice curr := by + fun_induction takeEndWhile.go s pat curr with + | case1 pos nextCurr h₁ h₂ ih => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih] + | case2 pos nextCurr h ih => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih] + | case3 pos h => + conv => rhs; rw [takeEndWhile.go] + simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice] + +public theorem takeEndWhile_string_eq_takeEndWhile_toSlice {pat : String} {s : Slice} : + s.takeEndWhile pat = s.takeEndWhile pat.toSlice := by + simpa only [takeEndWhile] using takeEndWhileGo_string_eq s.endPos + +end String.Slice diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean index 375930dd5e..50d1d1d852 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean @@ -8,6 +8,10 @@ module prelude public import Init.Data.String.Lemmas.Pattern.String.Basic public import Init.Data.String.Pattern.String +public import Init.Data.String.Slice +public import Init.Data.String.Search +import all Init.Data.String.Slice +import all Init.Data.String.Search import all Init.Data.String.Pattern.String import Init.Data.String.Lemmas.IsEmpty import Init.Data.Vector.Lemmas @@ -435,7 +439,6 @@ theorem Invariants.of_prefixFunction_eq {pat s : Slice} {stackPos needlePos : St rw [Nat.sub_add_cancel (by simp at h'; omega)] at this exact hk ▸ (h.partialMatch.partialMatch_iff.1 this).2 -set_option backward.isDefEq.respectTransparency false in theorem Invariants.isValidSearchFrom_toList {pat s : Slice} {stackPos needlePos : String.Pos.Raw} (it : Std.Iter (α := ForwardSliceSearcher s) (SearchStep s)) (h : Invariants pat s needlePos stackPos) @@ -600,30 +603,11 @@ end ForwardSliceSearcher namespace ForwardStringSearcher -private theorem isValidSearchFrom_iff_slice {pat : String} {s : Slice} {pos : s.Pos} - {l : List (SearchStep s)} : - IsValidSearchFrom (ρ := String) pat pos l ↔ - IsValidSearchFrom (ρ := Slice) pat.toSlice pos l := by - constructor - · intro h - induction h with - | endPos => exact .endPos - | matched hm _ ih => exact .matched (isLongestMatchAt_iff_slice.1 hm) ih - | mismatched hlt hnm _ ih => - exact .mismatched hlt (fun p hp₁ hp₂ hm => hnm p hp₁ hp₂ (matchesAt_iff_slice.2 hm)) ih - · intro h - induction h with - | endPos => exact .endPos - | matched hm _ ih => exact .matched (isLongestMatchAt_iff_slice.2 hm) ih - | mismatched hlt hnm _ ih => - exact .mismatched hlt (fun p hp₁ hp₂ hm => hnm p hp₁ hp₂ (matchesAt_iff_slice.1 hm)) ih - public theorem lawfulToForwardSearcherModel {pat : String} (hpat : pat ≠ "") : LawfulToForwardSearcherModel pat where - isValidSearchFrom_toList s := - isValidSearchFrom_iff_slice.2 - ((ForwardSliceSearcher.lawfulToForwardSearcherModel - (by rwa [isEmpty_toSlice, isEmpty_eq_false_iff])).isValidSearchFrom_toList s) + isValidSearchFrom_toList s := by + simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_toSlice] using + (ForwardSliceSearcher.lawfulToForwardSearcherModel (by simpa)).isValidSearchFrom_toList (pat := pat.toSlice) (s := s) public theorem toSearcher_empty (s : Slice) : ToForwardSearcher.toSearcher "" s = Std.Iter.mk (.emptyBefore s.startPos : ForwardSliceSearcher s) := by @@ -632,4 +616,18 @@ public theorem toSearcher_empty (s : Slice) : ToForwardSearcher.toSearcher "" s end ForwardStringSearcher -end String.Slice.Pattern.Model +end Pattern.Model + +public theorem contains_string_eq_contains_toSlice {pat : String} {s : Slice} : + s.contains pat = s.contains pat.toSlice := + (rfl) + +public theorem find?_string_eq_find?_toSlice {pat : String} {s : Slice} : + s.find? pat = s.find? pat.toSlice := + (rfl) + +public theorem Pos.find?_string_eq_find?_toSlice {pat : String} {s : Slice} {p : s.Pos} : + p.find? pat = p.find? pat.toSlice := + (rfl) + +end String.Slice diff --git a/src/Init/Data/String/Pattern/Char.lean b/src/Init/Data/String/Pattern/Char.lean index f5f0a0fd26..577010468f 100644 --- a/src/Init/Data/String/Pattern/Char.lean +++ b/src/Init/Data/String/Pattern/Char.lean @@ -6,12 +6,7 @@ Authors: Henrik Böving, Markus Himmel module prelude -public import Init.Data.String.Pattern.Basic -import Init.Data.String.Lemmas.FindPos -import Init.Data.String.Termination -import Init.Data.String.Lemmas.IsEmpty -import Init.Data.String.Lemmas.Order -import Init.Data.Option.Lemmas +public import Init.Data.String.Pattern.Pred set_option doc.verso true @@ -26,75 +21,31 @@ namespace String.Slice.Pattern namespace Char instance {c : Char} : ForwardPattern c where - dropPrefixOfNonempty? s h := - if s.startPos.get (by exact Slice.startPos_ne_endPos h) = c then - some (s.startPos.next (by exact Slice.startPos_ne_endPos h)) - else - none - dropPrefix? s := - if h : s.startPos = s.endPos then - none - else if s.startPos.get h = c then - some (s.startPos.next h) - else - none - startsWith s := - if h : s.startPos = s.endPos then - false - else - s.startPos.get h = c + dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (· == c) s h + dropPrefix? s := ForwardPattern.dropPrefix? (· == c) s + startsWith s := ForwardPattern.startsWith (· == c) s instance {c : Char} : StrictForwardPattern c where - ne_startPos {s h q} := by - simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some, - Option.some.injEq, ne_eq, and_imp] - rintro _ rfl - simp + ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (· == c)) h q instance {c : Char} : LawfulForwardPattern c where - dropPrefixOfNonempty?_eq {s h} := by - simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?, - Slice.startPos_eq_endPos_iff, h] - startsWith_eq {s} := by - simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?] - split <;> (try split) <;> simp_all + dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (· == c)) h + startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (· == c)) s -instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher c) := - .defaultImplementation +instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher (· == c)) where + toSearcher s := ToForwardSearcher.toSearcher (· == c) s instance {c : Char} : BackwardPattern c where - dropSuffixOfNonempty? s h := - if (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h))).get (by simp) = c then - some (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h))) - else - none - dropSuffix? s := - if h : s.endPos = s.startPos then - none - else if (s.endPos.prev h).get (by simp) = c then - some (s.endPos.prev h) - else - none - endsWith s := - if h : s.endPos = s.startPos then - false - else - (s.endPos.prev h).get (by simp) = c + dropSuffixOfNonempty? s h := BackwardPattern.dropSuffixOfNonempty? (· == c) s h + dropSuffix? s := BackwardPattern.dropSuffix? (· == c) s + endsWith s := BackwardPattern.endsWith (· == c) s instance {c : Char} : StrictBackwardPattern c where - ne_endPos {s h q} := by - simp only [BackwardPattern.dropSuffixOfNonempty?, Option.ite_none_right_eq_some, - Option.some.injEq, ne_eq, and_imp] - rintro _ rfl - simp + ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (· == c)) h q instance {c : Char} : LawfulBackwardPattern c where - dropSuffixOfNonempty?_eq {s h} := by - simp [BackwardPattern.dropSuffixOfNonempty?, BackwardPattern.dropSuffix?, - Eq.comm (a := s.endPos), Slice.startPos_eq_endPos_iff, h] - endsWith_eq {s} := by - simp only [BackwardPattern.endsWith, BackwardPattern.dropSuffix?] - split <;> (try split) <;> simp_all + dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (· == c)) h + endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (· == c)) s instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) := .defaultImplementation diff --git a/src/Init/Data/String/Pattern/Pred.lean b/src/Init/Data/String/Pattern/Pred.lean index c1ef5c54ba..2ce425d7e8 100644 --- a/src/Init/Data/String/Pattern/Pred.lean +++ b/src/Init/Data/String/Pattern/Pred.lean @@ -81,8 +81,8 @@ instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p where dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (decide <| p ·)) h startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (decide <| p ·)) s -instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p) := - .defaultImplementation +instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher (decide <| p ·)) where + toSearcher s := ToForwardSearcher.toSearcher (decide <| p ·) s end Decidable