diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 8f69de4f2e..23fc40da7d 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -827,12 +827,16 @@ def Slice.copy (s : Slice) : String := theorem Slice.toByteArray_copy {s : Slice} : s.copy.toByteArray = s.str.toByteArray.extract s.startInclusive.offset.byteIdx s.endExclusive.offset.byteIdx := (rfl) -@[simp] -theorem Slice.utf8ByteSize_copy {s : Slice} : +theorem Slice.utf8ByteSize_copy_eq_sub {s : Slice} : s.copy.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx:= by simp [← size_toByteArray, toByteArray_copy] rw [Nat.min_eq_left (by simpa [Pos.Raw.le_iff] using s.endExclusive.isValid.le_rawEndPos)] +@[simp] +theorem Slice.utf8ByteSize_copy {s : Slice} : + s.copy.utf8ByteSize = s.utf8ByteSize := by + rw [utf8ByteSize_copy_eq_sub, utf8ByteSize_eq] + @[simp] theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by simp [Pos.Raw.ext_iff, utf8ByteSize_eq] @@ -1461,6 +1465,12 @@ def Slice.Pos.toReplaceStart {s : Slice} (p₀ : s.Pos) (pos : s.Pos) (h : p₀ theorem Slice.Pos.offset_sliceFrom {s : Slice} {p₀ : s.Pos} {pos : s.Pos} {h} : (sliceFrom p₀ pos h).offset = pos.offset.unoffsetBy p₀.offset := (rfl) +@[simp] +theorem Slice.Pos.sliceFrom_inj {s : Slice} {p₀ : s.Pos} {pos pos' : s.Pos} {h h'} : + p₀.sliceFrom pos h = p₀.sliceFrom pos' h' ↔ pos = pos' := by + simp [Pos.ext_iff, Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h h' + omega + @[simp] theorem Slice.Pos.ofSliceFrom_startPos {s : Slice} {pos : s.Pos} : ofSliceFrom (s.sliceFrom pos).startPos = pos := @@ -1678,6 +1688,11 @@ position is not the past-the-end position, which guarantees that such a position def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos := ofToSlice (Slice.Pos.next pos.toSlice (ne_of_apply_ne Pos.ofToSlice (by simpa))) +@[simp] +theorem Pos.ofToSlice_next_toSlice {s : String} {pos : s.Pos} {h} : + ofToSlice (Slice.Pos.next pos.toSlice h) = pos.next (ne_of_apply_ne Pos.toSlice (by simpa)) := + rfl + @[simp] theorem Slice.Pos.str_inj {s : Slice} (p₁ p₂ : s.Pos) : p₁.str = p₂.str ↔ p₁ = p₂ := by simp [Slice.Pos.ext_iff, String.Pos.ext_iff, Pos.Raw.ext_iff] @@ -1940,7 +1955,7 @@ theorem Pos.get_eq_get_toSlice {s : String} {p : s.Pos} {h} : @[simp] theorem Pos.offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : (p.next h).offset = p.offset + p.get h := by - simp [next] + simp [next, -ofToSlice_next_toSlice] theorem Pos.byteIdx_offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : (p.next h).offset.byteIdx = p.offset.byteIdx + (p.get h).utf8Size := by @@ -1948,7 +1963,11 @@ theorem Pos.byteIdx_offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : theorem Pos.toSlice_next {s : String} {p : s.Pos} {h} : (p.next h).toSlice = p.toSlice.next (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by - simp [next] + simp [next, -ofToSlice_next_toSlice] + +theorem Pos.next_toSlice {s : String} {p : s.Pos} {h} : + p.toSlice.next h = (p.next (ne_of_apply_ne Pos.toSlice (by simpa))).toSlice := by + simp [Pos.toSlice_next] theorem Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) : p.offset.byteIdx < s.utf8ByteSize := by @@ -2163,6 +2182,14 @@ theorem Pos.Raw.isValidForSlice_stringSliceFrom {s : String} {p : s.Pos} {q : Po rw [sliceFrom, isValidForSlice_sliceFrom, isValidForSlice_toSlice_iff, Pos.offset_toSlice] +@[simp] +theorem sliceFrom_toSlice {s : String} {p : s.Pos} : + s.toSlice.sliceFrom p.toSlice = s.sliceFrom p := rfl + +@[simp] +theorem sliceTo_toSlice {s : String} {p : s.Pos} : + s.toSlice.sliceTo p.toSlice = s.sliceTo p := rfl + /-- Given a string and two valid positions within the string, obtain a slice on the string formed by the two positions. @@ -2188,6 +2215,15 @@ theorem endExclusive_slice {s : String} {startInclusive endExclusive h} : (s.slice startInclusive endExclusive h).endExclusive = endExclusive := by simp [slice] +@[simp] +theorem utf8ByteSize_slice {s : String} {p₁ p₂ : s.Pos} {h} : + (s.slice p₁ p₂ h).utf8ByteSize = p₂.offset.byteIdx - p₁.offset.byteIdx := by + simp [Slice.utf8ByteSize_eq] + +@[simp] +theorem slice_toSlice {s : String} {p₁ p₂ : s.Pos} {h} : + s.toSlice.slice p₁.toSlice p₂.toSlice h = s.slice p₁ p₂ h := rfl + /-- Given a string and two valid positions within the string, obtain a slice on the string formed by the new bounds, or return `none` if the given end is strictly less then the given start. -/ def slice? (s : String) (startInclusive endExclusive : s.Pos) := @@ -2251,6 +2287,12 @@ def Pos.toReplaceStart {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : p₀ ≤ p theorem Pos.offset_sliceFrom {s : String} {p₀ : s.Pos} {pos : s.Pos} {h} : (sliceFrom p₀ pos h).offset = pos.offset.unoffsetBy p₀.offset := (rfl) +@[simp] +theorem Pos.sliceFrom_inj {s : String} {p₀ : s.Pos} {pos pos' : s.Pos} {h h'} : + p₀.sliceFrom pos h = p₀.sliceFrom pos' h' ↔ pos = pos' := by + simp [Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h h' + omega + @[simp] theorem Pos.ofSliceFrom_startPos {s : String} {pos : s.Pos} : ofSliceFrom (s.sliceFrom pos).startPos = pos := @@ -2290,6 +2332,26 @@ theorem Pos.get_eq_get_ofSliceFrom {s : String} {p₀ : s.Pos} pos.get h = (ofSliceFrom pos).get (by rwa [← ofSliceFrom_endPos, ne_eq, ofSliceFrom_inj]) := by simp [Pos.get, Slice.Pos.get] +@[simp] +theorem Slice.Pos.ofSliceFrom_sliceFrom {s : Slice} {p₀ p : s.Pos} {h : p₀ ≤ p} : + Slice.Pos.ofSliceFrom (p₀.sliceFrom p h) = p := by + simpa [Pos.ext_iff] using Pos.Raw.offsetBy_unoffsetBy_of_le h + +@[simp] +theorem Slice.Pos.sliceFrom_ofSliceFrom {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} : + p₀.sliceFrom (Slice.Pos.ofSliceFrom p) Slice.Pos.le_ofSliceFrom = p := by + simp [← Slice.Pos.ofSliceFrom_inj] + +@[simp] +theorem Pos.ofSliceFrom_sliceFrom {s : String} {p₀ p : s.Pos} {h : p₀ ≤ p} : + Pos.ofSliceFrom (p₀.sliceFrom p h) = p := by + simpa [Pos.ext_iff] using Pos.Raw.offsetBy_unoffsetBy_of_le h + +@[simp] +theorem Pos.sliceFrom_ofSliceFrom {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} : + p₀.sliceFrom (Pos.ofSliceFrom p) Pos.le_ofSliceFrom = p := by + simp [← Pos.ofSliceFrom_inj] + /-- Given a position in `s.sliceTo p₀`, obtain the corresponding position in `s`. -/ @[inline] def Pos.ofSliceTo {s : String} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos where @@ -2344,6 +2406,26 @@ def Pos.toReplaceEnd {s : String} (p₀ : s.Pos) (pos : s.Pos) (h : pos ≤ p₀ theorem Pos.offset_sliceTo {s : String} {p₀ : s.Pos} {pos : s.Pos} {h : pos ≤ p₀} : (sliceTo p₀ pos h).offset = pos.offset := (rfl) +@[simp] +theorem Slice.Pos.ofSliceTo_sliceTo {s : Slice} {p₀ p : s.Pos} {h : p ≤ p₀} : + Slice.Pos.ofSliceTo (p₀.sliceTo p h) = p := by + simp [Pos.ext_iff] + +@[simp] +theorem Slice.Pos.sliceTo_ofSliceTo {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} : + p₀.sliceTo (Slice.Pos.ofSliceTo p) Slice.Pos.ofSliceTo_le = p := by + simp [← Slice.Pos.ofSliceTo_inj] + +@[simp] +theorem Pos.ofSliceTo_sliceTo {s : String} {p₀ p : s.Pos} {h : p ≤ p₀} : + Pos.ofSliceTo (p₀.sliceTo p h) = p := by + simp [Pos.ext_iff] + +@[simp] +theorem Pos.sliceTo_ofSliceTo {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} : + p₀.sliceTo (Pos.ofSliceTo p) Pos.ofSliceTo_le = p := by + simp [← Pos.ofSliceTo_inj] + theorem Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) : pos.IsValidForSlice (s.slice p₀ p₁ h) ↔ pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValidForSlice s := by @@ -2359,17 +2441,39 @@ theorem Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : theorem Pos.Raw.isValidForSlice_stringSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) : pos.IsValidForSlice (s.slice p₀ p₁ h) ↔ pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValid s := by - simp [slice, isValidForSlice_slice] + simp [← slice_toSlice, isValidForSlice_slice] /-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/ @[inline] def Slice.Pos.ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos where offset := pos.offset.offsetBy p₀.offset isValidForSlice := (Pos.Raw.isValidForSlice_slice _).1 pos.isValidForSlice |>.2 + @[simp] theorem Slice.Pos.offset_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h} {pos : (s.slice p₀ p₁ h).Pos} : (Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset := (rfl) +@[simp] +theorem Slice.Pos.ofSlice_startPos {s : Slice} {p₀ p₁ : s.Pos} {h} : + ofSlice (s.slice p₀ p₁ h).startPos = p₀ := by + simp [Pos.ext_iff] + +@[simp] +theorem Slice.Pos.offset_add_slice {s : Slice} {p₀ p₁ : s.Pos} {h} : + p₀.offset + s.slice p₀ p₁ h = p₁.offset := by + simp [Pos.Raw.ext_iff, Pos.Raw.byteDistance_eq, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h + omega + +@[simp] +theorem Slice.Pos.ofSlice_endPos {s : Slice} {p₀ p₁ : s.Pos} {h} : + ofSlice (s.slice p₀ p₁ h).endPos = p₁ := by + simp [Pos.ext_iff] + +@[simp] +theorem Slice.Pos.ofSlice_inj {s : Slice} {p₀ p₁ : s.Pos} {h} (pos₁ pos₂ : (s.slice p₀ p₁ h).Pos) : + ofSlice pos₁ = ofSlice pos₂ ↔ pos₁ = pos₂ := by + simp [Pos.ext_iff, Pos.Raw.ext_iff] + /-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`. -/ @[inline] def Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos := @@ -2379,6 +2483,27 @@ def Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : (s.slice p₀ p₁ h theorem Pos.offset_ofSlice {s : String} {p₀ p₁ : s.Pos} {h} {pos : (s.slice p₀ p₁ h).Pos} : (Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset := (rfl) +@[simp] +theorem Pos.ofSlice_startPos {s : String} {p₀ p₁ : s.Pos} {h} : + ofSlice (s.slice p₀ p₁ h).startPos = p₀ := by + simp [Pos.ext_iff] + +@[simp] +theorem Pos.offset_add_slice {s : String} {p₀ p₁ : s.Pos} {h} : + p₀.offset + s.slice p₀ p₁ h = p₁.offset := by + simp [Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h + omega + +@[simp] +theorem Pos.ofSlice_endPos {s : String} {p₀ p₁ : s.Pos} {h} : + ofSlice (s.slice p₀ p₁ h).endPos = p₁ := by + simp [Pos.ext_iff] + +@[simp] +theorem Pos.ofSlice_inj {s : String} {p₀ p₁ : s.Pos} {h} (pos₁ pos₂ : (s.slice p₀ p₁ h).Pos) : + ofSlice pos₁ = ofSlice pos₂ ↔ pos₁ = pos₂ := by + simp [Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff] + theorem Slice.Pos.le_trans {s : Slice} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r := by simpa [Pos.le_iff, Pos.Raw.le_iff] using Nat.le_trans diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean index 563a9b079e..0d61ec86a0 100644 --- a/src/Init/Data/String/Lemmas.lean +++ b/src/Init/Data/String/Lemmas.lean @@ -13,6 +13,7 @@ public import Init.Data.String.Lemmas.FindPos public import Init.Data.String.Lemmas.Basic public import Init.Data.String.Lemmas.Order public import Init.Data.String.Lemmas.IsEmpty +public import Init.Data.String.Lemmas.Pattern import Init.Data.Order.Lemmas public import Init.Data.String.Basic import Init.Data.Char.Lemmas diff --git a/src/Init/Data/String/Lemmas/Basic.lean b/src/Init/Data/String/Lemmas/Basic.lean index 448943ebc8..a7fb51daea 100644 --- a/src/Init/Data/String/Lemmas/Basic.lean +++ b/src/Init/Data/String/Lemmas/Basic.lean @@ -7,6 +7,8 @@ module prelude public import Init.Data.String.Basic +import Init.Data.ByteArray.Lemmas +import Init.Data.Nat.MinMax /-! # Basic lemmas about strings @@ -31,6 +33,14 @@ theorem push_inj : push s c = push t d ↔ s = t ∧ c = d := by theorem append_eq_empty_iff {s t : String} : s ++ t = "" ↔ s = "" ∧ t = "" := by rw [← toList_inj]; simp +@[simp] +theorem append_eq_left_iff {s t : String} : s ++ t = s ↔ t = "" := by + rw [← toList_inj]; simp + +@[simp] +theorem append_eq_right_iff {s t : String} : s ++ t = t ↔ s = "" := by + rw [← toList_inj]; simp + @[simp] theorem push_ne_empty : push s c ≠ "" := by rw [ne_eq, ← toList_inj]; simp @@ -68,4 +78,14 @@ theorem Pos.byte_eq_byte_toSlice {s : String} {p : s.Pos} {h} : p.byte h = p.toSlice.byte (ne_of_apply_ne Pos.ofToSlice (by simpa)) := by simp +theorem Slice.toByteArray_copy_slice {s : Slice} {p₁ p₂ : s.Pos} {h} : + (s.slice p₁ p₂ h).copy.toByteArray = s.copy.toByteArray.extract p₁.offset.byteIdx p₂.offset.byteIdx := by + simp [toByteArray_copy, ByteArray.extract_extract] + rw [Nat.min_eq_left] + simpa [String.Pos.le_iff, Pos.Raw.le_iff] using p₂.str_le_endExclusive + +theorem toByteArray_copy_slice {s : String} {p₁ p₂ : s.Pos} {h} : + (s.slice p₁ p₂ h).copy.toByteArray = s.toByteArray.extract p₁.offset.byteIdx p₂.offset.byteIdx := by + simp [← slice_toSlice, Slice.toByteArray_copy_slice] + end String diff --git a/src/Init/Data/String/Lemmas/IsEmpty.lean b/src/Init/Data/String/Lemmas/IsEmpty.lean index 9cae39065f..e9b08aa895 100644 --- a/src/Init/Data/String/Lemmas/IsEmpty.lean +++ b/src/Init/Data/String/Lemmas/IsEmpty.lean @@ -100,6 +100,16 @@ theorem isEmpty_toSlice {s : String} : s.toSlice.isEmpty = s.isEmpty := by theorem isEmpty_toSlice_iff {s : String} : s.toSlice.isEmpty ↔ s = "" := by simp +theorem Slice.isEmpty_copy {s : Slice} : s.copy.isEmpty = s.isEmpty := by + rw [isEmpty_eq_utf8ByteSize_beq_zero, Slice.utf8ByteSize_copy, isEmpty_eq] + +@[simp] +theorem Slice.copy_eq_empty_iff {s : Slice} : s.copy = "" ↔ s.isEmpty := by + simp [← Slice.isEmpty_copy] + +theorem Slice.copy_ne_empty_iff {s : Slice} : s.copy ≠ "" ↔ s.isEmpty = false := by + simp + theorem eq_empty_iff_forall_eq {s : String} : s = "" ↔ ∀ (p q : s.Pos), p = q := by rw [← isEmpty_toSlice_iff, Slice.isEmpty_iff_forall_eq] exact ⟨fun h p q => by simpa [Pos.toSlice_inj] using h p.toSlice q.toSlice, @@ -130,4 +140,26 @@ theorem isEmpty_sliceTo_eq_false_iff {s : String} {p : s.Pos} : (s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos := Decidable.not_iff_not.1 (by simp) +@[simp] +theorem isEmpty_slice {s : String} {p₁ p₂ h} : (s.slice p₁ p₂ h).isEmpty ↔ p₁ = p₂ := by + simp [← Slice.startPos_eq_endPos_iff, ← Pos.ofSlice_inj] + +@[simp] +theorem isEmpty_slice_eq_false_iff {s : String} {p₁ p₂ h} : + (s.slice p₁ p₂ h).isEmpty = false ↔ p₁ ≠ p₂ := by + rw [ne_eq, ← isEmpty_slice (h := h), Bool.not_eq_true] + +@[simp] +theorem Slice.isEmpty_slice {s : Slice} {p₁ p₂ h} : (s.slice p₁ p₂ h).isEmpty ↔ p₁ = p₂ := by + simp [← startPos_eq_endPos_iff, ← Pos.ofSlice_inj] + +@[simp] +theorem Slice.isEmpty_slice_eq_false_iff {s : Slice} {p₁ p₂ h} : + (s.slice p₁ p₂ h).isEmpty = false ↔ p₁ ≠ p₂ := by + rw [ne_eq, ← isEmpty_slice (h := h), Bool.not_eq_true] + +@[simp] +theorem length_eq_zero_iff {s : String} : s.length = 0 ↔ s = "" := by + simp [← length_toList] + end String diff --git a/src/Init/Data/String/Lemmas/Order.lean b/src/Init/Data/String/Lemmas/Order.lean index 10799ea104..8d811d9445 100644 --- a/src/Init/Data/String/Lemmas/Order.lean +++ b/src/Init/Data/String/Lemmas/Order.lean @@ -83,6 +83,16 @@ theorem Pos.offset_le_rawEndPos {s : String} {p : s.Pos} : p.offset ≤ s.rawEndPos := p.isValid.le_rawEndPos +@[simp] +theorem Slice.Pos.byteIdx_offset_le_utf8ByteSize {s : Slice} {p : s.Pos} : + p.offset.byteIdx ≤ s.utf8ByteSize := by + simp [← byteIdx_rawEndPos, ← Pos.Raw.le_iff] + +@[simp] +theorem Pos.byteIdx_offset_le_utf8ByteSize {s : String} {p : s.Pos} : + p.offset.byteIdx ≤ s.utf8ByteSize := by + simp [← byteIdx_rawEndPos, ← Pos.Raw.le_iff] + @[simp] theorem Slice.Pos.offset_lt_rawEndPos_iff {s : Slice} {p : s.Pos} : p.offset < s.rawEndPos ↔ p ≠ s.endPos := by diff --git a/src/Init/Data/String/Lemmas/Pattern.lean b/src/Init/Data/String/Lemmas/Pattern.lean new file mode 100644 index 0000000000..32473af7e1 --- /dev/null +++ b/src/Init/Data/String/Lemmas/Pattern.lean @@ -0,0 +1,9 @@ +/- +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.Basic diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean new file mode 100644 index 0000000000..c9d49c0723 --- /dev/null +++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean @@ -0,0 +1,256 @@ +/- +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.Pattern.Basic +public import Init.Data.String.Lemmas.Splits +public import Init.Data.Iterators.Consumers.Collect +import Init.Data.String.OrderInstances +import Init.Data.String.Lemmas.IsEmpty +import Init.Data.String.Lemmas.Order +import Init.Data.String.Termination +import Init.Data.Order.Lemmas +import Init.ByCases +import Init.Data.Option.Lemmas + +set_option doc.verso true + +public section + +namespace String.Slice.Pattern + +/-! +This file develops basic theory around searching in strings. + +We provide a typeclass for providing semantics to a pattern and then define the relevant notions +of matching a pattern that let us state compatibility typeclasses for {name}`ForwardPattern` and +{name}`ToForwardSearcher`. These typeclasses can then be required by correctness results for +string functions which are implemented using the pattern framework. +-/ + +/-- +This data-carrying typeclass is used to give semantics to a pattern type that implements +{name}`ForwardPattern` and/or {name}`ToForwardSearcher` by providing an abstract, not necessarily +decidable {name}`ForwardPatternModel.Matches` predicate that implementates of {name}`ForwardPattern` +and {name}`ToForwardSearcher` can be validated against. + +Correctness results for generic functions relying on the pattern infrastructure, for example the +correctness result for {name (scope := "Init.Data.String.Slice")}`String.Slice.split`, are then +stated in terms of {name}`ForwardPatternModel.Matches`, and can be specialized to specific patterns +from there. + +The corresponding compatibility typeclasses are +{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.LawfulForwardPatternModel` +and +{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.LawfulToForwardSearcherModel`. + +We include the condition that the empty string is not a match. This is necessary for the theory to +work out as there is just no reasonable notion of searching that works for the empty string that is +still specific enough to yield reasonably strong correctness results for operations based on +searching. + +This means that pattern types that allow searching for the empty string will have to special-case +the empty string in their correctness statements. +-/ +class ForwardPatternModel {ρ : Type} (pat : ρ) : Type where + /-- The predicate that says which strings match the pattern. -/ + Matches : String → Prop + not_matches_empty : ¬ Matches "" + +/-- +Predicate stating that the region between the start of the slice {name}`s` and the position +{name}`endPos` matches the pattern {name}`pat`. Note that there might be a longer match, see +{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.IsLongestMatch`. +-/ +structure IsMatch (pat : ρ) [ForwardPatternModel pat] {s : Slice} (endPos : s.Pos) : Prop where + matches_copy : ForwardPatternModel.Matches pat (s.sliceTo endPos).copy + +theorem IsMatch.ne_startPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} + (h : IsMatch pat pos) : pos ≠ s.startPos := by + intro hc + apply ForwardPatternModel.not_matches_empty (pat := pat) + simpa [hc] using h.matches_copy + +theorem isMatch_iff {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} : + IsMatch pat pos ↔ ForwardPatternModel.Matches pat (s.sliceTo pos).copy := + ⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩ + +theorem isMatch_iff_exists_splits {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} : + IsMatch pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ t₂ ∧ ForwardPatternModel.Matches pat t₁ := by + rw [isMatch_iff] + refine ⟨fun h => ⟨_, _, pos.splits, h⟩, fun ⟨t₁, t₂, h₁, h₂⟩ => ?_⟩ + rwa [h₁.eq_left pos.splits] at h₂ + +/-- +Predicate stating that the region between the start of the slice {name}`s` and the position +{name}`endPos` matches that pattern {name}`pat`, and that there is no longer match starting at the +beginning of the slice. This is what a correct matcher should match. + +In some cases, being a match and being a longest match will coincide, see +{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.NoPrefixForwardPatternModel`. +-/ +structure IsLongestMatch (pat : ρ) [ForwardPatternModel pat] {s : Slice} (pos : s.Pos) where + isMatch : IsMatch pat pos + not_isMatch : ∀ pos', pos < pos' → ¬ IsMatch pat pos' + +theorem IsLongestMatch.ne_startPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} + (h : IsLongestMatch pat pos) : pos ≠ s.startPos := + h.isMatch.ne_startPos + +theorem IsLongestMatch.eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos pos' : s.Pos} + (h : IsLongestMatch pat pos) (h' : IsLongestMatch pat pos') : pos = pos' := by + apply Std.le_antisymm + · exact Std.not_lt.1 (fun hlt => h'.not_isMatch _ hlt h.isMatch) + · exact Std.not_lt.1 (fun hlt => h.not_isMatch _ hlt h'.isMatch) + +open Classical in +theorem IsMatch.exists_isLongestMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos : s.Pos} : + IsMatch pat pos → ∃ (pos' : s.Pos), IsLongestMatch pat pos' := by + induction pos using WellFounded.induction Pos.wellFounded_gt with | h pos ih + intro h₁ + by_cases h₂ : ∃ pos', pos < pos' ∧ IsMatch pat pos' + · obtain ⟨pos', hp₁, hp₂⟩ := h₂ + exact ih _ hp₁ hp₂ + · exact ⟨pos, ⟨h₁, fun p' hp₁ hp₂ => h₂ ⟨_, hp₁, hp₂⟩⟩⟩ + +theorem IsLongestMatch.le_of_isMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice} {pos pos' : s.Pos} + (h : IsLongestMatch pat pos) (h' : IsMatch pat pos') : pos' ≤ pos := + Std.not_lt.1 (fun hlt => h.not_isMatch _ hlt h') + +/-- +Predicate stating that a match for a given pattern is never a proper prefix of another match. + +This implies that the notion of match and longest match coincide. +-/ +class NoPrefixForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPatternModel pat] : Prop where + eq_empty (s t) : ForwardPatternModel.Matches pat s → ForwardPatternModel.Matches pat (s ++ t) → t = "" + +theorem NoPrefixForwardPatternModel.of_length_eq {ρ : Type} {pat : ρ} [ForwardPatternModel pat] + (h : ∀ s t, ForwardPatternModel.Matches pat s → ForwardPatternModel.Matches pat t → s.length = t.length) : + NoPrefixForwardPatternModel pat where + eq_empty s t hs ht := by simpa using h s _ hs ht + +theorem isLongestMatch_iff_isMatch {ρ : Type} (pat : ρ) [ForwardPatternModel pat] [NoPrefixForwardPatternModel pat] + {s : Slice} {pos : s.Pos} : IsLongestMatch pat pos ↔ IsMatch pat pos := by + refine ⟨fun h => h.isMatch, fun h => ⟨h, fun pos' hpos' hm => ?_⟩⟩ + obtain ⟨t₁, t₂, ht₁, ht₂⟩ := isMatch_iff_exists_splits.1 h + obtain ⟨t₁', t₂', ht₁', ht₂'⟩ := isMatch_iff_exists_splits.1 hm + obtain ⟨t₅, ht₅, ht₅', ht₅''⟩ := (ht₁.lt_iff_exists_eq_append ht₁').1 hpos' + exact ht₅ (NoPrefixForwardPatternModel.eq_empty _ _ ht₂ (ht₅' ▸ ht₂')) + +/-- +Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match +of {name}`pat` in {name}`s` and it is longest among matches starting at {name}`startPos`. +-/ +structure IsLongestMatchAt (pat : ρ) [ForwardPatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where + le : startPos ≤ endPos + isLongestMatch_sliceFrom : IsLongestMatch pat (Slice.Pos.sliceFrom _ _ le) + +theorem IsLongestMatchAt.lt {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos} + (h : IsLongestMatchAt pat startPos endPos) : startPos < endPos := by + have := h.isLongestMatch_sliceFrom.ne_startPos + rw [← Pos.startPos_lt_iff, ← Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff] at this + simpa + +theorem IsLongestMatchAt.eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos} + (h : IsLongestMatchAt pat startPos endPos) (h' : IsLongestMatchAt pat startPos endPos') : + endPos = endPos' := by + simpa using h.isLongestMatch_sliceFrom.eq 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 + le := Slice.Pos.le_ofSliceFrom + isLongestMatch_sliceFrom := by simpa + +/-- +Predicate stating that there is a (longest) match starting at the given position. +-/ +structure MatchesAt (pat : ρ) [ForwardPatternModel pat] {s : Slice} (pos : s.Pos) : Prop where + exists_isMatchAt : ∃ endPos, IsLongestMatchAt pat pos endPos + +theorem matchesAt_iff_exists_isLongestMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice} + {pos : s.Pos} : + MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ h, IsLongestMatch pat (pos.sliceFrom endPos h) := + ⟨fun ⟨p, h⟩ => ⟨p, h.le, h.isLongestMatch_sliceFrom⟩, fun ⟨p, h₁, h₂⟩ => ⟨p, ⟨h₁, h₂⟩⟩⟩ + +theorem matchesAt_iff_exists_isMatch {pat : ρ} [ForwardPatternModel pat] {s : Slice} + {pos : s.Pos} : + MatchesAt pat pos ↔ ∃ (endPos : s.Pos), ∃ h, IsMatch pat (pos.sliceFrom endPos h) := by + refine ⟨fun ⟨p, h⟩ => ⟨p, h.le, h.isLongestMatch_sliceFrom.isMatch⟩, fun ⟨p, h₁, h₂⟩ => ?_⟩ + obtain ⟨q, hq⟩ := h₂.exists_isLongestMatch + exact ⟨Pos.ofSliceFrom q, + ⟨Std.le_trans h₁ (by simpa [← Pos.ofSliceFrom_le_ofSliceFrom_iff] using hq.le_of_isMatch h₂), + by simpa using hq⟩⟩ + +/-- +Predicate stating compatibility between {name}`ForwardPatternModel` and {name}`ForwardPattern`. + +This extends {name}`LawfulForwardPattern`, but it is much stronger because it forces the +{name}`ForwardPattern` to match the longest prefix of the given slice that matches the property +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 + +open Classical in +theorem LawfulForwardPatternModel.dropPrefix?_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 + rw [← Decidable.not_iff_not] + simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.dropPrefix?_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⟩ + +/-- +Inductive predicate stating that a list of search steps represents a valid search from a given +position in a slice. + +"Searching" here means always taking the longest match at the first position where the pattern +matches. + +Hence, this predicate determines the list of search steps up to grouping of rejections. +-/ +inductive IsValidSearchFrom (pat : ρ) [ForwardPatternModel pat] {s : Slice} : + s.Pos → List (SearchStep s) → Prop where + | endPos : IsValidSearchFrom pat s.endPos [] + | matched {startPos endPos : s.Pos} : + IsLongestMatchAt pat startPos endPos → IsValidSearchFrom pat endPos l → + IsValidSearchFrom pat startPos (.matched startPos endPos :: l) + | mismatched {startPos endPos : s.Pos} : startPos < endPos → + (∀ pos, startPos ≤ pos → pos < endPos → ¬ MatchesAt pat pos) → + IsValidSearchFrom pat endPos l → IsValidSearchFrom pat startPos (.rejected startPos endPos :: l) + +theorem IsValidSearchFrom.matched_of_eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} + {startPos startPos' endPos : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidSearchFrom pat endPos l) + (h₂ : IsLongestMatchAt pat startPos' endPos) + (h₃ : startPos = startPos') : IsValidSearchFrom pat startPos' (.matched startPos endPos :: l) := by + cases h₃ + exact IsValidSearchFrom.matched h₂ h₁ + +theorem IsValidSearchFrom.mismatched_of_eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} + {startPos startPos' endPos : s.Pos} {l : List (SearchStep s)} (h₁ : IsValidSearchFrom pat endPos l) + (h₀ : startPos' < endPos) + (h₂ : ∀ pos, startPos' ≤ pos → pos < endPos → ¬ MatchesAt pat pos) (h₃ : startPos = startPos') : + IsValidSearchFrom pat startPos' (.rejected startPos endPos :: l) := by + cases h₃ + exact IsValidSearchFrom.mismatched h₀ h₂ h₁ + +/-- +Predicate stating compatibility between {name}`ForwardPatternModel` and {name}`ToForwardSearcher`. + +We require the searcher to always match the longest match at the first position where the pattern +matches; see {name}`IsValidSearchFrom`. +-/ +class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type} + [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)] + [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where + isValidSearchFrom_toList (s) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList + +end String.Slice.Pattern diff --git a/src/Init/Data/String/Lemmas/Splits.lean b/src/Init/Data/String/Lemmas/Splits.lean index ee2b4bc39e..2a8973e26d 100644 --- a/src/Init/Data/String/Lemmas/Splits.lean +++ b/src/Init/Data/String/Lemmas/Splits.lean @@ -10,6 +10,11 @@ public import Init.Data.String.Basic import Init.Data.ByteArray.Lemmas import Init.Data.String.Lemmas.Basic import Init.Data.Nat.MinMax +import Init.Data.String.Lemmas.IsEmpty +import Init.Data.String.Lemmas.Order +import Init.Data.String.OrderInstances +import Init.Data.Nat.Order +import Init.Omega /-! # `Splits` predicates on `String.Pos` and `String.Slice.Pos`. @@ -123,6 +128,14 @@ theorem Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ := (splits_copy_iff.2 h₁).eq (splits_copy_iff.2 h₂) +theorem Pos.Splits.of_eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄} + (h : p.Splits t₁ t₂) (h₁ : t₁ = t₃) (h₂ : t₂ = t₄) : p.Splits t₃ t₄ := + h₁ ▸ h₂ ▸ h + +theorem Slice.Pos.Splits.of_eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄} + (h : p.Splits t₁ t₂) (h₁ : t₁ = t₃) (h₂ : t₂ = t₄) : p.Splits t₃ t₄ := + h₁ ▸ h₂ ▸ h + @[simp] theorem splits_endPos (s : String) : s.endPos.Splits s "" where eq_append := by simp @@ -248,4 +261,148 @@ theorem Slice.Pos.Splits.next {s : Slice} {p : s.Pos} obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp) exact splits_next p hp +theorem Slice.sliceTo_copy_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} : + (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by + refine ⟨?_, ?_⟩ + · rintro rfl + exact ⟨_, p.splits⟩ + · rintro ⟨t₂, h⟩ + exact p.splits.eq_left h + +theorem sliceTo_copy_eq_iff_exists_splits {s : String} {p : s.Pos} {t₁ : String} : + (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂ := by + refine ⟨?_, ?_⟩ + · rintro rfl + exact ⟨_, p.splits⟩ + · rintro ⟨t₂, h⟩ + exact p.splits.eq_left h + +theorem Slice.Pos.Splits.pos_eq {s : Slice} {p q : s.Pos} {s t : String} (h : p.Splits s t) + (h' : q.Splits s t) : p = q := by + rw [Slice.Pos.ext_iff, h.offset_eq_rawEndPos, h'.offset_eq_rawEndPos] + +theorem Pos.Splits.pos_eq {s : String} {p q : s.Pos} {s t : String} (h : p.Splits s t) + (h' : q.Splits s t) : p = q := by + rw [Pos.ext_iff, h.offset_eq_rawEndPos, h'.offset_eq_rawEndPos] + +theorem Slice.Pos.Splits.get_eq_of_singleton {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} + {t₁ t₂ : String} {c : Char} (hs : (p.next h).Splits (t₁ ++ singleton c) t₂) : p.get h = c := by + have := hs.eq_left (splits_next p h) + simp only [append_singleton, push_inj] at this + rw [this.2] + +theorem Pos.Splits.get_eq_of_singleton {s : String} {p : s.Pos} {h : p ≠ s.endPos} + {t₁ t₂ : String} {c : Char} (hs : (p.next h).Splits (t₁ ++ singleton c) t₂) : p.get h = c := by + have := hs.eq_left (splits_next p h) + simp only [append_singleton, push_inj] at this + rw [this.2] + +theorem Slice.splits_singleton_iff {s : Slice} {p : s.Pos} {c : Char} {t : String} : + p.Splits (singleton c) t ↔ + ∃ h, p = s.startPos.next h ∧ s.startPos.get h = c ∧ s.copy = singleton c ++ t := by + refine ⟨fun h => ?_, ?_⟩ + · have : s.startPos ≠ s.endPos := by + simp [startPos_ne_endPos_iff, ← copy_ne_empty_iff, h.eq_append] + have spl : (s.startPos.next this).Splits (singleton c) t := by + rw [← empty_append (s := singleton c)] + apply Pos.Splits.next + simp [h.eq_append] + refine ⟨this, ⟨h.pos_eq spl, ?_, h.eq_append⟩⟩ + rw [← empty_append (s := singleton c)] at spl + exact spl.get_eq_of_singleton + · rintro ⟨h, ⟨rfl, rfl, h'⟩⟩ + rw [← String.empty_append (s := singleton (s.startPos.get h))] + exact Pos.Splits.next (by simp [h']) + +theorem splits_singleton_iff {s : String} {p : s.Pos} {c : Char} {t : String} : + p.Splits (singleton c) t ↔ + ∃ h, p = s.startPos.next h ∧ s.startPos.get h = c ∧ s = singleton c ++ t := by + rw [← Pos.splits_toSlice_iff, Slice.splits_singleton_iff] + simp [← Pos.ofToSlice_inj] + +@[simp] +theorem Slice.copy_sliceTo_startPos {s : Slice} : (s.sliceTo s.startPos).copy = "" := + s.startPos.splits.eq_left s.splits_startPos + +@[simp] +theorem copy_sliceTo_startPos {s : String} : (s.sliceTo s.startPos).copy = "" := + s.startPos.splits.eq_left s.splits_startPos + +theorem Slice.splits_next_startPos {s : Slice} {h : s.startPos ≠ s.endPos} : + (s.startPos.next h).Splits + (singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy := by + rw [← String.empty_append (s := singleton (s.startPos.get h))] + apply Slice.Pos.Splits.next + have := Slice.Pos.splits_next_right s.startPos h + rwa [copy_sliceTo_startPos] at this + +theorem splits_next_startPos {s : String} {h : s.startPos ≠ s.endPos} : + (s.startPos.next h).Splits + (singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy := by + rw [← Pos.splits_toSlice_iff] + apply (Slice.splits_next_startPos).of_eq <;> simp [String.Pos.next_toSlice] + +theorem Slice.Pos.Splits.toByteArray_eq_left {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : + t₁.toByteArray = s.copy.toByteArray.extract 0 p.offset.byteIdx := by + rw [h.eq_left p.splits] + simp only [toByteArray_copy, str_sliceTo, startInclusive_sliceTo, endExclusive_sliceTo, + offset_str, Pos.Raw.byteIdx_offsetBy, ByteArray.extract_extract, Nat.add_zero] + rw [Nat.min_eq_left] + simpa [String.Pos.le_iff, Pos.Raw.le_iff] using p.str_le_endExclusive + +theorem Pos.Splits.toByteArray_eq_left {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : + t₁.toByteArray = s.toByteArray.extract 0 p.offset.byteIdx := by + rw [(splits_toSlice_iff.2 h).toByteArray_eq_left, copy_toSlice, Pos.offset_toSlice] + +theorem Slice.Pos.Splits.toByteArray_eq_right {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : + t₂.toByteArray = s.copy.toByteArray.extract p.offset.byteIdx s.copy.toByteArray.size := by + rw [h.eq_right p.splits] + simp only [toByteArray_copy, str_sliceFrom, startInclusive_sliceFrom, offset_str, + Pos.Raw.byteIdx_offsetBy, endExclusive_sliceFrom, ByteArray.size_extract, size_toByteArray, + ByteArray.extract_extract] + rw [Nat.min_eq_right] + rw [Nat.min_eq_left (by simp)] + have := s.startInclusive_le_endExclusive + rw [String.Pos.le_iff, Pos.Raw.le_iff] at this + omega + +theorem Pos.Splits.toByteArray_eq_right {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : + t₂.toByteArray = s.toByteArray.extract p.offset.byteIdx s.toByteArray.size := by + rw [(splits_toSlice_iff.2 h).toByteArray_eq_right, copy_toSlice, Pos.offset_toSlice] + +theorem Slice.Pos.Splits.le_iff_exists_eq_append {s : Slice} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} + (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : p₁ ≤ p₂ ↔ ∃ t₅, t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄ := by + refine ⟨fun hp => ?_, ?_⟩ + · refine ⟨(s.slice p₁ p₂ hp).copy, ?_, ?_⟩ + · simp only [← toByteArray_inj, toByteArray_append, h'.toByteArray_eq_left, + h.toByteArray_eq_left, toByteArray_copy_slice] + rw [← ByteArray.extract_eq_extract_append_extract _ (by simp) hp] + · simp [← toByteArray_inj, h.toByteArray_eq_right, h'.toByteArray_eq_right, + toByteArray_copy_slice, ← ByteArray.extract_eq_extract_append_extract _ hp] + · rintro ⟨t₅, rfl, rfl⟩ + simp [Pos.Raw.le_iff, Slice.Pos.le_iff, h.offset_eq_rawEndPos, h'.offset_eq_rawEndPos] + +theorem Slice.Pos.Splits.lt_iff_exists_eq_append {s : Slice} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} + (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : + p₁ < p₂ ↔ ∃ t₅, t₅ ≠ "" ∧ t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄ := by + rw [Std.lt_iff_le_and_ne, h.le_iff_exists_eq_append h'] + refine ⟨?_, ?_⟩ + · rintro ⟨⟨t₅, ⟨rfl, rfl⟩⟩, h₂⟩ + refine ⟨t₅, fun hx => ?_, rfl, rfl⟩ + simp [hx] at h h' + exact h₂ (h.pos_eq h') + · rintro ⟨t₅, ⟨ht₅, rfl, rfl⟩⟩ + refine ⟨⟨t₅, rfl, rfl⟩, fun hx => ht₅ ?_⟩ + have := h.eq_left (hx ▸ h') + simpa [eq_comm (a := t₁)] using (h.eq_left (hx ▸ h') :) + +theorem Pos.Splits.le_iff_exists_eq_append {s : String} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} + (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : p₁ ≤ p₂ ↔ ∃ t₅, t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄ := by + rw [← toSlice_le, (splits_toSlice_iff.2 h).le_iff_exists_eq_append (splits_toSlice_iff.2 h')] + +theorem Pos.Splits.lt_iff_exists_eq_append {s : String} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} + (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : + p₁ < p₂ ↔ ∃ t₅, t₅ ≠ "" ∧ t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄ := by + rw [← toSlice_lt, (splits_toSlice_iff.2 h).lt_iff_exists_eq_append (splits_toSlice_iff.2 h')] + end String diff --git a/src/Init/Data/String/Pattern/Basic.lean b/src/Init/Data/String/Pattern/Basic.lean index e34d1b1794..b51d589cfb 100644 --- a/src/Init/Data/String/Pattern/Basic.lean +++ b/src/Init/Data/String/Pattern/Basic.lean @@ -290,12 +290,14 @@ def memcmpSlice (lhs rhs : Slice) (lstart : String.Pos.Raw) (rstart : String.Pos (by have := lhs.startInclusive_le_endExclusive have := lhs.endExclusive.isValid.le_utf8ByteSize - simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at * + simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq, + -String.Pos.byteIdx_offset_le_utf8ByteSize] at * omega) (by have := rhs.startInclusive_le_endExclusive have := rhs.endExclusive.isValid.le_utf8ByteSize - simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at * + simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq, + -String.Pos.byteIdx_offset_le_utf8ByteSize] at * omega) end Internal