From c98646669623b2fef7845062f2a17be872a3f587 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 17 Jan 2026 13:48:02 +0100
Subject: [PATCH 1/4] wip

---
 HumanEvalLean/HumanEval121.lean | 118 ++++++++++++++++++++++++++++++--
 1 file changed, 114 insertions(+), 4 deletions(-)

diff --git a/HumanEvalLean/HumanEval121.lean b/HumanEvalLean/HumanEval121.lean
index c9cce5c..c449277 100644
--- a/HumanEvalLean/HumanEval121.lean
+++ b/HumanEvalLean/HumanEval121.lean
@@ -1,5 +1,115 @@
-def solution : Unit :=
-  ()
+-- This can't be a module right now because `Rxi.Iterator.Monadic.Step` is not exposed
+import Std
+
+open Std Std.PRange
+
+def solution (xs : List Int) : Int :=
+  ((0 : Nat)...*).iter.zip xs.iter
+    |>.filter (fun (i, _) => i % 2 = 0)
+    |>.fold (init := 0) (fun sum (_, x) => sum + x)
+
+attribute [grind =] Iter.toList_take_zero Nat.succ?_eq
+
+public theorem Rxi.Iterator.toList_take_eq_match
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    {it : Iter (α := Rxi.Iterator α) α} :
+    (it.take n).toList =  match n, it.internalState.next with
+      | 0, _ | _, none => []
+      | n + 1, some a =>
+          a :: ((⟨⟨UpwardEnumerable.succ? a⟩⟩ : Iter (α := Rxi.Iterator α) α).take n).toList := by
+  apply Eq.symm
+  simp only [Iter.toList_eq_match_step (it := it.take n), Iter.step_take]
+  cases n
+  · grind
+  · simp only
+    cases it.step using PlausibleIterStep.casesOn <;> rename_i heq
+    · rename_i it' _
+      rcases it with ⟨⟨next⟩⟩ | _
+      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
+        simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
+        simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+        cases heq.2
+        cases it'
+        simp at heq
+        simp [heq]
+    · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
+      simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+      split at heq <;> contradiction
+    · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
+      simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+      split at heq
+      · simp [*]
+      · contradiction
+
+theorem Nat.toList_take_iter_rci_eq_match {m n : Nat} :
+    ((m...*).iter.take n).toList =
+      match n with
+      | 0 => []
+      | n + 1 => m :: (((m + 1)...*).iter.take n).toList := by
+  rw [Rxi.Iterator.toList_take_eq_match]
+  cases n <;> grind [Rci.iter]
+
+@[grind =]
+theorem Nat.toList_take_zero_iter_rci {m : Nat} :
+    ((m...*).iter.take 0).toList = [] := by
+  rw [Nat.toList_take_iter_rci_eq_match]
+
+@[grind =]
+theorem Nat.toList_take_add_one_iter_rci {m n : Nat} :
+    ((m...*).iter.take (n + 1)).toList = m :: (((m + 1)...*).iter.take n).toList := by
+  rw [Nat.toList_take_iter_rci_eq_match]
+
+@[grind =]
+theorem Nat.toList_rco_self {m : Nat} :
+    (m...m).toList = [] := by
+  simp [toList_rco_eq_nil]
+
+@[grind =]
+theorem Nat.toList_take_iter_rci {m n : Nat} :
+    (((m : Nat)...*).iter.take n).toList = ((m : Nat)...(m + n : Nat)).toList := by
+  induction n generalizing m <;> grind [Nat.toList_rco_eq_cons, Nat.toList_take_add_one_iter_rci]
+
+@[grind =]
+theorem List.map_swap_zip {xs : List α} {ys : List β} :
+    (ys.zip xs).map Prod.swap = xs.zip ys := by
+  induction xs generalizing ys
+  · grind [zip_nil_right, zip_nil_left]
+  · cases ys
+    · grind [zip_nil_left, zip_nil_right]
+    · grind [zip_cons_cons, Prod.swap_prod_mk]
+
+theorem solution_spec {xs : List Int} :
+    solution xs = (xs.mapIdx (fun i x => if i % 2 = 0 then x else 0)).sum :=
+  match xs with
+  | [] => by
+    simp [solution, ← Iter.foldl_toList]
+    rw [Iter.toList_zip_of_finite_right]
+    grind [List.toList_iter, List.length_nil, List.zip_nil_right]
+  | [x] => by
+    simp [solution, ← Iter.foldl_toList]
+    rw [Iter.toList_zip_of_finite_right]
+    simp [Nat.toList_take_iter_rci]
+  | x :: y :: xs => by
+    have := solution_spec (xs := xs)
+    simp [solution, ← Iter.foldl_toList] at this ⊢
+    rw [Iter.toList_zip_of_finite_right]
+    simp [Nat.toList_take_iter_rci, Nat.toList_rco_eq_cons]
+    -- ugh, foldr would have been nicer
+
+
+theorem solution_spec {xs : List Int} :
+    solution xs = (xs.mapIdx (fun i x => if i % 2 = 0 then x else 0)).sum := by
+  simp [solution, ← Iter.foldl_toList]
+  rw [Iter.toList_zip_of_finite_right]
+  simp [Nat.toList_take_iter_rci]
+  rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.range'_eq_toList_rco]
+  simp
+  rw [← List.map_swap_zip]
+  induction xs
+  · simp
+  · simp [Nat.toList_rco_eq_cons]
+
 
 /-!
 ## Prompt
