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

feat: lemmas about splitting the empty string/slice (#12725)

Browse source 
This PR shows that lawful searchers split the empty string to `[""]`.
This commit is contained in:
Markus Himmel 2026-02-27 12:04:17 +01:00 • committed by GitHub
parent 9843794e3f
commit b4f768b67f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 38 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean
View file

@ -20,6 +20,7 @@ import Init.Data.String.OrderInstances
import Init.Data.Iterators.Lemmas.Basic
import Init.Data.Iterators.Lemmas.Consumers.Collect
import Init.Data.Iterators.Lemmas.Combinators.FilterMap
import Init.Data.String.Lemmas.IsEmpty
set_option doc.verso true
@ -164,12 +165,29 @@ end Pattern
open Pattern
public theorem toList_splitToSubslice_of_isEmpty {ρ : Type} (pat : ρ)
[Model.ForwardPatternModel pat] {σ : Slice → Type}
[ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
[∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
(h : s.isEmpty = true) :
(s.splitToSubslice pat).toList = [s.subsliceFrom s.endPos] := by
simp [toList_splitToSubslice_eq_modelSplit, Slice.startPos_eq_endPos_iff.2 h]
public theorem toList_split_eq_splitToSubslice {ρ : Type} (pat : ρ) {σ : Slice → Type}
[ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
[∀ s, Std.Iterators.Finite (σ s) Id] {s : Slice} :
(s.split pat).toList = (s.splitToSubslice pat).toList.map Subslice.toSlice := by
simp [split, Std.Iter.toList_map]
public theorem toList_split_of_isEmpty {ρ : Type} (pat : ρ)
[Model.ForwardPatternModel pat] {σ : Slice → Type}
[ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
[∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
(h : s.isEmpty = true) :
(s.split pat).toList.map Slice.copy = [""] := by
rw [toList_split_eq_splitToSubslice, toList_splitToSubslice_of_isEmpty _ h]
simp
end Slice
open Slice.Pattern
@ -178,4 +196,12 @@ public theorem split_eq_split_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Typ
[ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)] {s : String} :
s.split pat = s.toSlice.split pat := (rfl)
@[simp]
public theorem toList_split_empty {ρ : Type} (pat : ρ)
[Model.ForwardPatternModel pat] {σ : Slice → Type}
[ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
[∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] :
("".split pat).toList.map Slice.copy = [""] := by
rw [split_eq_split_toSlice, Slice.toList_split_of_isEmpty _ (by simp)]
end String

12
src/Init/Data/String/Subslice.lean
View file

@ -7,6 +7,8 @@ module
prelude
public import Init.Data.String.Basic
import Init.Data.String.Lemmas.IsEmpty
import Init.Data.String.Lemmas.Basic
set_option doc.verso true
@ -59,6 +61,11 @@ theorem startInclusive_toSlice {s : Slice} {sl : s.Subslice} :
theorem endExclusive_toSlice {s : Slice} {sl : s.Subslice} :
sl.toSlice.endExclusive = sl.endExclusive.str := rfl
@[simp]
theorem isEmpty_toSlice_iff {s : Slice} {sl : s.Subslice} :
sl.toSlice.isEmpty ↔ sl.startInclusive = sl.endExclusive := by
simp [toSlice]
instance {s : Slice} : CoeOut s.Subslice Slice where
coe := Subslice.toSlice
@ -144,6 +151,11 @@ theorem endExclusive_subsliceFrom {s : Slice} {newStart : s.Pos} :
theorem subslice_endPos {s : Slice} {newStart : s.Pos} :
s.subslice newStart s.endPos (Slice.Pos.le_endPos _) = s.subsliceFrom newStart := (rfl)
@[simp]
theorem toSlice_subsliceFrom {s : Slice} {newStart : s.Pos} :
(s.subsliceFrom newStart).toSlice = s.sliceFrom newStart := by
ext1 <;> simp
/-- The entire slice, as a subslice of itself. -/
@[inline]
def toSubslice (s : Slice) : s.Subslice :=