Progress on 158

Author: marcusrossel

HumanEvalLean/HumanEval158.lean

@@ -1,5 +1,102 @@
-def find_max : Unit :=
-  ()
+import Lean
+open Std
+
+def String.numUniqueChars (str : String) : Nat :=
+  str.foldl (·.insert) (∅ : HashSet _) |>.size
+
+def findMax (strs : List String) : Option String :=
+  strs.foldl (max? · ·) none
+where
+  max? : Option String → String → String
+  | none,      str  => str
+  | some str₁, str₂ => max str₁ str₂
+  max (str₁ str₂ : String) : String :=
+    match compare str₁.numUniqueChars str₂.numUniqueChars with
+    | .gt => str₁
+    | .lt => str₂
+    | .eq => if str₁ < str₂ then str₁ else str₂
+
+example : findMax ["name", "of", "string"] = "string"                    := by native_decide
+example : findMax ["name", "enam", "game"] = "enam"                      := by native_decide
+example : findMax ["aaaaaaa", "bb" ,"cc"] = "aaaaaaa"                    := by native_decide
+example : findMax ["name", "of", "string"] = "string"                    := by native_decide
+example : findMax ["name", "enam", "game"] = "enam"                      := by native_decide
+example : findMax ["aaaaaaa", "bb", "cc"] = "aaaaaaa"                    := by native_decide
+example : findMax ["abc", "cba"] = "abc"                                 := by native_decide
+example : findMax ["play", "this", "game", "of","footbott"] = "footbott" := by native_decide
+example : findMax ["we", "are", "gonna", "rock"] = "gonna"               := by native_decide
+example : findMax ["we", "are", "a", "mad", "nation"] = "nation"         := by native_decide
+example : findMax ["this", "is", "a", "prrk"] = "this"                   := by native_decide
+example : findMax ["b"] = "b"                                            := by native_decide
+example : findMax ["play", "play", "play"] = "play"                      := by native_decide
+
+theorem findMax_mem (h : findMax strs = some m) : m ∈ strs := by
+  induction strs generalizing m <;> rw [findMax] at h
+  case nil => contradiction
+  case cons ih =>
+    simp [findMax.max?] at h
+    sorry -- Problem: We can't use IH again, cause we haven't generalized over the fold's init.
+          -- Can we use `List.foldl_hom`?
+
+theorem findMax_cons : findMax (hd :: tl) = findMax.max? (findMax tl) hd := by
+  sorry
+
+-- TODO: Does this actually hold? If not, use some sort of lex compare function instead of `<`.
+theorem String.le_of_lt {s₁ s₂ : String} (h : s₁ < s₂) : s₁ ≤ s₂ :=
+  sorry
+
+structure UniqueMax (max : String) (strs : List String) : Prop where
+  mem        : max ∈ strs
+  max_unique : ∀ str ∈ strs, str.numUniqueChars ≤ max.numUniqueChars
+  min_lex    : ∀ str ∈ strs, str.numUniqueChars = max.numUniqueChars → max ≤ str
+
+namespace UniqueMax
+
+theorem tail (h : UniqueMax m (hd :: tl)) (hm : m ∈ tl) : UniqueMax m tl where
+  mem             := hm
+  max_unique _ hm := h.max_unique _ (.tail _ hm)
+  min_lex _ hm    := h.min_lex _ (.tail _ hm)
+
+theorem to_findMax_max (h : UniqueMax m strs) (hm : str ∈ strs) : findMax.max m str = m := by
+  rw [findMax.max]
+  split <;> (try split) <;> try rfl
+  next hc =>
+    rw [Nat.compare_eq_lt] at hc
+    have := h.max_unique _ hm
+    omega
+  next hc hl =>
+    rw [Nat.compare_eq_eq] at hc
+    have := h.min_lex _ hm hc.symm
+    exact String.le_antisymm hl this
+
+theorem to_findMax (h : UniqueMax m strs) : findMax strs = m := by
+  induction strs <;> cases h.mem
+  case cons.tail ih hm => simp [findMax_cons, ih (h.tail hm), findMax.max?, h.to_findMax_max]
+  case cons.head tl ih =>
+    simp only [findMax_cons, findMax.max?, findMax.max]
+    split <;> (try split) <;> (try split) <;> try rfl
+    next hf _ hc =>
+      rw [Nat.compare_eq_gt] at hc
+      have := h.max_unique _ (.tail _ <| findMax_mem hf)
+      omega
+    next hf _ hc hl =>
+      rw [Nat.compare_eq_eq] at hc
+      have := h.min_lex _ (.tail _ <| findMax_mem hf) hc
+      simp [String.le_antisymm (String.le_of_lt hl) this]
+
+theorem of_findMax (h : findMax strs = some m) : UniqueMax m strs where
+  mem := findMax_mem h
+  max_unique str hm := by
+    induction strs
+    case nil     => sorry
+    case cons ih => sorry -- Same problem in IH as with `findMax_mem` above.
+  min_lex := sorry -- Probably by induction with the same problem as commented on above.
+
+theorem iff_findMax : (UniqueMax m strs) ↔ (findMax strs = m) where
+  mp  := to_findMax
+  mpr := of_findMax
+
+end UniqueMax
 
 /-!
 ## Prompt
@@ -44,4 +141,4 @@ def check(candidate):
     assert (candidate(["play", "play", "play"]) == "play"), 't10'
 
 ```
--/
+-/

HumanEvalLean/HumanEval5.lean

@@ -1,5 +1,28 @@
-def intersperse : Unit :=
-  ()
+def intersperse : List Int → Int → List Int
+  | [],             _     => []
+  | [i],            _     => [i]
+  | i₁ :: i₂ :: tl, delim => i₁ :: delim :: intersperse (i₂ :: tl) delim
+
+example : intersperse [] 7 = []                              := rfl
+example : intersperse [5, 6, 3, 2] 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
+example : intersperse [2, 2, 2] 2 = [2, 2, 2, 2, 2]          := rfl
+
+theorem intersperse_length_le : (intersperse nums delim).length ≤ 2 * nums.length - 1 := by
+  fun_induction intersperse <;> simp only [intersperse, List.length_cons] at * <;> omega
+
+-- Every element of index `2 * i` is the `i`th element of the input list.
+theorem intersperse_get?_num (h : 1 < nums.length) :
+    (intersperse nums delim)[2 * i]? = nums[i]? := by
+  fun_induction intersperse generalizing i <;> try contradiction
+  next tl _ ih =>
+    cases tl <;> cases i
+    case nil.succ j =>
+      cases j <;> simp +arith [intersperse]
+    case cons.succ j =>
+      have hj : 2 * (j + 1) = 2 * j + 2 := rfl
+      rw [intersperse, hj]
+      simp [ih]
+    all_goals simp [intersperse]
 
 /-!
 ## Prompt
@@ -50,4 +73,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]
 ```
--/
+-/