Verification of String.Slice.splitToSubslice

This PR verifies the String.Slice.splitToSubslice function by relating it to a model implementation based on the String.Slice.Pattern.Model.PatternModel class.

This gives a low-level correctness proof from which higher-level API lemmas can be derived.

@[irreducible]

noncomputable def String.Slice.Pattern.Model.split {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat] {s : Slice} (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr) : List s.Subslice

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem String.Slice.Pattern.Model.split_endPos {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {firstRejected : s.Pos} : Model.split pat firstRejected s.endPos ⋯ = [s.subslice firstRejected s.endPos ⋯]

theorem String.Slice.Pattern.Model.split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {firstRejected start stop : s.Pos} {hle : firstRejected ≤ start} (h : IsLongestMatchAt pat start stop) : Model.split pat firstRejected start hle = s.subslice firstRejected start hle :: Model.split pat stop stop ⋯

theorem String.Slice.Pattern.Model.split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {firstRejected start : s.Pos} (stop : s.Pos) (h₀ : start ≤ stop) {hle : firstRejected ≤ start} (h : ∀ (p : s.Pos), start ≤ p → p < stop → ¬MatchesAt pat p) : Model.split pat firstRejected start hle = Model.split pat firstRejected stop ⋯

theorem String.Slice.Pattern.Model.split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {firstRejected start : s.Pos} {hle : firstRejected ≤ start} (hs : start ≠ s.endPos) (h : ¬MatchesAt pat start) : Model.split pat firstRejected start hle = Model.split pat firstRejected (start.next hs) ⋯

theorem String.Slice.Pattern.toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [Model.PatternModel pat] [Model.StrictPatternModel pat] {σ : Slice → Type} [ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] (s : Slice) : (s.splitToSubslice pat).toList = Model.split pat s.startPos s.startPos ⋯

theorem String.Slice.toList_splitToSubslice_of_isEmpty {ρ : Type} (pat : ρ) [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] {σ : Slice → Type} [Pattern.ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.Model.LawfulToForwardSearcherModel pat] {s : Slice} (h : s.isEmpty = true) : (s.splitToSubslice pat).toList = [s.subsliceFrom s.endPos]

theorem String.Slice.toList_split_eq_splitToSubslice {ρ : Type} (pat : ρ) {σ : Slice → Type} [Pattern.ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] {s : Slice} : (s.split pat).toList = List.map Subslice.toSlice (s.splitToSubslice pat).toList

theorem String.Slice.toList_split_of_isEmpty {ρ : Type} (pat : ρ) [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] {σ : Slice → Type} [Pattern.ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.Model.LawfulToForwardSearcherModel pat] {s : Slice} (h : s.isEmpty = true) : List.map copy (s.split pat).toList = [""]

theorem String.split_eq_split_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} [Slice.Pattern.ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] {s : String} : s.split pat = s.toSlice.split pat

@[simp]

theorem String.toList_split_empty {ρ : Type} (pat : ρ) [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] {σ : Slice → Type} [Slice.Pattern.ToForwardSearcher pat σ] [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Slice.Pattern.Model.LawfulToForwardSearcherModel pat] : List.map Slice.copy ("".split pat).toList = [""]