Done

Author: TwoFX

HumanEvalLean/HumanEval161.lean

@@ -1,4 +1,5 @@
 module
+import all Init.Data.String.Lemmas.Pattern.Find.Pred -- TODO: remove when `nightly-2026-03-06` is out
 
 def reverseString (s : String) : String :=
   s.revChars.fold (init := "") fun sofar c => sofar.push c
@@ -32,16 +33,12 @@ theorem toList_reverseString {s : String} : (reverseString s).toList = s.toList.
     List.foldl_reverse]
   induction s.toList <;> simp_all
 
-@[simp]
-theorem String.contains_bool {s : String} {p : Char → Bool} :
-    s.contains p = s.toList.any p := sorry
-
 theorem toList_solve {s : String} : (solve s).toList =
     if s.toList.any Char.isAlpha then
       s.toList.map swapCase
     else
       s.toList.reverse := by
-  simp only [solve, String.contains_bool, List.any_eq_true]
+  simp only [solve, String.contains_bool_eq, List.any_eq_true]
   rw [apply_ite String.toList, toList_reverseString, String.toList_map]
 
 /-!

HumanEvalLean/HumanEval7.lean

@@ -1,16 +1,14 @@
 module
 
 def filterBySubstring (strings : Array String) (substring : String) : Array String :=
+  -- Uses KMP string search!
   strings.filter (·.contains substring)
 
 example : filterBySubstring #[] "john" = #[] := by native_decide
 example : filterBySubstring #["xxx", "asd", "xxy", "john doe", "xxxAAA", "xxx"] "xxx" = #["xxx", "xxxAAA", "xxx"] := by native_decide
 example : filterBySubstring #["xxx", "asd", "aaaxxy", "john doe", "xxxAAA", "xxx"] "xx" = #["xxx", "aaaxxy", "xxxAAA", "xxx"] := by native_decide
 example : filterBySubstring #["grunt", "trumpet", "prune", "gruesome"] "run" = #["grunt", "prune"] := by native_decide
 
-@[simp]
-theorem String.contains_string_iff_infix {s t : String} : s.contains t ↔ t.toList <:+: s.toList := sorry
-
 open Classical in
 theorem filterBySubstring_eq {strings : Array String} {substring : String} :
     filterBySubstring strings substring = strings.filter (decide <| substring.toList <:+: ·.toList) := by

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-03-04
+leanprover/lean4:nightly-2026-03-05