HumanEval8

HumanEvalLean/HumanEval8.lean

@@ -1,5 +1,71 @@
-def sum_product : Unit :=
-  ()
+import Std.Tactic.Do
+open Std.Do
+set_option mvcgen.warning false
+
+def List.product (xs : List Int) : Int :=
+  match xs with
+  | [] => 1
+  | x :: xs' => x * (product xs')
+
+def sumProduct (xs : List Int) : Int × Int := (List.sum xs, List.product xs)
+
+def sumProductDo (xs : List Int) : Int × Int := Id.run do
+  let mut sum := 0
+  let mut product := 1
+  for x in xs do
+    sum := sum + x
+    product := product * x
+
+  return (sum, product)
+
+theorem List.sum_append (xs : List Int) (ys : List Int)
+  : sum (xs ++ ys) = sum xs + sum ys := by
+  induction xs with
+  | nil =>
+    change sum ys = 0 + sum ys
+    omega
+  | cons x xs hi =>
+    change x + sum (xs ++ ys) = x + sum xs + sum ys
+    rw [hi]
+    omega
+
+theorem List.product_append (xs : List Int) (ys : List Int)
+  : product (xs ++ ys) = product xs * product ys := by
+  induction xs with
+  | nil =>
+    change product ys = 1 * product ys
+    omega
+  | cons x xs hi =>
+    change x * product (xs ++ ys) = x * product xs * product ys
+    rw [hi]
+    simp only [Int.mul_assoc]
+
+theorem sumProductDo_correct (xs : List Int) : sumProductDo xs = sumProduct xs := by
+  generalize h : sumProductDo xs = ys
+  apply Id.of_wp_run_eq h
+  mvcgen
+  invariants
+  · ⇓ ⟨ cur, result ⟩ =>
+    ⌜ result.snd = List.sum cur.prefix ∧ result.fst = List.product cur.prefix ⌝
+  case vc1.step pref x suff h' result hi =>
+    obtain ⟨ hi₀, hi₁⟩ := hi
+    constructor
+    rw [hi₀, List.sum_append]
+    change List.sum pref + x = List.sum pref + (x + 0)
+    omega
+    rw [hi₁, List.product_append]
+    change List.product pref * x = List.product pref * (x * 1)
+    rw [Int.mul_one]
+  case vc3.a.post.success result h' =>
+    obtain ⟨ left, right ⟩ := h'
+    rw [left, right]
+    rfl
+
+example : sumProductDo [] = (0, 1) := by rfl
+example : sumProductDo [1, 1, 1] = (3, 1) := by rfl
+example : sumProductDo [100, 0] = (100, 0) := by rfl
+example : sumProductDo [3, 5, 7] = (3 + 5 + 7, 3 * 5 * 7) := by rfl
+example : sumProductDo [10] = (10, 10) := by rfl
 
 /-!
 ## Prompt
@@ -48,4 +114,4 @@ def check(candidate):
     assert candidate([3, 5, 7]) == (3 + 5 + 7, 3 * 5 * 7)
     assert candidate([10]) == (10, 10)
 ```
--/
+-/