From 54d467abeaf1a38a5237b583d4a2b2ab30912a6a Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 7 Jan 2026 11:54:32 +0100
Subject: [PATCH 1/6] wip

---
 HumanEvalLean/HumanEval12.lean | 218 ++++++++++++++++++++++++++++++++-
 1 file changed, 215 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index 2dcd6c5..06f9b47 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -1,5 +1,217 @@
-def longest : Unit :=
-  ()
+/-!
+## Implementation
+-/
+
+def argmax [LE β] [DecidableLE β] (f : α → β) (x y : α) : α :=
+  if f y ≤ f x then x else y
+
+def List.argmax [LE β] [DecidableLE β] (xs : List α) (f : α → β) (h : xs ≠ []) : α :=
+  match xs with
+  | x :: xs => xs.foldl (init := x) (_root_.argmax f)
+
+def List.argmax? [LE β] [DecidableLE β] (xs : List α) (f : α → β) : Option α :=
+  if h : xs ≠ [] then
+    some (xs.argmax f h)
+  else
+    none
+
+def longest (xs : List String) : Option String :=
+  xs.argmax? String.length
+
+/-!
+## Verification
+-/
+
+/--
+A list attains its maximum (with respect to function `f`) at element `x` if `x` appears in
+the list and the function applied to all elements is at most the function applied to `x`.
+-/
+def AttainsMaximumAt [LE β] (xs : List α) (f : α → β) (x : α) : Prop :=
+  x ∈ xs ∧ ∀ y ∈ xs, f y ≤ f x
+
+/--
+A string has maximum length in a list if it appears in the list and all strings in the
+list are at most as long.
+-/
+def HasMaxLength (s : String) (xs : List String) : Prop :=
+  s ∈ xs ∧ ∀ t ∈ xs, t.length ≤ s.length
+
+@[grind =]
+theorem List.argmax_singleton [LE β] [DecidableLE β] {x : α} {f : α → β} :
+    [x].argmax f (by grind) = x := by
+  grind [argmax]
+
+@[grind =]
+theorem argmax_assoc [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y z : α} :
+    argmax f (argmax f x y) z = argmax f x (argmax f y z) := by
+  grind [argmax]
+
+instance [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} :
+    Std.Associative (argmax f) where
+  assoc := by apply argmax_assoc
+
+theorem List.argmax_cons [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α} {f : α → β} :
+    (x :: xs).argmax f (by grind) = if h : xs = [] then x else _root_.argmax f x (xs.argmax f h) := by
+  simp only [argmax]
+  match xs with
+  | [] => simp
+  | y :: xs => simp [foldl_assoc]
+
+theorem List.foldl_etaExpand {α : Type u} {β : Type v} {f : α → β → α} {init : α} {xs : List β} :
+    xs.foldl (init := init) f = xs.foldl (init := init) fun a b => f a b := by
+  rfl
+
+theorem argmax_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
+    argmax f x y = x ∨ argmax f x y = y := by
+  grind [argmax]
+
+@[grind =]
+theorem argmax_self [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} :
+    argmax f x x = x := by
+  grind [argmax]
+
+@[grind =]
+theorem argmax_eq_left [LE β] [DecidableLE β] {f : α → β} {x y : α} (h : f y ≤ f x) :
+    argmax f x y = x := by
+  grind [argmax]
+
+@[grind =]
+theorem argmax_eq_right [LE β] [DecidableLE β] {f : α → β} {x y : α} (h : ¬ f y ≤ f x) :
+    argmax f x y = y := by
+  grind [argmax]
+
+@[grind =>]
+theorem apply_left_le_apply_argmax [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} :
+    f x ≤ f (argmax f x y) := by
+  grind [argmax]
+
+@[grind =>]
+theorem apply_right_le_apply_argmax [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} :
+    f y ≤ f (argmax f x y) := by
+  grind [argmax]
+
+@[grind .]
+theorem List.argmax_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {h : xs ≠ []} :
+    xs.argmax f h ∈ xs := by
+  simp only [List.argmax]
+  match xs with
+  | x :: xs =>
+    fun_induction xs.foldl (init := x) (_root_.argmax f) <;> grind [argmax_eq_or]
+
+theorem List.apply_le_apply_argmax [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {h : xs ≠ []} {y : α} (hx : y ∈ xs) :
+    f y ≤ f (xs.argmax f h) := by
+  simp only [List.argmax]
+  match xs with
+  | x :: xs =>
+    fun_induction xs.foldl (init := x) (_root_.argmax f) generalizing y <;> grind
+
+/-- `List.argmax xs f h` returns an element that attains the maximum of `f` over `xs`. -/
+theorem List.argmax_attainsMaximum [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
+    AttainsMaximumAt xs f (xs.argmax f h) := by
+  sorry
+
+/--
+`List.argmax xs f h` returns the first element that attains the maximum any other element
+that attains the maximum appears at an index greater than or equal to the returned element's index.
+-/
+theorem List.argmax_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
+    ∃ j : Nat, xs[j]? = some (xs.argmax f h) ∧
+      ∀ (i : Nat) (hi : i < xs.length), f (xs.argmax f h) ≤ f xs[i] → j ≤ i := by
+  simp only [List.argmax]
+  match xs with
+  | x :: xs =>
+    simp only
+    clear h
+    fun_induction xs.foldl (init := x) (_root_.argmax f)
+    · exact ⟨0, by grind⟩
+    · rename_i x y xs ih
+      obtain ⟨j, ih⟩ := ih
+      by_cases hj : j = 0
+      · cases hj
+        by_cases hm : f y ≤ f x
+        · exact ⟨0, by grind⟩
+        · exact ⟨1, by grind⟩
+      · refine ⟨j + 1, ?_⟩
+        obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj
+        apply And.intro
+        · grind
+        · intro i hi hle
+          have : i ≥ 2 := by have := ih.2 0; grind
+          obtain ⟨i, rfl⟩ := Nat.exists_eq_add_of_le this
+          have := ih.2 (i + 1)
+          grind
+
+@[grind =]
+theorem List.argmax_append [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
+    {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
+    (xs ++ ys).argmax f (by simp [hxs]) = _root_.argmax f (xs.argmax f hxs) (ys.argmax f hys) := by
+  match xs, ys with
+  | x :: xs, y :: ys => simp [argmax, foldl_assoc]
+
+/-- `List.argmax?` returns `none` when applied to an empty list. -/
+@[grind =]
+theorem List.argmax?_nil [LE β] [DecidableLE β] {f : α → β} :
+    ([] : List α).argmax? f = none := by
+  simp [argmax?]
+
+/-- `List.argmax?` returns `some` when applied to a non-empty list. -/
+@[grind =]
+theorem List.isSome_argmax? [LE β] [DecidableLE β] {f : α → β} {xs : List α} (hxs : xs ≠ []) :
+    (xs.argmax? f).isSome := by
+  grind [argmax?]
+
+@[grind =]
+theorem List.argmax?_cons [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} :
+    (x :: xs).argmax? f = (xs.argmax? f).elim x (_root_.argmax f x) := by
+  grind [argmax?, argmax_cons]
+
+/--
+When `List.argmax? xs f` returns `some x`, the element `x` is the first that attains the maximum.
+-/
+theorem List.argmax?_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (x : α)
+    (hx : xs.argmax? f = some x) :
+    ∃ j : Nat, xs[j]? = some x ∧ ∀ (i : Nat) (hi : i < xs.length), f x ≤ f xs[i] → j ≤ i := by
+  simp only [argmax?] at hx
+  split at hx
+  · simp only [Option.some.injEq] at hx
+    rw [← hx]
+    apply argmax_left_leaning
+  · grind
+
+@[grind =]
+theorem List.argmax?_append [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs ys : List α) (f : α → β) :
+    (xs ++ ys).argmax? f =
+      (xs.argmax? f).merge (_root_.argmax f) (ys.argmax? f) := by
+  grind [argmax?, append_eq_nil_iff]
+
+theorem List.attainsMaximum_argmax? [LE β] [DecidableLE β] {xs : List α} {f : α → β} {x : α}
+    (hx : xs.argmax? f = some x) :
+    AttainsMaximumAt xs f x := by
+  sorry
+
+/-- `longest` returns `none` when applied to an empty list. -/
+theorem longest_nil : longest [] = none := by
+  grind [longest]
+
+theorem longest_append {xs ys : List String} :
+    longest (xs ++ ys) = (longest xs).merge (_root_.argmax String.length) (longest ys) := by
+  grind [longest]
+
+/--
+`longest` returns a string with maximum length when applied to a non-empty list.
+-/
+theorem longest_hasMaxLength (xs : List String) (h : xs ≠ []) :
+    ∃ s, longest xs = some s ∧ HasMaxLength s xs := by
+  sorry
+
+/--
+`longest` returns the first string with maximum length: any other string with maximum length
+appears at an index greater than the returned string's index.
+-/
+theorem longest_left_leaning {xs : List String} {x : String} (h : longest xs = some x) :
+    ∃ j : Fin xs.length, xs[j] = x ∧ ∀ i : Fin j, xs[i].length < x.length := by
+  sorry
+
 
 /-!
 ## Prompt
@@ -48,4 +260,4 @@ def check(candidate):
     assert candidate(['x', 'y', 'z']) == 'x'
     assert candidate(['x', 'yyy', 'zzzz', 'www', 'kkkk', 'abc']) == 'zzzz'
 ```
--/
\ No newline at end of file
+-/

From a3f47da5cd142d371c4e61ec054665d32e5dde30 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 7 Jan 2026 12:25:40 +0100
Subject: [PATCH 2/6] wip

---
 HumanEvalLean/HumanEval12.lean | 94 +++++++++++++++++++---------------
 1 file changed, 53 insertions(+), 41 deletions(-)

diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index 06f9b47..2612e22 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -15,7 +15,7 @@ def List.argmax? [LE β] [DecidableLE β] (xs : List α) (f : α → β) : Optio
   else
     none
 
-def longest (xs : List String) : Option String :=
+def longest? (xs : List String) : Option String :=
   xs.argmax? String.length
 
 /-!
@@ -98,8 +98,10 @@ theorem List.argmax_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs :
   | x :: xs =>
     fun_induction xs.foldl (init := x) (_root_.argmax f) <;> grind [argmax_eq_or]
 
-theorem List.apply_le_apply_argmax [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {h : xs ≠ []} {y : α} (hx : y ∈ xs) :
-    f y ≤ f (xs.argmax f h) := by
+@[grind =>]
+theorem List.le_apply_argmax_of_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
+    f y ≤ f (xs.argmax f (List.ne_nil_of_mem hx)) := by
+  have h : xs ≠ [] := List.ne_nil_of_mem hx
   simp only [List.argmax]
   match xs with
   | x :: xs =>
@@ -115,30 +117,29 @@ theorem List.argmax_attainsMaximum [LE β] [DecidableLE β] [Std.IsLinearPreorde
 that attains the maximum appears at an index greater than or equal to the returned element's index.
 -/
 theorem List.argmax_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
-    ∃ j : Nat, xs[j]? = some (xs.argmax f h) ∧
-      ∀ (i : Nat) (hi : i < xs.length), f (xs.argmax f h) ≤ f xs[i] → j ≤ i := by
+    ∃ j : Fin xs.length, xs[j] = xs.argmax f h ∧
+      ∀ i : Fin j, ¬ f (xs.argmax f h) ≤ f xs[i] := by
   simp only [List.argmax]
   match xs with
   | x :: xs =>
     simp only
     clear h
     fun_induction xs.foldl (init := x) (_root_.argmax f)
-    · exact ⟨0, by grind⟩
+    · exact ⟨⟨0, by grind⟩, by grind⟩
     · rename_i x y xs ih
       obtain ⟨j, ih⟩ := ih
-      by_cases hj : j = 0
-      · cases hj
-        by_cases hm : f y ≤ f x
-        · exact ⟨0, by grind⟩
-        · exact ⟨1, by grind⟩
-      · refine ⟨j + 1, ?_⟩
-        obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj
+      by_cases hj : j.val = 0
+      · by_cases hm : f y ≤ f x
+        · exact ⟨⟨0, by grind⟩, by grind⟩
+        · exact ⟨⟨1, by grind⟩, by grind⟩
+      · refine ⟨⟨j + 1, by grind⟩, ?_⟩
+        obtain ⟨j, _⟩ := Nat.exists_eq_succ_of_ne_zero hj
         apply And.intro
         · grind
-        · intro i hi hle
-          have : i ≥ 2 := by have := ih.2 0; grind
-          obtain ⟨i, rfl⟩ := Nat.exists_eq_add_of_le this
-          have := ih.2 (i + 1)
+        · intro i hi
+          have : i.val ≥ 2 := by have := ih.2 ⟨0, by grind⟩; grind
+          obtain ⟨i, _⟩ := Nat.exists_eq_add_of_le this
+          have := ih.2 ⟨i + 1, by grind⟩
           grind
 
 @[grind =]
@@ -154,23 +155,29 @@ theorem List.argmax?_nil [LE β] [DecidableLE β] {f : α → β} :
     ([] : List α).argmax? f = none := by
   simp [argmax?]
 
-/-- `List.argmax?` returns `some` when applied to a non-empty list. -/
-@[grind =]
-theorem List.isSome_argmax? [LE β] [DecidableLE β] {f : α → β} {xs : List α} (hxs : xs ≠ []) :
-    (xs.argmax? f).isSome := by
-  grind [argmax?]
-
 @[grind =]
 theorem List.argmax?_cons [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} :
     (x :: xs).argmax? f = (xs.argmax? f).elim x (_root_.argmax f x) := by
   grind [argmax?, argmax_cons]
 
+@[grind =>]
+theorem List.isSome_argmax?_of_mem [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
+    (xs.argmax? f).isSome := by
+  grind [argmax?]
+
+theorem List.le_apply_argmax?_get_of_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
+    f x ≤ f ((xs.argmax? f).get (isSome_argmax?_of_mem h)) := by
+  grind [argmax?]
+
+-- The suggested patterns all involve `IsLinearPreorder`, which is a problem.
+grind_pattern List.le_apply_argmax?_get_of_mem => x ∈ xs, (xs.argmax? f).get _
+
 /--
 When `List.argmax? xs f` returns `some x`, the element `x` is the first that attains the maximum.
 -/
-theorem List.argmax?_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (x : α)
+theorem List.argmax?_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {x : α}
     (hx : xs.argmax? f = some x) :
-    ∃ j : Nat, xs[j]? = some x ∧ ∀ (i : Nat) (hi : i < xs.length), f x ≤ f xs[i] → j ≤ i := by
+    ∃ j : Fin xs.length, xs[j] = x ∧ ∀ i : Fin j, ¬ f x ≤ f xs[i] := by
   simp only [argmax?] at hx
   split at hx
   · simp only [Option.some.injEq] at hx
@@ -189,29 +196,34 @@ theorem List.attainsMaximum_argmax? [LE β] [DecidableLE β] {xs : List α} {f :
     AttainsMaximumAt xs f x := by
   sorry
 
-/-- `longest` returns `none` when applied to an empty list. -/
-theorem longest_nil : longest [] = none := by
-  grind [longest]
+/-- `longest?` returns `none` when applied to an empty list. -/
+theorem longest?_nil : longest? [] = none := by
+  grind [longest?]
 
-theorem longest_append {xs ys : List String} :
-    longest (xs ++ ys) = (longest xs).merge (_root_.argmax String.length) (longest ys) := by
-  grind [longest]
+theorem longest?_singleton : longest? [x] = some x := by
+  grind [longest?]
 
-/--
-`longest` returns a string with maximum length when applied to a non-empty list.
--/
-theorem longest_hasMaxLength (xs : List String) (h : xs ≠ []) :
-    ∃ s, longest xs = some s ∧ HasMaxLength s xs := by
-  sorry
+theorem longest?_append {xs ys : List String} :
+    longest? (xs ++ ys) = (longest? xs).merge (_root_.argmax String.length) (longest? ys) := by
+  grind [longest?]
+
+theorem isSome_longest?_of_mem {xs : List String} {x : String} (h : x ∈ xs) :
+    (longest? xs).isSome := by
+  grind [longest?]
+
+theorem le_length_longest?_get_of_mem {xs : List String} {x : String} (h : x ∈ xs) :
+    x.length ≤ ((longest? xs).get (isSome_longest?_of_mem h)).length := by
+  grind [longest?]
 
 /--
-`longest` returns the first string with maximum length: any other string with maximum length
+`longest?` returns the first string with maximum length: any other string with maximum length
 appears at an index greater than the returned string's index.
 -/
-theorem longest_left_leaning {xs : List String} {x : String} (h : longest xs = some x) :
+theorem longest?_left_leaning {xs : List String} {x : String} (h : longest? xs = some x) :
     ∃ j : Fin xs.length, xs[j] = x ∧ ∀ i : Fin j, xs[i].length < x.length := by
-  sorry
-
+  rw [longest?] at h
+  have := List.argmax?_left_leaning h
+  grind
 
 /-!
 ## Prompt

From cf90ca8c440ed78ede3430981e4beeeeae587cf9 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 7 Jan 2026 13:49:23 +0100
Subject: [PATCH 3/6] wip

---
 HumanEvalLean/HumanEval12.lean | 93 +++++++++++++++++-----------------
 1 file changed, 47 insertions(+), 46 deletions(-)

diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index 2612e22..0f6687e 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -1,3 +1,7 @@
+module
+
+open Std
+
 /-!
 ## Implementation
 -/
@@ -19,22 +23,16 @@ def longest? (xs : List String) : Option String :=
   xs.argmax? String.length
 
 /-!
-## Verification
+## Tests
 -/
 
-/--
-A list attains its maximum (with respect to function `f`) at element `x` if `x` appears in
-the list and the function applied to all elements is at most the function applied to `x`.
--/
-def AttainsMaximumAt [LE β] (xs : List α) (f : α → β) (x : α) : Prop :=
-  x ∈ xs ∧ ∀ y ∈ xs, f y ≤ f x
+example : longest? [] = none := by native_decide
+example : longest? ["x", "y", "z"] = some "x" := by native_decide
+example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by native_decide
 
-/--
-A string has maximum length in a list if it appears in the list and all strings in the
-list are at most as long.
+/-!
+## Verification
 -/
-def HasMaxLength (s : String) (xs : List String) : Prop :=
-  s ∈ xs ∧ ∀ t ∈ xs, t.length ≤ s.length
 
 @[grind =]
 theorem List.argmax_singleton [LE β] [DecidableLE β] {x : α} {f : α → β} :
@@ -42,16 +40,18 @@ theorem List.argmax_singleton [LE β] [DecidableLE β] {x : α} {f : α → β}
   grind [argmax]
 
 @[grind =]
-theorem argmax_assoc [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y z : α} :
+theorem argmax_assoc [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {x y z : α} :
     argmax f (argmax f x y) z = argmax f x (argmax f y z) := by
   grind [argmax]
 
-instance [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} :
-    Std.Associative (argmax f) where
+instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
+    Associative (argmax f) where
   assoc := by apply argmax_assoc
 
-theorem List.argmax_cons [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α} {f : α → β} :
-    (x :: xs).argmax f (by grind) = if h : xs = [] then x else _root_.argmax f x (xs.argmax f h) := by
+theorem List.argmax_cons
+    [LE β] [DecidableLE β] [IsLinearPreorder β] {x : α} {xs : List α} {f : α → β} :
+    (x :: xs).argmax f (by grind) =
+      if h : xs = [] then x else _root_.argmax f x (xs.argmax f h) := by
   simp only [argmax]
   match xs with
   | [] => simp
@@ -66,7 +66,7 @@ theorem argmax_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
   grind [argmax]
 
 @[grind =]
-theorem argmax_self [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} :
+theorem argmax_self [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {x : α} :
     argmax f x x = x := by
   grind [argmax]
 
@@ -81,25 +81,26 @@ theorem argmax_eq_right [LE β] [DecidableLE β] {f : α → β} {x y : α} (h :
   grind [argmax]
 
 @[grind =>]
-theorem apply_left_le_apply_argmax [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} :
-    f x ≤ f (argmax f x y) := by
+theorem apply_left_le_apply_argmax [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
+    {x y : α} : f x ≤ f (argmax f x y) := by
   grind [argmax]
 
 @[grind =>]
-theorem apply_right_le_apply_argmax [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} :
-    f y ≤ f (argmax f x y) := by
+theorem apply_right_le_apply_argmax [LE β] [DecidableLE β] [IsLinearPreorder β]
+    {f : α → β} {x y : α} : f y ≤ f (argmax f x y) := by
   grind [argmax]
 
 @[grind .]
-theorem List.argmax_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {h : xs ≠ []} :
-    xs.argmax f h ∈ xs := by
+theorem List.argmax_mem [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
+    {f : α → β} {h : xs ≠ []} : xs.argmax f h ∈ xs := by
   simp only [List.argmax]
   match xs with
   | x :: xs =>
     fun_induction xs.foldl (init := x) (_root_.argmax f) <;> grind [argmax_eq_or]
 
 @[grind =>]
-theorem List.le_apply_argmax_of_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
+theorem List.le_apply_argmax_of_mem [LE β] [DecidableLE β] [IsLinearPreorder β]
+    {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
     f y ≤ f (xs.argmax f (List.ne_nil_of_mem hx)) := by
   have h : xs ≠ [] := List.ne_nil_of_mem hx
   simp only [List.argmax]
@@ -107,16 +108,12 @@ theorem List.le_apply_argmax_of_mem [LE β] [DecidableLE β] [Std.IsLinearPreord
   | x :: xs =>
     fun_induction xs.foldl (init := x) (_root_.argmax f) generalizing y <;> grind
 
-/-- `List.argmax xs f h` returns an element that attains the maximum of `f` over `xs`. -/
-theorem List.argmax_attainsMaximum [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
-    AttainsMaximumAt xs f (xs.argmax f h) := by
-  sorry
-
 /--
 `List.argmax xs f h` returns the first element that attains the maximum any other element
 that attains the maximum appears at an index greater than or equal to the returned element's index.
 -/
-theorem List.argmax_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
+theorem List.argmax_left_leaning
+    [LE β] [DecidableLE β] [IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
     ∃ j : Fin xs.length, xs[j] = xs.argmax f h ∧
       ∀ i : Fin j, ¬ f (xs.argmax f h) ≤ f xs[i] := by
   simp only [List.argmax]
@@ -143,7 +140,7 @@ theorem List.argmax_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder
           grind
 
 @[grind =]
-theorem List.argmax_append [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
+theorem List.argmax_append [LE β] [DecidableLE β] [IsLinearPreorder β] {xs ys : List α}
     {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
     (xs ++ ys).argmax f (by simp [hxs]) = _root_.argmax f (xs.argmax f hxs) (ys.argmax f hys) := by
   match xs, ys with
@@ -156,26 +153,26 @@ theorem List.argmax?_nil [LE β] [DecidableLE β] {f : α → β} :
   simp [argmax?]
 
 @[grind =]
-theorem List.argmax?_cons [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} :
+theorem List.argmax?_cons
+    [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} :
     (x :: xs).argmax? f = (xs.argmax? f).elim x (_root_.argmax f x) := by
   grind [argmax?, argmax_cons]
 
 @[grind =>]
-theorem List.isSome_argmax?_of_mem [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
+theorem List.isSome_argmax?_of_mem
+    [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     (xs.argmax? f).isSome := by
   grind [argmax?]
 
-theorem List.le_apply_argmax?_get_of_mem [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
+theorem List.le_apply_argmax?_get_of_mem
+    [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     f x ≤ f ((xs.argmax? f).get (isSome_argmax?_of_mem h)) := by
   grind [argmax?]
 
--- The suggested patterns all involve `IsLinearPreorder`, which is a problem.
+-- The suggested patterns are not useful because all involve `IsLinearPreorder`.
 grind_pattern List.le_apply_argmax?_get_of_mem => x ∈ xs, (xs.argmax? f).get _
 
-/--
-When `List.argmax? xs f` returns `some x`, the element `x` is the first that attains the maximum.
--/
-theorem List.argmax?_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {x : α}
+theorem List.argmax?_left_leaning [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α} {f : α → β} {x : α}
     (hx : xs.argmax? f = some x) :
     ∃ j : Fin xs.length, xs[j] = x ∧ ∀ i : Fin j, ¬ f x ≤ f xs[i] := by
   simp only [argmax?] at hx
@@ -186,17 +183,21 @@ theorem List.argmax?_left_leaning [LE β] [DecidableLE β] [Std.IsLinearPreorder
   · grind
 
 @[grind =]
-theorem List.argmax?_append [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs ys : List α) (f : α → β) :
+theorem List.argmax?_append [LE β] [DecidableLE β] [IsLinearPreorder β] (xs ys : List α) (f : α → β) :
     (xs ++ ys).argmax? f =
       (xs.argmax? f).merge (_root_.argmax f) (ys.argmax? f) := by
   grind [argmax?, append_eq_nil_iff]
 
-theorem List.attainsMaximum_argmax? [LE β] [DecidableLE β] {xs : List α} {f : α → β} {x : α}
-    (hx : xs.argmax? f = some x) :
-    AttainsMaximumAt xs f x := by
-  sorry
+/-!
+### Main theorems
+
+The following theorems verify important properties of `longest?`.
+The requirements from the prompt are verified by `le_length_longest?_get_of_mem` and
+`longest?_left_leaning`.
+
+Some other useful properties are proved by the remaining lemmas.
+-/
 
-/-- `longest?` returns `none` when applied to an empty list. -/
 theorem longest?_nil : longest? [] = none := by
   grind [longest?]
 

From 2af3c47ff3d41d5aa5dfd8927633ef592e5d3e89 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 7 Jan 2026 14:21:30 +0100
Subject: [PATCH 4/6] failed attempt to prove lemma using argmax_append

---
 HumanEvalLean/HumanEval12.lean | 40 ++++++++++++++++++++++++++--------
 1 file changed, 31 insertions(+), 9 deletions(-)

diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index 0f6687e..5c13c71 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -108,14 +108,43 @@ theorem List.le_apply_argmax_of_mem [LE β] [DecidableLE β] [IsLinearPreorder 
   | x :: xs =>
     fun_induction xs.foldl (init := x) (_root_.argmax f) generalizing y <;> grind
 
+@[grind =]
+theorem List.argmax_append [LE β] [DecidableLE β] [IsLinearPreorder β] {xs ys : List α}
+    {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
+    (xs ++ ys).argmax f (by simp [hxs]) = _root_.argmax f (xs.argmax f hxs) (ys.argmax f hys) := by
+  match xs, ys with
+  | x :: xs, y :: ys => simp [argmax, foldl_assoc]
+
 /--
-`List.argmax xs f h` returns the first element that attains the maximum any other element
-that attains the maximum appears at an index greater than or equal to the returned element's index.
+`List.argmax xs f h` comes before any other element in `xs` where `f` attains its maximum.
 -/
 theorem List.argmax_left_leaning
     [LE β] [DecidableLE β] [IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
     ∃ j : Fin xs.length, xs[j] = xs.argmax f h ∧
       ∀ i : Fin j, ¬ f (xs.argmax f h) ≤ f xs[i] := by
+  -- open scoped Classical in
+  -- let j := xs.findIdx (· == xs.argmax f h)
+  -- have hj : xs[j]'(by grind) == xs.argmax f h := by grind
+  -- refine ⟨⟨j, by grind⟩, by grind, ?_⟩
+  -- intro i
+  -- let lhs := xs.take j
+  -- let rhs := xs.drop j
+  -- have h₁ : xs = lhs ++ rhs := by simp [lhs, rhs]
+  -- let ml := lhs.argmax? f
+  -- let mr := rhs.argmax? f
+  -- by_cases lhs = []; grind
+  -- by_cases rhs = []; grind
+  -- have h₂ := argmax_append (xs := lhs) (ys := rhs) (f := f) ‹_› ‹_›
+  -- simp only [h₁, h₂, Fin.getElem_fin] at hj ⊢
+  -- rw [getElem_append_left (by grind)]
+  -- rw [getElem_append_right (by grind)] at hj
+  -- simp only [show j - lhs.length = 0 by grind] at hj
+  -- have : rhs.argmax f (by grind) = rhs[0]'(by grind) := by grind
+  -- have : lhs.argmax f (by grind) = lhs[0]'(by grind) := by
+
+  -- have : ¬ f (rhs.argmax f (by grind)) ≤ f (lhs.argmax f (by grind)) := by
+  --   intro h
+  --   rw [_root_.argmax_eq_left ‹_›] at h₂
   simp only [List.argmax]
   match xs with
   | x :: xs =>
@@ -139,13 +168,6 @@ theorem List.argmax_left_leaning
           have := ih.2 ⟨i + 1, by grind⟩
           grind
 
-@[grind =]
-theorem List.argmax_append [LE β] [DecidableLE β] [IsLinearPreorder β] {xs ys : List α}
-    {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
-    (xs ++ ys).argmax f (by simp [hxs]) = _root_.argmax f (xs.argmax f hxs) (ys.argmax f hys) := by
-  match xs, ys with
-  | x :: xs, y :: ys => simp [argmax, foldl_assoc]
-
 /-- `List.argmax?` returns `none` when applied to an empty list. -/
 @[grind =]
 theorem List.argmax?_nil [LE β] [DecidableLE β] {f : α → β} :

From fbf4576401dd7939d7aa23493701d5a9476f0740 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 7 Jan 2026 14:32:24 +0100
Subject: [PATCH 5/6] remove commented code

---
 HumanEvalLean/HumanEval12.lean | 23 -----------------------
 1 file changed, 23 deletions(-)

diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index 5c13c71..bba6b10 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -122,29 +122,6 @@ theorem List.argmax_left_leaning
     [LE β] [DecidableLE β] [IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
     ∃ j : Fin xs.length, xs[j] = xs.argmax f h ∧
       ∀ i : Fin j, ¬ f (xs.argmax f h) ≤ f xs[i] := by
-  -- open scoped Classical in
-  -- let j := xs.findIdx (· == xs.argmax f h)
-  -- have hj : xs[j]'(by grind) == xs.argmax f h := by grind
-  -- refine ⟨⟨j, by grind⟩, by grind, ?_⟩
-  -- intro i
-  -- let lhs := xs.take j
-  -- let rhs := xs.drop j
-  -- have h₁ : xs = lhs ++ rhs := by simp [lhs, rhs]
-  -- let ml := lhs.argmax? f
-  -- let mr := rhs.argmax? f
-  -- by_cases lhs = []; grind
-  -- by_cases rhs = []; grind
-  -- have h₂ := argmax_append (xs := lhs) (ys := rhs) (f := f) ‹_› ‹_›
-  -- simp only [h₁, h₂, Fin.getElem_fin] at hj ⊢
-  -- rw [getElem_append_left (by grind)]
-  -- rw [getElem_append_right (by grind)] at hj
-  -- simp only [show j - lhs.length = 0 by grind] at hj
-  -- have : rhs.argmax f (by grind) = rhs[0]'(by grind) := by grind
-  -- have : lhs.argmax f (by grind) = lhs[0]'(by grind) := by
-
-  -- have : ¬ f (rhs.argmax f (by grind)) ≤ f (lhs.argmax f (by grind)) := by
-  --   intro h
-  --   rw [_root_.argmax_eq_left ‹_›] at h₂
   simp only [List.argmax]
   match xs with
   | x :: xs =>

From b369e2728bf7cd78a355b0898692fdffac0b6c78 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 7 Jan 2026 15:06:20 +0100
Subject: [PATCH 6/6] clean up

---
 HumanEvalLean/HumanEval12.lean | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index bba6b10..84a8192 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -9,6 +9,17 @@ open Std
 def argmax [LE β] [DecidableLE β] (f : α → β) (x y : α) : α :=
   if f y ≤ f x then x else y
 
+/-
+`List.argmax` exists in mathlib, but:
+* it returns an `Option`, so it should actually be named `argmax?`
+* it relies on mathlib's `Preorder` type class and `DecidableLT`. In the standard library,
+  it would be more consistent to use `LE` and `DecidableLE`.
+
+Moreover, lemmas such as `List.index_of_argmax` aren't easily applicable because one would need
+`BEq α` and `LawfulBEq α` in order to use `idxOf`. Moreover, some API about `idxOf` and `findIdx`
+is still missing. In this file, we avoid these difficulties by not relying on `idxOf` and `findIdx`
+at all.
+-/
 def List.argmax [LE β] [DecidableLE β] (xs : List α) (f : α → β) (h : xs ≠ []) : α :=
   match xs with
   | x :: xs => xs.foldl (init := x) (_root_.argmax f)
@@ -57,10 +68,6 @@ theorem List.argmax_cons
   | [] => simp
   | y :: xs => simp [foldl_assoc]
 
-theorem List.foldl_etaExpand {α : Type u} {β : Type v} {f : α → β → α} {init : α} {xs : List β} :
-    xs.foldl (init := init) f = xs.foldl (init := init) fun a b => f a b := by
-  rfl
-
 theorem argmax_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
     argmax f x y = x ∨ argmax f x y = y := by
   grind [argmax]
@@ -119,7 +126,7 @@ theorem List.argmax_append [LE β] [DecidableLE β] [IsLinearPreorder β] {xs ys
 `List.argmax xs f h` comes before any other element in `xs` where `f` attains its maximum.
 -/
 theorem List.argmax_left_leaning
-    [LE β] [DecidableLE β] [IsLinearPreorder β] (xs : List α) (f : α → β) (h : xs ≠ []) :
+    [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) :
     ∃ j : Fin xs.length, xs[j] = xs.argmax f h ∧
       ∀ i : Fin j, ¬ f (xs.argmax f h) ≤ f xs[i] := by
   simp only [List.argmax]