From 77c7568b2be4b50de36726769667282713cd9073 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Thu, 1 May 2025 08:13:06 +0200
Subject: [PATCH 01/25] Add (partial) solution to HumanEval5

---
 HumanEvalLean/HumanEval5.lean | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 7ab1ada..492403c 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -1,5 +1,28 @@
-def intersperse : Unit :=
-  ()
+def intersperse : List Int → Int → List Int
+  | [],             _     => []
+  | [i],            _     => [i]
+  | i₁ :: i₂ :: tl, delim => i₁ :: delim :: intersperse (i₂ :: tl) delim
+
+example : intersperse [] 7 = []                              := rfl
+example : intersperse [5, 6, 3, 2] 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
+example : intersperse [2, 2, 2] 2 = [2, 2, 2, 2, 2]          := rfl
+
+theorem intersperse_length_le : (intersperse nums delim).length ≤ 2 * nums.length - 1 := by
+  fun_induction intersperse <;> simp only [intersperse, List.length_cons] at * <;> omega
+
+-- Every element of index `2 * i` is the `i`th element of the input list.
+theorem intersperse_get?_num (h : 1 < nums.length) :
+    (intersperse nums delim)[2 * i]? = nums[i]? := by
+  fun_induction intersperse generalizing i <;> try contradiction
+  next tl _ ih =>
+    cases tl <;> cases i
+    case nil.succ j =>
+      cases j <;> simp +arith [intersperse]
+    case cons.succ j =>
+      have hj : 2 * (j + 1) = 2 * j + 2 := rfl
+      rw [intersperse, hj]
+      simp [ih]
+    all_goals simp [intersperse]
 
 /-!
 ## Prompt
@@ -50,4 +73,4 @@ def check(candidate):
     assert candidate([5, 6, 3, 2], 8) == [5, 8, 6, 8, 3, 8, 2]
     assert candidate([2, 2, 2], 2) == [2, 2, 2, 2, 2]
 ```
--/
\ No newline at end of file
+-/

From 7bacf0efe639790e8deb0294fb122658e8d92647 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Thu, 1 May 2025 11:15:11 +0200
Subject: [PATCH 02/25] Add solution to HumanEval155

---
 HumanEvalLean/HumanEval155.lean | 51 +++++++++++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index e77bbc6..f6cc36e 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,5 +1,50 @@
-def even_odd_count : Unit :=
-  ()
+def Int.toDigits (i : Int) : List Char :=
+  i.natAbs.toDigits (base := 10)
+
+def evenOddCount (num : Int) : Nat × Nat :=
+  num.toDigits.foldl countDigit (0, 0)
+where
+  countDigit (evenOdd : Nat × Nat) : Char → Nat × Nat
+    | '0' | '2' | '4' | '6' | '8' => (evenOdd.fst + 1, evenOdd.snd)
+    | _                           => (evenOdd.fst, evenOdd.snd + 1)
+
+example : evenOddCount (-12) = (1, 1)     := rfl
+example : evenOddCount 123 = (1, 2)       := rfl
+example : evenOddCount 7 = (0, 1)         := rfl
+example : evenOddCount (-78) = (1, 1)     := rfl
+example : evenOddCount 3452 = (2, 2)      := rfl
+example : evenOddCount 346211 = (3, 3)    := rfl
+example : evenOddCount (-345821) = (3, 3) := rfl
+example : evenOddCount (-2) = (1, 0)      := rfl
+example : evenOddCount (-45347) = (2, 3)  := rfl
+example : evenOddCount 0 = (1, 0)         := rfl
+
+def Prod.sum : Nat × Nat → Nat
+  | (n₁, n₂) => n₁ + n₂
+
+-- Applying `evenOddCount.countDigit` increases the total digit count by `1`.
+theorem evenOddCount.countDigit_sum (evenOdd : Nat × Nat) (d : Char) :
+    (evenOddCount.countDigit evenOdd d).sum = evenOdd.sum + 1 := by
+  unfold evenOddCount.countDigit
+  split <;> simp +arith [Prod.sum]
+
+-- Folding `evenOddCount.countDigit` over a given digit count `init` produces the same total digit
+-- count as folding `evenOddCount.countDigit` over `(0, 0)` and adding that to `init`.
+theorem evenOddCount.countDigit_sum_foldl (ds : List Char) (init : Nat × Nat) :
+    (ds.foldl evenOddCount.countDigit init).sum =
+    (ds.foldl evenOddCount.countDigit (0, 0)).sum + init.sum := by
+  induction ds generalizing init
+  case nil     => simp [Prod.sum]
+  case cons ih => simp +arith only [List.foldl_cons, ih (countDigit _ _), countDigit_sum]; rfl
+
+-- The total digit count produced by `evenOddCount` matches the number of digits in the input.
+theorem evenOddCount_sum_eq_length : (evenOddCount i).sum = i.toDigits.length := by
+  rw [evenOddCount]
+  generalize i.toDigits = ds
+  induction ds
+  case nil => rfl
+  case cons ih => rw [List.foldl_cons, List.length_cons, evenOddCount.countDigit_sum_foldl, ih,
+                      evenOddCount.countDigit_sum, Prod.sum]
 
 /-!
 ## Prompt
@@ -48,4 +93,4 @@ def check(candidate):
     assert True
 
 ```
--/
\ No newline at end of file
+-/

From 38a452823e2689610f6f99a943fb9e72a11f574a Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 5 May 2025 19:23:15 +0200
Subject: [PATCH 03/25] Use `List.intersperse`

---
 HumanEvalLean/HumanEval5.lean | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 492403c..26f48fc 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -1,27 +1,27 @@
-def intersperse : List Int → Int → List Int
-  | [],             _     => []
-  | [i],            _     => [i]
-  | i₁ :: i₂ :: tl, delim => i₁ :: delim :: intersperse (i₂ :: tl) delim
+example : [].intersperse 7 = []                              := rfl
+example : [5, 6, 3, 2].intersperse 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
+example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
 
-example : intersperse [] 7 = []                              := rfl
-example : intersperse [5, 6, 3, 2] 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
-example : intersperse [2, 2, 2] 2 = [2, 2, 2, 2, 2]          := rfl
+namespace List
 
-theorem intersperse_length_le : (intersperse nums delim).length ≤ 2 * nums.length - 1 := by
-  fun_induction intersperse <;> simp only [intersperse, List.length_cons] at * <;> omega
+theorem intersperse_length_le (l : List α) : (l.intersperse delim).length ≤ 2 * l.length - 1 := by
+  fun_induction intersperse <;> simp only [intersperse, length_cons] at * <;> try omega
+  next h _ =>
+    have := length_pos_iff.mpr h
+    omega
 
 -- Every element of index `2 * i` is the `i`th element of the input list.
-theorem intersperse_get?_num (h : 1 < nums.length) :
-    (intersperse nums delim)[2 * i]? = nums[i]? := by
+theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) :
+    (l.intersperse delim)[2 * i]? = l[i]? := by
   fun_induction intersperse generalizing i <;> try contradiction
