22 (#234)

This PR solves problem 22.

Author: datokrat

HumanEvalLean/HumanEval22.lean

@@ -1,7 +1,55 @@
 module
 
-def filter_integers : Unit :=
-  ()
+public import Std
+open Std
+
+public section
+
+/-!
+## Implementation
+
+This Problem assumes a language with dynamic typing. We approximate this by defining an inductive
+`Any` type.
+-/
+
+inductive Any where
+  | int : Int → Any
+  | float : Float → Any
+  | string : String → Any
+
+@[grind =]
+def Any.int? (x : Any) : Option Int :=
+  if let .int a := x then
+    some a
+  else
+    none
+
+@[grind =]
+def filterIntegers (xs : Array Any): Array Int :=
+  xs.filterMap Any.int?
+
+/-! ## Tests -/
+
+example : filterIntegers #[] = #[] := by native_decide
+example : filterIntegers #[.int 4, .float 23.2, .int 9, .string "adasd"] = #[4, 9] := by native_decide
+example : filterIntegers #[.int 3, .string "c", .int 3, .int 3, .string "a", .string "b"] = #[3, 3, 3] := by native_decide
+
+/-! ## Verification -/
+
+section Verification
+
+variable {xs ys : Array Any}
+
+theorem filterIntegers_empty : filterIntegers #[] = #[] := by grind
+theorem filterIntegers_singleton_int : filterIntegers #[.int x] = #[x] := by grind
+theorem filterIntegers_singleton_float : filterIntegers #[.float x] = #[] := by grind
+theorem filterIntegers_singleton_string : filterIntegers #[.string x] = #[] := by grind
+theorem filterIntegers_push_int : filterIntegers (xs.push (.int x)) = (filterIntegers xs).push x := by grind
+theorem filterIntegers_push_float : filterIntegers (xs.push (.float x)) = filterIntegers xs := by grind
+theorem filterIntegers_push_string : filterIntegers (xs.push (.string x)) = filterIntegers xs := by grind
+theorem filterIntegers_append : filterIntegers (x ++ y) = filterIntegers x ++ filterIntegers y := by grind
+
+end Verification
 
 /-!
 ## Prompt
@@ -41,4 +89,4 @@ def check(candidate):
     assert candidate([4, {}, [], 23.2, 9, 'adasd']) == [4, 9]
     assert candidate([3, 'c', 3, 3, 'a', 'b']) == [3, 3, 3]
 ```
--/
+-/