52

Author: datokrat

HumanEvalLean/HumanEval52.lean

@@ -1,7 +1,28 @@
 module
 
-def below_threshold : Unit :=
-  ()
+set_option cbv.warning false
+
+public section
+
+/-! ## Implementation -/
+
+def belowThreshold (xs : List Nat) (t : Nat) : Bool :=
+  xs.all (· < t)
+
+/-! ## Tests -/
+
+example : belowThreshold [1, 2, 4, 10] 100 = true := by cbv
+example : belowThreshold [1, 20, 4, 10] 5 = false := by cbv
+example : belowThreshold [1, 20, 4, 10] 21 = true := by cbv
+example : belowThreshold [1, 20, 4, 10] 22 = true := by cbv
+example : belowThreshold [1, 8, 4, 10] 11 = true := by cbv
+example : belowThreshold [1, 8, 4, 10] 10 = false := by cbv
+
+/-! ## Verification -/
+
+theorem belowThreshold_iff :
+    belowThreshold xs t ↔ ∀ x ∈ xs, x < t := by
+  grind [belowThreshold]
 
 /-!
 ## Prompt
@@ -44,4 +65,4 @@ def check(candidate):
     assert not candidate([1, 8, 4, 10], 10)
 
 ```
--/
+-/