Verification of KMP string search

In this file, we instantiate LawfulToForwardSearcherModel for Slice patterns, which amounts to verifying that our implementation of KMP string search in Init.Data.String.Pattern.String is correct.

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.lawfulToForwardSearcherModel {pat : Slice} (hpat : pat.isEmpty = false) : LawfulToForwardSearcherModel pat

@[simp]

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.toList_atEnd_eq {s : Slice} : { internalState := ForwardSliceSearcher.atEnd }.toList = []

@[simp]

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.toList_emptyAt_eq (s : Slice) (pos : s.Pos) (h : pos ≠ s.endPos) : { internalState := ForwardSliceSearcher.emptyAt pos h }.toList = SearchStep.rejected pos (pos.next h) :: { internalState := ForwardSliceSearcher.emptyBefore (pos.next h) }.toList

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.toList_emptyBefore_eq (s : Slice) (pos : s.Pos) : { internalState := ForwardSliceSearcher.emptyBefore pos }.toList = if h : pos = s.endPos then [SearchStep.matched pos pos] else SearchStep.matched pos pos :: { internalState := ForwardSliceSearcher.emptyAt pos h }.toList

theorem String.Slice.Pattern.Model.ForwardSliceSearcher.toSearcher_of_isEmpty {pat : Slice} (hpat : pat.isEmpty = true) (s : Slice) : ToForwardSearcher.toSearcher pat s = { internalState := ForwardSliceSearcher.emptyBefore s.startPos }

theorem String.Slice.Pattern.Model.ForwardStringSearcher.lawfulToForwardSearcherModel {pat : String} (hpat : pat ≠ "") : LawfulToForwardSearcherModel pat

theorem String.Slice.Pattern.Model.ForwardStringSearcher.toSearcher_empty (s : Slice) : ToForwardSearcher.toSearcher "" s = { internalState := ForwardSliceSearcher.emptyBefore s.startPos }

theorem String.Slice.contains_string_eq_contains_toSlice {pat : String} {s : Slice} : s.contains pat = s.contains pat.toSlice

theorem String.Slice.find?_string_eq_find?_toSlice {pat : String} {s : Slice} : s.find? pat = s.find? pat.toSlice

theorem String.Slice.Pos.find?_string_eq_find?_toSlice {pat : String} {s : Slice} {p : s.Pos} : p.find? pat = p.find? pat.toSlice