From 55be02ae6d895809abd89b31cded41a3556b1468 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Mon, 23 Mar 2026 13:22:29 +0000
Subject: [PATCH 1/2] WIP

---
 HumanEvalLean/HumanEval17.lean | 84 ++++++++++++++++++++++++++++++++--
 1 file changed, 80 insertions(+), 4 deletions(-)

diff --git a/HumanEvalLean/HumanEval17.lean b/HumanEvalLean/HumanEval17.lean
index 417dc0c..7f8779c 100644
--- a/HumanEvalLean/HumanEval17.lean
+++ b/HumanEvalLean/HumanEval17.lean
@@ -1,7 +1,83 @@
 module
 
-def parse_music : Unit :=
-  ()
+import Std.Data.HashMap.Lemmas
+
+open Std
+
+instance : LawfulHashable String.Slice := sorry -- will be in the next nightly
+instance : EquivBEq String.Slice := sorry
+
+def parseMusic (musicString : String) : List Nat :=
+  let noteMap : HashMap String.Slice Nat := .ofList [("o", 4), ("o|", 2), (".|", 1)]
+  (musicString.split ' ').filterMap (noteMap[·]?) |>.toList
+
+example : parseMusic "" = [] := by native_decide
+example : parseMusic "o o o o" = [4, 4, 4, 4] := by native_decide
+example : parseMusic ".| .| .| .|" = [1, 1, 1, 1] := by native_decide
+example : parseMusic "o| o| .| .| o o o o" = [2, 2, 1, 1, 4, 4, 4, 4] := by native_decide
+example : parseMusic "o| .| o| .| o o| o o|" = [2, 1, 2, 1, 4, 2, 4, 2] := by native_decide
+
+def noteForValue (value : Nat) (h : value = 1 ∨ value = 2 ∨ value = 4) : String :=
+  match value with
+  | 0 => False.elim (by simp at h)
+  | 1 => ".|"
+  | 2 => "o|"
+  | 3 => False.elim (by simp at h)
+  | 4 => "o"
+  | _ + 5 => False.elim (by simp at h)
+
+def formatMusic (l : List Nat) (hl : ∀ value ∈ l, value = 1 ∨ value = 2 ∨ value = 4) : String :=
+  " ".intercalate ((l.attachWith _ hl).map (fun p => noteForValue p.1 p.2))
+
+@[simp]
+theorem String.copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id := by
+  ext; simp
+
+@[simp]
+theorem String.Slice.beq_list_iff {l l' : List String.Slice} : l == l' ↔ l.map String.Slice.copy = l'.map String.Slice.copy := by
+  induction l generalizing l' with
+  | nil => simp_all
+  | cons => cases l' <;> simp_all
+
+theorem String.toList_split_intercalate_beq {l : List String} (h : ∀ s ∈ l, ¬c ∈ s.toList) :
+    (((String.singleton c).intercalate l).split c).toList ==
+      if l = [] then ["".toSlice] else l.map String.toSlice := by
+  split <;> simp_all [String.toList_split_intercalate h]
+
+theorem List.filterMap_beq_congr [BEq α] {l l' : List α} {f : α → Option β}
+    (hf : ∀ a a', a == a' → f a = f a') (hl : l == l') : l.filterMap f = l'.filterMap f := by
+  induction l generalizing l' with
+  | nil => simp_all
+  | cons h₁ t₁ ih =>
+    match l' with
+    | [] => simp_all
+    | h₂ :: t₂ =>
+      simp at hl
+      simp [List.filterMap_cons, ih hl.2, hf _ _ hl.1]
+
+theorem parseMusic_formatMusic {l : List Nat} {hl} : parseMusic (formatMusic l hl) = l := by
+  rw [parseMusic, formatMusic, Iter.toList_filterMap]
+  -- TODO: use simproc from next nightly to avoid `erw`
+  erw [List.filterMap_beq_congr (fun _ _ => HashMap.getElem?_congr) (String.toList_split_intercalate_beq _)]
+  · simp
+    by_cases hl : l = []
+    · simp [hl]
+    · simp [hl]
+      clear hl
+      induction l with
+      | nil => simp
+      | cons ht tl ih =>
+        simp
+        rw [List.filterMap_cons_some (b := ht)]
+        · simp only [List.filterMap_map, List.cons.injEq, true_and]
+          apply ih
+          refine fun v hv => hl _ (by simp [hv])
+        · simp
+          obtain (rfl|rfl|rfl) := hl ht (by simp) <;>
+            simp [noteForValue, HashMap.ofList_equiv_foldl.getElem_eq, HashMap.getElem_insert]
+  · simp
+    rintro _ val hval rfl
+    obtain (rfl|rfl|rfl) := hl _ hval <;> simp [noteForValue]
 
 /-!
 ## Prompt
@@ -25,7 +101,7 @@ def parse_music(music_string: str) -> List[int]:
     """
 ```
 
-## Canonical solution
+## Canonical soluton
 
 ```python3
     note_map = {'o': 4, 'o|': 2, '.|': 1}
@@ -50,4 +126,4 @@ def check(candidate):
     assert candidate('o| o| .| .| o o o o') == [2, 2, 1, 1, 4, 4, 4, 4]
     assert candidate('o| .| o| .| o o| o o|') == [2, 1, 2, 1, 4, 2, 4, 2]
 ```
--/
\ No newline at end of file
+-/

From 342957cc905628adf087b1af4a8b6040b543d0fb Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 07:55:06 +0000
Subject: [PATCH 2/2] Finish

---
 HumanEvalLean/HumanEval17.lean | 30 +++++++-----------------------
 1 file changed, 7 insertions(+), 23 deletions(-)

diff --git a/HumanEvalLean/HumanEval17.lean b/HumanEvalLean/HumanEval17.lean
index 7f8779c..590f22a 100644
--- a/HumanEvalLean/HumanEval17.lean
+++ b/HumanEvalLean/HumanEval17.lean
@@ -4,9 +4,6 @@ import Std.Data.HashMap.Lemmas
 
 open Std
 
-instance : LawfulHashable String.Slice := sorry -- will be in the next nightly
-instance : EquivBEq String.Slice := sorry
-
 def parseMusic (musicString : String) : List Nat :=
   let noteMap : HashMap String.Slice Nat := .ofList [("o", 4), ("o|", 2), (".|", 1)]
   (musicString.split ' ').filterMap (noteMap[·]?) |>.toList
@@ -29,21 +26,6 @@ def noteForValue (value : Nat) (h : value = 1 ∨ value = 2 ∨ value = 4) : Str
 def formatMusic (l : List Nat) (hl : ∀ value ∈ l, value = 1 ∨ value = 2 ∨ value = 4) : String :=
   " ".intercalate ((l.attachWith _ hl).map (fun p => noteForValue p.1 p.2))
 
-@[simp]
-theorem String.copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id := by
-  ext; simp
-
-@[simp]
-theorem String.Slice.beq_list_iff {l l' : List String.Slice} : l == l' ↔ l.map String.Slice.copy = l'.map String.Slice.copy := by
-  induction l generalizing l' with
-  | nil => simp_all
-  | cons => cases l' <;> simp_all
-
-theorem String.toList_split_intercalate_beq {l : List String} (h : ∀ s ∈ l, ¬c ∈ s.toList) :
-    (((String.singleton c).intercalate l).split c).toList ==
-      if l = [] then ["".toSlice] else l.map String.toSlice := by
-  split <;> simp_all [String.toList_split_intercalate h]
-
 theorem List.filterMap_beq_congr [BEq α] {l l' : List α} {f : α → Option β}
     (hf : ∀ a a', a == a' → f a = f a') (hl : l == l') : l.filterMap f = l'.filterMap f := by
   induction l generalizing l' with
@@ -57,9 +39,10 @@ theorem List.filterMap_beq_congr [BEq α] {l l' : List α} {f : α → Option β
 
 theorem parseMusic_formatMusic {l : List Nat} {hl} : parseMusic (formatMusic l hl) = l := by
   rw [parseMusic, formatMusic, Iter.toList_filterMap]
-  -- TODO: use simproc from next nightly to avoid `erw`
-  erw [List.filterMap_beq_congr (fun _ _ => HashMap.getElem?_congr) (String.toList_split_intercalate_beq _)]
-  · simp
+  simp +instances only [String.reduceToSingleton]
+  rw [List.filterMap_beq_congr (fun _ _ => HashMap.getElem?_congr) (String.toList_split_intercalate_beq _)]
+  · simp only [↓Char.isValue, String.reduceSingleton, List.map_attachWith, List.map_eq_nil_iff,
+      List.attach_eq_nil_iff, List.map_map]
     by_cases hl : l = []
     · simp [hl]
     · simp [hl]
@@ -67,7 +50,7 @@ theorem parseMusic_formatMusic {l : List Nat} {hl} : parseMusic (formatMusic l h
       induction l with
       | nil => simp
       | cons ht tl ih =>
-        simp
+        simp only [List.attach_cons]
         rw [List.filterMap_cons_some (b := ht)]
         · simp only [List.filterMap_map, List.cons.injEq, true_and]
           apply ih
@@ -75,7 +58,8 @@ theorem parseMusic_formatMusic {l : List Nat} {hl} : parseMusic (formatMusic l h
         · simp
           obtain (rfl|rfl|rfl) := hl ht (by simp) <;>
             simp [noteForValue, HashMap.ofList_equiv_foldl.getElem_eq, HashMap.getElem_insert]
-  · simp
+  · simp only [List.map_attachWith, List.mem_map, List.mem_attach, true_and, Subtype.exists,
+      ↓Char.isValue, forall_exists_index]
     rintro _ val hval rfl
     obtain (rfl|rfl|rfl) := hl _ hval <;> simp [noteForValue]