From 9c5d2bf62e114f38c78c23e730a0ef75e8840579 Mon Sep 17 00:00:00 2001 From: Markus Himmel <2065352+TwoFX@users.noreply.github.com> Date: Thu, 19 Mar 2026 14:05:55 +0100 Subject: [PATCH] refactor: rename `ForwardPattern.dropPrefix?` to `ForwardPattern.skipPrefix?` (#12984) This PR renames the function `ForwardPattern.dropPrefix?` to `ForwardPattern.skipPrefix`? This function `(s : String.Slice) -> Option s.Pos` is not to be confused with `String.Slice.dropPrefix? : (s : String.Slice) -> Option String.Slice`. --- .../Data/String/Lemmas/Pattern/Basic.lean | 16 +++---- src/Init/Data/String/Lemmas/Pattern/Char.lean | 20 ++++----- src/Init/Data/String/Lemmas/Pattern/Pred.lean | 30 ++++++------- .../Lemmas/Pattern/String/ForwardPattern.lean | 42 +++++++++---------- src/Init/Data/String/Pattern/Basic.lean | 30 +++++++------ src/Init/Data/String/Pattern/Char.lean | 6 +-- src/Init/Data/String/Pattern/Pred.lean | 18 ++++---- src/Init/Data/String/Pattern/String.lean | 6 +-- src/Init/Data/String/Slice.lean | 6 +-- src/Std/Data/String/ToNat.lean | 1 - 10 files changed, 89 insertions(+), 86 deletions(-) diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean index 37338e54a1..4433d46f21 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean @@ -272,14 +272,14 @@ supplied by the {name}`ForwardPatternModel` instance. -/ class LawfulForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPattern pat] [ForwardPatternModel pat] : Prop extends LawfulForwardPattern pat where - dropPrefix?_eq_some_iff (pos) : ForwardPattern.dropPrefix? pat s = some pos ↔ IsLongestMatch pat pos + skipPrefix?_eq_some_iff (pos) : ForwardPattern.skipPrefix? pat s = some pos ↔ IsLongestMatch pat pos open Classical in -theorem LawfulForwardPatternModel.dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat] +theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat] [LawfulForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} : - ForwardPattern.dropPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by + ForwardPattern.skipPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by rw [← Decidable.not_iff_not] - simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.dropPrefix?_eq_some_iff] + simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.skipPrefix?_eq_some_iff] refine ⟨fun ⟨p, hp⟩ => ?_, fun ⟨p, hp⟩ => ?_⟩ · exact ⟨Slice.Pos.ofSliceFrom p, hp.isLongestMatchAt_ofSliceFrom⟩ · exact ⟨p₀.sliceFrom p hp.le, hp.isLongestMatch_sliceFrom⟩ @@ -358,8 +358,8 @@ theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPa Std.PlausibleIterStep.yield, Std.IterStep.yield.injEq] at heq rw [← heq.1, ← heq.2] apply IsValidSearchFrom.matched - · rw [LawfulForwardPattern.dropPrefixOfNonempty?_eq, - LawfulForwardPatternModel.dropPrefix?_eq_some_iff] at heq' + · rw [LawfulForwardPattern.skipPrefixOfNonempty?_eq, + LawfulForwardPatternModel.skipPrefix?_eq_some_iff] at heq' exact heq'.isLongestMatchAt_ofSliceFrom · simp only [Std.IterM.toIter] apply ih @@ -372,8 +372,8 @@ theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPa apply IsValidSearchFrom.mismatched (by simp) _ (ih _ (by simp)) intro p' hp' hp'' obtain rfl : pos = p' := Std.le_antisymm hp' (by simpa using hp'') - rwa [LawfulForwardPattern.dropPrefixOfNonempty?_eq, - LawfulForwardPatternModel.dropPrefix?_eq_none_iff] at heq' + rwa [LawfulForwardPattern.skipPrefixOfNonempty?_eq, + LawfulForwardPatternModel.skipPrefix?_eq_none_iff] at heq' · split at heq <;> simp at heq · split at heq <;> simp at heq diff --git a/src/Init/Data/String/Lemmas/Pattern/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Char.lean index 605b4e08ad..fb3b60c7c8 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Char.lean @@ -57,8 +57,8 @@ theorem isLongestMatchAt_of_get_eq {c : Char} {s : Slice} {pos : s.Pos} {h : pos isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩ instance {c : Char} : LawfulForwardPatternModel c where - dropPrefix?_eq_some_iff {s} pos := by - simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)] + skipPrefix?_eq_some_iff {s} pos := by + simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)] theorem toSearcher_eq {c : Char} {s : Slice} : ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (· == c) s := (rfl) @@ -136,21 +136,21 @@ theorem dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} : 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) +theorem Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} : + skipPrefix? c s = skipPrefix? (· == 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] + simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih] | case2 pos nextCurr h ih => conv => rhs; rw [dropWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih] + simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih] | case3 pos h => conv => rhs; rw [dropWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq] + simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq] theorem dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} : s.dropWhile c = s.dropWhile (· == c) := by @@ -161,13 +161,13 @@ private theorem takeWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) : 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] + simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih] | case2 pos nextCurr h ih => conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih] + simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih] | case3 pos h => conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq] + simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq] theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} : s.takeWhile c = s.takeWhile (· == c) := by diff --git a/src/Init/Data/String/Lemmas/Pattern/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Pred.lean index 4492f6f077..d55e8a92a9 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Pred.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Pred.lean @@ -57,8 +57,8 @@ theorem isLongestMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩ instance {p : Char → Bool} : LawfulForwardPatternModel p where - dropPrefix?_eq_some_iff {s} pos := by - simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)] + skipPrefix?_eq_some_iff {s} pos := by + simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)] instance {p : Char → Bool} : LawfulToForwardSearcherModel p := .defaultImplementation @@ -126,13 +126,13 @@ theorem matchAt?_eq_matchAt?_decide {p : Char → Prop} [DecidablePred p] {s : S 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 +theorem skipPrefix?_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] : + ForwardPattern.skipPrefix? p = ForwardPattern.skipPrefix? (decide <| p ·) := rfl instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p where - dropPrefix?_eq_some_iff {s} pos := by - rw [dropPrefix?_eq_dropPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide] - exact LawfulForwardPatternModel.dropPrefix?_eq_some_iff .. + skipPrefix?_eq_some_iff {s} pos := by + rw [skipPrefix?_eq_skipPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide] + exact LawfulForwardPatternModel.skipPrefix?_eq_some_iff .. theorem toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} : ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (decide <| p ·) s := (rfl) @@ -181,22 +181,22 @@ theorem dropPrefix?_prop_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePre 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 +theorem Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : - dropPrefix? p s = dropPrefix? (decide <| p ·) s := (rfl) + skipPrefix? p s = skipPrefix? (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] + simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih] | case2 pos nextCurr h ih => conv => rhs; rw [dropWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih] + simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih] | case3 pos h => conv => rhs; rw [dropWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide] + simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide] theorem dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.dropWhile p = s.dropWhile (decide <| p ·) := by @@ -207,13 +207,13 @@ private theorem takeWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} 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] + simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih] | case2 pos nextCurr h ih => conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih] + simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih] | case3 pos h => conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide] + simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide] theorem takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} : s.takeWhile p = s.takeWhile (decide <| p ·) := by diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean index 4aea20d8c9..9f627cb836 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.lean @@ -39,9 +39,9 @@ theorem startsWith_iff {pat s : Slice} : startsWith pat s ↔ ∃ t, s.copy = pa · rintro ⟨t, rfl⟩ simp [-size_toByteArray, ByteArray.extract_append] -theorem dropPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} : - dropPrefix? pat s = some pos ↔ (s.sliceTo pos).copy = pat.copy := by - fun_cases dropPrefix? with +theorem skipPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} : + skipPrefix? pat s = some pos ↔ (s.sliceTo pos).copy = pat.copy := by + fun_cases skipPrefix? with | case1 h => simp only [offset_startPos, Pos.Raw.offsetBy_zero, Option.some.injEq] obtain ⟨t, ht⟩ := startsWith_iff.1 h @@ -58,8 +58,8 @@ theorem dropPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} : have := h (s.sliceFrom pos).copy simp [← heq, pos.splits.eq_append] at this -theorem isSome_dropPrefix? {pat s : Slice} : (dropPrefix? pat s).isSome = startsWith pat s := by - fun_cases dropPrefix? <;> simp_all +theorem isSome_skipPrefix? {pat s : Slice} : (skipPrefix? pat s).isSome = startsWith pat s := by + fun_cases skipPrefix? <;> simp_all end ForwardSliceSearcher @@ -69,10 +69,10 @@ open Pattern.ForwardSliceSearcher public theorem lawfulForwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) : LawfulForwardPatternModel pat where - dropPrefixOfNonempty?_eq h := rfl - startsWith_eq s := isSome_dropPrefix?.symm - dropPrefix?_eq_some_iff pos := by - simp [ForwardPattern.dropPrefix?, dropPrefix?_eq_some_iff, isLongestMatch_iff hpat] + skipPrefixOfNonempty?_eq h := rfl + startsWith_eq s := isSome_skipPrefix?.symm + skipPrefix?_eq_some_iff pos := by + simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat] end Model.ForwardSliceSearcher @@ -82,10 +82,10 @@ open Pattern.ForwardSliceSearcher public theorem lawfulForwardPatternModel {pat : String} (hpat : pat ≠ "") : LawfulForwardPatternModel pat where - dropPrefixOfNonempty?_eq h := rfl - startsWith_eq s := isSome_dropPrefix?.symm - dropPrefix?_eq_some_iff pos := by - simp [ForwardPattern.dropPrefix?, dropPrefix?_eq_some_iff, isLongestMatch_iff hpat] + skipPrefixOfNonempty?_eq h := rfl + startsWith_eq s := isSome_skipPrefix?.symm + skipPrefix?_eq_some_iff pos := by + simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat] end Model.ForwardStringSearcher @@ -100,22 +100,22 @@ public theorem dropPrefix?_string_eq_dropPrefix?_toSlice {pat : String} {s : Sli 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 +public theorem Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice {pat : String} {s : Slice} : - dropPrefix? pat s = dropPrefix? pat.toSlice s := (rfl) + skipPrefix? pat s = skipPrefix? 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] + simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h₁, h₂, ih] | case2 pos nextCurr h ih => conv => rhs; rw [dropWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih] + simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h, ih] | case3 pos h => conv => rhs; rw [dropWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice] + simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice] public theorem dropWhile_string_eq_dropWhile_toSlice {pat : String} {s : Slice} : s.dropWhile pat = s.dropWhile pat.toSlice := by @@ -126,13 +126,13 @@ private theorem takeWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) 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] + simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h₁, h₂, ih] | case2 pos nextCurr h ih => conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih] + simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h, ih] | case3 pos h => conv => rhs; rw [takeWhile.go] - simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice] + simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice] public theorem takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice} : s.takeWhile pat = s.takeWhile pat.toSlice := by diff --git a/src/Init/Data/String/Pattern/Basic.lean b/src/Init/Data/String/Pattern/Basic.lean index 3c8a197f87..68a2211438 100644 --- a/src/Init/Data/String/Pattern/Basic.lean +++ b/src/Init/Data/String/Pattern/Basic.lean @@ -106,20 +106,24 @@ class ForwardPattern {ρ : Type} (pat : ρ) where Checks whether the slice starts with the pattern. If it does, the slice is returned with the prefix removed; otherwise the result is {name}`none`. -/ - dropPrefix? : (s : Slice) → Option s.Pos + skipPrefix? : (s : Slice) → Option s.Pos /-- Checks whether the slice starts with the pattern. If it does, the slice is returned with the prefix removed; otherwise the result is {name}`none`. -/ - dropPrefixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => dropPrefix? s + skipPrefixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => skipPrefix? s /-- Checks whether the slice starts with the pattern. -/ - startsWith : (s : Slice) → Bool := fun s => (dropPrefix? s).isSome + startsWith : (s : Slice) → Bool := fun s => (skipPrefix? s).isSome + +@[deprecated ForwardPattern.dropPrefix? (since := "2026-03-19")] +def ForwardPattern.dropPrefix? {ρ : Type} (pat : ρ) [ForwardPattern pat] (s : Slice) : Option s.Pos := + ForwardPattern.skipPrefix? pat s /-- -A lawful forward pattern is one where the three functions {name}`ForwardPattern.dropPrefix?`, -{name}`ForwardPattern.dropPrefixOfNonempty?` and {name}`ForwardPattern.startsWith` agree for any +A lawful forward pattern is one where the three functions {name}`ForwardPattern.skipPrefix?`, +{name}`ForwardPattern.skipPrefixOfNonempty?` and {name}`ForwardPattern.startsWith` agree for any given input slice. Note that this is a relatively weak condition. It is non-uniform in the sense that the functions @@ -127,14 +131,14 @@ can still return completely different results on different slices, even if they string. There is a stronger lawfulness typeclass {lit}`LawfulForwardPatternModel` that asserts that the -{name}`ForwardPattern.dropPrefix?` function behaves like a function that drops the longest prefix +{name}`ForwardPattern.skipPrefix?` function behaves like a function that drops the longest prefix according to some notion of matching. -/ class LawfulForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where - dropPrefixOfNonempty?_eq {s : Slice} (h) : - ForwardPattern.dropPrefixOfNonempty? pat s h = ForwardPattern.dropPrefix? pat s + skipPrefixOfNonempty?_eq {s : Slice} (h) : + ForwardPattern.skipPrefixOfNonempty? pat s h = ForwardPattern.skipPrefix? pat s startsWith_eq (s : Slice) : - ForwardPattern.startsWith pat s = (ForwardPattern.dropPrefix? pat s).isSome + ForwardPattern.startsWith pat s = (ForwardPattern.skipPrefix? pat s).isSome /-- A strict forward pattern is one which never drops an empty prefix. @@ -144,7 +148,7 @@ iterator. -/ class StrictForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where ne_startPos {s : Slice} (h) (q) : - ForwardPattern.dropPrefixOfNonempty? pat s h = some q → q ≠ s.startPos + ForwardPattern.skipPrefixOfNonempty? pat s h = some q → q ≠ s.startPos /-- Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches @@ -188,11 +192,11 @@ instance (s : Slice) [ForwardPattern pat] : Std.Iterator (DefaultForwardSearcher pat s) Id (SearchStep s) where IsPlausibleStep it | .yield it' (.rejected p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos), - ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = none ∧ + ForwardPattern.skipPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = none ∧ p₁ = it.internalState.currPos ∧ p₂ = it.internalState.currPos.next h ∧ it'.internalState.currPos = it.internalState.currPos.next h | .yield it' (.matched p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos), ∃ pos, - ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = some pos ∧ + ForwardPattern.skipPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = some pos ∧ p₁ = it.internalState.currPos ∧ p₂ = Slice.Pos.ofSliceFrom pos ∧ it'.internalState.currPos = Slice.Pos.ofSliceFrom pos | .done => it.internalState.currPos = s.endPos @@ -201,7 +205,7 @@ instance (s : Slice) [ForwardPattern pat] : if h : it.internalState.currPos = s.endPos then pure (.deflate ⟨.done, by simp [h]⟩) else - match h' : ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) with + match h' : ForwardPattern.skipPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) with | some pos => pure (.deflate ⟨.yield ⟨⟨Slice.Pos.ofSliceFrom pos⟩⟩ (.matched it.internalState.currPos (Slice.Pos.ofSliceFrom pos)), by simp [h, h']⟩) diff --git a/src/Init/Data/String/Pattern/Char.lean b/src/Init/Data/String/Pattern/Char.lean index 577010468f..26eee1ab2e 100644 --- a/src/Init/Data/String/Pattern/Char.lean +++ b/src/Init/Data/String/Pattern/Char.lean @@ -21,15 +21,15 @@ namespace String.Slice.Pattern namespace Char instance {c : Char} : ForwardPattern c where - dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (· == c) s h - dropPrefix? s := ForwardPattern.dropPrefix? (· == c) s + skipPrefixOfNonempty? s h := ForwardPattern.skipPrefixOfNonempty? (· == c) s h + skipPrefix? s := ForwardPattern.skipPrefix? (· == c) s startsWith s := ForwardPattern.startsWith (· == c) s instance {c : Char} : StrictForwardPattern c where ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (· == c)) h q instance {c : Char} : LawfulForwardPattern c where - dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (· == c)) h + skipPrefixOfNonempty?_eq h := LawfulForwardPattern.skipPrefixOfNonempty?_eq (pat := (· == c)) h startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (· == c)) s instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher (· == c)) where diff --git a/src/Init/Data/String/Pattern/Pred.lean b/src/Init/Data/String/Pattern/Pred.lean index 2ce425d7e8..f16d1764b8 100644 --- a/src/Init/Data/String/Pattern/Pred.lean +++ b/src/Init/Data/String/Pattern/Pred.lean @@ -30,12 +30,12 @@ namespace CharPred @[default_instance] instance {p : Char → Bool} : ForwardPattern p where - dropPrefixOfNonempty? s h := + skipPrefixOfNonempty? s h := if p (s.startPos.get (Slice.startPos_ne_endPos h)) then some (s.startPos.next (Slice.startPos_ne_endPos h)) else none - dropPrefix? s := + skipPrefix? s := if h : s.startPos = s.endPos then none else if p (s.startPos.get h) then @@ -50,17 +50,17 @@ instance {p : Char → Bool} : ForwardPattern p where instance {p : Char → Bool} : StrictForwardPattern p where ne_startPos {s h q} := by - simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some, + simp only [ForwardPattern.skipPrefixOfNonempty?, Option.ite_none_right_eq_some, Option.some.injEq, ne_eq, and_imp] rintro _ rfl simp instance {p : Char → Bool} : LawfulForwardPattern p where - dropPrefixOfNonempty?_eq {s} h := by - simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?, + skipPrefixOfNonempty?_eq {s} h := by + simp [ForwardPattern.skipPrefixOfNonempty?, ForwardPattern.skipPrefix?, Slice.startPos_eq_endPos_iff, h] startsWith_eq s := by - simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?] + simp only [ForwardPattern.startsWith, ForwardPattern.skipPrefix?] split <;> (try split) <;> simp_all @[default_instance] @@ -70,15 +70,15 @@ instance {p : Char → Bool} : ToForwardSearcher p (ToForwardSearcher.DefaultFor namespace Decidable instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p where - dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (decide <| p ·) s h - dropPrefix? s := ForwardPattern.dropPrefix? (decide <| p ·) s + skipPrefixOfNonempty? s h := ForwardPattern.skipPrefixOfNonempty? (decide <| p ·) s h + skipPrefix? s := ForwardPattern.skipPrefix? (decide <| p ·) s startsWith s := ForwardPattern.startsWith (decide <| p ·) s instance {p : Char → Prop} [DecidablePred p] : StrictForwardPattern p where ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (decide <| p ·)) h q instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p where - dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (decide <| p ·)) h + skipPrefixOfNonempty?_eq h := LawfulForwardPattern.skipPrefixOfNonempty?_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 (decide <| p ·)) where diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean index f1909c25be..942472d8af 100644 --- a/src/Init/Data/String/Pattern/String.lean +++ b/src/Init/Data/String/Pattern/String.lean @@ -280,7 +280,7 @@ def startsWith (pat : Slice) (s : Slice) : Bool := false @[inline] -def dropPrefix? (pat : Slice) (s : Slice) : Option s.Pos := +def skipPrefix? (pat : Slice) (s : Slice) : Option s.Pos := if startsWith pat s then some <| s.pos! <| pat.rawEndPos.offsetBy s.startPos.offset else @@ -288,14 +288,14 @@ def dropPrefix? (pat : Slice) (s : Slice) : Option s.Pos := instance {pat : Slice} : ForwardPattern pat where startsWith := startsWith pat - dropPrefix? := dropPrefix? pat + skipPrefix? := skipPrefix? pat instance {pat : String} : ToForwardSearcher pat ForwardSliceSearcher where toSearcher := iter pat.toSlice instance {pat : String} : ForwardPattern pat where startsWith := startsWith pat.toSlice - dropPrefix? := dropPrefix? pat.toSlice + skipPrefix? := skipPrefix? pat.toSlice end ForwardSliceSearcher diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index 3170a59b57..aa2c5d4855 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -344,7 +344,7 @@ Examples: -/ @[inline] def dropPrefix? (s : Slice) (pat : ρ) [ForwardPattern pat] : Option Slice := - (ForwardPattern.dropPrefix? pat s).map s.sliceFrom + (ForwardPattern.skipPrefix? pat s).map s.sliceFrom /-- If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`s` unmodified @@ -416,7 +416,7 @@ def dropWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice := where @[specialize pat] go (curr : s.Pos) : Slice := - if let some nextCurr := ForwardPattern.dropPrefix? pat (s.sliceFrom curr) then + if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom curr) then if curr < Pos.ofSliceFrom nextCurr then go (Pos.ofSliceFrom nextCurr) else @@ -476,7 +476,7 @@ def takeWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice := where @[specialize pat] go (curr : s.Pos) : Slice := - if let some nextCurr := ForwardPattern.dropPrefix? pat (s.sliceFrom curr) then + if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom curr) then if curr < Pos.ofSliceFrom nextCurr then go (Pos.ofSliceFrom nextCurr) else diff --git a/src/Std/Data/String/ToNat.lean b/src/Std/Data/String/ToNat.lean index 9b112c7216..2b2b035e21 100644 --- a/src/Std/Data/String/ToNat.lean +++ b/src/Std/Data/String/ToNat.lean @@ -50,7 +50,6 @@ theorem NoRepetition.not_isSuffix_of_append_singleton {α : Type u} {a : α} {l theorem NoRepetition.append_singleton_of_not_suffix {α : Type u} {a : α} {l : List α} (h : NoRepetition a l) (h' : ¬ [a] <:+ l) : NoRepetition a (l ++ [a]) := by simp only [noRepetition_iff, List.infix_concat_iff, not_or] at ⊢ h - exact ⟨by rwa [← List.singleton_append, List.suffix_append_self_iff], h⟩ theorem NoRepetition.append_singleton_of_ne {α : Type u} {a b : α} {l : List α}