@@ -8,7 +118,7 @@ def solution : Unit :=
 
 def solution(lst):
     """Given a non-empty list of integers, return the sum of all of the odd elements that are in even positions.
-    
+
 
     Examples
     solution([5, 8, 7, 1]) ==> 12
@@ -40,4 +150,4 @@ def check(candidate):
     # Check some edge cases that are easy to work out by hand.
 
 ```
--/
\ No newline at end of file
+-/

From 7d27f2546283687e815ab60fe268b93359379929 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 19 Jan 2026 17:27:32 +0100
Subject: [PATCH 2/4] wip

---
 HumanEvalLean/HumanEval121.lean | 105 ++++++++++++++++++++------------
 1 file changed, 67 insertions(+), 38 deletions(-)

diff --git a/HumanEvalLean/HumanEval121.lean b/HumanEvalLean/HumanEval121.lean
index c449277..a68714d 100644
--- a/HumanEvalLean/HumanEval121.lean
+++ b/HumanEvalLean/HumanEval121.lean
@@ -1,13 +1,48 @@
 -- This can't be a module right now because `Rxi.Iterator.Monadic.Step` is not exposed
 import Std
 
-open Std Std.PRange
+open Std Std.PRange Std.Do
 
 def solution (xs : List Int) : Int :=
   ((0 : Nat)...*).iter.zip xs.iter
-    |>.filter (fun (i, _) => i % 2 = 0)
+    |>.filter (fun (i, x) => i % 2 = 0 ∧ x % 2 = 1)
     |>.fold (init := 0) (fun sum (_, x) => sum + x)
 
+def solution' (xs : List Int) : Int := Id.run do
+  let mut even := true
+  let mut sum := 0
+  for x in xs do
+    if even ∧ x % 2 = 1 then
+      sum := sum + x
+    even := ! even
+  return sum
+
+def solution'' (xs : List Int) : Int :=
+  go xs 0
+where go (xs : List Int) (acc : Int) :=
+  match xs with
+  | [] => acc
+  | [x] => if x % 2 = 1 then acc + x else acc
+  | x :: _ :: ys =>
+    if x % 2 = 1 then go ys (acc + x) else go ys acc
+
+theorem List.sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  sorry
+
+theorem solution'_spec {xs : List Int} :
+    solution' xs = (xs.mapIdx (fun i x => if i % 2 = 0 ∧ x % 2 = 1 then x else 0)).sum := by
+  generalize h : solution' xs = r
+  apply Id.of_wp_run_eq h
+  mvcgen
+  · exact ⇓⟨cur, even, sum⟩ => ⌜even = (cur.prefix.length % 2 = 0) ∧ sum = (cur.prefix.mapIdx (fun i x => if i % 2 = 0 ∧ x % 2 = 1 then x else 0)).sum⌝
+  · mleave
+    simp [List.sum_append_int]
+    grind
+  · simp [List.sum_append_int]
+    grind
+  · grind
+  · grind
+
 attribute [grind =] Iter.toList_take_zero Nat.succ?_eq
 
 public theorem Rxi.Iterator.toList_take_eq_match
@@ -70,46 +105,40 @@ theorem Nat.toList_take_iter_rci {m n : Nat} :
     (((m : Nat)...*).iter.take n).toList = ((m : Nat)...(m + n : Nat)).toList := by
   induction n generalizing m <;> grind [Nat.toList_rco_eq_cons, Nat.toList_take_add_one_iter_rci]
 
-@[grind =]
-theorem List.map_swap_zip {xs : List α} {ys : List β} :
-    (ys.zip xs).map Prod.swap = xs.zip ys := by
-  induction xs generalizing ys
-  · grind [zip_nil_right, zip_nil_left]
-  · cases ys
-    · grind [zip_nil_left, zip_nil_right]
-    · grind [zip_cons_cons, Prod.swap_prod_mk]
+theorem bla {xs : List α} {f : α → Int} : xs.foldl (init := 0) (· + f ·) = (xs.map f).sum := by
+  sorry
 
-theorem solution_spec {xs : List Int} :
-    solution xs = (xs.mapIdx (fun i x => if i % 2 = 0 then x else 0)).sum :=
-  match xs with
-  | [] => by
-    simp [solution, ← Iter.foldl_toList]
-    rw [Iter.toList_zip_of_finite_right]
-    grind [List.toList_iter, List.length_nil, List.zip_nil_right]
-  | [x] => by
-    simp [solution, ← Iter.foldl_toList]
-    rw [Iter.toList_zip_of_finite_right]
-    simp [Nat.toList_take_iter_rci]
-  | x :: y :: xs => by
-    have := solution_spec (xs := xs)
-    simp [solution, ← Iter.foldl_toList] at this ⊢
-    rw [Iter.toList_zip_of_finite_right]
-    simp [Nat.toList_take_iter_rci, Nat.toList_rco_eq_cons]
-    -- ugh, foldr would have been nicer
+attribute [grind =] List.zip_nil_right List.toList_iter Iter.toList_filter List.sum_append_int
+  List.zip_cons_cons
 
+theorem solution_nil :
+    solution [] = 0 := by
+  -- fails:
+  -- grind [solution, =_ Iter.foldl_toList, ! . Iter.toList_zip_of_finite_right]
 
-theorem solution_spec {xs : List Int} :
-    solution xs = (xs.mapIdx (fun i x => if i % 2 = 0 then x else 0)).sum := by
-  simp [solution, ← Iter.foldl_toList]
-  rw [Iter.toList_zip_of_finite_right]
-  simp [Nat.toList_take_iter_rci]
-  rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.range'_eq_toList_rco]
-  simp
-  rw [← List.map_swap_zip]
-  induction xs
-  · simp
-  · simp [Nat.toList_rco_eq_cons]
+  -- succeeds:
+  -- grind =>
+  --   instantiate only [solution]
+  --   finish [=_ Iter.foldl_toList, ! . Iter.toList_zip_of_finite_right]
+
+  simp [solution, ← Iter.foldl_toList, Iter.toList_zip_of_finite_right]
 
+theorem solution_append_singleton {xs : List Int} {x : Int} :
+    solution (xs ++ [x]) =
+      if xs.length % 2 = 0 ∧ x % 2 = 1 then solution xs + x else solution xs := by
+  simp only [solution, Bool.decide_and, ← Iter.foldl_toList,
+    Iter.toList_filter, Iter.toList_zip_of_finite_right, List.toList_iter, List.length_append,
+    List.length_cons, List.length_nil, Nat.zero_add, Nat.toList_take_iter_rci]
+  rw [Nat.toList_rco_succ_right_eq_append (by simp), List.zip_append (by simp)]
+  grind
+
+theorem solution_spec {xs : List Int} :
+    solution xs = (xs.mapIdx (fun i x => if i % 2 = 0 ∧ x % 2 = 1 then x else 0)).sum := by
+  rw [← List.reverse_reverse (as := xs)]
+  induction xs.reverse
+  · simp [solution_nil]
+  · simp only [List.reverse_cons]
+    grind [solution_append_singleton]
 
 /-!
 ## Prompt

From b2d2fb1df7a84685cc4ab5c39d0b52d7b52f7209 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 19 Jan 2026 17:40:28 +0100
Subject: [PATCH 3/4] done

---
 HumanEvalLean/HumanEval121.lean | 99 +++++++++++++++++++++++++++------
 1 file changed, 83 insertions(+), 16 deletions(-)

diff --git a/HumanEvalLean/HumanEval121.lean b/HumanEvalLean/HumanEval121.lean
index a68714d..25d318f 100644
--- a/HumanEvalLean/HumanEval121.lean
+++ b/HumanEvalLean/HumanEval121.lean
@@ -3,19 +3,11 @@ import Std
 
 open Std Std.PRange Std.Do
 
-def solution (xs : List Int) : Int :=
-  ((0 : Nat)...*).iter.zip xs.iter
-    |>.filter (fun (i, x) => i % 2 = 0 ∧ x % 2 = 1)
-    |>.fold (init := 0) (fun sum (_, x) => sum + x)
+set_option mvcgen.warning false
 
-def solution' (xs : List Int) : Int := Id.run do
-  let mut even := true
-  let mut sum := 0
-  for x in xs do
-    if even ∧ x % 2 = 1 then
-      sum := sum + x
-    even := ! even
-  return sum
+/-!
+## Implementation 1
+-/
 
 def solution'' (xs : List Int) : Int :=
   go xs 0
@@ -26,8 +18,61 @@ where go (xs : List Int) (acc : Int) :=
   | x :: _ :: ys =>
     if x % 2 = 1 then go ys (acc + x) else go ys acc
 
+/-!
+## Tests 1
+-/
+
+example : solution'' [5, 8, 7, 1] = 12 := by decide
+example : solution'' [3, 3, 3, 3, 3] = 9 := by decide
+example : solution'' [30, 13, 24, 321] = 0 := by decide
+example : solution'' [5, 9] = 5 := by decide
+example : solution'' [2, 4, 8] = 0 := by decide
+example : solution'' [30, 13, 23, 32] = 23 := by decide
+example : solution'' [3, 13, 2, 9] = 3 := by decide
+
+/-!
+## Verification 1
+-/
+
+theorem solution''_aux {xs : List Int} {acc : Int} :
+    solution''.go xs acc = acc + (xs.mapIdx (fun i x => if i % 2 = 0 ∧ x % 2 = 1 then x else 0)).sum := by
+  fun_induction solution''.go xs acc <;> grind
+
+theorem solution''_spec {xs : List Int} :
+    solution'' xs = (xs.mapIdx (fun i x => if i % 2 = 0 ∧ x % 2 = 1 then x else 0)).sum := by
+  simp [solution'', solution''_aux]
+
+/-!
+## Implementation 2
+-/
+
+def solution' (xs : List Int) : Int := Id.run do
+  let mut even := true
+  let mut sum := 0
+  for x in xs do
+    if even ∧ x % 2 = 1 then
+      sum := sum + x
+    even := ! even
+  return sum
+
+/-!
+## Tests 2
+-/
+
+example : solution' [5, 8, 7, 1] = 12 := by decide
+example : solution' [3, 3, 3, 3, 3] = 9 := by decide
+example : solution' [30, 13, 24, 321] = 0 := by decide
+example : solution' [5, 9] = 5 := by decide
+example : solution' [2, 4, 8] = 0 := by decide
+example : solution' [30, 13, 23, 32] = 23 := by decide
+example : solution' [3, 13, 2, 9] = 3 := by decide
+
+/-!
+## Verification 2
+-/
+
 theorem List.sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  sorry
+  induction l₁ generalizing l₂ <;> simp_all [Int.add_assoc]
 
 theorem solution'_spec {xs : List Int} :
     solution' xs = (xs.mapIdx (fun i x => if i % 2 = 0 ∧ x % 2 = 1 then x else 0)).sum := by
@@ -43,6 +88,31 @@ theorem solution'_spec {xs : List Int} :
   · grind
   · grind
 
+/-!
+## Implementation 3
+-/
+
+def solution (xs : List Int) : Int :=
+  ((0 : Nat)...*).iter.zip xs.iter
+    |>.filter (fun (i, x) => i % 2 = 0 ∧ x % 2 = 1)
+    |>.fold (init := 0) (fun sum (_, x) => sum + x)
+
+/-!
+## Tests 3
+-/
+
+example : solution [5, 8, 7, 1] = 12 := by native_decide
+example : solution [3, 3, 3, 3, 3] = 9 := by native_decide
+example : solution [30, 13, 24, 321] = 0 := by native_decide
+example : solution [5, 9] = 5 := by native_decide
+example : solution [2, 4, 8] = 0 := by native_decide
+example : solution [30, 13, 23, 32] = 23 := by native_decide
+example : solution [3, 13, 2, 9] = 3 := by native_decide
+
+/-!
+## Verification 3
+-/
+
 attribute [grind =] Iter.toList_take_zero Nat.succ?_eq
 
 public theorem Rxi.Iterator.toList_take_eq_match
@@ -105,9 +175,6 @@ theorem Nat.toList_take_iter_rci {m n : Nat} :
     (((m : Nat)...*).iter.take n).toList = ((m : Nat)...(m + n : Nat)).toList := by
   induction n generalizing m <;> grind [Nat.toList_rco_eq_cons, Nat.toList_take_add_one_iter_rci]
 
-theorem bla {xs : List α} {f : α → Int} : xs.foldl (init := 0) (· + f ·) = (xs.map f).sum := by
-  sorry
-
 attribute [grind =] List.zip_nil_right List.toList_iter Iter.toList_filter List.sum_append_int
   List.zip_cons_cons
 

From 115f57710b1ff3adfd4e5d2f3ac47e63a520b4ae Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 20 Jan 2026 08:48:26 +0100
Subject: [PATCH 4/4] remove non-terminal simps

---
 HumanEvalLean/HumanEval121.lean | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/HumanEvalLean/HumanEval121.lean b/HumanEvalLean/HumanEval121.lean
index 25d318f..0c91a75 100644
--- a/HumanEvalLean/HumanEval121.lean
+++ b/HumanEvalLean/HumanEval121.lean
@@ -130,19 +130,20 @@ public theorem Rxi.Iterator.toList_take_eq_match
     cases it.step using PlausibleIterStep.casesOn <;> rename_i heq
     · rename_i it' _
       rcases it with ⟨⟨next⟩⟩ | _
-      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
-        simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
-      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
-        simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Rxi.Iterator.Monadic.step, Iter.toIterM] at heq
+      · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+        IterStep.mapIterator_yield, Iter.toIterM, Rxi.Iterator.Monadic.step, IterStep.yield.injEq,
+        IterM.mk'.injEq] at heq
         cases heq.2
         cases it'
         simp at heq
         simp [heq]
-    · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
-      simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+    · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+        IterStep.mapIterator_skip, Iter.toIterM, Rxi.Iterator.Monadic.step] at heq
       split at heq <;> contradiction
-    · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] at heq
-      simp [Rxi.Iterator.Monadic.step, Iter.toIterM] at heq -- ugly
+    · simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+      IterStep.mapIterator_done, Rxi.Iterator.Monadic.step, Iter.toIterM] at heq
       split at heq
       · simp [*]
       · contradiction