feat(init/data/string/ops): add string.split

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) :=

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⟩

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

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