From 61187c22d81908429211c0048aebfae2b2b520c4 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Mon, 23 Mar 2026 09:43:59 +0000
Subject: [PATCH 1/2] 16

---
 HumanEvalLean/HumanEval16.lean | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval16.lean b/HumanEvalLean/HumanEval16.lean
index 7ccdee8..592f46b 100644
--- a/HumanEvalLean/HumanEval16.lean
+++ b/HumanEvalLean/HumanEval16.lean
@@ -1,7 +1,31 @@
 module
+import Std.Data.Iterators.Consumers.Set
+import Std.Data.Iterators.Lemmas.Consumers.Set
+import Std.Data.HashSet.Lemmas
 
-def count_distinct_characters : Unit :=
-  ()
+open Std
+
+def countDistinctCharacters (s : String) : Nat :=
+  (s.chars.map Char.toLower).toHashSet.size
+
+theorem countDistinctCharacters_eq {s : String} :
+    countDistinctCharacters s = (HashSet.ofList (s.toList.map Char.toLower)).size := by
+  simp [countDistinctCharacters, Iter.toHashSet_equiv_ofList.size_eq]
+
+theorem countDistinctCharacters_empty : countDistinctCharacters "" = 0 := by
+  simp [countDistinctCharacters_eq]
+
+theorem countDistinctCharacters_push {s : String} {c : Char} :
+    countDistinctCharacters (s.push c) =
+      if c.toLower ∈ s.toList.map Char.toLower then
+        countDistinctCharacters s
+      else
+        countDistinctCharacters s + 1 := by
+  simp only [countDistinctCharacters_eq, String.toList_push, List.map_append, List.map_cons,
+    List.map_nil, List.mem_map]
+  rw [HashSet.ofList_equiv_foldl.size_eq, List.foldl_append, List.foldl_cons, List.foldl_nil,
+    HashSet.size_insert]
+  simp [← HashSet.ofList_equiv_foldl.mem_iff, ← HashSet.ofList_equiv_foldl.size_eq]
 
 /-!
 ## Prompt
@@ -42,4 +66,4 @@ def check(candidate):
     assert candidate('aaaaAAAAaaaa') == 1
     assert candidate('Jerry jERRY JeRRRY') == 5
 ```
--/
\ No newline at end of file
+-/

From a05e03b2ffd960de36a12af75ea3f4986020c642 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Mon, 23 Mar 2026 09:48:19 +0000
Subject: [PATCH 2/2] Examples

---
 HumanEvalLean/HumanEval16.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/HumanEvalLean/HumanEval16.lean b/HumanEvalLean/HumanEval16.lean
index 592f46b..deff3dd 100644
--- a/HumanEvalLean/HumanEval16.lean
+++ b/HumanEvalLean/HumanEval16.lean
@@ -8,6 +8,12 @@ open Std
 def countDistinctCharacters (s : String) : Nat :=
   (s.chars.map Char.toLower).toHashSet.size
 
+example : countDistinctCharacters "" = 0 := by native_decide
+example : countDistinctCharacters "abcde" = 5 := by native_decide
+example : countDistinctCharacters ("abcde" ++ "cade" ++ "CADE") = 5 := by native_decide
+example : countDistinctCharacters "aaaaAAAAaaaa" = 1 := by native_decide
+example : countDistinctCharacters "Jerry jERRY JeRRRY" = 5 := by native_decide
+
 theorem countDistinctCharacters_eq {s : String} :
     countDistinctCharacters s = (HashSet.ofList (s.toList.map Char.toLower)).size := by
   simp [countDistinctCharacters, Iter.toHashSet_equiv_ofList.size_eq]