7 and 161

HumanEvalLean/HumanEval161.lean

@@ -1,7 +1,45 @@
 module
+import all Init.Data.String.Lemmas.Pattern.Find.Pred -- TODO: remove when `nightly-2026-03-06` is out
 
-def solve : Unit :=
-  ()
+def reverseString (s : String) : String :=
+  s.revChars.fold (init := "") fun sofar c => sofar.push c
+
+def swapCase (c : Char) : Char :=
+  if c.isUpper then
+    c.toLower
+  else if c.isLower then
+    c.toUpper
+  else
+    c
+
+def solve (s : String) : String :=
+  if s.contains Char.isAlpha then
+    s.map swapCase
+  else
+    reverseString s
+
+example : solve "AsDf" = "aSdF" := by native_decide
+example : solve "1234" = "4321" := by native_decide
+example : solve "ab" = "AB" := by native_decide
+example : solve "#a@C" = "#A@c" := by native_decide
+example : solve "#AsdfW^45" = "#aSDFw^45" := by native_decide
+example : solve "#6@2" = "2@6#" := by native_decide
+example : solve "#$a^D" = "#$A^d" := by native_decide
+example : solve "#ccc" = "#CCC" := by native_decide
+
+@[simp]
+theorem toList_reverseString {s : String} : (reverseString s).toList = s.toList.reverse := by
+  simp only [reverseString, ne_eq, ← Std.Iter.foldl_toList, String.toList_revChars,
+    List.foldl_reverse]
+  induction s.toList <;> simp_all
+
+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_eq, List.any_eq_true]
+  rw [apply_ite String.toList, toList_reverseString, String.toList_map]
 
 /-!
 ## Prompt
@@ -10,7 +48,7 @@ def solve : Unit :=
 
 def solve(s):
     """You are given a string s.
-    if s[i] is a letter, reverse its case from lower to upper or vise versa, 
+    if s[i] is a letter, reverse its case from lower to upper or vise versa,
     otherwise keep it as it is.
     If the string contains no letters, reverse the string.
     The function should return the resulted string.
@@ -59,4 +97,4 @@ def check(candidate):
 
     # Don't remove this line:
 ```
--/
+-/

HumanEvalLean/HumanEval7.lean

@@ -1,7 +1,21 @@
 module
 
-def filter_by_substring : Unit :=
-  ()
+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
+
+open Classical in
+theorem filterBySubstring_eq {strings : Array String} {substring : String} :
+    filterBySubstring strings substring = strings.filter (decide <| substring.toList <:+: ·.toList) := by
+  rw [filterBySubstring]
+  congr
+  ext
+  exact Bool.eq_iff_iff.2 (by simp)
 
 /-!
 ## Prompt
@@ -42,4 +56,4 @@ def check(candidate):
     assert candidate(['xxx', 'asd', 'aaaxxy', 'john doe', 'xxxAAA', 'xxx'], 'xx') == ['xxx', 'aaaxxy', 'xxxAAA', 'xxx']
     assert candidate(['grunt', 'trumpet', 'prune', 'gruesome'], 'run') == ['grunt', 'prune']
 ```
--/
+-/

lean-toolchain

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