86

HumanEvalLean/HumanEval86.lean

@@ -1,7 +1,41 @@
 module
 
-def anti_shuffle : Unit :=
-  ()
+def antiShuffle (s : String) : String :=
+  s.split ' '
+    |>.map (fun sl => String.ofList (Array.mergeSort sl.chars.toArray).toList)
+    |>.intercalateString " "
+
+example : antiShuffle "Hi" = "Hi" := by native_decide
+example : antiShuffle "hello" = "ehllo" := by native_decide
+example : antiShuffle "Hello World!!!" = "Hello !!!Wdlor" := by native_decide
+example : antiShuffle "number" = "bemnru" := by native_decide
+example : antiShuffle "abcd" = "abcd" := by native_decide
+example : antiShuffle "" = "" := by native_decide
+example : antiShuffle "Hi. My name is Mister Robot. How are you?" = ".Hi My aemn is Meirst .Rboot How aer ?ouy" := by native_decide
+
+@[simp]
+theorem String.toString_eq : (ToString.toString (α := String)) = id := rfl
+
+/-- Taking a list of words, joining them together separated by spaces and calling `antiShuffle` on that
+is the same as first sorting the characters in every word and then joining that together. -/
+theorem antiShuffle_intercalate {l : List (List Char)} (hl : ∀ s ∈ l, ' ' ∉ s) :
+    antiShuffle (" ".intercalate (l.map String.ofList)) =
+      " ".intercalate (l.map (fun s => String.ofList s.mergeSort)) := by
+  rw [antiShuffle]
+  simp +instances only [String.reduceToSingleton]
+  rw [Std.Iter.intercalateString_eq, String.copy_toSlice, Std.Iter.toList_map]
+  simp only [← Std.Iter.toArray_toList, String.Slice.toList_chars]
+  have : (fun (sl : String.Slice) => String.ofList (sl.copy.toList.toArray.mergeSort).toList) =
+    (fun (s : String) => String.ofList (s.toList.toArray.mergeSort).toList) ∘ String.Slice.copy := rfl
+  simp only [this, ← List.map_map]
+  rw [String.toList_split_intercalate (by simpa)]
+  simp only [↓Char.isValue, String.reduceSingleton, List.map_eq_nil_iff, List.map_map]
+  split
+  · simp_all
+  · simp only [String.toString_eq, Function.id_comp, List.map_map]
+    congr
+    ext1 s
+    simp [Array.toList_mergeSort]
 
 /-!
 ## Prompt
@@ -46,4 +80,4 @@ def check(candidate):
     assert True
 
 ```
--/
+-/