From 20d6d2e0c75c55408735d6ba57aaca7ba53d31b8 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 07:04:21 +0000
Subject: [PATCH] 27

---
 HumanEvalLean/HumanEval27.lean | 42 +++++++++++++++++++++++++++++++---
 1 file changed, 39 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval27.lean b/HumanEvalLean/HumanEval27.lean
index e933640..7b3edd2 100644
--- a/HumanEvalLean/HumanEval27.lean
+++ b/HumanEvalLean/HumanEval27.lean
@@ -1,7 +1,43 @@
 module
 
-def flip_case : Unit :=
-  ()
+def Char.flipCase (c : Char) : Char :=
+  if c.isLower then
+    c.toUpper
+  else if c.isUpper then
+    c.toLower
+  else
+    c
+
+def flipCase (string : String) : String :=
+  string.map Char.flipCase
+
+example : flipCase "" = "" := by cbv
+example : flipCase "Hello!" = "hELLO!" := by cbv
+example : flipCase "These violent delights have violent ends" = "tHESE VIOLENT DELIGHTS HAVE VIOLENT ENDS" := by cbv
+
+theorem toList_flipCase {string : String} : (flipCase string).toList = string.toList.map Char.flipCase := by
+  simp [flipCase]
+
+namespace Char
+
+@[simp]
+theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
+  simp [← toNat_val]
+
+theorem isUpper_flipCase {c : Char} : c.flipCase.isUpper ↔ c.isLower := by
+  grind [flipCase, isUpper, isLower, toUpper, toLower]
+
+theorem isLower_flipCase {c : Char} : c.flipCase.isLower ↔ c.isUpper := by
+  grind [flipCase, isUpper, isLower, toUpper, toLower]
+
+theorem toLower_flipCase {c : Char} : c.flipCase.toLower = c.toLower := by
+  -- https://github.com/leanprover/lean4/issues/13089
+  simp [flipCase, isUpper, isLower, toUpper, toLower, ← toNat_inj, apply_dite Char.toNat,
+    apply_ite Char.toNat, UInt32.le_iff_toNat_le]
+  grind
+
+end Char
+
 
 /-!
 ## Prompt
@@ -38,4 +74,4 @@ def check(candidate):
     assert candidate('Hello!') == 'hELLO!'
     assert candidate('These violent delights have violent ends') == 'tHESE VIOLENT DELIGHTS HAVE VIOLENT ENDS'
 ```
--/
\ No newline at end of file
+-/