From fda375de3f3ddf0d2611d9db4b9004e14d92ca06 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 12 Feb 2024 23:27:35 +0900 Subject: [PATCH 1/4] feat: add lemmas about `Nat.add` and `Nat.le` --- Batteries/Data/Nat/Lemmas.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean index 7fa93705f7..bb0d7d53ff 100644 --- a/Batteries/Data/Nat/Lemmas.lean +++ b/Batteries/Data/Nat/Lemmas.lean @@ -149,6 +149,18 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a := | .eq => .inr (.inl (Nat.compare_eq_eq.1 h)) | .gt => .inr (.inr (Nat.compare_eq_gt.1 h)) +/-! ## add -/ + +protected theorem add_left_le_self {n m : Nat} : n + m ≤ m ↔ n = 0 := by + conv => lhs; rhs; rw [← Nat.zero_add m] + rw [Nat.add_le_add_iff_right] + apply Nat.le_zero + +protected theorem add_right_le_self {n m : Nat} : n + m ≤ n ↔ m = 0 := by + conv => lhs; rhs; rw [← Nat.add_zero n] + rw [Nat.add_le_add_iff_left] + apply Nat.le_zero + /-! ### div/mod -/ -- TODO mod_core_congr, mod_def From 3101dcd916266bf301d7dd72038ff755d13a0865 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 18 Mar 2024 16:27:14 +0900 Subject: [PATCH 2/4] feat: add lemmas about lists I need these lemmas to prove `String.splitOn_of_valid`. --- Batteries/Data/List/Lemmas.lean | 55 +++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 6a956f9b1d..e8e7df7da2 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -19,6 +19,16 @@ namespace List @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff +/-! ### head -/ + +theorem headD_eq_head : ∀ (l : List α) {a₀ : α} (hne : l ≠ []), headD l a₀ = head l hne + | _::_, _, _ => rfl + +/-! ### head and tail -/ + +theorem head_cons_tail : ∀ (l : List α) (hne : l ≠ []), l.head hne :: l.tail = l + | _::_, _ => rfl + /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl @@ -54,6 +64,10 @@ theorem get?_inj /-! ### modifyHead -/ +theorem modifyHead_id : ∀ (l : List α), l.modifyHead id = l + | [] => rfl + | _::_ => rfl + @[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) : (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead] @@ -482,6 +496,47 @@ theorem Sublist.erase_diff_erase_sublist {a : α} : end Diff +/-! ### prefix, suffix, infix -/ + +theorem IsInfix.length_lt_of_ne (hin : l₁ <:+: l₂) (hne : l₁ ≠ l₂) : l₁.length < l₂.length := + Nat.lt_of_le_of_ne (IsInfix.length_le hin) (mt (IsInfix.eq_of_length hin) hne) + +theorem IsPrefix.length_lt_of_ne (hpf : l₁ <+: l₂) (hne : l₁ ≠ l₂) : l₁.length < l₂.length := + Nat.lt_of_le_of_ne (IsPrefix.length_le hpf) (mt (IsPrefix.eq_of_length hpf) hne) + +theorem IsSuffix.length_lt_of_ne (hsf : l₁ <:+ l₂) (hne : l₁ ≠ l₂) : l₁.length < l₂.length := + Nat.lt_of_le_of_ne (IsSuffix.length_le hsf) (mt (IsSuffix.eq_of_length hsf) hne) + +theorem eq_of_cons_prefix_cons (h : a :: l₁ <+: b :: l₂) : a = b := + (cons_prefix_cons.mp h).1 + +theorem head_eq_head_of_prefix (hl₁ : l₁ ≠ []) (hl₂ : l₂ ≠ []) (h : l₁ <+: l₂) : + l₁.head hl₁ = l₂.head hl₂ := by + obtain ⟨a, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil hl₁ + obtain ⟨b, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil hl₂ + simp [eq_of_cons_prefix_cons h, head_cons] + +theorem tail_prefix_tail_of_prefix (hl₁ : l₁ ≠ []) (hl₂ : l₂ ≠ []) (h : l₁ <+: l₂) : + l₁.tail <+: l₂.tail := by + have heq := head_eq_head_of_prefix hl₁ hl₂ h + let ⟨t, ht⟩ := h + rw [← head_cons_tail l₁ hl₁, ← head_cons_tail l₂ hl₂, ← heq] at ht + simp only [cons_append, cons.injEq, true_and] at ht + exact ⟨t, ht⟩ + +theorem prefix_iff_head_eq_and_tail_prefix (hl₁ : l₁ ≠ []) (hl₂ : l₂ ≠ []) : + l₁ <+: l₂ ↔ l₁.head hl₁ = l₂.head hl₂ ∧ l₁.tail <+: l₂.tail := by + constructor <;> intro h + · exact ⟨head_eq_head_of_prefix hl₁ hl₂ h, tail_prefix_tail_of_prefix hl₁ hl₂ h⟩ + · let ⟨t, ht⟩ := h.2 + exists t + rw [← head_cons_tail l₁ hl₁, ← head_cons_tail l₂ hl₂] + simpa [h.1] + +theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by + intro heq + simp [heq, nil_prefix] at h + /-! ### drop -/ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n) From 4d97a5bc774099582a892874a152e46c51d1d51d Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 18 Mar 2024 16:30:41 +0900 Subject: [PATCH 3/4] feat: add `Batteries.Data.List.SplitOnList` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `List.splitOnceP` returns `(l₁, l₂)` for the first split `l = l₁ ++ l₂` such that `P l₂` returns true. * `List.splitOnList` splits a list at every occurrence of a separator list. The separators are not in the result. * `List.splitOnListAux` is an auxiliary definition for proving `String.splitOnAux_of_valid`. Co-authored-by: Mario Carneiro Co-authored-by: Kim Morrison --- Batteries/Data/List.lean | 1 + Batteries/Data/List/SplitOnList.lean | 281 +++++++++++++++++++++++++++ 2 files changed, 282 insertions(+) create mode 100644 Batteries/Data/List/SplitOnList.lean diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean index f93f90a6c2..c55d917d3a 100644 --- a/Batteries/Data/List.lean +++ b/Batteries/Data/List.lean @@ -6,3 +6,4 @@ import Batteries.Data.List.Lemmas import Batteries.Data.List.OfFn import Batteries.Data.List.Pairwise import Batteries.Data.List.Perm +import Batteries.Data.List.SplitOnList diff --git a/Batteries/Data/List/SplitOnList.lean b/Batteries/Data/List/SplitOnList.lean new file mode 100644 index 0000000000..fd83f0c002 --- /dev/null +++ b/Batteries/Data/List/SplitOnList.lean @@ -0,0 +1,281 @@ +/- +Copyright (c) 2024 Bulhwi Cha, Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bulhwi Cha, Mario Carneiro +-/ +import Batteries.Data.List.Lemmas +import Batteries.Tactic.SeqFocus + +/-! +# `List.splitOnList` + +This file introduces the `List.splitOnList` function, which is a specification for `String.splitOn`. +We need it to prove `String.splitOn_of_valid` in `Batteries.Data.String.Lemmas`. +``` +[1, 1, 2, 3, 2, 4, 4].splitOnList [] = [[1, 1, 2, 3, 2, 4, 4]] +[1, 1, 2, 3, 2, 4, 4].splitOnList [5, 6] = [[1, 1, 2, 3, 2, 4, 4]] +[1, 1, 2, 3, 2, 4, 4].splitOnList [2, 3] = [[1, 1], [2, 4, 4]] +``` +-/ + +namespace List + +/-- Returns `(l₁, l₂)` for the first split `l = l₁ ++ l₂` such that `P l₂` returns true. -/ +def splitOnceRightP (P : List α → Bool) (l : List α) : Option (List α × List α) := + if P l then + some ([], l) + else + match l with + | [] => none + | a::l => (splitOnceRightP P l).map fun (l, r) => (a :: l, r) + +theorem splitOnceRightP_of_P {P : List α → Bool} {l} (h : P l) : + splitOnceRightP P l = some ([], l) := by + unfold splitOnceRightP + simp [h] + +theorem splitOnceRightP_nil (P : List α → Bool) : + splitOnceRightP P [] = if P [] then some ([], []) else none := + rfl + +theorem splitOnceRightP_of_ne_nil_of_not_P {P : List α → Bool} {l} (hne : l ≠ []) (hnp : ¬P l) : + splitOnceRightP P l = (splitOnceRightP P l.tail).map fun (lf, rt) => (l.head hne :: lf, rt) := + by + obtain ⟨a, l, rfl⟩ := exists_cons_of_ne_nil hne + conv => lhs; unfold splitOnceRightP + simp [hnp] + +theorem eq_append_of_splitOnceRightP {P : List α → Bool} {l} : + ∀ l₁ l₂, splitOnceRightP P l = some (l₁, l₂) → l = l₁ ++ l₂ := by + induction l with + | nil => simp [splitOnceRightP] + | cons a l ih => + if h : P (a :: l) then + simp [splitOnceRightP, h] + else + simp only [splitOnceRightP, h] + match e : splitOnceRightP P l with + | none => simp + | some (lf, rt) => simp; apply ih; assumption + +theorem P_of_splitOnceRightP {P : List α → Bool} {l} : + ∀ l₁ l₂, splitOnceRightP P l = some (l₁, l₂) → P l₂ := by + induction l with + | nil => + simp only [splitOnceRightP, Option.ite_none_right_eq_some, Option.some.injEq, Prod.mk.injEq, + nil_eq, and_imp] + intro _l₁ l₂ hp _hl₁ hl₂ + rwa [hl₂] + | cons a l ih => + if h : P (a :: l) then + simp [splitOnceRightP, h] + else + simp only [splitOnceRightP, h] + match e : splitOnceRightP P l with + | none => simp + | some (lf, rt) => simp; apply ih; assumption + +theorem splitOnceRightP_isPrefixOf_eq_none_of_length_lt [BEq α] [LawfulBEq α] {l sep : List α} + (h : l.length < sep.length) : splitOnceRightP sep.isPrefixOf l = none := by + have not_isPrefixOf_of_length_lt {l} (h : l.length < sep.length) : ¬sep.isPrefixOf l := by + simp [mt IsPrefix.length_le (Nat.not_le_of_lt h)] + induction l with + | nil => unfold splitOnceRightP; simp [not_isPrefixOf_of_length_lt h] + | cons a l ih => + unfold splitOnceRightP + simp only [not_isPrefixOf_of_length_lt h, Bool.false_eq_true, ↓reduceIte, Option.map_eq_none'] + have h' : l.length < sep.length := + calc + l.length < (a :: l).length := by simp + _ < sep.length := h + exact ih h' + +/-- +Split a list at every occurrence of a separator list. The separators are not in the result. +``` +[1, 1, 2, 3, 2, 4, 4].splitOnList [] = [[1, 1, 2, 3, 2, 4, 4]] +[1, 1, 2, 3, 2, 4, 4].splitOnList [5, 6] = [[1, 1, 2, 3, 2, 4, 4]] +[1, 1, 2, 3, 2, 4, 4].splitOnList [2, 3] = [[1, 1], [2, 4, 4]] +``` +-/ +def splitOnList [BEq α] [LawfulBEq α] (l sep : List α) : List (List α) := + if _h : sep.isEmpty then + [l] + else + match _e : splitOnceRightP sep.isPrefixOf l with + | none => [l] + | some (l₁, l₂) => l₁ :: splitOnList (l₂.drop sep.length) sep +termination_by l.length +decreasing_by + simp_wf + rw [eq_append_of_splitOnceRightP l₁ l₂ _e, length_append] + calc + l₂.length - sep.length < l₂.length := Nat.sub_lt_self (by simp [length_pos, ← isEmpty_iff, _h]) + (IsPrefix.length_le <| isPrefixOf_iff_prefix.mp (P_of_splitOnceRightP l₁ l₂ _e)) + _ ≤ l₁.length + l₂.length := Nat.le_add_left .. + +variable [BEq α] [LawfulBEq α] + +theorem splitOnList_nil_left (sep : List α) : splitOnList [] sep = [[]] := by + cases sep <;> unfold splitOnList <;> rfl + +theorem splitOnList_nil_right (l : List α) : splitOnList l [] = [l] := by + simp [splitOnList] + +theorem splitOnList_append_append_of_isPrefixOf {l : List α} (sep₁) {sep₂} (hsp₂ : sep₂ ≠ []) + (hpf : sep₂.isPrefixOf l) : + splitOnList (sep₁ ++ l) (sep₁ ++ sep₂) = + [] :: splitOnList (l.drop sep₂.length) (sep₁ ++ sep₂) := by + have hnem : ¬(sep₁ ++ sep₂).isEmpty := by simp [isEmpty_iff, hsp₂] + have hpf' : (sep₁ ++ sep₂).isPrefixOf (sep₁ ++ l) := by simpa [prefix_append_right_inj] using hpf + conv => lhs; unfold splitOnList + simp only [hnem, ↓reduceDIte, length_append] + rw [splitOnceRightP_of_P hpf'] + simp [drop_append] + +theorem splitOnList_of_isPrefixOf {l sep : List α} (hsp : sep ≠ []) (hpf : sep.isPrefixOf l) : + splitOnList l sep = [] :: splitOnList (l.drop sep.length) sep := + splitOnList_append_append_of_isPrefixOf [] hsp hpf + +theorem splitOnList_refl_of_ne_nil (l : List α) (h : l ≠ []) : splitOnList l l = [[], []] := by + have hpf : l.isPrefixOf l := isPrefixOf_iff_prefix.mpr (prefix_refl l) + simp [splitOnList_of_isPrefixOf h hpf, splitOnList_nil_left] + +theorem splitOnList_of_ne_nil_of_not_isPrefixOf {l sep : List α} (hne : l ≠ []) + (hnpf : ¬sep.isPrefixOf l) : + splitOnList l sep = modifyHead (l.head hne :: ·) (splitOnList l.tail sep) := by + unfold splitOnList + obtain ⟨a, sep, rfl⟩ := exists_cons_of_ne_nil <| ne_nil_of_not_prefix <| + mt isPrefixOf_iff_prefix.mpr hnpf + simp only [isEmpty_cons, ↓reduceDIte] + rw [splitOnceRightP_of_ne_nil_of_not_P hne hnpf] + match splitOnceRightP (a::sep).isPrefixOf l.tail with + | none => simp [head_cons_tail] + | some (lf, rt) => rfl + +theorem splitOnList_eq_singleton_of_length_lt {l sep : List α} (h : l.length < sep.length) : + splitOnList l sep = [l] := by + have hne : ¬sep.isEmpty := by + simpa [isEmpty_iff, length_pos] using Nat.lt_of_le_of_lt (Nat.zero_le l.length) h + unfold splitOnList + simp only [hne, Bool.false_eq_true, ↓reduceDIte] + rw [splitOnceRightP_isPrefixOf_eq_none_of_length_lt h] + +variable [DecidableEq α] + +/-- An alternative definition of `splitOnList`. -/ +theorem splitOnList_def (l sep : List α) : + splitOnList l sep = + if h : l = [] ∨ sep = [] then + [l] + else if sep.isPrefixOf l then + [] :: splitOnList (l.drop sep.length) sep + else + modifyHead (l.head (not_or.mp h).1 :: ·) (splitOnList l.tail sep) := by + split + · next h => + match h with + | .inl hls => rw [hls, splitOnList_nil_left] + | .inr hsp => rw [hsp, splitOnList_nil_right] + · next h => + let ⟨hls, hsp⟩ := not_or.mp h + split <;> rename_i hpf + · exact splitOnList_of_isPrefixOf hsp hpf + · exact splitOnList_of_ne_nil_of_not_isPrefixOf hls hpf + +/-- +Auxiliary definition for proving `String.splitOnAux_of_valid`. + +* `sep₁ ++ l`: the list with elements of the type `α` that `splitOnListAux` will split. +* `sep₁ ++ sep₂`: the separator. The list will be split on occurrences of this. +* `sep₁`: the common prefix of the list and the separator. +* `l`: the latter part of the list. +* `sep₂`: the latter part of the separator. +-/ +def splitOnListAux (l sep₁ sep₂ : List α) (h : sep₂ ≠ []) : List (List α) := + if hls : l = [] then + [sep₁] + else + if l.head hls = sep₂.head h then + if htl₂ : sep₂.tail = [] then + [] :: splitOnListAux l.tail [] (sep₁ ++ [sep₂.head h]) (by simp) + else + splitOnListAux l.tail (sep₁ ++ [l.head hls]) sep₂.tail htl₂ + else + modifyHead ((sep₁ ++ l).head (by simp [hls]) :: ·) <| splitOnListAux (sep₁ ++ l).tail [] + (sep₁ ++ sep₂) (by simp [h]) +termination_by (sep₁.length + l.length, sep₂.length) +decreasing_by + all_goals simp_wf + · left; calc + l.length - 1 < l.length := Nat.pred_lt (mt length_eq_zero.mp hls) + _ ≤ sep₁.length + l.length := Nat.le_add_left .. + · have heq : sep₁.length + 1 + (l.length - 1) = sep₁.length + l.length := by + rw [← Nat.add_sub_assoc (show 1 ≤ l.length from length_pos.mpr hls), Nat.add_right_comm, + Nat.add_sub_cancel] + rw [heq]; clear heq + right + exact Nat.pred_lt (mt length_eq_zero.mp h) + · left + apply Nat.pred_lt; show ¬length sep₁ + length l = 0 + rw [Nat.add_eq_zero_iff, length_eq_zero (l := l)] + exact not_and_of_not_right _ hls + +theorem splitOnListAux_eq_splitOnList_append_append (l sep₁ sep₂ : List α) (h : sep₂ ≠ []) : + splitOnListAux l sep₁ sep₂ h = splitOnList (sep₁ ++ l) (sep₁ ++ sep₂) := by + rw [splitOnListAux] + split + · next hls => + simp only [hls, append_nil] + rw [splitOnList_eq_singleton_of_length_lt] + exact IsPrefix.length_lt_of_ne (prefix_append ..) (Ne.symm <| mt append_right_eq_self.mp h) + · next hls => + split + · next hhd => + split + · next htl₂ => + conv => rhs; rw [← head_cons_tail sep₂ h, htl₂] + have hpf : (sep₁ ++ [sep₂.head h]).isPrefixOf (sep₁ ++ l) := by + rw [← head_cons_tail l hls, hhd, isPrefixOf_iff_prefix, append_cons _ _ l.tail] + apply prefix_append + have hdr : (sep₁ ++ [sep₂.head h] ++ l.tail).drop (sep₁ ++ [sep₂.head h]).length = l.tail := + drop_append 0 + simp only [splitOnList_of_isPrefixOf (by simp) hpf, cons.injEq, true_and] + conv => rhs; arg 1; arg 2; rw [← head_cons_tail l hls, hhd, append_cons] + rw [hdr] + exact splitOnListAux_eq_splitOnList_append_append l.tail [] (sep₁++[sep₂.head h]) (by simp) + · next htl₂ => + have ih := splitOnListAux_eq_splitOnList_append_append l.tail (sep₁++[l.head hls]) sep₂.tail + htl₂ + simp only [append_assoc, singleton_append, head_cons_tail] at ih + conv at ih => rhs; arg 2; rw [hhd, head_cons_tail] + exact ih + · next hhd => + have hnpf : ¬isPrefixOf (sep₁ ++ sep₂) (sep₁ ++ l) := by + rw [isPrefixOf_iff_prefix, prefix_append_right_inj, prefix_iff_head_eq_and_tail_prefix h + hls] + exact not_and_of_not_left _ (Ne.symm hhd) + rw [splitOnList_of_ne_nil_of_not_isPrefixOf (by simp [hls]) hnpf] + apply congrArg + exact splitOnListAux_eq_splitOnList_append_append (sep₁++l).tail [] (sep₁++sep₂) (by simp [h]) +termination_by (sep₁.length + l.length, sep₂.length) +decreasing_by + all_goals simp_wf + · rename_i _₀ _₁ _₂ _₃ _₄ _₅ hls _hhd; clear _₀ _₁ _₂ _₃ _₄ _₅ + left + rw [Nat.add_sub_assoc (show 1 ≤ l.length from length_pos.mpr hls), Nat.add_lt_add_iff_left] + exact Nat.pred_lt (mt length_eq_zero.mp hls) + · rename_i _₀ _₁ _₂ _₃ _₄ _₅ hls _hhd _htl₂; clear _₀ _₁ _₂ _₃ _₄ _₅ + have heq : sep₁.length + 1 + (l.length - 1) = sep₁.length + l.length := by + rw [← Nat.add_sub_assoc (show 1 ≤ l.length from length_pos.mpr hls), Nat.add_right_comm, + Nat.add_sub_cancel] + rw [heq]; clear heq + right + exact Nat.pred_lt (mt length_eq_zero.mp h) + · rename_i _₀ _₁ _₂ _₃ _₄ _₅ hls _hhd _htl₂; clear _₀ _₁ _₂ _₃ _₄ _₅ + left + calc + l.length - 1 < l.length := Nat.pred_lt (mt length_eq_zero.mp hls) + l.length ≤ sep₁.length + l.length := Nat.le_add_left .. + +end List From 2292378911f64cda6663cdecbe8b8b9df0af124b Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Tue, 3 Sep 2024 14:41:52 +0900 Subject: [PATCH 4/4] feat: add `String.splitOn_of_valid` Add `String.splitOnAux_of_valid` and `String.splitOn_of_valid`. --- Batteries/Data/String/Lemmas.lean | 82 ++++++++++++++++++++++++++++++- 1 file changed, 80 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean index 490c34908b..19f18d7f2b 100644 --- a/Batteries/Data/String/Lemmas.lean +++ b/Batteries/Data/String/Lemmas.lean @@ -3,8 +3,10 @@ Copyright (c) 2023 Bulhwi Cha. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bulhwi Cha, Mario Carneiro -/ +import Batteries.Logic import Batteries.Data.Char -import Batteries.Data.List.Lemmas +import Batteries.Data.Nat.Lemmas +import Batteries.Data.List.SplitOnList import Batteries.Data.String.Basic import Batteries.Tactic.Lint.Misc import Batteries.Tactic.SeqFocus @@ -440,7 +442,83 @@ theorem splitAux_of_valid (p l m r acc) : theorem split_of_valid (s p) : split s p = (List.splitOnP p s.1).map mk := by simpa [split] using splitAux_of_valid p [] [] s.1 [] --- TODO: splitOn +theorem splitOnAux_of_valid (sep₁ sep₂ l m r acc) (h : sep₂ ≠ []) : + splitOnAux ⟨l ++ m ++ sep₁ ++ r⟩ ⟨sep₁ ++ sep₂⟩ ⟨utf8Len l⟩ ⟨utf8Len (l ++ m ++ sep₁)⟩ + ⟨utf8Len sep₁⟩ acc = + acc.reverse ++ (List.modifyHead (m ++ ·) <| List.splitOnListAux r sep₁ sep₂ h).map mk := by + obtain ⟨c₂, sep₂, rfl⟩ := sep₂.exists_cons_of_ne_nil h + rw [splitOnAux, List.splitOnListAux] + simp only [List.append_assoc, utf8Len_append, atEnd_iff, endPos_eq, Pos.mk_le_mk, + Nat.add_le_add_iff_left, Nat.add_right_le_self, utf8Len_eq_zero, by simpa only + [List.append_assoc, utf8Len_append] using (⟨get_of_valid (l++m++sep₁) r, next_of_valid + (l++m++sep₁) (r.headD default) r, extract_of_valid l (m++sep₁) r⟩ : _∧_∧_), List.reverse_cons, + get_of_valid, List.headD_cons, beq_iff_eq, next, Pos.addChar_eq, utf8Len_cons, + Nat.add_left_le_self, Pos.sub_eq, dite_eq_ite] + split + · simp + · next hls => + obtain ⟨cᵣ, r, rfl⟩ := r.exists_cons_of_ne_nil hls + simp only [List.headD_cons, List.head_cons, List.tail_cons, false_or] + split + · next hc => + subst c₂ + rw [← Nat.add_assoc, Nat.add_assoc, Nat.add_sub_cancel, Nat.add_assoc] + split + · subst sep₂ + have ih := by simpa only [List.append_assoc, List.append_nil, List.singleton_append, + List.nil_append, utf8Len_append, utf8Len_cons, utf8Len_nil, Nat.zero_add, Pos.mk_zero, + List.reverse_cons, ← Function.id_def, List.modifyHead_id] using (splitOnAux_of_valid [] + (sep₁++[cᵣ]) (l++m++sep₁++[cᵣ]) [] r (⟨m⟩::acc) (by simp)) + simp [by simpa using extract_of_valid l m (sep₁++cᵣ::r), ih] + · next hsp₂ => + simpa using splitOnAux_of_valid (sep₁++[cᵣ]) sep₂ l m r acc hsp₂ + · next hc => + have hget := by simpa only [List.append_assoc, utf8Len_append] + using get_of_valid (l++m) (sep₁++cᵣ::r) + have ih := by simpa only [List.append_assoc, List.append_nil, List.singleton_append, + List.nil_append, utf8Len_append, utf8Len_cons, utf8Len_nil, Nat.zero_add, Pos.mk_zero, + List.head_cons_tail (sep₁++cᵣ::r) (by simp)] using (splitOnAux_of_valid [] (sep₁++c₂::sep₂) + l (m++[(sep₁++cᵣ::r).head (by simp)]) (sep₁++cᵣ::r).tail acc (by simp)) + rw [Nat.add_sub_assoc, Nat.add_sub_cancel, hget, List.headD_eq_head (sep₁++cᵣ::r) (by simp), + Nat.add_assoc, ih, List.append_cancel_left_eq, List.modifyHead_modifyHead, + Function.comp_def]; clear hget ih + apply Nat.le_add_left +termination_by (utf8Len sep₁ + utf8Len r, utf8Len sep₂) +decreasing_by + all_goals simp_wf + · rename_i _₀ _₁ _sep₂ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _ _₁₃ _₁₄ _ _hc + clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ + subst _r _sep₂ + left + rw [← utf8Len_append] + conv => rhs; rw [← List.head_cons_tail (sep₁++cᵣ::r) (by simp), utf8Len_cons] + apply Pos.lt_addChar + · rename_i _₀ _₁ _sep₂ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _ _₁₃ _₁₄ _₁₅ _ _hc _hsp₂ + clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ + subst _r _sep₂ c₂ + repeat rw [utf8Len_cons] + rw [Nat.add_right_comm, Nat.add_assoc] + right + apply Pos.lt_addChar + · rename_i _₀ _₁ _sep₂ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _ _₁₃ _₁₄ _₁₅ _ _hc _₁₆ _hsp₂ + clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ + subst _r _sep₂ + left + rw [utf8Len_cons] + calc + utf8Len r < utf8Len r + cᵣ.utf8Size := Pos.lt_addChar .. + utf8Len r + cᵣ.utf8Size ≤ utf8Len sep₁ + (utf8Len r + cᵣ.utf8Size) := Nat.le_add_left .. + +theorem splitOn_of_valid (s sep) : splitOn s sep = (List.splitOnList s.1 sep.1).map mk := by + simp only [splitOn, beq_iff_eq] + split <;> rename_i hsp + · simp [hsp, List.splitOnList] + · have aux := by simpa only [List.append_nil, List.nil_append, utf8Len_nil, Pos.mk_zero, + List.reverse_nil, ← Function.id_def, List.modifyHead_id] using + splitOnAux_of_valid [] sep.1 [] [] s.1 [] (hsp ∘ ext) + rw [aux]; clear aux + apply congrArg + simp [List.splitOnListAux_eq_splitOnList_append_append] @[simp] theorem toString_toSubstring (s : String) : s.toSubstring.toString = s := extract_zero_endPos _