15

HumanEvalLean/HumanEval15.lean

@@ -1,7 +1,30 @@
 module
+import Std.Data.Iterators.Producers.Range
+import Std
 
-def string_sequence : Unit :=
-  ()
+def stringSequence (n : Nat) : String :=
+  Std.Iter.intercalateString.{0} " " ((0...=n).iter.map (String.toSlice ∘ Nat.repr))
+
+example : stringSequence 0 = "0" := by native_decide
+example : stringSequence 3 = "0 1 2 3" := by native_decide
+example : stringSequence 10 = "0 1 2 3 4 5 6 7 8 9 10" := by native_decide
+
+/-- Calling `stringSequence` and then splitting the result at space characters and attempting to
+parse the components into natural numbers yields the sequence `[some 0, some 1, ..., some n]`. -/
+theorem map_ofNat?_stringSequence {n : Nat} :
+    ((stringSequence n).split ' ').toList.map String.Slice.toNat? =
+      (0...=n).toList.map Option.some := by
+  rw [stringSequence, ← String.Slice.toNat?_comp_copy, ← List.map_map,
+    Std.Iter.intercalateString_eq, String.Slice.toStringToString_eq, String.copy_toSlice]
+  simp +instances only [String.reduceToSingleton]
+  rw [String.toList_split_intercalate]
+  · rw [Std.Iter.toList_map]
+    simp
+  · rw [Std.Iter.toList_map]
+    simp only [Std.Rcc.toList_iter, List.mem_map, Function.comp_apply, ↓Char.isValue,
+      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, String.copy_toSlice, Nat.toList_repr]
+    intro a ha h
+    simpa using Nat.isDigit_of_mem_toDigits (by decide) (by decide) h
 
 /-!
 ## Prompt
@@ -40,4 +63,4 @@ def check(candidate):
     assert candidate(3) == '0 1 2 3'
     assert candidate(10) == '0 1 2 3 4 5 6 7 8 9 10'
 ```
--/
+-/