64

Author: TwoFX

HumanEvalLean/HumanEval64.lean

@@ -1,7 +1,38 @@
 module
+import Std
 
-def vowels_count : Unit :=
-  ()
+open Std
+
+def vowelsList : List Char :=
+  ['a', 'e', 'i', 'o', 'u', 'A', 'E', 'I', 'O', 'U']
+
+def vowels : HashSet Char :=
+  .ofList vowelsList
+
+def vowelsCount (s : String) : Nat :=
+  let nVowels := s.chars.filter (· ∈ vowels) |>.length
+  let atEnd := if s.back?.any (fun c => c == 'y' || c == 'Y') then 1 else 0
+  nVowels + atEnd
+
+example : vowelsCount "abcde" = 2 := by native_decide
+example : vowelsCount "Alone" = 3 := by native_decide
+example : vowelsCount "key" = 2 := by native_decide
+example : vowelsCount "bye" = 1 := by native_decide
+example : vowelsCount "keY" = 2 := by native_decide
+example : vowelsCount "bYe" = 1 := by native_decide
+example : vowelsCount "ACEDY" = 3 := by native_decide
+
+theorem String.back?_eq {s : String} : s.back? = s.toList.getLast? :=
+  sorry -- https://github.com/leanprover/lean4/pull/13105
+
+theorem vowelsCount_eq {s : String} :
+    vowelsCount s = (s.toList.filter (· ∈ vowelsList)).length +
+      (if s.toList.getLast? = some 'y' ∨ s.toList.getLast? = some 'Y' then 1 else 0) := by
+  simp only [vowelsCount, ne_eq, ← Iter.length_toList_eq_length,
+    Iter.toList_filter, String.toList_chars, ↓Char.isValue]
+  simp only [vowels, HashSet.mem_ofList, List.contains_eq_mem, decide_eq_true_eq, ↓Char.isValue,
+    Option.any_eq_true, Bool.or_eq_true, beq_iff_eq, Nat.add_left_cancel_iff]
+  simp [and_comm, String.back?_eq]
 
 /-!
 ## Prompt
@@ -54,4 +85,4 @@ def check(candidate):
     assert True, "This prints if this assert fails 2 (also good for debugging!)"
 
 ```
--/
+-/