From ff346f875befc99105a87b54a2fde6be890ffb5c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 4 Jan 2018 00:56:49 +0100
Subject: [PATCH] feat(init/data/string/ops): add `string.split`

---
 library/init/coe.lean                 |  2 +-
 library/init/data/bool/lemmas.lean    |  6 ++++
 library/init/data/string/default.lean |  2 +-
 library/init/data/string/ops.lean     | 48 +++++++++++++++++++++++++++
 4 files changed, 56 insertions(+), 2 deletions(-)
 create mode 100644 library/init/data/string/ops.lean

diff --git a/library/init/coe.lean b/library/init/coe.lean
index ad6163c6f4..f84ba6e6a1 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -146,7 +146,7 @@ instance coe_to_lift {a : Sort u} {b : Sort v} [has_coe_t a b] : has_lift_t a b
 instance coe_bool_to_Prop : has_coe bool Prop :=
 ⟨λ y, y = tt⟩
 
-instance coe_sort_bool : has_coe_to_sort bool :=
+@[reducible] instance coe_sort_bool : has_coe_to_sort bool :=
 ⟨Prop, λ y, y = tt⟩
 
 instance coe_decidable_eq (x : bool) : decidable (coe x) :=
diff --git a/library/init/data/bool/lemmas.lean b/library/init/data/bool/lemmas.lean
index 35facc3a6b..f648e60c34 100644
--- a/library/init/data/bool/lemmas.lean
+++ b/library/init/data/bool/lemmas.lean
@@ -101,6 +101,12 @@ show (ff = tt) = false, by simp
 @[simp] lemma coe_tt : ↑tt = true :=
 show (tt = tt) = true, by simp
 
+@[simp] lemma coe_sort_ff : ↥ff = false :=
+show (ff = tt) = false, by simp
+
+@[simp] lemma coe_sort_tt : ↥tt = true :=
+show (tt = tt) = true, by simp
+
 @[simp] theorem to_bool_iff (p : Prop) [d : decidable p] : (to_bool p = tt) ↔ p :=
 match d with
 | is_true hp := ⟨λh, hp, λ_, rfl⟩
diff --git a/library/init/data/string/default.lean b/library/init/data/string/default.lean
index 41af8d0c3f..106a8a6380 100644
--- a/library/init/data/string/default.lean
+++ b/library/init/data/string/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.string.basic init.data.string.instances
+import init.data.string.basic init.data.string.instances init.data.string.ops
diff --git a/library/init/data/string/ops.lean b/library/init/data/string/ops.lean
new file mode 100644
index 0000000000..7874e840fc
--- /dev/null
+++ b/library/init/data/string/ops.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import init.data.bool.lemmas
+import init.data.string.basic
+import init.meta.well_founded_tactics
+
+namespace string
+
+namespace iterator
+
+@[simp] lemma next_to_string_mk_iterator (s : string) : s.mk_iterator.next_to_string = s :=
+by induction s; refl
+
+@[simp] lemma length_next_to_string_next (it : iterator) :
+  it.next.next_to_string.length = it.next_to_string.length - 1 :=
+by cases it; cases it_snd; simp [iterator.next, iterator.next_to_string, string.length, nat.add_sub_cancel_left]
+
+lemma zero_lt_length_next_to_string_of_has_next {it : iterator} :
+  it.has_next → 0 < it.next_to_string.length :=
+by cases it; cases it_snd; simp [iterator.has_next, iterator.next_to_string, string.length, nat.zero_lt_one_add]
+
+end iterator
+
+-- TODO(Sebastian): generalize to something like https://doc.rust-lang.org/std/primitive.str.html#method.split
+-- TODO(Sebastian): run-time quadratic in the number of occurrences because of string copies
+private def split_core (p : char → bool) : iterator → list string
+| it :=
+if h : it.has_next then
+  -- wf hint
+  have it.next_to_string.length - 1 < it.next_to_string.length,
+    from nat.sub_lt (iterator.zero_lt_length_next_to_string_of_has_next h) dec_trivial,
+  if p it.curr then
+    let rest := it.next.next_to_string in
+    it.prev_to_string :: split_core rest.mk_iterator
+  else
+    split_core it.next
+else
+  [it.to_string]
+using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ it, it.next_to_string.length)⟩] }
+
+def split (p : char → bool) (s : string) : list string :=
+split_core p s.mk_iterator
+
+end string