HumanEval5

HumanEvalLean/HumanEval5.lean

@@ -1,5 +1,36 @@
-def intersperse : Unit :=
-  ()
+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 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
+
+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
 
 /-!
 ## Prompt
@@ -50,4 +81,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]
 ```
--/
+-/