-  next tl _ ih =>
+  next hn ih =>
+    have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
     cases tl <;> cases i
     case nil.succ j =>
-      cases j <;> simp +arith [intersperse]
+      cases j <;> simp +arith [hn, intersperse]
     case cons.succ j =>
       have hj : 2 * (j + 1) = 2 * j + 2 := rfl
-      rw [intersperse, hj]
-      simp [ih]
+      rw [intersperse, hj] <;> simp_all
     all_goals simp [intersperse]
 
 /-!

From 3ac961c2d3e900ed9876a5d7ed5ee600fb016772 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 5 May 2025 19:26:05 +0200
Subject: [PATCH 04/25] Simplify proof

---
 HumanEvalLean/HumanEval5.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 26f48fc..60dceb9 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -17,11 +17,8 @@ theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) :
   next hn ih =>
     have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
     cases tl <;> cases i
-    case nil.succ j =>
-      cases j <;> simp +arith [hn, intersperse]
-    case cons.succ j =>
-      have hj : 2 * (j + 1) = 2 * j + 2 := rfl
-      rw [intersperse, hj] <;> simp_all
+    case nil.succ  j => cases j <;> simp_all +arith
+    case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all
     all_goals simp [intersperse]
 
 /-!

From 6a07760da32236f98849e6fb196993d5e1770667 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 5 May 2025 19:38:47 +0200
Subject: [PATCH 05/25] Add proof for odd case

---
 HumanEvalLean/HumanEval5.lean | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 60dceb9..3f705a7 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -4,7 +4,7 @@ example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
 
 namespace List
 
-theorem intersperse_length_le (l : List α) : (l.intersperse delim).length ≤ 2 * l.length - 1 := by
+theorem intersperse_length_le (l : List α) : (l.intersperse sep).length ≤ 2 * l.length - 1 := by
   fun_induction intersperse <;> simp only [intersperse, length_cons] at * <;> try omega
   next h _ =>
     have := length_pos_iff.mpr h
@@ -12,15 +12,25 @@ theorem intersperse_length_le (l : List α) : (l.intersperse delim).length ≤ 2
 
 -- Every element of index `2 * i` is the `i`th element of the input list.
 theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) :
-    (l.intersperse delim)[2 * i]? = l[i]? := by
+    (l.intersperse sep)[2 * i]? = l[i]? := by
   fun_induction intersperse generalizing i <;> try contradiction
-  next hn ih =>
+  next hn _ =>
     have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
     cases tl <;> cases i
     case nil.succ  j => cases j <;> simp_all +arith
     case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all
     all_goals simp [intersperse]
 
+-- Every element of index `2 * i + 1` is the separator element.
+theorem intersperse_getElem?_odd {l : List α} (h₁ : 1 < l.length) (h₂ : i < l.length - 1) :
+    (l.intersperse sep)[2 * i + 1]? = sep := by
+  fun_induction intersperse generalizing i <;> try contradiction
+  next hn _ =>
+    have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
+    cases tl <;> cases i
+    case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all
+    all_goals simp_all
+
 /-!
 ## Prompt
 

From 52ffa4dd82c3a0ee223306a2df925f4a43482372 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 5 May 2025 19:41:11 +0200
Subject: [PATCH 06/25] Gardening

---
 HumanEvalLean/HumanEval5.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 3f705a7..0ca381c 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -10,9 +10,10 @@ theorem intersperse_length_le (l : List α) : (l.intersperse sep).length ≤ 2 *
     have := length_pos_iff.mpr h
     omega
 
+variable {l : List α}
+
 -- Every element of index `2 * i` is the `i`th element of the input list.
-theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) :
-    (l.intersperse sep)[2 * i]? = l[i]? := by
+theorem intersperse_getElem?_even (h : 1 < l.length) : (l.intersperse sep)[2 * i]? = l[i]? := by
   fun_induction intersperse generalizing i <;> try contradiction
   next hn _ =>
     have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
@@ -22,7 +23,7 @@ theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) :
     all_goals simp [intersperse]
 
 -- Every element of index `2 * i + 1` is the separator element.
-theorem intersperse_getElem?_odd {l : List α} (h₁ : 1 < l.length) (h₂ : i < l.length - 1) :
+theorem intersperse_getElem?_odd (h₁ : 1 < l.length) (h₂ : i < l.length - 1) :
     (l.intersperse sep)[2 * i + 1]? = sep := by
   fun_induction intersperse generalizing i <;> try contradiction
   next hn _ =>

From c7516756da6dfff0bb7c3e610363042c14845f4b Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 6 May 2025 13:12:56 +0200
Subject: [PATCH 07/25] Turn < into =

---
 HumanEvalLean/HumanEval5.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 0ca381c..37e6d63 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -4,11 +4,9 @@ example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
 
 namespace List
 
