HumanEval155

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
 
 ```
--/
+-/