refactor: reduce duplication in string pattern lemmas (#12793)
This PR takes a more principled approach in deriving `String` pattern lemmas by reducing to simpler cases similar to how the instances are defined. This reduces duplication of complex arguments (at the expense of having to state more simple lemmas; however these lemmas are useful to users as well).
This commit is contained in:
Markus Himmel
GitHub
parent
8526edb1fc
commit
10ece4e082
12 changed files with 587 additions and 260 deletions
|
|
@ -8,6 +8,12 @@ module
|
|||
prelude
|
||||
public import Init.Data.String.Pattern.Char
|
||||
public import Init.Data.String.Lemmas.Pattern.Basic
|
||||
public import Init.Data.String.Slice
|
||||
public import Init.Data.String.Lemmas.Pattern.Pred
|
||||
public import Init.Data.String.Search
|
||||
import all Init.Data.String.Slice
|
||||
import all Init.Data.String.Pattern.Char
|
||||
import all Init.Data.String.Search
|
||||
import Init.Data.Option.Lemmas
|
||||
import Init.Data.String.Lemmas.Basic
|
||||
import Init.Data.String.Lemmas.Order
|
||||
|
|
@ -54,8 +60,8 @@ instance {c : Char} : LawfulForwardPatternModel c where
|
|||
dropPrefix?_eq_some_iff {s} pos := by
|
||||
simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)]
|
||||
|
||||
instance {c : Char} : LawfulToForwardSearcherModel c :=
|
||||
.defaultImplementation
|
||||
theorem toSearcher_eq {c : Char} {s : Slice} :
|
||||
ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (· == c) s := (rfl)
|
||||
|
||||
theorem matchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} :
|
||||
MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c := by
|
||||
|
|
@ -80,4 +86,153 @@ theorem matchAt?_eq {s : Slice} {pos : s.Pos} {c : Char} :
|
|||
if h₀ : ∃ (h : pos ≠ s.endPos), pos.get h = c then some (pos.next h₀.1) else none := by
|
||||
split <;> simp_all [isLongestMatchAt_iff, matchesAt_iff]
|
||||
|
||||
end String.Slice.Pattern.Model.Char
|
||||
theorem isMatch_iff_isMatch_beq {c : Char} {s : Slice} {pos : s.Pos} :
|
||||
IsMatch c pos ↔ IsMatch (· == c) pos := by
|
||||
simp [isMatch_iff, CharPred.isMatch_iff, beq_iff_eq]
|
||||
|
||||
theorem isLongestMatch_iff_isLongestMatch_beq {c : Char} {s : Slice} {pos : s.Pos} :
|
||||
IsLongestMatch c pos ↔ IsLongestMatch (· == c) pos := by
|
||||
simp [isLongestMatch_iff_isMatch, isMatch_iff_isMatch_beq]
|
||||
|
||||
theorem isLongestMatchAt_iff_isLongestMatchAt_beq {c : Char} {s : Slice}
|
||||
{pos pos' : s.Pos} :
|
||||
IsLongestMatchAt c pos pos' ↔ IsLongestMatchAt (· == c) pos pos' := by
|
||||
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_beq]
|
||||
|
||||
theorem matchesAt_iff_matchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} :
|
||||
MatchesAt c pos ↔ MatchesAt (· == c) pos := by
|
||||
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_beq]
|
||||
|
||||
theorem matchAt?_eq_matchAt?_beq {c : Char} {s : Slice} {pos : s.Pos} :
|
||||
matchAt? c pos = matchAt? (· == c) pos := by
|
||||
refine Option.ext (fun pos' => ?_)
|
||||
simp [matchAt?_eq_some_iff, isLongestMatchAt_iff_isLongestMatchAt_beq]
|
||||
|
||||
theorem isValidSearchFrom_iff_isValidSearchFrom_beq {c : Char} {s : Slice} {p : s.Pos}
|
||||
{l : List (SearchStep s)} : IsValidSearchFrom c p l ↔ IsValidSearchFrom (· == c) p l := by
|
||||
refine ⟨fun h => ?_, fun h => ?_⟩
|
||||
· induction h with
|
||||
| endPos => simpa using IsValidSearchFrom.endPos
|
||||
| matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_beq]
|
||||
| mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_beq]
|
||||
· induction h with
|
||||
| endPos => simpa using IsValidSearchFrom.endPos
|
||||
| matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_beq]
|
||||
| mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_beq]
|
||||
|
||||
instance {c : Char} : LawfulToForwardSearcherModel c where
|
||||
isValidSearchFrom_toList s := by
|
||||
simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_beq] using
|
||||
LawfulToForwardSearcherModel.isValidSearchFrom_toList (pat := (· == c)) (s := s)
|
||||
|
||||
end Pattern.Model.Char
|
||||
|
||||
theorem startsWith_char_eq_startsWith_beq {c : Char} {s : Slice} :
|
||||
s.startsWith c = s.startsWith (· == c) := (rfl)
|
||||
|
||||
theorem dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} :
|
||||
s.dropPrefix? c = s.dropPrefix? (· == c) := (rfl)
|
||||
|
||||
theorem dropPrefix_char_eq_dropPrefix_beq {c : Char} {s : Slice} :
|
||||
s.dropPrefix c = s.dropPrefix (· == c) := (rfl)
|
||||
|
||||
theorem Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} :
|
||||
dropPrefix? c s = dropPrefix? (· == c) s := (rfl)
|
||||
|
||||
private theorem dropWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
|
||||
dropWhile.go s c curr = dropWhile.go s (· == c) curr := by
|
||||
fun_induction dropWhile.go s c curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq]
|
||||
|
||||
theorem dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} :
|
||||
s.dropWhile c = s.dropWhile (· == c) := by
|
||||
simpa only [dropWhile] using dropWhileGo_eq s.startPos
|
||||
|
||||
private theorem takeWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
|
||||
takeWhile.go s c curr = takeWhile.go s (· == c) curr := by
|
||||
fun_induction takeWhile.go s c curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq]
|
||||
|
||||
theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} :
|
||||
s.takeWhile c = s.takeWhile (· == c) := by
|
||||
simp only [takeWhile]; exact takeWhileGo_eq s.startPos
|
||||
|
||||
theorem all_char_eq_all_beq {c : Char} {s : Slice} :
|
||||
s.all c = s.all (· == c) := by
|
||||
simp only [all, dropWhile_char_eq_dropWhile_beq]
|
||||
|
||||
theorem find?_char_eq_find?_beq {c : Char} {s : Slice} :
|
||||
s.find? c = s.find? (· == c) :=
|
||||
(rfl)
|
||||
|
||||
theorem Pos.find?_char_eq_find?_beq {c : Char} {s : Slice} {p : s.Pos} :
|
||||
p.find? c = p.find? (· == c) :=
|
||||
(rfl)
|
||||
|
||||
theorem contains_char_eq_contains_beq {c : Char} {s : Slice} :
|
||||
s.contains c = s.contains (· == c) :=
|
||||
(rfl)
|
||||
|
||||
theorem endsWith_char_eq_endsWith_beq {c : Char} {s : Slice} :
|
||||
s.endsWith c = s.endsWith (· == c) := (rfl)
|
||||
|
||||
theorem dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} :
|
||||
s.dropSuffix? c = s.dropSuffix? (· == c) := (rfl)
|
||||
|
||||
theorem dropSuffix_char_eq_dropSuffix_beq {c : Char} {s : Slice} :
|
||||
s.dropSuffix c = s.dropSuffix (· == c) := (rfl)
|
||||
|
||||
theorem Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} :
|
||||
dropSuffix? c s = dropSuffix? (· == c) s := (rfl)
|
||||
|
||||
private theorem dropEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
|
||||
dropEndWhile.go s c curr = dropEndWhile.go s (· == c) curr := by
|
||||
fun_induction dropEndWhile.go s c curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq]
|
||||
|
||||
theorem dropEndWhile_char_eq_dropEndWhile_beq {c : Char} {s : Slice} :
|
||||
s.dropEndWhile c = s.dropEndWhile (· == c) := by
|
||||
simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos
|
||||
|
||||
private theorem takeEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
|
||||
takeEndWhile.go s c curr = takeEndWhile.go s (· == c) curr := by
|
||||
fun_induction takeEndWhile.go s c curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq]
|
||||
|
||||
theorem takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} :
|
||||
s.takeEndWhile c = s.takeEndWhile (· == c) := by
|
||||
simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos
|
||||
|
||||
end String.Slice
|
||||
|
|
|
|||
|
|
@ -143,6 +143,18 @@ theorem Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : String} {po
|
|||
rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff]
|
||||
exact Slice.Pos.find?_char_eq_none_iff_not_mem_of_splits (Pos.splits_toSlice_iff.mpr hs)
|
||||
|
||||
theorem Pos.find?_char_eq_find?_beq {c : Char} {s : String} {pos : s.Pos} :
|
||||
pos.find? c = pos.find? (· == c) := by
|
||||
simp only [Pos.find?_eq_find?_toSlice, Slice.Pos.find?_char_eq_find?_beq]
|
||||
|
||||
theorem find?_char_eq_find?_beq {c : Char} {s : String} :
|
||||
s.find? c = s.find? (· == c) := by
|
||||
simp only [find?_eq_find?_toSlice, Slice.find?_char_eq_find?_beq]
|
||||
|
||||
theorem contains_char_eq_contains_beq {c : Char} {s : String} :
|
||||
s.contains c = s.contains (· == c) := by
|
||||
simp only [contains_eq_contains_toSlice, Slice.contains_char_eq_contains_beq]
|
||||
|
||||
theorem find?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
|
||||
s.find? c = some pos ↔
|
||||
∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (Pos.ne_endPos_of_lt h') ≠ c := by
|
||||
|
|
|
|||
|
|
@ -7,6 +7,8 @@ module
|
|||
|
||||
prelude
|
||||
public import Init.Data.String.Slice
|
||||
import all Init.Data.String.Slice
|
||||
import all Init.Data.String.Search
|
||||
import Init.Data.String.Lemmas.Pattern.Find.Basic
|
||||
import Init.Data.String.Lemmas.Pattern.Pred
|
||||
import Init.Data.String.Lemmas.Basic
|
||||
|
|
@ -27,7 +29,8 @@ theorem find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
|
|||
theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
|
||||
s.find? p = some pos ↔
|
||||
∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by
|
||||
grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff]
|
||||
simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} :
|
||||
s.find? p = some pos ↔
|
||||
|
|
@ -48,17 +51,8 @@ theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s :
|
|||
{pos : s.Pos} :
|
||||
s.find? p = some pos ↔
|
||||
∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬ p d := by
|
||||
rw [find?_prop_eq_some_iff]
|
||||
refine ⟨?_, ?_⟩
|
||||
· rintro ⟨h, hp, hmin⟩
|
||||
exact ⟨_, _, _, pos.splits_next_right h, hp, fun d hd => by
|
||||
obtain ⟨pos', hlt, hpget⟩ := (pos.splits_next_right h).mem_toList_left_iff.mp hd
|
||||
subst hpget; exact hmin _ hlt⟩
|
||||
· rintro ⟨t, c, u, hs, hpc, hmin⟩
|
||||
have hne := hs.ne_endPos_of_singleton
|
||||
refine ⟨hne, ?_, fun pos' hlt => hmin _ (hs.mem_toList_left_iff.mpr ⟨pos', hlt, rfl⟩)⟩
|
||||
rw [(singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm]
|
||||
exact hpc
|
||||
simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff_splits, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
@[simp]
|
||||
theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy.toList.any p := by
|
||||
|
|
@ -70,10 +64,7 @@ theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy
|
|||
@[simp]
|
||||
theorem contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.contains p = s.copy.toList.any p := by
|
||||
rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff]
|
||||
simp only [Pattern.Model.CharPred.Decidable.matchesAt_iff, ne_eq, List.any_eq_true,
|
||||
mem_toList_copy_iff_exists_get, decide_eq_true_eq]
|
||||
exact ⟨fun ⟨pos, h, hp⟩ => ⟨_, ⟨_, _, rfl⟩, hp⟩, fun ⟨_, ⟨p, h, h'⟩, hp⟩ => ⟨p, h, h' ▸ hp⟩⟩
|
||||
rw [contains_prop_eq_contains_decide, contains_bool_eq]
|
||||
|
||||
theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} :
|
||||
pos.find? p = some pos' ↔
|
||||
|
|
@ -141,64 +132,48 @@ theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Sl
|
|||
pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
|
||||
∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
|
||||
¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by
|
||||
grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff]
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
{pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
|
||||
pos.find? p = some pos' ↔
|
||||
∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬ p d := by
|
||||
rw [Pos.find?_prop_eq_some_iff]
|
||||
refine ⟨?_, ?_⟩
|
||||
· rintro ⟨hle, ⟨hne, hp⟩, hmin⟩
|
||||
have hsplit := pos'.splits_next_right hne
|
||||
obtain ⟨v, hv1, hv2⟩ := (hs.le_iff_exists_eq_append hsplit).mp hle
|
||||
refine ⟨v, pos'.get hne, _, hsplit.of_eq hv1 rfl, hp, fun d hd => ?_⟩
|
||||
obtain ⟨_, hcopy⟩ :=
|
||||
Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hv2, hsplit.of_eq hv1 rfl⟩
|
||||
rw [← hcopy] at hd
|
||||
obtain ⟨q, hq, hqget⟩ := mem_toList_copy_iff_exists_get.mp hd
|
||||
have hlt : Pos.ofSlice q < pos' := by
|
||||
simpa [← Slice.Pos.lt_endPos_iff, ← Pos.ofSlice_lt_ofSlice_iff] using hq
|
||||
subst hqget; rw [Slice.Pos.get_eq_get_ofSlice]; exact hmin _ Pos.le_ofSlice hlt
|
||||
· rintro ⟨v, c, w, hsplit, hpc, hmin⟩
|
||||
have hne := hsplit.ne_endPos_of_singleton
|
||||
have hu : u = v ++ (singleton c ++ w) :=
|
||||
append_right_inj t |>.mp (hs.eq_append.symm.trans (by rw [hsplit.eq_append, append_assoc]))
|
||||
have hle : pos ≤ pos' := (hs.le_iff_exists_eq_append hsplit).mpr ⟨v, rfl, hu⟩
|
||||
refine ⟨hle, ⟨hne, ?_⟩, fun pos'' hle' hlt => hmin _ ?_⟩
|
||||
· rw [(singleton_append_inj.mp (hsplit.eq_right (pos'.splits_next_right hne))).1.symm]
|
||||
exact hpc
|
||||
· obtain ⟨_, hcopy⟩ :=
|
||||
Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hu, hsplit⟩
|
||||
rw [← hcopy]
|
||||
exact mem_toList_copy_iff_exists_get.mpr
|
||||
⟨pos''.slice pos pos' hle' (Std.le_of_lt hlt),
|
||||
fun h => Std.ne_of_lt hlt
|
||||
(by rw [← Slice.Pos.ofSlice_slice (h₁ := hle') (h₂ := Std.le_of_lt hlt), h,
|
||||
Slice.Pos.ofSlice_endPos]),
|
||||
by rw [Slice.Pos.get_eq_get_ofSlice]
|
||||
simp [Slice.Pos.ofSlice_slice]⟩
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff_splits hs, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
|
||||
pos.find? p = none ↔
|
||||
∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → ¬ p (pos'.get h) := by
|
||||
grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff]
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff, decide_eq_false_iff_not]
|
||||
|
||||
theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
{pos : s.Pos} {t u : String} (hs : pos.Splits t u) :
|
||||
pos.find? p = none ↔ ∀ c ∈ u.toList, ¬ p c := by
|
||||
rw [Pos.find?_prop_eq_none_iff]
|
||||
constructor
|
||||
· intro h c hc
|
||||
obtain ⟨pos', hle, hne, hget⟩ := hs.mem_toList_right_iff.mp hc
|
||||
subst hget; exact h pos' hle hne
|
||||
· intro h pos' hle hne
|
||||
exact h _ (hs.mem_toList_right_iff.mpr ⟨pos', hle, hne, rfl⟩)
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff_of_splits hs,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
end String.Slice
|
||||
|
||||
namespace String
|
||||
|
||||
theorem Pos.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : String}
|
||||
{pos : s.Pos} : pos.find? p = pos.find? (decide <| p ·) := by
|
||||
show (pos.toSlice.find? p).map Pos.ofToSlice = (pos.toSlice.find? (decide <| p ·)).map Pos.ofToSlice
|
||||
simp only [show pos.toSlice.find? p = pos.toSlice.find? (decide <| p ·) from
|
||||
Slice.Pos.find?_prop_eq_find?_decide]
|
||||
|
||||
theorem find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : String} :
|
||||
s.find? p = s.find? (decide <| p ·) := by
|
||||
show (s.toSlice.find? p).map Pos.ofToSlice = (s.toSlice.find? (decide <| p ·)).map Pos.ofToSlice
|
||||
simp only [show s.toSlice.find? p = s.toSlice.find? (decide <| p ·) from
|
||||
Slice.find?_prop_eq_find?_decide]
|
||||
|
||||
theorem contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {s : String} :
|
||||
s.contains p = s.contains (decide <| p ·) := by
|
||||
show s.toSlice.contains p = s.toSlice.contains (decide <| p ·)
|
||||
exact Slice.contains_prop_eq_contains_decide
|
||||
|
||||
theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos pos' : s.Pos} :
|
||||
pos.find? p = some pos' ↔
|
||||
pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
|
||||
|
|
@ -257,52 +232,27 @@ theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : St
|
|||
pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
|
||||
∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
|
||||
¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by
|
||||
simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
|
||||
Slice.Pos.find?_prop_eq_some_iff, endPos_toSlice]
|
||||
refine ⟨?_, ?_⟩
|
||||
· rintro ⟨pos', ⟨h₁, ⟨h₂, hp⟩, h₃⟩, rfl⟩
|
||||
refine ⟨by simpa [Pos.ofToSlice_le_iff] using h₁,
|
||||
⟨by simpa [← Pos.ofToSlice_inj] using h₂, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩
|
||||
intro pos'' h₄ h₅
|
||||
simpa using h₃ pos''.toSlice (by simpa [Pos.toSlice_le] using h₄) (by simpa using h₅)
|
||||
· rintro ⟨h₁, ⟨h₂, hp⟩, h₃⟩
|
||||
refine ⟨pos'.toSlice, ⟨by simpa [Pos.toSlice_le] using h₁,
|
||||
⟨by simpa [← Pos.toSlice_inj] using h₂, by simpa using hp⟩, fun p hp₁ hp₂ => ?_⟩,
|
||||
by simp⟩
|
||||
simpa using h₃ (Pos.ofToSlice p)
|
||||
(by simpa [Pos.ofToSlice_le_iff] using hp₁) (by simpa using hp₂)
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String}
|
||||
{pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
|
||||
pos.find? p = some pos' ↔
|
||||
∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬ p d := by
|
||||
simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
|
||||
Slice.Pos.find?_prop_eq_some_iff_splits (Pos.splits_toSlice_iff.mpr hs)]
|
||||
constructor
|
||||
· rintro ⟨q, ⟨v, c, w, hsplit, hpc, hmin⟩, rfl⟩
|
||||
exact ⟨v, c, w, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩
|
||||
· rintro ⟨v, c, w, hsplit, hpc, hmin⟩
|
||||
exact ⟨pos'.toSlice, ⟨v, c, w, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff_splits hs, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : String}
|
||||
{pos : s.Pos} :
|
||||
pos.find? p = none ↔
|
||||
∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → ¬ p (pos'.get h) := by
|
||||
simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff,
|
||||
Slice.Pos.find?_prop_eq_none_iff, endPos_toSlice]
|
||||
refine ⟨?_, ?_⟩
|
||||
· intro h pos' h₁ h₂
|
||||
simpa [Pos.get_ofToSlice] using
|
||||
h pos'.toSlice (by simpa [Pos.toSlice_le] using h₁) (by simpa [← Pos.toSlice_inj] using h₂)
|
||||
· intro h pos' h₁ h₂
|
||||
simpa using h (Pos.ofToSlice pos')
|
||||
(by simpa [Pos.ofToSlice_le_iff] using h₁) (by simpa [← Pos.ofToSlice_inj] using h₂)
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff, decide_eq_false_iff_not]
|
||||
|
||||
theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : String}
|
||||
{pos : s.Pos} {t u : String} (hs : pos.Splits t u) :
|
||||
pos.find? p = none ↔ ∀ c ∈ u.toList, ¬ p c := by
|
||||
rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff]
|
||||
exact Slice.Pos.find?_prop_eq_none_iff_of_splits (Pos.splits_toSlice_iff.mpr hs)
|
||||
simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_none_iff_of_splits hs,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
|
||||
s.find? p = some pos ↔
|
||||
|
|
@ -332,28 +282,15 @@ theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.
|
|||
theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} :
|
||||
s.find? p = some pos ↔
|
||||
∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by
|
||||
simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_prop_eq_some_iff,
|
||||
endPos_toSlice, exists_and_right]
|
||||
refine ⟨?_, ?_⟩
|
||||
· rintro ⟨pos, ⟨⟨h, hp⟩, h'⟩, rfl⟩
|
||||
refine ⟨⟨by simpa [← Pos.ofToSlice_inj] using h, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩
|
||||
intro pos' hp
|
||||
simpa using h' pos'.toSlice hp
|
||||
· rintro ⟨⟨h, hp⟩, hmin⟩
|
||||
exact ⟨pos.toSlice, ⟨⟨by simpa [← Pos.toSlice_inj] using h, by simpa using hp⟩,
|
||||
fun pos' hp => by simpa using hmin (Pos.ofToSlice pos') hp⟩, by simp⟩
|
||||
simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String}
|
||||
{pos : s.Pos} :
|
||||
s.find? p = some pos ↔
|
||||
∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬ p d := by
|
||||
simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff,
|
||||
Slice.find?_prop_eq_some_iff_splits]
|
||||
constructor
|
||||
· rintro ⟨q, ⟨t, c, u, hsplit, hpc, hmin⟩, rfl⟩
|
||||
exact ⟨t, c, u, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩
|
||||
· rintro ⟨t, c, u, hsplit, hpc, hmin⟩
|
||||
exact ⟨pos.toSlice, ⟨t, c, u, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩
|
||||
simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff_splits, decide_eq_true_eq,
|
||||
decide_eq_false_iff_not]
|
||||
|
||||
@[simp]
|
||||
theorem contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toList.any p := by
|
||||
|
|
@ -362,6 +299,6 @@ theorem contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toL
|
|||
@[simp]
|
||||
theorem contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : String} :
|
||||
s.contains p = s.toList.any p := by
|
||||
simp [contains_eq_contains_toSlice, Slice.contains_prop_eq, copy_toSlice]
|
||||
rw [contains_prop_eq_contains_decide, contains_bool_eq]
|
||||
|
||||
end String
|
||||
|
|
|
|||
|
|
@ -8,6 +8,7 @@ module
|
|||
prelude
|
||||
public import Init.Data.String.Search
|
||||
import all Init.Data.String.Slice
|
||||
import all Init.Data.String.Pattern.String
|
||||
import Init.ByCases
|
||||
import Init.Data.String.Lemmas.Pattern.Find.Basic
|
||||
import Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
|
||||
|
|
@ -55,11 +56,7 @@ theorem contains_slice_iff {t s : Slice} :
|
|||
@[simp]
|
||||
theorem contains_string_iff {t : String} {s : Slice} :
|
||||
s.contains t ↔ t.toList <:+: s.copy.toList := by
|
||||
by_cases ht : t = ""
|
||||
· simp [contains_string_eq_true_of_empty ht s, ht]
|
||||
· have := Pattern.Model.ForwardStringSearcher.lawfulToForwardSearcherModel (pat := t) ht
|
||||
simp only [Pattern.Model.contains_eq_true_iff,
|
||||
Pattern.Model.ForwardStringSearcher.exists_matchesAt_iff_eq_append ht, isInfix_toList_iff]
|
||||
simp [contains_string_eq_contains_toSlice, contains_slice_iff, copy_toSlice]
|
||||
|
||||
@[simp]
|
||||
theorem contains_slice_eq_false_iff {t s : Slice} :
|
||||
|
|
|
|||
|
|
@ -8,6 +8,11 @@ module
|
|||
prelude
|
||||
public import Init.Data.String.Pattern.Pred
|
||||
public import Init.Data.String.Lemmas.Pattern.Basic
|
||||
public import Init.Data.String.Slice
|
||||
public import Init.Data.String.Search
|
||||
import all Init.Data.String.Slice
|
||||
import all Init.Data.String.Pattern.Pred
|
||||
import all Init.Data.String.Search
|
||||
import Init.Data.Option.Lemmas
|
||||
import Init.Data.String.Lemmas.Basic
|
||||
import Init.Data.String.Lemmas.Order
|
||||
|
|
@ -112,6 +117,15 @@ theorem isLongestMatchAt_of_get {p : Char → Prop} [DecidablePred p] {s : Slice
|
|||
{h : pos ≠ s.endPos} (hc : p (pos.get h)) : IsLongestMatchAt p pos (pos.next h) :=
|
||||
isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩
|
||||
|
||||
theorem matchesAt_iff_matchesAt_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
{pos : s.Pos} : MatchesAt p pos ↔ MatchesAt (decide <| p ·) pos := by
|
||||
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_decide]
|
||||
|
||||
theorem matchAt?_eq_matchAt?_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
{pos : s.Pos} : matchAt? p pos = matchAt? (decide <| p ·) pos := by
|
||||
ext endPos
|
||||
simp [isLongestMatchAt_iff_isLongestMatchAt_decide]
|
||||
|
||||
theorem dropPrefix?_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] :
|
||||
ForwardPattern.dropPrefix? p = ForwardPattern.dropPrefix? (decide <| p ·) := rfl
|
||||
|
||||
|
|
@ -120,8 +134,26 @@ instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p whe
|
|||
rw [dropPrefix?_eq_dropPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide]
|
||||
exact LawfulForwardPatternModel.dropPrefix?_eq_some_iff ..
|
||||
|
||||
instance {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p :=
|
||||
.defaultImplementation
|
||||
theorem toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (decide <| p ·) s := (rfl)
|
||||
|
||||
theorem isValidSearchFrom_iff_isValidSearchFrom_decide {p : Char → Prop} [DecidablePred p]
|
||||
{s : Slice} {pos : s.Pos} {l : List (SearchStep s)} :
|
||||
IsValidSearchFrom p pos l ↔ IsValidSearchFrom (decide <| p ·) pos l := by
|
||||
refine ⟨fun h => ?_, fun h => ?_⟩
|
||||
· induction h with
|
||||
| endPos => simpa using IsValidSearchFrom.endPos
|
||||
| matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_decide]
|
||||
| mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_decide]
|
||||
· induction h with
|
||||
| endPos => simpa using IsValidSearchFrom.endPos
|
||||
| matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_decide]
|
||||
| mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_decide]
|
||||
|
||||
instance {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p where
|
||||
isValidSearchFrom_toList s := by
|
||||
simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_decide] using
|
||||
LawfulToForwardSearcherModel.isValidSearchFrom_toList (pat := (decide <| p ·)) (s := s)
|
||||
|
||||
theorem matchesAt_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
|
||||
MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) := by
|
||||
|
|
@ -138,4 +170,121 @@ theorem matchAt?_eq {s : Slice} {pos : s.Pos} {p : Char → Prop} [DecidablePred
|
|||
|
||||
end Decidable
|
||||
|
||||
end String.Slice.Pattern.Model.CharPred
|
||||
end Pattern.Model.CharPred
|
||||
|
||||
theorem startsWith_prop_eq_startsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.startsWith p = s.startsWith (decide <| p ·) := (rfl)
|
||||
|
||||
theorem dropPrefix?_prop_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.dropPrefix? p = s.dropPrefix? (decide <| p ·) := (rfl)
|
||||
|
||||
theorem dropPrefix_prop_eq_dropPrefix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.dropPrefix p = s.dropPrefix (decide <| p ·) := (rfl)
|
||||
|
||||
theorem Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide
|
||||
{p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
dropPrefix? p s = dropPrefix? (decide <| p ·) s := (rfl)
|
||||
|
||||
private theorem dropWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) :
|
||||
dropWhile.go s p curr = dropWhile.go s (decide <| p ·) curr := by
|
||||
fun_induction dropWhile.go s p curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide]
|
||||
|
||||
theorem dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.dropWhile p = s.dropWhile (decide <| p ·) := by
|
||||
simpa only [dropWhile] using dropWhileGo_eq s.startPos
|
||||
|
||||
private theorem takeWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) :
|
||||
takeWhile.go s p curr = takeWhile.go s (decide <| p ·) curr := by
|
||||
fun_induction takeWhile.go s p curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide]
|
||||
|
||||
theorem takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.takeWhile p = s.takeWhile (decide <| p ·) := by
|
||||
simp only [takeWhile]; exact takeWhileGo_eq s.startPos
|
||||
|
||||
theorem all_prop_eq_all_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.all p = s.all (decide <| p ·) := by
|
||||
simp only [all, dropWhile_prop_eq_dropWhile_decide]
|
||||
|
||||
theorem find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.find? p = s.find? (decide <| p ·) :=
|
||||
(rfl)
|
||||
|
||||
theorem Pos.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
{pos : s.Pos} :
|
||||
pos.find? p = pos.find? (decide <| p ·) :=
|
||||
(rfl)
|
||||
|
||||
theorem contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.contains p = s.contains (decide <| p ·) :=
|
||||
(rfl)
|
||||
|
||||
theorem endsWith_prop_eq_endsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.endsWith p = s.endsWith (decide <| p ·) := (rfl)
|
||||
|
||||
theorem dropSuffix?_prop_eq_dropSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.dropSuffix? p = s.dropSuffix? (decide <| p ·) := (rfl)
|
||||
|
||||
theorem dropSuffix_prop_eq_dropSuffix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
s.dropSuffix p = s.dropSuffix (decide <| p ·) := (rfl)
|
||||
|
||||
theorem Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide
|
||||
{p : Char → Prop} [DecidablePred p] {s : Slice} :
|
||||
dropSuffix? p s = dropSuffix? (decide <| p ·) s := (rfl)
|
||||
|
||||
private theorem dropEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
(curr : s.Pos) :
|
||||
dropEndWhile.go s p curr = dropEndWhile.go s (decide <| p ·) curr := by
|
||||
fun_induction dropEndWhile.go s p curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide]
|
||||
|
||||
theorem dropEndWhile_prop_eq_dropEndWhile_decide {p : Char → Prop} [DecidablePred p]
|
||||
{s : Slice} :
|
||||
s.dropEndWhile p = s.dropEndWhile (decide <| p ·) := by
|
||||
simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos
|
||||
|
||||
private theorem takeEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
(curr : s.Pos) :
|
||||
takeEndWhile.go s p curr = takeEndWhile.go s (decide <| p ·) curr := by
|
||||
fun_induction takeEndWhile.go s p curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide]
|
||||
|
||||
theorem takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidablePred p]
|
||||
{s : Slice} :
|
||||
s.takeEndWhile p = s.takeEndWhile (decide <| p ·) := by
|
||||
simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos
|
||||
|
||||
end String.Slice
|
||||
|
|
|
|||
|
|
@ -9,10 +9,14 @@ prelude
|
|||
public import Init.Data.String.Slice
|
||||
public import Init.Data.String.Search
|
||||
public import Init.Data.List.SplitOn.Basic
|
||||
public import Init.Data.String.Lemmas.Pattern.Split.Basic
|
||||
public import Init.Data.String.Lemmas.Pattern.Char
|
||||
import all Init.Data.String.Lemmas.Pattern.Split.Basic
|
||||
import Init.Data.String.Termination
|
||||
import Init.Data.Order.Lemmas
|
||||
import Init.Data.Iterators.Lemmas.Combinators.FilterMap
|
||||
import Init.Data.String.Lemmas.Pattern.Split.Basic
|
||||
import Init.Data.String.Lemmas.Pattern.Split.Pred
|
||||
import Init.Data.String.Lemmas.Pattern.Char
|
||||
import Init.ByCases
|
||||
import Init.Data.String.OrderInstances
|
||||
|
|
@ -26,28 +30,26 @@ namespace String.Slice
|
|||
|
||||
open Pattern.Model Pattern.Model.Char
|
||||
|
||||
theorem Pattern.Model.split_char_eq_split_beq {c : Char} {s : Slice}
|
||||
(f curr : s.Pos) (hle : f ≤ curr) :
|
||||
Model.split c f curr hle = Model.split (· == c) f curr hle := by
|
||||
fun_induction Model.split c f curr hle with
|
||||
| case1 fr h => simp
|
||||
| case2 fr curr hle h pos h₁ h₂ ih =>
|
||||
conv => rhs; rw [Model.split]
|
||||
simp only [h, ↓reduceDIte]
|
||||
split <;> simp_all [matchAt?_eq_matchAt?_beq]
|
||||
| case3 fr curr hle h pos ih =>
|
||||
conv => rhs; rw [Model.split]
|
||||
simp only [h, ↓reduceDIte]
|
||||
split <;> simp_all [matchAt?_eq_matchAt?_beq]
|
||||
|
||||
theorem toList_splitToSubslice_char {s : Slice} {c : Char} :
|
||||
(s.splitToSubslice c).toList.map (Slice.copy ∘ Subslice.toSlice) =
|
||||
(s.copy.toList.splitOn c).map String.ofList := by
|
||||
simp only [Pattern.toList_splitToSubslice_eq_modelSplit]
|
||||
suffices ∀ (f p : s.Pos) (hle : f ≤ p) (t₁ t₂ : String),
|
||||
p.Splits t₁ t₂ → (Pattern.Model.split c f p hle).map (copy ∘ Subslice.toSlice) =
|
||||
(t₂.toList.splitOnPPrepend (· == c) (s.subslice f p hle).copy.toList.reverse).map String.ofList by
|
||||
simpa [List.splitOn_eq_splitOnP] using this s.startPos s.startPos (Std.le_refl _) "" s.copy
|
||||
intro f p hle t₁ t₂ hp
|
||||
induction p using Pos.next_induction generalizing f t₁ t₂ with
|
||||
| next p h ih =>
|
||||
obtain ⟨t₂, rfl⟩ := hp.exists_eq_singleton_append h
|
||||
by_cases hpc : p.get h = c
|
||||
· simp [split_eq_of_isLongestMatchAt (isLongestMatchAt_of_get_eq hpc),
|
||||
ih _ (Std.le_refl _) _ _ hp.next,
|
||||
List.splitOnPPrepend_cons_pos (p := (· == c)) (beq_iff_eq.2 hpc)]
|
||||
· rw [split_eq_next_of_not_matchesAt h (not_matchesAt_of_get_ne hpc)]
|
||||
simp only [toList_append, toList_singleton, List.cons_append, List.nil_append, Subslice.copy_eq]
|
||||
rw [ih _ _ _ _ hp.next, List.splitOnPPrepend_cons_neg (by simpa)]
|
||||
have := (splits_slice (Std.le_trans hle (by simp)) (p.slice f (p.next h) hle (by simp))).eq_append
|
||||
simp_all
|
||||
| endPos => simp_all
|
||||
have : (s.splitToSubslice c).toList = (s.splitToSubslice (· == c)).toList := by
|
||||
simp only [Pattern.toList_splitToSubslice_eq_modelSplit, Pattern.Model.split_char_eq_split_beq]
|
||||
simp only [this, List.splitOn_eq_splitOnP, toList_splitToSubslice_bool]
|
||||
|
||||
theorem toList_split_char {s : Slice} {c : Char} :
|
||||
(s.split c).toList.map Slice.copy = (s.copy.toList.splitOn c).map String.ofList := by
|
||||
|
|
|
|||
|
|
@ -9,7 +9,10 @@ prelude
|
|||
public import Init.Data.String.Slice
|
||||
public import Init.Data.String.Search
|
||||
public import Init.Data.List.SplitOn.Basic
|
||||
public import Init.Data.String.Lemmas.Pattern.Split.Basic
|
||||
public import Init.Data.String.Lemmas.Pattern.Pred
|
||||
import Init.Data.String.Termination
|
||||
import all Init.Data.String.Lemmas.Pattern.Split.Basic
|
||||
import Init.Data.Order.Lemmas
|
||||
import Init.Data.Iterators.Lemmas.Combinators.FilterMap
|
||||
import Init.Data.String.Lemmas.Pattern.Split.Basic
|
||||
|
|
@ -61,28 +64,27 @@ section
|
|||
|
||||
open Pattern.Model Pattern.Model.CharPred.Decidable
|
||||
|
||||
theorem Pattern.Model.split_eq_split_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
|
||||
(f curr : s.Pos) (hle : f ≤ curr) :
|
||||
Model.split p f curr hle = Model.split (decide <| p ·) f curr hle := by
|
||||
fun_induction Model.split p f curr hle with
|
||||
| case1 fr h => simp
|
||||
| case2 fr curr hle h pos h₁ h₂ ih =>
|
||||
conv => rhs; rw [Model.split]
|
||||
simp only [h, ↓reduceDIte]
|
||||
split <;> simp_all [matchAt?_eq_matchAt?_decide]
|
||||
| case3 fr curr hle h pos ih =>
|
||||
conv => rhs; rw [Model.split]
|
||||
simp only [h, ↓reduceDIte]
|
||||
split <;> simp_all [matchAt?_eq_matchAt?_decide]
|
||||
|
||||
theorem toList_splitToSubslice_prop {s : Slice} {p : Char → Prop} [DecidablePred p] :
|
||||
(s.splitToSubslice p).toList.map (Slice.copy ∘ Subslice.toSlice) =
|
||||
(s.copy.toList.splitOnP p).map String.ofList := by
|
||||
simp only [Pattern.toList_splitToSubslice_eq_modelSplit]
|
||||
suffices ∀ (f pos : s.Pos) (hle : f ≤ pos) (t₁ t₂ : String),
|
||||
pos.Splits t₁ t₂ → (Pattern.Model.split p f pos hle).map (copy ∘ Subslice.toSlice) =
|
||||
(t₂.toList.splitOnPPrepend p (s.subslice f pos hle).copy.toList.reverse).map String.ofList by
|
||||
simpa using this s.startPos s.startPos (Std.le_refl _) "" s.copy
|
||||
intro f pos hle t₁ t₂ hp
|
||||
induction pos using Pos.next_induction generalizing f t₁ t₂ with
|
||||
| next pos h ih =>
|
||||
obtain ⟨t₂, rfl⟩ := hp.exists_eq_singleton_append h
|
||||
by_cases hpc : p (pos.get h)
|
||||
· simp [split_eq_of_isLongestMatchAt (isLongestMatchAt_of_get hpc),
|
||||
ih _ (Std.le_refl _) _ _ hp.next,
|
||||
List.splitOnPPrepend_cons_pos (p := (decide <| p ·)) (by simpa using hpc)]
|
||||
· rw [split_eq_next_of_not_matchesAt h (not_matchesAt_of_get hpc)]
|
||||
simp only [toList_append, toList_singleton, List.cons_append, List.nil_append, Subslice.copy_eq]
|
||||
rw [ih _ _ _ _ hp.next, List.splitOnPPrepend_cons_neg (by simpa)]
|
||||
have := (splits_slice (Std.le_trans hle (by simp)) (pos.slice f (pos.next h) hle (by simp))).eq_append
|
||||
simp_all
|
||||
| endPos => simp_all
|
||||
have : (s.splitToSubslice p).toList = (s.splitToSubslice (decide <| p ·)).toList := by
|
||||
simp only [Pattern.toList_splitToSubslice_eq_modelSplit, split_eq_split_decide]
|
||||
rw [this]
|
||||
exact toList_splitToSubslice_bool
|
||||
|
||||
theorem toList_split_prop {s : Slice} {p : Char → Prop} [DecidablePred p] :
|
||||
(s.split p).toList.map Slice.copy = (s.copy.toList.splitOnP p).map String.ofList := by
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Author: Markus Himmel
|
|||
module
|
||||
|
||||
prelude
|
||||
public import Init.Data.String.Pattern.String
|
||||
public import Init.Data.String.Lemmas.Pattern.Basic
|
||||
import Init.Data.String.Lemmas.IsEmpty
|
||||
import Init.Data.String.Lemmas.Basic
|
||||
|
|
@ -150,19 +151,19 @@ theorem isMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} :
|
|||
IsMatch (ρ := String) pat pos ↔ IsMatch (ρ := Slice) pat.toSlice pos := by
|
||||
simp only [Model.isMatch_iff, ForwardPatternModel.Matches, copy_toSlice]
|
||||
|
||||
theorem isLongestMatch_iff_slice {pat : String} {s : Slice} {pos : s.Pos} :
|
||||
theorem isLongestMatch_iff_isLongestMatch_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
|
||||
IsLongestMatch (ρ := String) pat pos ↔ IsLongestMatch (ρ := Slice) pat.toSlice pos where
|
||||
mp h := ⟨isMatch_iff_slice.1 h.isMatch, fun p hp hm => h.not_isMatch p hp (isMatch_iff_slice.2 hm)⟩
|
||||
mpr h := ⟨isMatch_iff_slice.2 h.isMatch, fun p hp hm => h.not_isMatch p hp (isMatch_iff_slice.1 hm)⟩
|
||||
|
||||
theorem isLongestMatchAt_iff_slice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
|
||||
theorem isLongestMatchAt_iff_isLongestMatchAt_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
|
||||
IsLongestMatchAt (ρ := String) pat pos₁ pos₂ ↔
|
||||
IsLongestMatchAt (ρ := Slice) pat.toSlice pos₁ pos₂ := by
|
||||
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_slice]
|
||||
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_toSlice]
|
||||
|
||||
theorem matchesAt_iff_slice {pat : String} {s : Slice} {pos : s.Pos} :
|
||||
theorem matchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
|
||||
MatchesAt (ρ := String) pat pos ↔ MatchesAt (ρ := Slice) pat.toSlice pos := by
|
||||
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_slice]
|
||||
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
|
||||
|
||||
private theorem toSlice_isEmpty (h : pat ≠ "") : pat.toSlice.isEmpty = false := by
|
||||
rwa [isEmpty_toSlice, isEmpty_eq_false_iff]
|
||||
|
|
@ -178,7 +179,7 @@ theorem isLongestMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠
|
|||
|
||||
theorem isLongestMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat ≠ "") :
|
||||
IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ h, (s.slice pos₁ pos₂ h).copy = pat := by
|
||||
rw [isLongestMatchAt_iff_slice,
|
||||
rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
|
||||
ForwardSliceSearcher.isLongestMatchAt_iff (toSlice_isEmpty h)]
|
||||
simp
|
||||
|
||||
|
|
@ -186,7 +187,7 @@ theorem isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ :
|
|||
(h : pat ≠ "") :
|
||||
IsLongestMatchAt pat pos₁ pos₂ ↔
|
||||
∃ t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂ := by
|
||||
rw [isLongestMatchAt_iff_slice,
|
||||
rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
|
||||
ForwardSliceSearcher.isLongestMatchAt_iff_splits (toSlice_isEmpty h)]
|
||||
simp
|
||||
|
||||
|
|
@ -194,7 +195,7 @@ theorem isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ :
|
|||
(h : pat ≠ "") :
|
||||
IsLongestMatchAt pat pos₁ pos₂ ↔
|
||||
s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray := by
|
||||
rw [isLongestMatchAt_iff_slice,
|
||||
rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
|
||||
ForwardSliceSearcher.isLongestMatchAt_iff_extract (toSlice_isEmpty h)]
|
||||
simp
|
||||
|
||||
|
|
@ -203,11 +204,11 @@ theorem offset_of_isLongestMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s
|
|||
pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
|
||||
rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm]
|
||||
exact ForwardSliceSearcher.offset_of_isLongestMatchAt (toSlice_isEmpty h)
|
||||
(isLongestMatchAt_iff_slice.1 h')
|
||||
(isLongestMatchAt_iff_isLongestMatchAt_toSlice.1 h')
|
||||
|
||||
theorem matchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
|
||||
MatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ (pat ++ t₂) := by
|
||||
rw [matchesAt_iff_slice,
|
||||
rw [matchesAt_iff_toSlice,
|
||||
ForwardSliceSearcher.matchesAt_iff_splits (toSlice_isEmpty h)]
|
||||
simp
|
||||
|
||||
|
|
@ -229,8 +230,8 @@ theorem matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos}
|
|||
IsLongestMatchAt pat pos (s.pos _ h) := by
|
||||
have key := ForwardSliceSearcher.matchesAt_iff_isLongestMatchAt (pat := pat.toSlice)
|
||||
(toSlice_isEmpty h) (pos := pos)
|
||||
simp only [utf8ByteSize_toSlice, ← isLongestMatchAt_iff_slice] at key
|
||||
rwa [matchesAt_iff_slice]
|
||||
simp only [utf8ByteSize_toSlice, ← isLongestMatchAt_iff_isLongestMatchAt_toSlice] at key
|
||||
rwa [matchesAt_iff_toSlice]
|
||||
|
||||
theorem matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "") :
|
||||
MatchesAt pat pos ↔
|
||||
|
|
@ -240,13 +241,33 @@ theorem matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat
|
|||
have key := ForwardSliceSearcher.matchesAt_iff_getElem (pat := pat.toSlice)
|
||||
(toSlice_isEmpty h) (pos := pos)
|
||||
simp only [copy_toSlice] at key
|
||||
rwa [matchesAt_iff_slice]
|
||||
rwa [matchesAt_iff_toSlice]
|
||||
|
||||
theorem le_of_matchesAt {pat : String} {s : Slice} {pos : s.Pos} (h : pat ≠ "")
|
||||
(h' : MatchesAt pat pos) : pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos := by
|
||||
rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm]
|
||||
exact ForwardSliceSearcher.le_of_matchesAt (toSlice_isEmpty h)
|
||||
(matchesAt_iff_slice.1 h')
|
||||
(matchesAt_iff_toSlice.1 h')
|
||||
|
||||
theorem matchesAt_iff_matchesAt_toSlice {pat : String} {s : Slice}
|
||||
{pos : s.Pos} : MatchesAt pat pos ↔ MatchesAt pat.toSlice pos := by
|
||||
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
|
||||
|
||||
theorem toSearcher_eq {pat : String} {s : Slice} :
|
||||
ToForwardSearcher.toSearcher pat s = ToForwardSearcher.toSearcher pat.toSlice s := (rfl)
|
||||
|
||||
theorem isValidSearchFrom_iff_isValidSearchFrom_toSlice {pat : String}
|
||||
{s : Slice} {pos : s.Pos} {l : List (SearchStep s)} :
|
||||
IsValidSearchFrom pat pos l ↔ IsValidSearchFrom pat.toSlice pos l := by
|
||||
refine ⟨fun h => ?_, fun h => ?_⟩
|
||||
· induction h with
|
||||
| endPos => simpa using IsValidSearchFrom.endPos
|
||||
| matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
|
||||
| mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_toSlice]
|
||||
· induction h with
|
||||
| endPos => simpa using IsValidSearchFrom.endPos
|
||||
| matched => simp_all [IsValidSearchFrom.matched, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
|
||||
| mismatched => simp_all [IsValidSearchFrom.mismatched, matchesAt_iff_matchesAt_toSlice]
|
||||
|
||||
end ForwardStringSearcher
|
||||
|
||||
|
|
|
|||
|
|
@ -8,7 +8,10 @@ module
|
|||
prelude
|
||||
public import Init.Data.String.Lemmas.Pattern.String.Basic
|
||||
public import Init.Data.String.Pattern.String
|
||||
public import Init.Data.String.Slice
|
||||
import all Init.Data.String.Pattern.String
|
||||
import all Init.Data.String.Slice
|
||||
import Init.Data.String.Lemmas.Pattern.Pred
|
||||
import Init.Data.String.Lemmas.Pattern.Memcmp
|
||||
import Init.Data.String.Lemmas.Basic
|
||||
import Init.Data.ByteArray.Lemmas
|
||||
|
|
@ -86,4 +89,104 @@ public theorem lawfulForwardPatternModel {pat : String} (hpat : pat ≠ "") :
|
|||
|
||||
end Model.ForwardStringSearcher
|
||||
|
||||
end String.Slice.Pattern
|
||||
end Pattern
|
||||
|
||||
public theorem startsWith_string_eq_startsWith_toSlice {pat : String} {s : Slice} :
|
||||
s.startsWith pat = s.startsWith pat.toSlice := (rfl)
|
||||
|
||||
public theorem dropPrefix?_string_eq_dropPrefix?_toSlice {pat : String} {s : Slice} :
|
||||
s.dropPrefix? pat = s.dropPrefix? pat.toSlice := (rfl)
|
||||
|
||||
public theorem dropPrefix_string_eq_dropPrefix_toSlice {pat : String} {s : Slice} :
|
||||
s.dropPrefix pat = s.dropPrefix pat.toSlice := (rfl)
|
||||
|
||||
public theorem Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice
|
||||
{pat : String} {s : Slice} :
|
||||
dropPrefix? pat s = dropPrefix? pat.toSlice s := (rfl)
|
||||
|
||||
private theorem dropWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
|
||||
dropWhile.go s pat curr = dropWhile.go s pat.toSlice curr := by
|
||||
fun_induction dropWhile.go s pat curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [dropWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice]
|
||||
|
||||
public theorem dropWhile_string_eq_dropWhile_toSlice {pat : String} {s : Slice} :
|
||||
s.dropWhile pat = s.dropWhile pat.toSlice := by
|
||||
simpa only [dropWhile] using dropWhileGo_string_eq s.startPos
|
||||
|
||||
private theorem takeWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
|
||||
takeWhile.go s pat curr = takeWhile.go s pat.toSlice curr := by
|
||||
fun_induction takeWhile.go s pat curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [takeWhile.go]
|
||||
simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice]
|
||||
|
||||
public theorem takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice} :
|
||||
s.takeWhile pat = s.takeWhile pat.toSlice := by
|
||||
simp only [takeWhile]; exact takeWhileGo_string_eq s.startPos
|
||||
|
||||
public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} :
|
||||
s.all pat = s.all pat.toSlice := by
|
||||
simp only [all, dropWhile_string_eq_dropWhile_toSlice]
|
||||
|
||||
public theorem endsWith_string_eq_endsWith_toSlice {pat : String} {s : Slice} :
|
||||
s.endsWith pat = s.endsWith pat.toSlice := (rfl)
|
||||
|
||||
public theorem dropSuffix?_string_eq_dropSuffix?_toSlice {pat : String} {s : Slice} :
|
||||
s.dropSuffix? pat = s.dropSuffix? pat.toSlice := (rfl)
|
||||
|
||||
public theorem dropSuffix_string_eq_dropSuffix_toSlice {pat : String} {s : Slice} :
|
||||
s.dropSuffix pat = s.dropSuffix pat.toSlice := (rfl)
|
||||
|
||||
public theorem Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice
|
||||
{pat : String} {s : Slice} :
|
||||
dropSuffix? pat s = dropSuffix? pat.toSlice s := (rfl)
|
||||
|
||||
private theorem dropEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
|
||||
dropEndWhile.go s pat curr = dropEndWhile.go s pat.toSlice curr := by
|
||||
fun_induction dropEndWhile.go s pat curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [dropEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice]
|
||||
|
||||
public theorem dropEndWhile_string_eq_dropEndWhile_toSlice {pat : String} {s : Slice} :
|
||||
s.dropEndWhile pat = s.dropEndWhile pat.toSlice := by
|
||||
simpa only [dropEndWhile] using dropEndWhileGo_string_eq s.endPos
|
||||
|
||||
private theorem takeEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
|
||||
takeEndWhile.go s pat curr = takeEndWhile.go s pat.toSlice curr := by
|
||||
fun_induction takeEndWhile.go s pat curr with
|
||||
| case1 pos nextCurr h₁ h₂ ih =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih]
|
||||
| case2 pos nextCurr h ih =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih]
|
||||
| case3 pos h =>
|
||||
conv => rhs; rw [takeEndWhile.go]
|
||||
simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice]
|
||||
|
||||
public theorem takeEndWhile_string_eq_takeEndWhile_toSlice {pat : String} {s : Slice} :
|
||||
s.takeEndWhile pat = s.takeEndWhile pat.toSlice := by
|
||||
simpa only [takeEndWhile] using takeEndWhileGo_string_eq s.endPos
|
||||
|
||||
end String.Slice
|
||||
|
|
|
|||
|
|
@ -8,6 +8,10 @@ module
|
|||
prelude
|
||||
public import Init.Data.String.Lemmas.Pattern.String.Basic
|
||||
public import Init.Data.String.Pattern.String
|
||||
public import Init.Data.String.Slice
|
||||
public import Init.Data.String.Search
|
||||
import all Init.Data.String.Slice
|
||||
import all Init.Data.String.Search
|
||||
import all Init.Data.String.Pattern.String
|
||||
import Init.Data.String.Lemmas.IsEmpty
|
||||
import Init.Data.Vector.Lemmas
|
||||
|
|
@ -435,7 +439,6 @@ theorem Invariants.of_prefixFunction_eq {pat s : Slice} {stackPos needlePos : St
|
|||
rw [Nat.sub_add_cancel (by simp at h'; omega)] at this
|
||||
exact hk ▸ (h.partialMatch.partialMatch_iff.1 this).2
|
||||
|
||||
set_option backward.isDefEq.respectTransparency false in
|
||||
theorem Invariants.isValidSearchFrom_toList {pat s : Slice} {stackPos needlePos : String.Pos.Raw}
|
||||
(it : Std.Iter (α := ForwardSliceSearcher s) (SearchStep s))
|
||||
(h : Invariants pat s needlePos stackPos)
|
||||
|
|
@ -600,30 +603,11 @@ end ForwardSliceSearcher
|
|||
|
||||
namespace ForwardStringSearcher
|
||||
|
||||
private theorem isValidSearchFrom_iff_slice {pat : String} {s : Slice} {pos : s.Pos}
|
||||
{l : List (SearchStep s)} :
|
||||
IsValidSearchFrom (ρ := String) pat pos l ↔
|
||||
IsValidSearchFrom (ρ := Slice) pat.toSlice pos l := by
|
||||
constructor
|
||||
· intro h
|
||||
induction h with
|
||||
| endPos => exact .endPos
|
||||
| matched hm _ ih => exact .matched (isLongestMatchAt_iff_slice.1 hm) ih
|
||||
| mismatched hlt hnm _ ih =>
|
||||
exact .mismatched hlt (fun p hp₁ hp₂ hm => hnm p hp₁ hp₂ (matchesAt_iff_slice.2 hm)) ih
|
||||
· intro h
|
||||
induction h with
|
||||
| endPos => exact .endPos
|
||||
| matched hm _ ih => exact .matched (isLongestMatchAt_iff_slice.2 hm) ih
|
||||
| mismatched hlt hnm _ ih =>
|
||||
exact .mismatched hlt (fun p hp₁ hp₂ hm => hnm p hp₁ hp₂ (matchesAt_iff_slice.1 hm)) ih
|
||||
|
||||
public theorem lawfulToForwardSearcherModel {pat : String} (hpat : pat ≠ "") :
|
||||
LawfulToForwardSearcherModel pat where
|
||||
isValidSearchFrom_toList s :=
|
||||
isValidSearchFrom_iff_slice.2
|
||||
((ForwardSliceSearcher.lawfulToForwardSearcherModel
|
||||
(by rwa [isEmpty_toSlice, isEmpty_eq_false_iff])).isValidSearchFrom_toList s)
|
||||
isValidSearchFrom_toList s := by
|
||||
simpa [toSearcher_eq, isValidSearchFrom_iff_isValidSearchFrom_toSlice] using
|
||||
(ForwardSliceSearcher.lawfulToForwardSearcherModel (by simpa)).isValidSearchFrom_toList (pat := pat.toSlice) (s := s)
|
||||
|
||||
public theorem toSearcher_empty (s : Slice) : ToForwardSearcher.toSearcher "" s =
|
||||
Std.Iter.mk (.emptyBefore s.startPos : ForwardSliceSearcher s) := by
|
||||
|
|
@ -632,4 +616,18 @@ public theorem toSearcher_empty (s : Slice) : ToForwardSearcher.toSearcher "" s
|
|||
|
||||
end ForwardStringSearcher
|
||||
|
||||
end String.Slice.Pattern.Model
|
||||
end Pattern.Model
|
||||
|
||||
public theorem contains_string_eq_contains_toSlice {pat : String} {s : Slice} :
|
||||
s.contains pat = s.contains pat.toSlice :=
|
||||
(rfl)
|
||||
|
||||
public theorem find?_string_eq_find?_toSlice {pat : String} {s : Slice} :
|
||||
s.find? pat = s.find? pat.toSlice :=
|
||||
(rfl)
|
||||
|
||||
public theorem Pos.find?_string_eq_find?_toSlice {pat : String} {s : Slice} {p : s.Pos} :
|
||||
p.find? pat = p.find? pat.toSlice :=
|
||||
(rfl)
|
||||
|
||||
end String.Slice
|
||||
|
|
|
|||
|
|
@ -6,12 +6,7 @@ Authors: Henrik Böving, Markus Himmel
|
|||
module
|
||||
|
||||
prelude
|
||||
public import Init.Data.String.Pattern.Basic
|
||||
import Init.Data.String.Lemmas.FindPos
|
||||
import Init.Data.String.Termination
|
||||
import Init.Data.String.Lemmas.IsEmpty
|
||||
import Init.Data.String.Lemmas.Order
|
||||
import Init.Data.Option.Lemmas
|
||||
public import Init.Data.String.Pattern.Pred
|
||||
|
||||
set_option doc.verso true
|
||||
|
||||
|
|
@ -26,75 +21,31 @@ namespace String.Slice.Pattern
|
|||
namespace Char
|
||||
|
||||
instance {c : Char} : ForwardPattern c where
|
||||
dropPrefixOfNonempty? s h :=
|
||||
if s.startPos.get (by exact Slice.startPos_ne_endPos h) = c then
|
||||
some (s.startPos.next (by exact Slice.startPos_ne_endPos h))
|
||||
else
|
||||
none
|
||||
dropPrefix? s :=
|
||||
if h : s.startPos = s.endPos then
|
||||
none
|
||||
else if s.startPos.get h = c then
|
||||
some (s.startPos.next h)
|
||||
else
|
||||
none
|
||||
startsWith s :=
|
||||
if h : s.startPos = s.endPos then
|
||||
false
|
||||
else
|
||||
s.startPos.get h = c
|
||||
dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (· == c) s h
|
||||
dropPrefix? s := ForwardPattern.dropPrefix? (· == c) s
|
||||
startsWith s := ForwardPattern.startsWith (· == c) s
|
||||
|
||||
instance {c : Char} : StrictForwardPattern c where
|
||||
ne_startPos {s h q} := by
|
||||
simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some,
|
||||
Option.some.injEq, ne_eq, and_imp]
|
||||
rintro _ rfl
|
||||
simp
|
||||
ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (· == c)) h q
|
||||
|
||||
instance {c : Char} : LawfulForwardPattern c where
|
||||
dropPrefixOfNonempty?_eq {s h} := by
|
||||
simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?,
|
||||
Slice.startPos_eq_endPos_iff, h]
|
||||
startsWith_eq {s} := by
|
||||
simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?]
|
||||
split <;> (try split) <;> simp_all
|
||||
dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (· == c)) h
|
||||
startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (· == c)) s
|
||||
|
||||
instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher c) :=
|
||||
.defaultImplementation
|
||||
instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher (· == c)) where
|
||||
toSearcher s := ToForwardSearcher.toSearcher (· == c) s
|
||||
|
||||
instance {c : Char} : BackwardPattern c where
|
||||
dropSuffixOfNonempty? s h :=
|
||||
if (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h))).get (by simp) = c then
|
||||
some (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h)))
|
||||
else
|
||||
none
|
||||
dropSuffix? s :=
|
||||
if h : s.endPos = s.startPos then
|
||||
none
|
||||
else if (s.endPos.prev h).get (by simp) = c then
|
||||
some (s.endPos.prev h)
|
||||
else
|
||||
none
|
||||
endsWith s :=
|
||||
if h : s.endPos = s.startPos then
|
||||
false
|
||||
else
|
||||
(s.endPos.prev h).get (by simp) = c
|
||||
dropSuffixOfNonempty? s h := BackwardPattern.dropSuffixOfNonempty? (· == c) s h
|
||||
dropSuffix? s := BackwardPattern.dropSuffix? (· == c) s
|
||||
endsWith s := BackwardPattern.endsWith (· == c) s
|
||||
|
||||
instance {c : Char} : StrictBackwardPattern c where
|
||||
ne_endPos {s h q} := by
|
||||
simp only [BackwardPattern.dropSuffixOfNonempty?, Option.ite_none_right_eq_some,
|
||||
Option.some.injEq, ne_eq, and_imp]
|
||||
rintro _ rfl
|
||||
simp
|
||||
ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (· == c)) h q
|
||||
|
||||
instance {c : Char} : LawfulBackwardPattern c where
|
||||
dropSuffixOfNonempty?_eq {s h} := by
|
||||
simp [BackwardPattern.dropSuffixOfNonempty?, BackwardPattern.dropSuffix?,
|
||||
Eq.comm (a := s.endPos), Slice.startPos_eq_endPos_iff, h]
|
||||
endsWith_eq {s} := by
|
||||
simp only [BackwardPattern.endsWith, BackwardPattern.dropSuffix?]
|
||||
split <;> (try split) <;> simp_all
|
||||
dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (· == c)) h
|
||||
endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (· == c)) s
|
||||
|
||||
instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) :=
|
||||
.defaultImplementation
|
||||
|
|
|
|||
|
|
@ -81,8 +81,8 @@ instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p where
|
|||
dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (decide <| p ·)) h
|
||||
startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (decide <| p ·)) s
|
||||
|
||||
instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher p) :=
|
||||
.defaultImplementation
|
||||
instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher (decide <| p ·)) where
|
||||
toSearcher s := ToForwardSearcher.toSearcher (decide <| p ·) s
|
||||
|
||||
end Decidable
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue