Overhaul definitions

Author: marcusrossel

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
 
 /-!