diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index a85ef8747d..c2a8c99946 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1978,6 +1978,7 @@ theorem Pos.ne_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ q := by theorem Pos.lt_of_lt_of_le {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by simpa [Pos.lt_iff, Pos.le_iff] using Pos.Raw.lt_of_lt_of_le +@[simp] theorem Pos.le_endPos {s : String} (p : s.Pos) : p ≤ s.endPos := by simpa [Pos.le_iff] using p.isValid.le_rawEndPos diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean index d028b82c13..578e2ad156 100644 --- a/src/Init/Data/String/Lemmas/Iterate.lean +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -16,6 +16,9 @@ import Init.ByCases import Init.Data.Iterators.Lemmas.Combinators.FilterMap import Init.Data.String.Lemmas.Basic import Init.Data.Iterators.Lemmas.Consumers.Loop +public import Init.Data.String.Lemmas.Order +import Init.Data.String.OrderInstances +import Init.Data.Subtype.Basic set_option doc.verso true @@ -47,6 +50,19 @@ theorem Model.positionsFrom_eq_cons {s : Slice} {p : s.Pos} (hp : p ≠ s.endPos rw [Model.positionsFrom] simp [hp] +@[simp] +theorem Model.mem_positionsFrom {s : Slice} {p : s.Pos} {q : { q : s.Pos // q ≠ s.endPos } } : + q ∈ Model.positionsFrom p ↔ p ≤ q := by + induction p using Pos.next_induction with + | next p h ih => + rw [Model.positionsFrom_eq_cons h, List.mem_cons, ih] + simp [Subtype.ext_iff, Std.le_iff_lt_or_eq (a := p), or_comm, eq_comm] + | endPos => simp [q.property] + +theorem Model.mem_positionsFrom_startPos {s : Slice} {q : { q : s.Pos // q ≠ s.endPos} } : + q ∈ Model.positionsFrom s.startPos := by + simp + theorem Model.map_get_positionsFrom_of_splits {s : Slice} {p : s.Pos} {t₁ t₂ : String} (hp : p.Splits t₁ t₂) : (Model.positionsFrom p).map (fun p => p.1.get p.2) = t₂.toList := by induction p using Pos.next_induction generalizing t₁ t₂ with @@ -60,7 +76,6 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} : (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList := Model.map_get_positionsFrom_of_splits (splits_startPos s) -set_option backward.isDefEq.respectTransparency false in @[simp] theorem toList_positionsFrom {s : Slice} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p := by @@ -80,6 +95,38 @@ theorem toList_positions {s : Slice} : s.positions.toList = Model.positionsFrom theorem toList_chars {s : Slice} : s.chars.toList = s.copy.toList := by simp [chars, Model.map_get_positionsFrom_startPos] +theorem mem_toList_copy_iff_exists_get {s : Slice} {c : Char} : + c ∈ s.copy.toList ↔ ∃ (p : s.Pos) (h : p ≠ s.endPos), p.get h = c := by + simp [← Model.map_get_positionsFrom_startPos] + +theorem Pos.Splits.mem_toList_left_iff {s : Slice} {pos : s.Pos} {t u : String} {c : Char} + (hs : pos.Splits t u) : + c ∈ t.toList ↔ ∃ pos', ∃ (h : pos' < pos), pos'.get (Pos.ne_endPos_of_lt h) = c := by + rw [hs.eq_left pos.splits, mem_toList_copy_iff_exists_get] + refine ⟨?_, ?_⟩ + · rintro ⟨p, hp, hpget⟩ + have hlt : Pos.ofSliceTo p < pos := by + simpa using Pos.ofSliceTo_lt_ofSliceTo_iff.mpr ((Pos.lt_endPos_iff _).mpr hp) + exact ⟨_, hlt, by rwa [Pos.get_eq_get_ofSliceTo] at hpget⟩ + · rintro ⟨pos', hlt, hget⟩ + exact ⟨pos.sliceTo pos' (Std.le_of_lt hlt), + by simpa [← Pos.ofSliceTo_inj] using Std.ne_of_lt hlt, + by rw [Slice.Pos.get_eq_get_ofSliceTo]; simpa using hget⟩ + +theorem Pos.Splits.mem_toList_right_iff {s : Slice} {pos : s.Pos} {t u : String} {c : Char} + (hs : pos.Splits t u) : + c ∈ u.toList ↔ ∃ pos', ∃ (_ : pos ≤ pos') (h : pos' ≠ s.endPos), pos'.get h = c := by + rw [hs.eq_right pos.splits, mem_toList_copy_iff_exists_get] + refine ⟨?_, ?_⟩ + · rintro ⟨p, hp, hpget⟩ + exact ⟨Pos.ofSliceFrom p, Pos.le_ofSliceFrom, + fun h => hp (Pos.ofSliceFrom_inj.mp (h.trans (Pos.ofSliceFrom_endPos (pos := pos)).symm)), + by rwa [Pos.get_eq_get_ofSliceFrom] at hpget⟩ + · rintro ⟨pos', hle, hne, hget⟩ + exact ⟨pos.sliceFrom pos' hle, + fun h => hne (by simpa using congrArg Pos.ofSliceFrom h), + by rw [Pos.get_eq_get_ofSliceFrom]; simpa using hget⟩ + /-- A list of all positions strictly before {name}`p`, ordered from largest to smallest. @@ -115,7 +162,6 @@ theorem Model.map_get_revPositionsFrom_endPos {s : Slice} : (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.copy.toList.reverse := Model.map_get_revPositionsFrom_of_splits (splits_endPos s) -set_option backward.isDefEq.respectTransparency false in @[simp] theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} : (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by @@ -168,6 +214,19 @@ theorem Model.positionsFrom_eq_cons {s : String} {p : s.Pos} (hp : p ≠ s.endPo rw [Model.positionsFrom] simp [hp] +@[simp] +theorem Model.mem_positionsFrom {s : String} {p : s.Pos} {q : { q : s.Pos // q ≠ s.endPos } } : + q ∈ Model.positionsFrom p ↔ p ≤ q := by + induction p using Pos.next_induction with + | next p h ih => + rw [Model.positionsFrom_eq_cons h, List.mem_cons, ih] + simp [Subtype.ext_iff, Std.le_iff_lt_or_eq (a := p), or_comm, eq_comm] + | endPos => simp [q.property] + +theorem Model.mem_positionsFrom_startPos {s : String} {q : { q : s.Pos // q ≠ s.endPos} } : + q ∈ Model.positionsFrom s.startPos := by + simp + theorem Model.positionsFrom_eq_map {s : String} {p : s.Pos} : Model.positionsFrom p = (Slice.Model.positionsFrom p.toSlice).map (fun p => ⟨Pos.ofToSlice p.1, by simpa [← Pos.toSlice_inj] using p.2⟩) := by @@ -199,6 +258,38 @@ theorem toList_positions {s : String} : s.positions.toList = Model.positionsFrom theorem toList_chars {s : String} : s.chars.toList = s.toList := by simp [chars] +theorem mem_toList_iff_exists_get {s : String} {c : Char} : + c ∈ s.toList ↔ ∃ (p : s.Pos) (h : p ≠ s.endPos), p.get h = c := by + simp [← Model.map_get_positionsFrom_startPos] + +theorem Pos.Splits.mem_toList_left_iff {s : String} {pos : s.Pos} {t u : String} {c : Char} + (hs : pos.Splits t u) : + c ∈ t.toList ↔ ∃ pos', ∃ (h : pos' < pos), pos'.get (Pos.ne_endPos_of_lt h) = c := by + rw [hs.eq_left pos.splits, Slice.mem_toList_copy_iff_exists_get] + refine ⟨?_, ?_⟩ + · rintro ⟨p, hp, hpget⟩ + have hlt : Pos.ofSliceTo p < pos := by + simpa using Pos.ofSliceTo_lt_ofSliceTo_iff.mpr ((Slice.Pos.lt_endPos_iff _).mpr hp) + exact ⟨_, hlt, by rwa [Pos.get_eq_get_ofSliceTo] at hpget⟩ + · rintro ⟨pos', hlt, hget⟩ + exact ⟨pos.sliceTo pos' (Std.le_of_lt hlt), + fun h => Std.ne_of_lt hlt (by simpa using congrArg Pos.ofSliceTo h), + by rw [Pos.get_eq_get_ofSliceTo]; simpa using hget⟩ + +theorem Pos.Splits.mem_toList_right_iff {s : String} {pos : s.Pos} {t u : String} {c : Char} + (hs : pos.Splits t u) : + c ∈ u.toList ↔ ∃ pos', ∃ (_ : pos ≤ pos') (h : pos' ≠ s.endPos), pos'.get h = c := by + rw [hs.eq_right pos.splits, Slice.mem_toList_copy_iff_exists_get] + refine ⟨?_, ?_⟩ + · rintro ⟨p, hp, hpget⟩ + exact ⟨Pos.ofSliceFrom p, Pos.le_ofSliceFrom, + fun h => hp (Pos.ofSliceFrom_inj.mp (h.trans Pos.ofSliceFrom_endPos.symm)), + by rwa [Pos.get_eq_get_ofSliceFrom] at hpget⟩ + · rintro ⟨pos', hle, hne, hget⟩ + exact ⟨pos.sliceFrom pos' hle, + fun h => hne (by simpa using congrArg Pos.ofSliceFrom h), + by rw [Pos.get_eq_get_ofSliceFrom]; simpa using hget⟩ + /-- A list of all positions strictly before {name}`p`, ordered from largest to smallest. diff --git a/src/Init/Data/String/Lemmas/Order.lean b/src/Init/Data/String/Lemmas/Order.lean index dbccd68810..f4a050b68e 100644 --- a/src/Init/Data/String/Lemmas/Order.lean +++ b/src/Init/Data/String/Lemmas/Order.lean @@ -290,6 +290,70 @@ theorem Pos.ofSliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).P Pos.ofSliceTo p ≤ q ↔ ∀ h, p ≤ Pos.sliceTo p₀ q h := by simp [← Std.not_lt, Pos.lt_ofSliceTo_iff] +theorem Slice.Pos.lt_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + p < Slice.Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p < q := by + simp [ofSliceFrom_lt_iff, h] + +theorem Slice.Pos.sliceFrom_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + Slice.Pos.sliceFrom p₀ q h ≤ p ↔ q ≤ Pos.ofSliceFrom p := by + simp [← Std.not_lt, lt_sliceFrom_iff] + +theorem Slice.Pos.le_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + p ≤ Slice.Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p ≤ q := by + simp [ofSliceFrom_le_iff, h] + +theorem Slice.Pos.sliceFrom_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + Slice.Pos.sliceFrom p₀ q h < p ↔ q < Pos.ofSliceFrom p := by + simp [← Std.not_le, le_sliceFrom_iff] + +theorem Pos.lt_sliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + p < Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p < q := by + simp [ofSliceFrom_lt_iff, h] + +theorem Pos.sliceFrom_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + Pos.sliceFrom p₀ q h ≤ p ↔ q ≤ Pos.ofSliceFrom p := by + simp [← Std.not_lt, lt_sliceFrom_iff] + +theorem Pos.le_sliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + p ≤ Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p ≤ q := by + simp [ofSliceFrom_le_iff, h] + +theorem Pos.sliceFrom_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} : + Pos.sliceFrom p₀ q h < p ↔ q < Pos.ofSliceFrom p := by + simp [← Std.not_le, le_sliceFrom_iff] + +theorem Slice.Pos.sliceTo_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + Pos.sliceTo p₀ q h ≤ p ↔ q ≤ Pos.ofSliceTo p := by + simp [le_ofSliceTo_iff, h] + +theorem Slice.Pos.lt_sliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + p < Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p < q := by + simp [← Std.not_le, sliceTo_le_iff] + +theorem Slice.Pos.sliceTo_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + Slice.Pos.sliceTo p₀ q h < p ↔ q < Pos.ofSliceTo p := by + simp [lt_ofSliceTo_iff, h] + +theorem Slice.Pos.le_sliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + p ≤ Slice.Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p ≤ q := by + simp [← Std.not_lt, sliceTo_lt_iff] + +theorem Pos.sliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + Pos.sliceTo p₀ q h ≤ p ↔ q ≤ Pos.ofSliceTo p := by + simp [le_ofSliceTo_iff, h] + +theorem Pos.lt_sliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + p < Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p < q := by + simp [← Std.not_le, sliceTo_le_iff] + +theorem Pos.sliceTo_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + Pos.sliceTo p₀ q h < p ↔ q < Pos.ofSliceTo p := by + simp [lt_ofSliceTo_iff, h] + +theorem Pos.le_sliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} : + p ≤ Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p ≤ q := by + simp [← Std.not_lt, sliceTo_lt_iff] + theorem Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} (h : p ≠ (s.sliceTo p₀).endPos) : Pos.ofSliceTo p ≠ s.endPos := by refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀)) diff --git a/src/Init/Data/String/Lemmas/Pattern.lean b/src/Init/Data/String/Lemmas/Pattern.lean index c828ee10d3..bba764c2f6 100644 --- a/src/Init/Data/String/Lemmas/Pattern.lean +++ b/src/Init/Data/String/Lemmas/Pattern.lean @@ -12,3 +12,4 @@ public import Init.Data.String.Lemmas.Pattern.Pred public import Init.Data.String.Lemmas.Pattern.Char public import Init.Data.String.Lemmas.Pattern.String public import Init.Data.String.Lemmas.Pattern.Split +public import Init.Data.String.Lemmas.Pattern.Find diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean index e1dda18d85..37338e54a1 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean @@ -12,6 +12,7 @@ public import Init.Data.Iterators.Consumers.Collect import all Init.Data.String.Pattern.Basic import Init.Data.String.OrderInstances import Init.Data.String.Lemmas.IsEmpty +import Init.Data.String.Lemmas.Basic import Init.Data.String.Lemmas.Order import Init.Data.String.Termination import Init.Data.Order.Lemmas @@ -168,6 +169,24 @@ theorem IsLongestMatchAt.eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} {st endPos = endPos' := by simpa using h.isLongestMatch_sliceFrom.eq h'.isLongestMatch_sliceFrom +private theorem isLongestMatch_of_eq {pat : ρ} [ForwardPatternModel pat] {s t : Slice} + {pos : s.Pos} {pos' : t.Pos} (h_eq : s = t) (h_pos : pos.offset = pos'.offset) + (hm : IsLongestMatch pat pos) : IsLongestMatch pat pos' := by + subst h_eq; exact (Slice.Pos.ext h_pos) ▸ hm + +theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] + {s : Slice} {base : s.Pos} {startPos endPos : (s.sliceFrom base).Pos} : + IsLongestMatchAt pat startPos endPos ↔ IsLongestMatchAt pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos) := by + constructor + · intro h + refine ⟨Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff.mpr h.le, ?_⟩ + exact isLongestMatch_of_eq Slice.sliceFrom_sliceFrom + (by simp [Pos.Raw.ext_iff]; omega) h.isLongestMatch_sliceFrom + · intro h + refine ⟨Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff.mp h.le, ?_⟩ + exact isLongestMatch_of_eq Slice.sliceFrom_sliceFrom.symm + (by simp [Pos.Raw.ext_iff]; omega) h.isLongestMatch_sliceFrom + theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} (h : IsLongestMatch pat pos) : IsLongestMatchAt pat p₀ (Slice.Pos.ofSliceFrom pos) where @@ -198,6 +217,27 @@ theorem matchesAt_iff_exists_isMatch {pat : ρ} [ForwardPatternModel pat] {s : S ⟨Std.le_trans h₁ (by simpa [← Pos.ofSliceFrom_le_ofSliceFrom_iff] using hq.le_of_isMatch h₂), by simpa using hq⟩⟩ +@[simp] +theorem not_matchesAt_endPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} : + ¬ MatchesAt pat s.endPos := by + simp only [matchesAt_iff_exists_isMatch, Pos.endPos_le, exists_prop_eq] + intro h + simpa [← Pos.ofSliceFrom_inj] using h.ne_startPos + +theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] {s : Slice} {base : s.Pos} + {pos : (s.sliceFrom base).Pos} : MatchesAt pat pos ↔ MatchesAt pat (Pos.ofSliceFrom pos) := by + simp only [matchesAt_iff_exists_isLongestMatchAt] + constructor + · rintro ⟨endPos, h⟩ + exact ⟨Pos.ofSliceFrom endPos, isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom.mp h⟩ + · rintro ⟨endPos, h⟩ + exact ⟨base.sliceFrom endPos (Std.le_trans Slice.Pos.le_ofSliceFrom h.le), + isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom.mpr (by simpa using h)⟩ + +theorem IsLongestMatchAt.matchesAt {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos} + (h : IsLongestMatchAt pat startPos endPos) : MatchesAt pat startPos where + exists_isLongestMatchAt := ⟨_, h⟩ + open Classical in /-- Noncomputable model function returning the end point of the longest match starting at the given diff --git a/src/Init/Data/String/Lemmas/Pattern/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Char.lean index 20c126ca78..6bb7a39cc1 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Char.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Char.lean @@ -61,6 +61,16 @@ theorem matchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} : MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c := by simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff, exists_comm] +theorem matchesAt_iff_splits {c : Char} {s : Slice} {pos : s.Pos} : + MatchesAt c pos ↔ ∃ t₁ t₂, pos.Splits t₁ (singleton c ++ t₂) := by + rw [matchesAt_iff] + refine ⟨?_, ?_⟩ + · rintro ⟨h, rfl⟩ + exact ⟨_, _, pos.splits_next_right h⟩ + · rintro ⟨t₁, t₂, hs⟩ + have hne := hs.ne_endPos_of_singleton + exact ⟨hne, (singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm⟩ + theorem not_matchesAt_of_get_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} (hc : pos.get h ≠ c) : ¬ MatchesAt c pos := by simp [matchesAt_iff, hc] diff --git a/src/Init/Data/String/Lemmas/Pattern/Find.lean b/src/Init/Data/String/Lemmas/Pattern/Find.lean new file mode 100644 index 0000000000..085060f353 --- /dev/null +++ b/src/Init/Data/String/Lemmas/Pattern/Find.lean @@ -0,0 +1,11 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Lemmas.Pattern.Find.Basic +public import Init.Data.String.Lemmas.Pattern.Find.Char +public import Init.Data.String.Lemmas.Pattern.Find.Pred diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Basic.lean new file mode 100644 index 0000000000..0df4b1df2e --- /dev/null +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Basic.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Slice +public import Init.Data.String.Search +public import Init.Data.String.Lemmas.Pattern.Basic +import all Init.Data.String.Slice +import all Init.Data.String.Search +import Init.Data.Iterators.Lemmas.Consumers.Loop +import Init.Data.String.Lemmas.Order +import Init.Data.String.Lemmas.Basic +import Init.Data.String.OrderInstances +import Init.Grind + +public section + +open Std String.Slice Pattern Pattern.Model + +namespace String.Slice + +theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} : + s.find? pat = some pos ↔ MatchesAt pat pos ∧ (∀ pos', pos' < pos → ¬ MatchesAt pat pos') := by + rw [find?, ← Iter.findSome?_toList] + suffices ∀ (l : List (SearchStep s)) (pos : s.Pos) (hl : IsValidSearchFrom pat pos l) (pos' : s.Pos), + l.findSome? (fun | .matched s _ => some s | .rejected .. => none) = some pos' ↔ + pos ≤ pos' ∧ MatchesAt pat pos' ∧ ∀ pos'', pos ≤ pos'' → pos'' < pos' → ¬ MatchesAt pat pos'' by + simpa using this (ToForwardSearcher.toSearcher pat s).toList s.startPos + (LawfulToForwardSearcherModel.isValidSearchFrom_toList s) pos + intro l pos hl pos' + induction hl with + | endPos => simp +contextual + | matched h₁ _ _ => have := h₁.matchesAt; grind + | mismatched => grind + +theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} : + s.find? pat = none ↔ ∀ (pos : s.Pos), ¬ MatchesAt pat pos := by + simp only [Option.eq_none_iff_forall_ne_some, ne_eq, find?_eq_some_iff, not_and, + Classical.not_forall, Classical.not_not] + refine ⟨fun _ pos => ?_, by grind⟩ + induction pos using WellFounded.induction Pos.wellFounded_lt with grind + +@[simp] +theorem isSome_find? {ρ : Type} (pat : ρ) {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] {s : Slice} : (s.find? pat).isSome = s.contains pat := by + rw [find?, contains, ← Iter.findSome?_toList, ← Iter.any_toList] + induction (ToForwardSearcher.toSearcher pat s).toList <;> grind + +@[simp] +theorem find?_eq_none_iff {ρ : Type} (pat : ρ) {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] {s : Slice} : s.find? pat = none ↔ s.contains pat = false := by + rw [← Option.isNone_iff_eq_none, ← Option.isSome_eq_false_iff, isSome_find?] + +theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} : + s.contains pat = false ↔ ∀ (pos : s.Pos), ¬ MatchesAt pat pos := by + rw [← find?_eq_none_iff, Slice.find?_eq_none_iff] + +theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} : + s.contains pat ↔ ∃ (pos : s.Pos), MatchesAt pat pos := by + simp [← Bool.not_eq_false, contains_eq_false_iff] + +theorem Pos.find?_eq_find?_sliceFrom {ρ : Type} {pat : ρ} {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] + {s : Slice} {p : s.Pos} : + p.find? pat = ((s.sliceFrom p).find? pat).map Pos.ofSliceFrom := + (rfl) + +theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos pos' : s.Pos} : + pos.find? pat = some pos' ↔ pos ≤ pos' ∧ MatchesAt pat pos' ∧ (∀ pos'', pos ≤ pos'' → pos'' < pos' → ¬ MatchesAt pat pos'') := by + simp only [Pos.find?_eq_find?_sliceFrom, Option.map_eq_some_iff, find?_eq_some_iff, + matchesAt_iff_matchesAt_ofSliceFrom] + refine ⟨?_, ?_⟩ + · rintro ⟨pos', ⟨h₁, h₂⟩, rfl⟩ + refine ⟨Pos.le_ofSliceFrom, h₁, fun p hp₁ hp₂ => ?_⟩ + simpa using h₂ (Pos.sliceFrom _ _ hp₁) (Pos.sliceFrom_lt_iff.2 hp₂) + · rintro ⟨h₁, h₂, h₃⟩ + refine ⟨Pos.sliceFrom _ _ h₁, ⟨by simpa using h₂, fun p hp₁ hp₂ => ?_⟩, by simp⟩ + exact h₃ (Pos.ofSliceFrom p) Slice.Pos.le_ofSliceFrom (Pos.lt_sliceFrom_iff.1 hp₁) hp₂ + +theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id] + [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id] + [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} : + pos.find? pat = none ↔ ∀ pos', pos ≤ pos' → ¬ MatchesAt pat pos' := by + rw [Pos.find?_eq_find?_sliceFrom, Option.map_eq_none_iff, Pattern.Model.find?_eq_none_iff] + simpa only [matchesAt_iff_matchesAt_ofSliceFrom] using ⟨fun h p hp => + by simpa using h (Pos.sliceFrom _ _ hp), fun h p => by simpa using h _ Pos.le_ofSliceFrom⟩ + +end Slice + +theorem Pos.find?_eq_find?_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] + {s : String} {p : s.Pos} : p.find? pat = (p.toSlice.find? pat).map Pos.ofToSlice := + (rfl) + +theorem find?_eq_find?_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] + {s : String} : s.find? pat = (s.toSlice.find? pat).map Pos.ofToSlice := + (rfl) + +theorem contains_eq_contains_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} + [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] + {s : String} : s.contains pat = s.toSlice.contains pat := + (rfl) + +end String diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean new file mode 100644 index 0000000000..9e80ce4992 --- /dev/null +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Slice +import Init.Data.String.Lemmas.Pattern.Find.Basic +import Init.Data.String.Lemmas.Pattern.Char +import Init.Data.String.Lemmas.Basic +import Init.Data.String.Lemmas.Order +import Init.Data.String.Termination +import Init.Data.String.Lemmas.Iterate +import Init.Grind +import Init.Data.Option.Lemmas +import Init.Data.String.OrderInstances + +namespace String.Slice + +theorem find?_char_eq_some_iff {c : Char} {s : Slice} {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 + grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.Char.matchesAt_iff] + +@[simp] +theorem contains_char_eq {c : Char} {s : Slice} : s.contains c = decide (c ∈ s.copy.toList) := by + rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff] + simp [Pattern.Model.Char.matchesAt_iff, mem_toList_copy_iff_exists_get] + +theorem find?_char_eq_some_iff_splits {c : Char} {s : Slice} {pos : s.Pos} : + s.find? c = some pos ↔ ∃ t u, pos.Splits t (singleton c ++ u) ∧ c ∉ t.toList := by + rw [find?_char_eq_some_iff] + refine ⟨?_, ?_⟩ + · rintro ⟨h, hget, hmin⟩ + refine ⟨_, _, hget ▸ pos.splits_next_right h, fun hmem => ?_⟩ + obtain ⟨pos', hlt, hpget⟩ := (hget ▸ pos.splits_next_right h).mem_toList_left_iff.mp hmem + exact absurd hpget (hmin _ hlt) + · rintro ⟨t, u, hs, hnotin⟩ + have hne := hs.ne_endPos_of_singleton + exact ⟨hne, (singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm, + fun pos' hlt hget => hnotin (hs.mem_toList_left_iff.mpr ⟨pos', hlt, hget⟩)⟩ + +theorem Pos.find?_char_eq_some_iff {c : Char} {s : Slice} {pos pos' : s.Pos} : + pos.find? c = some pos' ↔ + pos ≤ pos' ∧ (∃ h, pos'.get h = c) ∧ + ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (Pos.ne_endPos_of_lt h') ≠ c := by + grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.Char.matchesAt_iff] + +theorem Pos.find?_char_eq_some_iff_splits {c : Char} {s : Slice} {pos : s.Pos} + {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : + pos.find? c = some pos' ↔ ∃ v w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ c ∉ v.toList := by + rw [Pos.find?_char_eq_some_iff] + refine ⟨?_, ?_⟩ + · rintro ⟨hle, ⟨hne, hget⟩, hmin⟩ + have hsplit := hget ▸ pos'.splits_next_right hne + obtain ⟨v, hv1, hv2⟩ := (hs.le_iff_exists_eq_append hsplit).mp hle + refine ⟨v, _, hsplit.of_eq hv1 rfl, fun hmem => ?_⟩ + obtain ⟨_, hcopy⟩ := + Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hv2, hsplit.of_eq hv1 rfl⟩ + rw [← hcopy] at hmem + obtain ⟨p, hp, hpget⟩ := mem_toList_copy_iff_exists_get.mp hmem + have hlt : Pos.ofSlice p < pos' := by + simpa [← Slice.Pos.lt_endPos_iff, ← Pos.ofSlice_lt_ofSlice_iff] using hp + exact absurd (Pos.get_eq_get_ofSlice ▸ hpget) (hmin _ Pos.le_ofSlice hlt) + · rintro ⟨v, w, hsplit, hnotin⟩ + 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, (singleton_append_inj.mp (hsplit.eq_right (pos'.splits_next_right hne))).1.symm⟩, + fun pos'' hle' hlt hget => hnotin ?_⟩ + 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] + exact hget⟩ + +theorem Pos.find?_char_eq_none_iff {c : Char} {s : Slice} {pos : s.Pos} : + pos.find? c = none ↔ ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → pos'.get h ≠ c := by + grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.Char.matchesAt_iff] + +theorem Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : Slice} {pos : s.Pos} + {t u : String} (hs : pos.Splits t u) : + pos.find? c = none ↔ c ∉ u.toList := by + simp [Pos.find?_char_eq_none_iff, hs.mem_toList_right_iff] + +end Slice + +theorem Pos.find?_char_eq_some_iff {c : Char} {s : String} {pos pos' : s.Pos} : + pos.find? c = some pos' ↔ + pos ≤ pos' ∧ (∃ h, pos'.get h = c) ∧ + ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (Pos.ne_endPos_of_lt h') ≠ c := by + simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff, + Slice.Pos.find?_char_eq_some_iff, ne_eq, endPos_toSlice] + refine ⟨?_, ?_⟩ + · rintro ⟨pos', ⟨h₁, ⟨h₂, rfl⟩, h₃⟩, rfl⟩ + refine ⟨by simpa [Pos.ofToSlice_le_iff] using h₁, + ⟨by simpa [← Pos.ofToSlice_inj] using h₂, by simp [Pos.get_ofToSlice]⟩, ?_⟩ + intro pos'' h₄ h₅ + simpa using h₃ pos''.toSlice (by simpa [Pos.toSlice_le] using h₄) (by simpa using h₅) + · rintro ⟨h₁, ⟨h₂, hget⟩, h₃⟩ + refine ⟨pos'.toSlice, ⟨by simpa [Pos.toSlice_le] using h₁, + ⟨by simpa [← Pos.toSlice_inj] using h₂, by simpa using hget⟩, fun p hp₁ hp₂ => ?_⟩, + by simp⟩ + simpa using h₃ (Pos.ofToSlice p) + (by simpa [Pos.ofToSlice_le_iff] using hp₁) (by simpa using hp₂) + +theorem Pos.find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} + {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : + pos.find? c = some pos' ↔ ∃ v w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ c ∉ v.toList := by + simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff, + Slice.Pos.find?_char_eq_some_iff_splits (Pos.splits_toSlice_iff.mpr hs)] + constructor + · rintro ⟨q, ⟨v, w, hsplit, hnotin⟩, rfl⟩ + exact ⟨v, w, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hnotin⟩ + · rintro ⟨v, w, hsplit, hnotin⟩ + exact ⟨pos'.toSlice, ⟨v, w, Pos.splits_toSlice_iff.mpr hsplit, hnotin⟩, by simp⟩ + +theorem Pos.find?_char_eq_none_iff {c : Char} {s : String} {pos : s.Pos} : + pos.find? c = none ↔ ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → pos'.get h ≠ c := by + simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff, + Slice.Pos.find?_char_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₂) + +theorem Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : String} {pos : s.Pos} + {t u : String} (hs : pos.Splits t u) : + pos.find? c = none ↔ c ∉ u.toList := by + 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 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 + simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_char_eq_some_iff, ne_eq, + endPos_toSlice, exists_and_right] + refine ⟨?_, ?_⟩ + · rintro ⟨pos, ⟨⟨h, rfl⟩, h'⟩, rfl⟩ + refine ⟨⟨by simpa [← Pos.ofToSlice_inj] using h, by simp [Pos.get_ofToSlice]⟩, ?_⟩ + intro pos' hp + simpa using h' pos'.toSlice hp + · rintro ⟨⟨h, hget⟩, hmin⟩ + exact ⟨pos.toSlice, ⟨⟨by simpa [← Pos.toSlice_inj] using h, by simpa using hget⟩, + fun pos' hp => by simpa using hmin (Pos.ofToSlice pos') hp⟩, by simp⟩ + +theorem find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} : + s.find? c = some pos ↔ ∃ t u, pos.Splits t (singleton c ++ u) ∧ c ∉ t.toList := by + simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, + Slice.find?_char_eq_some_iff_splits] + constructor + · rintro ⟨q, ⟨t, u, hsplit, hnotin⟩, rfl⟩ + exact ⟨t, u, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hnotin⟩ + · rintro ⟨t, u, hsplit, hnotin⟩ + exact ⟨pos.toSlice, ⟨t, u, Pos.splits_toSlice_iff.mpr hsplit, hnotin⟩, by simp⟩ + +@[simp] +theorem contains_char_eq {c : Char} {s : String} : s.contains c = decide (c ∈ s.toList) := by + simp [contains_eq_contains_toSlice, Slice.contains_char_eq, copy_toSlice] + +end String diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean new file mode 100644 index 0000000000..d766da2f4f --- /dev/null +++ b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean @@ -0,0 +1,367 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.String.Slice +import Init.Data.String.Lemmas.Pattern.Find.Basic +import Init.Data.String.Lemmas.Pattern.Pred +import Init.Data.String.Lemmas.Basic +import Init.Data.String.Lemmas.Order +import Init.Data.String.Termination +import Init.Data.String.Lemmas.Iterate +import Init.Grind +import Init.Data.Option.Lemmas +import Init.Data.String.OrderInstances + +namespace String.Slice + +theorem find?_bool_eq_some_iff {p : Char → Bool} {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')) = false := by + grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.CharPred.matchesAt_iff] + +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] + +theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} : + s.find? p = some pos ↔ + ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, p d = false := by + rw [find?_bool_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 + +theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice} + {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] +theorem contains_bool_eq {p : Char → Bool} {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.matchesAt_iff, ne_eq, List.any_eq_true, + mem_toList_copy_iff_exists_get] + exact ⟨fun ⟨pos, h, hp⟩ => ⟨_, ⟨_, _, rfl⟩, hp⟩, fun ⟨_, ⟨p, h, h'⟩, hp⟩ => ⟨p, h, h' ▸ hp⟩⟩ + +@[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⟩⟩ + +theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} : + pos.find? p = some pos' ↔ + pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧ + ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → + p (pos''.get (Pos.ne_endPos_of_lt h')) = false := by + grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.CharPred.matchesAt_iff] + +theorem Pos.find?_bool_eq_some_iff_splits {p : Char → Bool} {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 = false := by + rw [Pos.find?_bool_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]⟩ + +theorem Pos.find?_bool_eq_none_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : + pos.find? p = none ↔ + ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → p (pos'.get h) = false := by + grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.CharPred.matchesAt_iff] + +theorem Pos.find?_bool_eq_none_iff_of_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} + {t u : String} (hs : pos.Splits t u) : + pos.find? p = none ↔ ∀ c ∈ u.toList, p c = false := by + rw [Pos.find?_bool_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⟩) + +theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice} + {pos pos' : s.Pos} : + pos.find? p = some pos' ↔ + 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] + +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]⟩ + +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] + +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⟩) + +end String.Slice + +namespace String + +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)) ∧ + ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → + p (pos''.get (Pos.ne_endPos_of_lt h')) = false := by + simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff, + Slice.Pos.find?_bool_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₂) + +theorem Pos.find?_bool_eq_some_iff_splits {p : Char → Bool} {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 = false := by + simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff, + Slice.Pos.find?_bool_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⟩ + +theorem Pos.find?_bool_eq_none_iff {p : Char → Bool} {s : String} {pos : s.Pos} : + pos.find? p = none ↔ + ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → p (pos'.get h) = false := by + simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff, + Slice.Pos.find?_bool_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₂) + +theorem Pos.find?_bool_eq_none_iff_of_splits {p : Char → Bool} {s : String} {pos : s.Pos} + {t u : String} (hs : pos.Splits t u) : + pos.find? p = none ↔ ∀ c ∈ u.toList, p c = false := by + rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff] + exact Slice.Pos.find?_bool_eq_none_iff_of_splits (Pos.splits_toSlice_iff.mpr hs) + +theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} + {pos pos' : s.Pos} : + pos.find? p = some pos' ↔ + 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₂) + +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⟩ + +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₂) + +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) + +theorem find?_bool_eq_some_iff {p : Char → Bool} {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')) = false := by + simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_bool_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⟩ + +theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {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 = false := by + simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, + Slice.find?_bool_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⟩ + +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⟩ + +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] +theorem contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toList.any p := by + simp [contains_eq_contains_toSlice, Slice.contains_bool_eq, copy_toSlice] + +@[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] + +end String diff --git a/src/Init/Data/String/Search.lean b/src/Init/Data/String/Search.lean index b8c984aa3c..b7a4826846 100644 --- a/src/Init/Data/String/Search.lean +++ b/src/Init/Data/String/Search.lean @@ -125,7 +125,7 @@ Examples: -/ @[inline] def find? (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.Pos := - s.startPos.find? pattern + (s.toSlice.find? pattern).map Pos.ofToSlice /-- Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s`. If there @@ -140,7 +140,7 @@ Examples: -/ @[inline] def find (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : s.Pos := - s.startPos.find pattern + Pos.ofToSlice (s.toSlice.find pattern) /-- Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s` that is @@ -189,7 +189,7 @@ Examples: -/ @[inline] def revFind? (s : String) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.Pos := - s.endPos.revFind? pattern + (s.toSlice.revFind? pattern).map Pos.ofToSlice @[export lean_string_posof] def Internal.posOfImpl (s : String) (c : Char) : Pos.Raw := diff --git a/tests/lean/interactive/compNamespace.lean b/tests/lean/interactive/compNamespace.lean index 039cc1242c..e957dcfbe5 100644 --- a/tests/lean/interactive/compNamespace.lean +++ b/tests/lean/interactive/compNamespace.lean @@ -3,12 +3,12 @@ namespace LongNamespaceExample def x := 10 -#check LongNam - --^ completion +#check LongName + --^ completion end LongNamespaceExample -#check LongNam - --^ completion +#check LongName + --^ completion end Foo #check Foo. @@ -18,5 +18,5 @@ end Foo --^ completion open Foo -#check LongNam - --^ completion +#check LongName + --^ completion diff --git a/tests/lean/interactive/compNamespace.lean.expected.out b/tests/lean/interactive/compNamespace.lean.expected.out index 9179e00d19..ee4ff48dc4 100644 --- a/tests/lean/interactive/compNamespace.lean.expected.out +++ b/tests/lean/interactive/compNamespace.lean.expected.out @@ -1,29 +1,29 @@ {"textDocument": {"uri": "file:///compNamespace.lean"}, - "position": {"line": 5, "character": 14}} + "position": {"line": 5, "character": 15}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", - "data": ["file:///compNamespace.lean", 5, 14, 0]}], + "data": ["file:///compNamespace.lean", 5, 15, 0]}], "isIncomplete": false} Resolution of LongNamespaceExample: {"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", - "data": ["file:///compNamespace.lean", 5, 14, 0]} + "data": ["file:///compNamespace.lean", 5, 15, 0]} {"textDocument": {"uri": "file:///compNamespace.lean"}, - "position": {"line": 9, "character": 14}} + "position": {"line": 9, "character": 15}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", - "data": ["file:///compNamespace.lean", 9, 14, 0]}], + "data": ["file:///compNamespace.lean", 9, 15, 0]}], "isIncomplete": false} Resolution of LongNamespaceExample: {"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", - "data": ["file:///compNamespace.lean", 9, 14, 0]} + "data": ["file:///compNamespace.lean", 9, 15, 0]} {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 13, "character": 11}} {"items": @@ -51,15 +51,15 @@ Resolution of LongNamespaceExample: "detail": "namespace", "data": ["file:///compNamespace.lean", 16, 16, 0]} {"textDocument": {"uri": "file:///compNamespace.lean"}, - "position": {"line": 20, "character": 14}} + "position": {"line": 20, "character": 15}} {"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", - "data": ["file:///compNamespace.lean", 20, 14, 0]}], + "data": ["file:///compNamespace.lean", 20, 15, 0]}], "isIncomplete": false} Resolution of LongNamespaceExample: {"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", - "data": ["file:///compNamespace.lean", 20, 14, 0]} + "data": ["file:///compNamespace.lean", 20, 15, 0]}