60,63 (#269)

This PR solves problems 60 and 63.

Author: datokrat

HumanEvalLean/HumanEval60.lean

@@ -1,7 +1,59 @@
 module
 
-def sum_to_n : Unit :=
-  ()
+public import Std
+open Std
+
+set_option cbv.warning false
+
+/-! ## Implementation 1 -/
+
+def sumToN (n : Nat) : Nat :=
+  (n + 1) * n / 2
+
+/-! ## Tests 1 -/
+
+example : sumToN 1 = 1 := by cbv
+example : sumToN 6 = 21 := by cbv
+example : sumToN 11 = 66 := by cbv
+example : sumToN 30 = 465 := by cbv
+example : sumToN 100 = 5050 := by cbv
+
+/-! ## Verification 1 -/
+
+theorem sumToN_zero :
+    sumToN 0 = 0 := by
+  cbv
+
+theorem sumToN_add_one :
+    sumToN (n + 1) = sumToN n + n + 1 := by
+  grind [sumToN]
+
+/-! ## Implementation 2 -/
+
+def sumToN' (n : Nat) : Nat :=
+    (1...=n).iter.fold (init := 0) (· + ·)
+
+/-! ## Tests 2 -/
+
+example : sumToN' 1 = 1 := by native_decide
+example : sumToN' 6 = 21 := by native_decide
+example : sumToN' 11 = 66 := by native_decide
+example : sumToN' 30 = 465 := by native_decide
+example : sumToN' 100 = 5050 := by native_decide
+
+/-! ## Verification 2 -/
+
+theorem sumToN'_zero :
+    sumToN' 0 = 0 := by
+  simp [sumToN', ← Iter.foldl_toList]
+
+theorem sumToN'_add_one :
+    sumToN' (n + 1) = sumToN' n + n + 1 := by
+  simp [sumToN', ← Iter.foldl_toList, Nat.toList_rcc_eq_toList_rco, Nat.add_assoc]
+
+theorem sumToN_eq_sumToN' :
+    sumToN n = sumToN' n := by
+  induction n <;> grind [sumToN_zero, sumToN'_zero, sumToN_add_one, sumToN'_add_one]
 
 /-!
 ## Prompt
@@ -46,4 +98,4 @@ def check(candidate):
     assert candidate(100) == 5050
 
 ```
--/
+-/

HumanEvalLean/HumanEval63.lean

@@ -1,7 +1,86 @@
 module
 
-def fibfib : Unit :=
-  ()
+public import Std
+open Std Std.Do
+
+set_option mvcgen.warning false
+
+/-!
+## Implementation
+
+(See also problem 46.)
+-/
+
+def fibfib (n : Nat) : Nat := Id.run do
+  let mut lastThree : Vector Nat 3 := #v[0, 0, 1]
+  for i in *...(n - 2) do
+    lastThree := lastThree.set (i % 3) (lastThree[0] + lastThree[1] + lastThree[2])
+  return lastThree[n % 3]
+
+/-! ## Tests -/
+
+example : fibfib 2 = 1 := by native_decide
+example : fibfib 1 = 0 := by native_decide
+example : fibfib 5 = 4 := by native_decide
+example : fibfib 8 = 24 := by native_decide
+example : fibfib 10 = 81 := by native_decide
+example : fibfib 12 = 274 := by native_decide
+example : fibfib 14 = 927 := by native_decide
+
+/-! ## Missing API -/
+
+theorem eq_getElem_append_cons {pref suff : List α} {cur : α} :
+    (pref ++ cur :: suff)[pref.length]? = cur := by
+  simp
+
+grind_pattern eq_getElem_append_cons => pref ++ cur :: suff
+attribute [grind =] Nat.getElem?_toList_rio
+attribute [grind =] Nat.length_toList_rio
+
+/-! ## Verification -/
+
+def fibfibReference : Nat → Nat
+  | 0 => 0
+  | 1 => 0
+  | 2 => 1
+  | k + 3 =>
+    fibfibReference (k + 2) + fibfibReference (k + 1) + fibfibReference k
+
+theorem sum_mod_eq_sum {vec : Vector Nat 3} :
+    ∀ i, vec[i % 3] + vec[(i + 1) % 3] + vec[(i + 2) % 3] =
+        vec[0] + vec[1] + vec[2]
+  | 0 | 1 | 2 => by grind
+  | i + 3 => by
+    have := sum_mod_eq_sum (vec := vec) (i := i)
+    simp only [Nat.add_mod_right]
+    grind
+
+theorem fibfib_eq_fibfibReference :
+    fibfib n = fibfibReference n := by
+  generalize hwp : fibfib n = wp
+  apply Id.of_wp_run_eq hwp
+  mvcgen
+  invariants
+  · ⇓⟨cur, lastThree⟩ => ⌜∀ i, i < 3 → lastThree[(cur.pos + i) % 3] = fibfibReference (cur.pos + i)⌝
+  case vc1 pref cur suff heq _ _ h =>
+    simp_all only [List.Cursor.pos_mk, List.length_append, List.length_cons, List.length_nil]
+    intro i hi
+    by_cases i = 2
+    · rename_i hi'
+      rw [hi', fibfibReference]
+      simp only [show (pref.length + 1 + 2) % 3 = cur % 3 by grind]
+      grind [sum_mod_eq_sum, h 0 (by grind), h 1 (by grind), h 2 (by grind),
+        Vector.getElem_set_self]
+    · specialize h (i + 1) (by grind)
+      grind
+  case vc2 =>
+    simp only [List.Cursor.pos_mk, Vector.getElem_eq_iff]
+    decide
+  case vc3 h =>
+    by_cases hn : n < 3
+    · grind
+    · specialize h 2 (by grind)
+      grind
 
 /-!
 ## Prompt
@@ -55,4 +134,4 @@ def check(candidate):
     assert candidate(14) == 927
 
 ```
--/
+-/