-theorem intersperse_length_le (l : List α) : (l.intersperse sep).length ≤ 2 * l.length - 1 := by
-  fun_induction intersperse <;> simp only [intersperse, length_cons] at * <;> try omega
-  next h _ =>
-    have := length_pos_iff.mpr h
-    omega
+theorem intersperse_length (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by
+  fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at * <;> try omega
+  next h _ => have := length_pos_iff.mpr h; omega
 
 variable {l : List α}
 

From ddadf48d2843e8eefb64ffafb931eb89018b945b Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 6 May 2025 14:06:14 +0200
Subject: [PATCH 08/25] Rename theorem

---
 HumanEvalLean/HumanEval5.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 37e6d63..2e1093d 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -4,7 +4,7 @@ example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
 
 namespace List
 
-theorem intersperse_length (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by
+theorem length_intersperse (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by
   fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at * <;> try omega
   next h _ => have := length_pos_iff.mpr h; omega
 

From 08dc3d3331924e391b572f9d1818eaaba3b4497a Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Wed, 14 May 2025 17:38:39 +0200
Subject: [PATCH 09/25] Use Lean's theorems

---
 HumanEvalLean/HumanEval5.lean | 35 ++++++++---------------------------
 1 file changed, 8 insertions(+), 27 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 2e1093d..605d7ef 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -2,33 +2,14 @@ example : [].intersperse 7 = []                              := rfl
 example : [5, 6, 3, 2].intersperse 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
 example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
 
-namespace List
-
-theorem length_intersperse (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by
-  fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at * <;> try omega
-  next h _ => have := length_pos_iff.mpr h; omega
-
-variable {l : List α}
-
--- Every element of index `2 * i` is the `i`th element of the input list.
-theorem intersperse_getElem?_even (h : 1 < l.length) : (l.intersperse sep)[2 * i]? = l[i]? := by
-  fun_induction intersperse generalizing i <;> try contradiction
-  next hn _ =>
-    have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
-    cases tl <;> cases i
-    case nil.succ  j => cases j <;> simp_all +arith
-    case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all
-    all_goals simp [intersperse]
-
--- Every element of index `2 * i + 1` is the separator element.
-theorem intersperse_getElem?_odd (h₁ : 1 < l.length) (h₂ : i < l.length - 1) :
-    (l.intersperse sep)[2 * i + 1]? = sep := by
-  fun_induction intersperse generalizing i <;> try contradiction
-  next hn _ =>
-    have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn
-    cases tl <;> cases i
-    case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all
-    all_goals simp_all
+open List
+
+#check length_intersperse
+#check getElem?_intersperse_two_mul
+#check getElem?_intersperse_two_mul_add_one
+#check getElem_intersperse_two_mul
+#check getElem_intersperse_two_mul_add_one
+#check getElem_eq_getElem_intersperse_two_mul
 
 /-!
 ## Prompt

From c33ec7f60af5bd9555bfd096cc3c28aa63cc276e Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Wed, 14 May 2025 17:50:40 +0200
Subject: [PATCH 10/25] Define decomposition theorem

---
 HumanEvalLean/HumanEval155.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index f6cc36e..a0596db 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -19,9 +19,15 @@ example : evenOddCount (-2) = (1, 0)      := rfl
 example : evenOddCount (-45347) = (2, 3)  := rfl
 example : evenOddCount 0 = (1, 0)         := rfl
 
-def Prod.sum : Nat × Nat → Nat
+def Prod.sum : (Nat × Nat) → Nat
   | (n₁, n₂) => n₁ + n₂
 
+instance : Add (Nat × Nat) where
+  add | (l₁, r₁), (l₂, r₂) => (l₁ + l₂, r₁ + r₂)
+
+instance : Sub (Nat × Nat) where
+  sub | (l₁, r₁), (l₂, r₂) => (l₁ - l₂, r₁ - r₂)
+
 -- Applying `evenOddCount.countDigit` increases the total digit count by `1`.
 theorem evenOddCount.countDigit_sum (evenOdd : Nat × Nat) (d : Char) :
     (evenOddCount.countDigit evenOdd d).sum = evenOdd.sum + 1 := by
@@ -46,6 +52,10 @@ theorem evenOddCount_sum_eq_length : (evenOddCount i).sum = i.toDigits.length :=
   case cons ih => rw [List.foldl_cons, List.length_cons, evenOddCount.countDigit_sum_foldl, ih,
                       evenOddCount.countDigit_sum, Prod.sum]
 
+theorem evenOddCount_decompose :
+    evenOddCount (10 * n + d) = evenOddCount n + evenOddCount (d % 10) - (1, 0) :=
+  sorry
+
 /-!
 ## Prompt
 

From 871954bb026bf7d026a23127ced3dc592e848c2c Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 3 Jun 2025 20:51:19 +0200
Subject: [PATCH 11/25] Update to Lean v4.21.0-rc2

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index b2153cd..2ed974a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.21.0-rc2

From c6cd38acf7f583b485595453401fcc56659781cb Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sat, 7 Jun 2025 19:56:08 +0200
Subject: [PATCH 12/25] Overhaul definitions

---
 HumanEvalLean/HumanEval155.lean | 117 +++++++++++++++++---------------
 1 file changed, 64 insertions(+), 53 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index a0596db..86b616f 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,59 +1,70 @@
-def Int.toDigits (i : Int) : List Char :=
-  i.natAbs.toDigits (base := 10)
-
-def evenOddCount (num : Int) : Nat × Nat :=
-  num.toDigits.foldl countDigit (0, 0)
-where
-  countDigit (evenOdd : Nat × Nat) : Char → Nat × Nat
-    | '0' | '2' | '4' | '6' | '8' => (evenOdd.fst + 1, evenOdd.snd)
-    | _                           => (evenOdd.fst, evenOdd.snd + 1)
-
-example : evenOddCount (-12) = (1, 1)     := rfl
-example : evenOddCount 123 = (1, 2)       := rfl
-example : evenOddCount 7 = (0, 1)         := rfl
-example : evenOddCount (-78) = (1, 1)     := rfl
-example : evenOddCount 3452 = (2, 2)      := rfl
-example : evenOddCount 346211 = (3, 3)    := rfl
-example : evenOddCount (-345821) = (3, 3) := rfl
-example : evenOddCount (-2) = (1, 0)      := rfl
-example : evenOddCount (-45347) = (2, 3)  := rfl
-example : evenOddCount 0 = (1, 0)         := rfl
-
-def Prod.sum : (Nat × Nat) → Nat
-  | (n₁, n₂) => n₁ + n₂
-
-instance : Add (Nat × Nat) where
-  add | (l₁, r₁), (l₂, r₂) => (l₁ + l₂, r₁ + r₂)
-
-instance : Sub (Nat × Nat) where
-  sub | (l₁, r₁), (l₂, r₂) => (l₁ - l₂, r₁ - r₂)
-
--- Applying `evenOddCount.countDigit` increases the total digit count by `1`.
-theorem evenOddCount.countDigit_sum (evenOdd : Nat × Nat) (d : Char) :
-    (evenOddCount.countDigit evenOdd d).sum = evenOdd.sum + 1 := by
-  unfold evenOddCount.countDigit
-  split <;> simp +arith [Prod.sum]
-
--- Folding `evenOddCount.countDigit` over a given digit count `init` produces the same total digit
--- count as folding `evenOddCount.countDigit` over `(0, 0)` and adding that to `init`.
-theorem evenOddCount.countDigit_sum_foldl (ds : List Char) (init : Nat × Nat) :
-    (ds.foldl evenOddCount.countDigit init).sum =
-    (ds.foldl evenOddCount.countDigit (0, 0)).sum + init.sum := by
-  induction ds generalizing init
-  case nil     => simp [Prod.sum]
-  case cons ih => simp +arith only [List.foldl_cons, ih (countDigit _ _), countDigit_sum]; rfl
+-- https://github.com/leanprover-community/batteries/pull/1267
+theorem Nat.isDigit_digitChar_iff_lt : n.digitChar.isDigit ↔ (n < 10) := sorry
+theorem Nat.mem_toDigits_base_10_isDigit (h : c ∈ toDigits 10 n) : c.isDigit := sorry
+
+abbrev Digit := { c : Char // c.isDigit }
+
+def Int.digits (i : Int) : List Digit :=
+  i.natAbs
+    |>.toDigits (base := 10)
+    |>.attach
+    |>.map fun ⟨j, h⟩ => ⟨j, Nat.mem_toDigits_base_10_isDigit h⟩
+
+structure Tally where
+  even : Nat
+  odd  : Nat
+deriving Inhabited
+
+namespace Tally
 
--- The total digit count produced by `evenOddCount` matches the number of digits in the input.
-theorem evenOddCount_sum_eq_length : (evenOddCount i).sum = i.toDigits.length := by
-  rw [evenOddCount]
-  generalize i.toDigits = ds
+instance : Add Tally where
+  add t₁ t₂ := { even := t₁.even + t₂.even, odd := t₁.odd + t₂.odd }
+
+def total (t : Tally) : Nat :=
+  t.even + t.odd
+
+def log (t : Tally) (d : Digit) : Tally :=
+  match d.val with
+  | '0' | '2' | '4' | '6' | '8' => { t with even := t.even + 1 }
+  | _                           => { t with odd  := t.odd  + 1 }
+
+-- Applying `log` increases a tally's total by `1`.
+theorem log_total (d : Digit) (t : Tally) : (t.log d).total = t.total + 1 := by
+  rw [log]
+  split <;> simp +arith [total]
+
+-- Folding `log` over a given tally `init` produces the same total digit count as folding `log` over
+-- `⟨0, 0⟩` and adding that to `init`.
+theorem log_total_foldl {ds : List Digit} (init : Tally) :
+    (ds.foldl log init).total = (ds.foldl log ⟨0, 0⟩).total + init.total := by
+  induction ds generalizing init
+  case' cons hd _ ih => simp +arith only [List.foldl_cons, ih (log _ hd), log_total]
+  all_goals simp [total]
+
+def count (i : Int) : Tally :=
+  i.digits.foldl log ⟨0, 0⟩
+
+example : count (-12) = ⟨1, 1⟩     := rfl
+example : count 123 = ⟨1, 2⟩       := rfl
+example : count 7 = ⟨0, 1⟩         := rfl
+example : count (-78) = ⟨1, 1⟩     := rfl
+example : count 3452 = ⟨2, 2⟩      := rfl
+example : count 346211 = ⟨3, 3⟩    := rfl
+example : count (-345821) = ⟨3, 3⟩ := rfl
+example : count (-2) = ⟨1, 0⟩      := rfl
+example : count (-45347) = ⟨2, 3⟩  := rfl
+example : count 0 = ⟨1, 0⟩         := rfl
+
+-- The tally total produced by `count` matches the number of digits in the input.
+theorem count_total_eq_length : (count i).total = i.digits.length := by
+  rw [count]
+  generalize i.digits = ds
   induction ds
-  case nil => rfl
-  case cons ih => rw [List.foldl_cons, List.length_cons, evenOddCount.countDigit_sum_foldl, ih,
-                      evenOddCount.countDigit_sum, Prod.sum]
+  case nil     => rfl
+  case cons ih => rw [List.foldl_cons, List.length_cons, log_total_foldl, ih, log_total]; rfl
 
-theorem evenOddCount_decompose :
-    evenOddCount (10 * n + d) = evenOddCount n + evenOddCount (d % 10) - (1, 0) :=
+theorem count_decompose {d : Nat} (hd : d < 10) :
+    count (10 * n + d) = count n + ⟨d % 2, 1 - d % 2⟩ := by
   sorry
 
 /-!

From b27e88877189aeb5adb905bb49ebf17444e27f25 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 8 Jun 2025 17:20:33 +0200
Subject: [PATCH 13/25] Reduce `count_decompose` to "simple" lemmas

---
 HumanEvalLean/HumanEval155.lean | 121 ++++++++++++++++++++++++++++----
 1 file changed, 107 insertions(+), 14 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 86b616f..a5fe015 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,15 +1,60 @@
+-- TODO: This already exists in Mathlib.
+@[simp] theorem Nat.natAbs_cast (n : Nat) : (n : Int).natAbs = n := rfl
+
+section Batteries
+
 -- https://github.com/leanprover-community/batteries/pull/1267
-theorem Nat.isDigit_digitChar_iff_lt : n.digitChar.isDigit ↔ (n < 10) := sorry
+@[simp] theorem isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) := sorry
 theorem Nat.mem_toDigits_base_10_isDigit (h : c ∈ toDigits 10 n) : c.isDigit := sorry
 
+theorem Nat.toDigits_10_of_lt_10 (h : n < 10) : toDigits 10 n = [n.digitChar] := by
+  sorry
+
+theorem Nat.toDigits_10_decompose (h : d < 10) (n : Nat) :
+    toDigits 10 (10 * n + d) = (toDigits 10 n) ++ (toDigits 10 d) :=
+  sorry
+
+@[simp]
+theorem Nat.toDigits_10_natAbs_cast (n : Nat) : toDigits 10 (n : Int).natAbs = toDigits 10 n :=
+  sorry
+
+end Batteries
+
 abbrev Digit := { c : Char // c.isDigit }
 
-def Int.digits (i : Int) : List Digit :=
-  i.natAbs
-    |>.toDigits (base := 10)
+namespace Nat
+
+def digits (n : Nat) : List Digit :=
+  n.toDigits (base := 10)
     |>.attach
     |>.map fun ⟨j, h⟩ => ⟨j, Nat.mem_toDigits_base_10_isDigit h⟩
 
+theorem digits_of_lt_10 (h : n < 10) : n.digits = [⟨n.digitChar, by simp_all⟩] := by
+  sorry
+
+theorem digits_decompose (h : d < 10) (n : Nat) : (10 * n + d).digits = n.digits ++ d.digits := by
+  simp [digits]
+  -- PROBLEM: When appending lists with `attach`es, the membership witnesses change.
+  -- rw [toDigits_10_decompose h]
+  sorry
+
+end Nat
+
+namespace Int
+
+def digits (i : Int) : List Digit :=
+  i.natAbs.digits
+
+@[simp]
+theorem digits_cast (n : Nat) : (n : Int).digits = n.digits := by
+  simp [digits]
+
+theorem digits_decompose {d : Nat} (h : d < 10) (n : Nat) :
+    digits (10 * n + d : Nat) = n.digits ++ d.digits := by
+  rw [digits, Nat.natAbs_cast, Nat.digits_decompose h]
+
+end Int
+
 structure Tally where
   even : Nat
   odd  : Nat
@@ -20,26 +65,65 @@ namespace Tally
 instance : Add Tally where
   add t₁ t₂ := { even := t₁.even + t₂.even, odd := t₁.odd + t₂.odd }
 
+@[simp]
+theorem empty_add (t : Tally) : ⟨0, 0⟩ + t = t := by
+  simp only [(· + ·), Add.add]
+  simp
+
+@[simp]
+theorem add_even (t₁ t₂ : Tally) : (t₁ + t₂).even = t₁.even + t₂.even := by
+  simp only [(· + ·), Add.add]
+
+@[simp]
+theorem add_odd (t₁ t₂ : Tally) : (t₁ + t₂).odd = t₁.odd + t₂.odd := by
+  simp only [(· + ·), Add.add]
+
+theorem add_comm (t₁ t₂ : Tally) : t₁ + t₂ = t₂ + t₁ := by
+  simp only [(· + ·), Add.add]
+  simp +arith
+
+theorem add_assoc (t₁ t₂ : Tally) : t₁ + t₂ + t₃ = t₁ + (t₂ + t₃) := by
+  simp only [(· + ·), Add.add]
+  simp +arith
+
 def total (t : Tally) : Nat :=
   t.even + t.odd
 
+@[simp]
+theorem total_add (t₁ t₂ : Tally) : (t₁ + t₂).total = t₁.total + t₂.total := by
+  simp +arith [total]
+
 def log (t : Tally) (d : Digit) : Tally :=
   match d.val with
   | '0' | '2' | '4' | '6' | '8' => { t with even := t.even + 1 }
   | _                           => { t with odd  := t.odd  + 1 }
 
--- Applying `log` increases a tally's total by `1`.
-theorem log_total (d : Digit) (t : Tally) : (t.log d).total = t.total + 1 := by
-  rw [log]
-  split <;> simp +arith [total]
+theorem log_add (t₁ t₂ : Tally) (d : Digit) : (t₁.log d) + t₂ = (t₁ + t₂).log d := by
+  sorry
+
+theorem log_digitChar (h : d < 10) (t : Tally) :
+    t.log ⟨d.digitChar, by simp_all⟩ = t + ⟨1 - d % 2, d % 2⟩ :=
+  sorry
+
+-- Folding `log` over a given tally `init` produces the same tally as folding `log` over `⟨0, 0⟩`
+-- and adding that to `init`.
+theorem log_foldl {ds : List Digit} (init : Tally) :
+    (ds.foldl log init) = (ds.foldl log ⟨0, 0⟩) + init := by
+  induction ds generalizing init
+  case nil          => simp
+  case cons hd _ ih => simp +arith [List.foldl_cons, ih (log _ hd), add_assoc, log_add]
 
 -- Folding `log` over a given tally `init` produces the same total digit count as folding `log` over
 -- `⟨0, 0⟩` and adding that to `init`.
 theorem log_total_foldl {ds : List Digit} (init : Tally) :
     (ds.foldl log init).total = (ds.foldl log ⟨0, 0⟩).total + init.total := by
-  induction ds generalizing init
-  case' cons hd _ ih => simp +arith only [List.foldl_cons, ih (log _ hd), log_total]
-  all_goals simp [total]
+  rw [log_foldl]
+  simp
+
+-- Applying `log` increases a tally's total by `1`.
+theorem log_total (d : Digit) (t : Tally) : (t.log d).total = t.total + 1 := by
+  rw [log]
+  split <;> simp +arith [total]
 
 def count (i : Int) : Tally :=
   i.digits.foldl log ⟨0, 0⟩
@@ -63,9 +147,18 @@ theorem count_total_eq_length : (count i).total = i.digits.length := by
   case nil     => rfl
   case cons ih => rw [List.foldl_cons, List.length_cons, log_total_foldl, ih, log_total]; rfl
 
-theorem count_decompose {d : Nat} (hd : d < 10) :
-    count (10 * n + d) = count n + ⟨d % 2, 1 - d % 2⟩ := by
-  sorry
+variable {n d : Nat}
+
+theorem count_of_lt_10 (hd : d < 10) : count d = ⟨1 - d % 2, d % 2⟩ := by
+  simp [count, Nat.digits_of_lt_10, log_digitChar, hd]
+
+theorem count_decompose (hd : d < 10) : count (10 * n + d : Nat) = count n + count d := by
+  simp only [count, Int.digits_cast, Nat.digits_decompose hd, List.foldl_append]
+  rw [log_foldl, add_comm]
+
+theorem count_decompose' (hd : d < 10) :
+    count (10 * n + d : Nat) = count n + ⟨1 - d % 2, d % 2⟩ := by
+  rw [← count_of_lt_10 hd, count_decompose hd]
 
 /-!
 ## Prompt

From a30a5f1f5ac021b24227c863e46ac3c540008d13 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 8 Jun 2025 17:26:04 +0200
Subject: [PATCH 14/25] Decouple "`Int`-ness"

---
 HumanEvalLean/HumanEval155.lean | 57 +++++++++++++--------------------
 1 file changed, 23 insertions(+), 34 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index a5fe015..a074dc7 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -40,20 +40,9 @@ theorem digits_decompose (h : d < 10) (n : Nat) : (10 * n + d).digits = n.digits
 
 end Nat
 
-namespace Int
-
-def digits (i : Int) : List Digit :=
-  i.natAbs.digits
-
 @[simp]
-theorem digits_cast (n : Nat) : (n : Int).digits = n.digits := by
-  simp [digits]
-
-theorem digits_decompose {d : Nat} (h : d < 10) (n : Nat) :
-    digits (10 * n + d : Nat) = n.digits ++ d.digits := by
-  rw [digits, Nat.natAbs_cast, Nat.digits_decompose h]
-
-end Int
+theorem Int.digits_natAbs_cast (n : Nat) : (n : Int).natAbs.digits = n.digits := by
+  simp [Nat.digits]
 
 structure Tally where
   even : Nat
@@ -125,41 +114,41 @@ theorem log_total (d : Digit) (t : Tally) : (t.log d).total = t.total + 1 := by
   rw [log]
   split <;> simp +arith [total]
 
-def count (i : Int) : Tally :=
-  i.digits.foldl log ⟨0, 0⟩
-
-example : count (-12) = ⟨1, 1⟩     := rfl
-example : count 123 = ⟨1, 2⟩       := rfl
-example : count 7 = ⟨0, 1⟩         := rfl
-example : count (-78) = ⟨1, 1⟩     := rfl
-example : count 3452 = ⟨2, 2⟩      := rfl
-example : count 346211 = ⟨3, 3⟩    := rfl
-example : count (-345821) = ⟨3, 3⟩ := rfl
-example : count (-2) = ⟨1, 0⟩      := rfl
-example : count (-45347) = ⟨2, 3⟩  := rfl
-example : count 0 = ⟨1, 0⟩         := rfl
+def count (n : Nat) : Tally :=
+  n.digits.foldl log ⟨0, 0⟩
 
 -- The tally total produced by `count` matches the number of digits in the input.
-theorem count_total_eq_length : (count i).total = i.digits.length := by
+theorem count_total_eq_length : (count n).total = n.digits.length := by
   rw [count]
-  generalize i.digits = ds
+  generalize n.digits = ds
   induction ds
   case nil     => rfl
   case cons ih => rw [List.foldl_cons, List.length_cons, log_total_foldl, ih, log_total]; rfl
 
-variable {n d : Nat}
-
 theorem count_of_lt_10 (hd : d < 10) : count d = ⟨1 - d % 2, d % 2⟩ := by
   simp [count, Nat.digits_of_lt_10, log_digitChar, hd]
 
-theorem count_decompose (hd : d < 10) : count (10 * n + d : Nat) = count n + count d := by
-  simp only [count, Int.digits_cast, Nat.digits_decompose hd, List.foldl_append]
+theorem count_decompose (hd : d < 10) : count (10 * n + d) = count n + count d := by
+  simp only [count, Int.digits_natAbs_cast, Nat.digits_decompose hd, List.foldl_append]
   rw [log_foldl, add_comm]
 
-theorem count_decompose' (hd : d < 10) :
-    count (10 * n + d : Nat) = count n + ⟨1 - d % 2, d % 2⟩ := by
+theorem count_decompose' (hd : d < 10) : count (10 * n + d) = count n + ⟨1 - d % 2, d % 2⟩ := by
   rw [← count_of_lt_10 hd, count_decompose hd]
 
+def evenOddCount (i : Int) : Tally :=
+  count i.natAbs
+
+example : evenOddCount (-12) = ⟨1, 1⟩     := rfl
+example : evenOddCount 123 = ⟨1, 2⟩       := rfl
+example : evenOddCount 7 = ⟨0, 1⟩         := rfl
+example : evenOddCount (-78) = ⟨1, 1⟩     := rfl
+example : evenOddCount 3452 = ⟨2, 2⟩      := rfl
+example : evenOddCount 346211 = ⟨3, 3⟩    := rfl
+example : evenOddCount (-345821) = ⟨3, 3⟩ := rfl
+example : evenOddCount (-2) = ⟨1, 0⟩      := rfl
+example : evenOddCount (-45347) = ⟨2, 3⟩  := rfl
+example : evenOddCount 0 = ⟨1, 0⟩         := rfl
+
 /-!
 ## Prompt
 

From 2a80c5353383bbf103acd600ad93ec915fe4c570 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 8 Jun 2025 17:26:47 +0200
Subject: [PATCH 15/25] Remove redundant lemma

---
 HumanEvalLean/HumanEval155.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index a074dc7..3c64ac3 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,6 +1,3 @@
--- TODO: This already exists in Mathlib.
-@[simp] theorem Nat.natAbs_cast (n : Nat) : (n : Int).natAbs = n := rfl
-
 section Batteries
 
 -- https://github.com/leanprover-community/batteries/pull/1267

From 418be3b3de1738654edeb2fa6f142e7572cf088a Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 8 Jun 2025 17:42:42 +0200
Subject: [PATCH 16/25] Prove `digits_of_lt_10`

---
 HumanEvalLean/HumanEval155.lean | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 3c64ac3..be3c543 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,20 +1,15 @@
 section Batteries
 
 -- https://github.com/leanprover-community/batteries/pull/1267
-@[simp] theorem isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) := sorry
+@[simp] theorem Nat.isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) := sorry
 theorem Nat.mem_toDigits_base_10_isDigit (h : c ∈ toDigits 10 n) : c.isDigit := sorry
-
-theorem Nat.toDigits_10_of_lt_10 (h : n < 10) : toDigits 10 n = [n.digitChar] := by
-  sorry
+theorem Nat.toDigits_10_of_lt_10 (h : n < 10) : toDigits 10 n = [n.digitChar] := sorry
+@[simp] theorem Nat.toDigits_10_natAbs_ofNat (n : Nat) : toDigits 10 (n : Int).natAbs = toDigits 10 n := sorry
 
 theorem Nat.toDigits_10_decompose (h : d < 10) (n : Nat) :
     toDigits 10 (10 * n + d) = (toDigits 10 n) ++ (toDigits 10 d) :=
   sorry
 
-@[simp]
-theorem Nat.toDigits_10_natAbs_cast (n : Nat) : toDigits 10 (n : Int).natAbs = toDigits 10 n :=
-  sorry
-
 end Batteries
 
 abbrev Digit := { c : Char // c.isDigit }
@@ -27,7 +22,10 @@ def digits (n : Nat) : List Digit :=
     |>.map fun ⟨j, h⟩ => ⟨j, Nat.mem_toDigits_base_10_isDigit h⟩
 
 theorem digits_of_lt_10 (h : n < 10) : n.digits = [⟨n.digitChar, by simp_all⟩] := by
-  sorry
+  simp only [digits, List.map_eq_singleton_iff, Subtype.mk.injEq, Subtype.exists, exists_and_right,
+             exists_eq_right]
+  rw [toDigits_10_of_lt_10 h]
+  exists List.mem_singleton_self _
 
 theorem digits_decompose (h : d < 10) (n : Nat) : (10 * n + d).digits = n.digits ++ d.digits := by
   simp [digits]

From cd38c4b9dc6d15c175b6c3db49c08687d3d26c4a Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 8 Jun 2025 18:36:30 +0200
Subject: [PATCH 17/25] Remove redundant lemma

---
 HumanEvalLean/HumanEval155.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index be3c543..241816a 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -4,7 +4,6 @@ section Batteries
 @[simp] theorem Nat.isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) := sorry
 theorem Nat.mem_toDigits_base_10_isDigit (h : c ∈ toDigits 10 n) : c.isDigit := sorry
 theorem Nat.toDigits_10_of_lt_10 (h : n < 10) : toDigits 10 n = [n.digitChar] := sorry
-@[simp] theorem Nat.toDigits_10_natAbs_ofNat (n : Nat) : toDigits 10 (n : Int).natAbs = toDigits 10 n := sorry
 
 theorem Nat.toDigits_10_decompose (h : d < 10) (n : Nat) :
     toDigits 10 (10 * n + d) = (toDigits 10 n) ++ (toDigits 10 d) :=

From 7faf093f311d7c4d72e662c2dece7ede357a3e2a Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 8 Jun 2025 21:46:10 +0200
Subject: [PATCH 18/25] Prove more lemmas

---
 HumanEvalLean/HumanEval155.lean | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 241816a..73535af 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -82,11 +82,17 @@ def log (t : Tally) (d : Digit) : Tally :=
   | _                           => { t with odd  := t.odd  + 1 }
 
 theorem log_add (t₁ t₂ : Tally) (d : Digit) : (t₁.log d) + t₂ = (t₁ + t₂).log d := by
-  sorry
+  simp only [log]
+  split
+  all_goals
+    simp only [(· + ·), Add.add]
+    simp +arith
 
 theorem log_digitChar (h : d < 10) (t : Tally) :
-    t.log ⟨d.digitChar, by simp_all⟩ = t + ⟨1 - d % 2, d % 2⟩ :=
-  sorry
+    t.log ⟨d.digitChar, by simp_all⟩ = t + ⟨1 - d % 2, d % 2⟩ := by
+  match d with
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => rfl
+  | _ + 10                                => contradiction
 
 -- Folding `log` over a given tally `init` produces the same tally as folding `log` over `⟨0, 0⟩`
 -- and adding that to `init`.

From f8085eb2cd410c4f01973f61e5ce1e746a911cd4 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 9 Jun 2025 16:24:28 +0200
Subject: [PATCH 19/25] Update batteries theorems

---
 HumanEvalLean/HumanEval155.lean | 33 ++++++++++++++++++++++++---------
 1 file changed, 24 insertions(+), 9 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 73535af..e681fcc 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,16 +1,31 @@
-section Batteries
+section Batteries -- https://github.com/leanprover-community/batteries/pull/1267
 
--- https://github.com/leanprover-community/batteries/pull/1267
-@[simp] theorem Nat.isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) := sorry
-theorem Nat.mem_toDigits_base_10_isDigit (h : c ∈ toDigits 10 n) : c.isDigit := sorry
-theorem Nat.toDigits_10_of_lt_10 (h : n < 10) : toDigits 10 n = [n.digitChar] := sorry
+@[simp]
+theorem Nat.isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) :=
+  sorry
+
+theorem Nat.isDigit_of_mem_toDigits (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ toDigits b n) :
+    c.isDigit :=
+  sorry
 
-theorem Nat.toDigits_10_decompose (h : d < 10) (n : Nat) :
-    toDigits 10 (10 * n + d) = (toDigits 10 n) ++ (toDigits 10 d) :=
+theorem Nat.toDigits_of_lt_base (h : n < b) : toDigits b n = [n.digitChar] :=
+  sorry
+
+theorem Nat.toDigits_append_toDigits (hb₁ : 1 < b) (hb₂ : b ≤ 10) (hn : 0 < n) (hd : d < b) :
+    (toDigits b n) ++ (toDigits b d) = toDigits b (b * n + d) := by
   sorry
 
 end Batteries
 
+-- TODO: If you want to use induction or recursion here, you probably have to state a lemma for
+--       `Nat.toDigitsCore`, too.
+theorem Nat.toDigits_decompose (hb₁ : 1 < b) (hb₂ : b ≤ 10) (hd : d < b) (n : Nat) :
+    toDigits b (b * n + d) = (toDigits b n) ++ (toDigits b d) := by
+  rw [toDigits, toDigitsCore]
+  split
+  · sorry
+  · sorry
+
 abbrev Digit := { c : Char // c.isDigit }
 
 namespace Nat
@@ -18,12 +33,12 @@ namespace Nat
 def digits (n : Nat) : List Digit :=
   n.toDigits (base := 10)
     |>.attach
-    |>.map fun ⟨j, h⟩ => ⟨j, Nat.mem_toDigits_base_10_isDigit h⟩
+    |>.map fun ⟨j, h⟩ => ⟨j, Nat.isDigit_of_mem_toDigits (by decide) (by decide) h⟩
 
 theorem digits_of_lt_10 (h : n < 10) : n.digits = [⟨n.digitChar, by simp_all⟩] := by
   simp only [digits, List.map_eq_singleton_iff, Subtype.mk.injEq, Subtype.exists, exists_and_right,
              exists_eq_right]
-  rw [toDigits_10_of_lt_10 h]
+  rw [toDigits_of_lt_base h]
   exists List.mem_singleton_self _
 
 theorem digits_decompose (h : d < 10) (n : Nat) : (10 * n + d).digits = n.digits ++ d.digits := by

From 43cce5670187bd82a8203666a86931d5c1281ff0 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 9 Jun 2025 16:25:03 +0200
Subject: [PATCH 20/25] Remove redundant lemma

---
 HumanEvalLean/HumanEval155.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index e681fcc..fb13e32 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -17,15 +17,6 @@ theorem Nat.toDigits_append_toDigits (hb₁ : 1 < b) (hb₂ : b ≤ 10) (hn : 0
 
 end Batteries
 
--- TODO: If you want to use induction or recursion here, you probably have to state a lemma for
---       `Nat.toDigitsCore`, too.
-theorem Nat.toDigits_decompose (hb₁ : 1 < b) (hb₂ : b ≤ 10) (hd : d < b) (n : Nat) :
-    toDigits b (b * n + d) = (toDigits b n) ++ (toDigits b d) := by
-  rw [toDigits, toDigitsCore]
-  split
-  · sorry
-  · sorry
-
 abbrev Digit := { c : Char // c.isDigit }
 
 namespace Nat

From d713664f2bad53b026687ce0890ccfad15759910 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 9 Jun 2025 16:39:32 +0200
Subject: [PATCH 21/25] Fix incorrect lemmas

---
 HumanEvalLean/HumanEval155.lean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index fb13e32..756a95e 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -32,7 +32,8 @@ theorem digits_of_lt_10 (h : n < 10) : n.digits = [⟨n.digitChar, by simp_all
   rw [toDigits_of_lt_base h]
   exists List.mem_singleton_self _
 
-theorem digits_decompose (h : d < 10) (n : Nat) : (10 * n + d).digits = n.digits ++ d.digits := by
+theorem digits_append_digits (hn : 0 < n) (hd : d < 10) :
+    n.digits ++ d.digits = (10 * n + d).digits := by
   simp [digits]
   -- PROBLEM: When appending lists with `attach`es, the membership witnesses change.
   -- rw [toDigits_10_decompose h]
@@ -134,12 +135,14 @@ theorem count_total_eq_length : (count n).total = n.digits.length := by
 theorem count_of_lt_10 (hd : d < 10) : count d = ⟨1 - d % 2, d % 2⟩ := by
   simp [count, Nat.digits_of_lt_10, log_digitChar, hd]
 
-theorem count_decompose (hd : d < 10) : count (10 * n + d) = count n + count d := by
-  simp only [count, Int.digits_natAbs_cast, Nat.digits_decompose hd, List.foldl_append]
-  rw [log_foldl, add_comm]
+theorem count_add (hn : 0 < n) (hd : d < 10) : count n + count d = count (10 * n + d) := by
+  simp only [count, ← Nat.digits_append_digits hn hd, List.foldl_append]
+  conv => rhs; rw [log_foldl]
+  apply add_comm
 
-theorem count_decompose' (hd : d < 10) : count (10 * n + d) = count n + ⟨1 - d % 2, d % 2⟩ := by
-  rw [← count_of_lt_10 hd, count_decompose hd]
+theorem count_decompose (hn : 0 < n) (hd : d < 10) :
+    count (10 * n + d) = count n + ⟨1 - d % 2, d % 2⟩ := by
+  rw [← count_of_lt_10 hd, count_add hn hd]
 
 def evenOddCount (i : Int) : Tally :=
   count i.natAbs

From b4964e0179ce427452604aec8c9e2527c74ff0ad Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 9 Jun 2025 16:41:33 +0200
Subject: [PATCH 22/25] Remove redundant lemma

---
 HumanEvalLean/HumanEval155.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 756a95e..6bbf2e6 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -41,10 +41,6 @@ theorem digits_append_digits (hn : 0 < n) (hd : d < 10) :
 
 end Nat
 
-@[simp]
-theorem Int.digits_natAbs_cast (n : Nat) : (n : Int).natAbs.digits = n.digits := by
-  simp [Nat.digits]
-
 structure Tally where
   even : Nat
   odd  : Nat

From 1d31d93c00d97d3ffd66621456cf15bd800b7d04 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Mon, 9 Jun 2025 16:57:31 +0200
Subject: [PATCH 23/25] Complete all proofs

---
 HumanEvalLean/HumanEval155.lean | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 6bbf2e6..68c9197 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -23,21 +23,14 @@ namespace Nat
 
 def digits (n : Nat) : List Digit :=
   n.toDigits (base := 10)
-    |>.attach
-    |>.map fun ⟨j, h⟩ => ⟨j, Nat.isDigit_of_mem_toDigits (by decide) (by decide) h⟩
+    |>.attachWith (·.isDigit) fun _ h => Nat.isDigit_of_mem_toDigits (by decide) (by decide) h
 
 theorem digits_of_lt_10 (h : n < 10) : n.digits = [⟨n.digitChar, by simp_all⟩] := by
-  simp only [digits, List.map_eq_singleton_iff, Subtype.mk.injEq, Subtype.exists, exists_and_right,
-             exists_eq_right]
-  rw [toDigits_of_lt_base h]
-  exists List.mem_singleton_self _
+  simp [digits, toDigits_of_lt_base h]
 
 theorem digits_append_digits (hn : 0 < n) (hd : d < 10) :
     n.digits ++ d.digits = (10 * n + d).digits := by
-  simp [digits]
-  -- PROBLEM: When appending lists with `attach`es, the membership witnesses change.
-  -- rw [toDigits_10_decompose h]
-  sorry
+  simp [digits, ← toDigits_append_toDigits, *]
 
 end Nat
 

From a4a67e6447f6745d07968e9650b3c269e68b1f52 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 10 Jun 2025 19:00:29 +0200
Subject: [PATCH 24/25] Sorry-free version

---
 HumanEvalLean/HumanEval155.lean | 86 ++++++++++++++++++++++++++++-----
 1 file changed, 74 insertions(+), 12 deletions(-)

diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
index 68c9197..c458cf4 100644
--- a/HumanEvalLean/HumanEval155.lean
+++ b/HumanEvalLean/HumanEval155.lean
@@ -1,19 +1,81 @@
 section Batteries -- https://github.com/leanprover-community/batteries/pull/1267
 
-@[simp]
-theorem Nat.isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) :=
-  sorry
-
-theorem Nat.isDigit_of_mem_toDigits (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ toDigits b n) :
-    c.isDigit :=
-  sorry
-
-theorem Nat.toDigits_of_lt_base (h : n < b) : toDigits b n = [n.digitChar] :=
-  sorry
+namespace Nat
 
-theorem Nat.toDigits_append_toDigits (hb₁ : 1 < b) (hb₂ : b ≤ 10) (hn : 0 < n) (hd : d < b) :
+@[simp]
+theorem isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) :=
+  match n with
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => by simp [digitChar]
+  | _ + 10 => by
+    simp only [digitChar, ↓reduceIte, Nat.reduceEqDiff]
+    (repeat' split) <;> simp
+
+private theorem isDigit_of_mem_toDigitsCore
+    (hc : c ∈ cs → c.isDigit) (hb₁ : 0 < b) (hb₂ : b ≤ 10) (h : c ∈ toDigitsCore b fuel n cs) :
+    c.isDigit := by
+  induction fuel generalizing n cs with rw [toDigitsCore] at h
+  | zero => exact hc h
+  | succ _ ih =>
+    split at h
+    case' isFalse => apply ih (fun h => ?_) h
+    all_goals
+      cases h with
+      | head      => simp [Nat.lt_of_lt_of_le (mod_lt _ hb₁) hb₂]
+      | tail _ hm => exact hc hm
+
+theorem isDigit_of_mem_toDigits (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ toDigits b n) : c.isDigit :=
+  isDigit_of_mem_toDigitsCore (fun _ => by contradiction) hb₁ hb₂ hc
+
+private theorem toDigitsCore_of_lt_base (hb : n < b) (hf : n < fuel) :
+    toDigitsCore b fuel n cs = n.digitChar :: cs := by
+  unfold toDigitsCore
+  split <;> simp_all [mod_eq_of_lt]
+
+theorem toDigits_of_lt_base (h : n < b) : toDigits b n = [n.digitChar] :=
+  toDigitsCore_of_lt_base h (lt_succ_self _)
+
+theorem toDigits_zero : (b : Nat) → toDigits b 0 = ['0']
+  | 0     => rfl
+  | _ + 1 => toDigits_of_lt_base (zero_lt_succ _)
+
+private theorem toDigitsCore_append :
+    toDigitsCore b fuel n cs₁ ++ cs₂ = toDigitsCore b fuel n (cs₁ ++ cs₂) := by
+  induction fuel generalizing n cs₁ with simp only [toDigitsCore]
+  | succ => split <;> simp_all
+
+private theorem toDigitsCore_eq_of_lt_fuel (hb : 1 < b) (h₁ : n < fuel₁) (h₂ : n < fuel₂) :
+    toDigitsCore b fuel₁ n cs = toDigitsCore b fuel₂ n cs := by
+  cases fuel₁ <;> cases fuel₂ <;> try contradiction
+  simp only [toDigitsCore, Nat.div_eq_zero_iff]
+  split
+  · simp
+  · have := Nat.div_lt_self (by omega : 0 < n) hb
+    exact toDigitsCore_eq_of_lt_fuel hb (by omega) (by omega)
+
+private theorem toDigitsCore_toDigitsCore
+    (hb : 1 < b) (hn : 0 < n) (hd : d < b) (hf : b * n + d < fuel) (hnf : n < nf) (hdf : d < df) :
+    toDigitsCore b nf n (toDigitsCore b df d cs) = toDigitsCore b fuel (b * n + d) cs := by
+  cases fuel with
+  | zero => contradiction
+  | succ fuel =>
+    rw [toDigitsCore]
+    split
+    case isTrue h =>
+      have : b ≤ b * n + d := Nat.le_trans (Nat.le_mul_of_pos_right _ hn) (le_add_right _ _)
+      cases Nat.div_eq_zero_iff.mp h <;> omega
+    case isFalse =>
+      have h : (b * n + d) / b = n := by
+        rw [mul_add_div (by omega), Nat.div_eq_zero_iff.mpr (.inr hd), Nat.add_zero]
+      have := (Nat.lt_mul_iff_one_lt_left hn).mpr hb
+      simp only [toDigitsCore_of_lt_base hd hdf, mul_add_mod_self_left, mod_eq_of_lt hd, h]
+      apply toDigitsCore_eq_of_lt_fuel hb hnf (by omega)
+
+theorem toDigits_append_toDigits (hb : 1 < b) (hn : 0 < n) (hd : d < b) :
     (toDigits b n) ++ (toDigits b d) = toDigits b (b * n + d) := by
-  sorry
+  rw [toDigits, toDigitsCore_append]
+  exact toDigitsCore_toDigitsCore hb hn hd (lt_succ_self _) (lt_succ_self _) (lt_succ_self _)
+
+end Nat
 
 end Batteries
 

From 0ff492479c454350f34ef644f81b545f06cdfc8e Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 10 Jun 2025 19:02:31 +0200
Subject: [PATCH 25/25] Undo accidental change

---
 HumanEvalLean/HumanEval5.lean | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index 605d7ef..be980d4 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -1,15 +1,5 @@
-example : [].intersperse 7 = []                              := rfl
-example : [5, 6, 3, 2].intersperse 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
-example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
-
-open List
-
-#check length_intersperse
-#check getElem?_intersperse_two_mul
-#check getElem?_intersperse_two_mul_add_one
-#check getElem_intersperse_two_mul
-#check getElem_intersperse_two_mul_add_one
-#check getElem_eq_getElem_intersperse_two_mul
+def intersperse : Unit :=
+  ()
 
 /-!
 ## Prompt