max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: basic infrastructure for verification of string patterns (#12333)

Browse source 
This PR adds the basic typeclasses that will be used in the verification
of our string searching infrastructure.
This commit is contained in:
Markus Himmel 2026-02-05 17:37:50 +01:00 • committed by GitHub
parent c3779bc8d5
commit 52bc216351
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 619 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

135
src/Init/Data/String/Basic.lean
View file

@ -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

1
src/Init/Data/String/Lemmas.lean
View file

@ -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

20
src/Init/Data/String/Lemmas/Basic.lean
View file

@ -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

32
src/Init/Data/String/Lemmas/IsEmpty.lean
View file

@ -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

10
src/Init/Data/String/Lemmas/Order.lean
View file

@ -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

9
src/Init/Data/String/Lemmas/Pattern.lean Normal file
View file

@ -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

256
src/Init/Data/String/Lemmas/Pattern/Basic.lean Normal file
View file

@ -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

157
src/Init/Data/String/Lemmas/Splits.lean
View file

@ -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

6
src/Init/Data/String/Pattern/Basic.lean
View file

@ -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