72

HumanEvalLean/HumanEval72.lean

@@ -1,7 +1,83 @@
 module
 
-def will_it_fly : Unit :=
-  ()
+/-!
+## Missing API
+-/
+
+@[specialize P]
+def decideBallLTImpl (Q : Nat → Prop) (n : Nat) (h : ∀ k, k < n → Q k) (P : ∀ k : Nat, Q k → Bool) : Bool :=
+  match n with
+  | 0 => true
+  | n' + 1 => P n' (h n' (Nat.lt_add_one _)) && decideBallLTImpl Q n' (fun _ h' => h _ (Nat.lt_add_right 1 h')) P
+
+theorem decidableBallLTImpl_iff :
+    decideBallLTImpl Q n h P ↔ ∀ (k : Nat) (hk : k < n), P k (h k hk) := by
+  induction n
+  · simp [decideBallLTImpl]
+  · rename_i n ih
+    simp [decideBallLTImpl, ih]
+    constructor
+    · intro h k hk
+      by_cases hkn : k = n
+      · exact hkn ▸ h.1
+      · apply h.2
+        omega
+    · intro h
+      constructor
+      · apply h
+        exact Nat.lt_add_one _
+      · intro k hk
+        apply h k
+        exact Nat.lt_add_right 1 hk
+
+theorem decideBallLTImpl_eq_false_iff :
+    decideBallLTImpl Q n h P = false ↔ ∃ (k : Nat) (hk : k < n), ¬ P k (h k hk) := by
+  rw [← Bool.not_eq_true, decidableBallLTImpl_iff]
+  simp
+
+instance decidableBallLTImpl (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)] :
+    Decidable (∀ n h, P n h) :=
+  match h : decideBallLTImpl _ n (fun _ => id) (P · ·) with
+  | false => isFalse (by simpa [decideBallLTImpl_eq_false_iff] using h)
+  | true => isTrue (by simpa [decidableBallLTImpl_iff] using h)
+
+attribute [- instance] Nat.decidableBallLT
+
+/-!
+## Implementation
+-/
+
+/--
+Efficient, short-circuiting
+-/
+def willItFly (q : List Nat) (w : Nat) : Bool :=
+  q.sum ≤ w ∧ ∀ (i : Nat) (hi : i < q.length / 2), q[i] = q[q.length - 1 - i]
+
+/-!
+## Tests
+-/
+
+set_option cbv.warning false
+
+example : willItFly [3, 2, 3] 9 = true := by cbv
+example : willItFly [1, 2] 5 = false := by cbv
+example : willItFly [3] 5 = true := by cbv
+example : willItFly [3, 2, 3] 1 = false := by cbv
+example : willItFly [1, 2, 3] 6 = false := by cbv
+example : willItFly [5] 5 = true := by cbv
+
+/-!
+## Verification
+-/
+
+theorem willItFly_iff_le_and_forall :
+    willItFly q w ↔ q.sum ≤ w ∧ ∀ (i : Nat) (hi : i < q.length), q[i] = q[q.length - 1 - i] := by
+  grind [willItFly]
+
+theorem willItFly_iff_le_and_reverse_eq_self :
+    willItFly q w ↔ q.sum ≤ w ∧ q.reverse = q := by
+  rw [List.ext_getElem_iff]
+  grind [willItFly]
 
 /-!
 ## Prompt
@@ -14,7 +90,7 @@ def will_it_fly(q,w):
     The object q will fly if it's balanced (it is a palindromic list) and the sum of its elements is less than or equal the maximum possible weight w.
 
     Example:
-    will_it_fly([1, 2], 5) ➞ False 
+    will_it_fly([1, 2], 5) ➞ False
     # 1+2 is less than the maximum possible weight, but it's unbalanced.
 
     will_it_fly([3, 2, 3], 1) ➞ False
@@ -60,4 +136,4 @@ def check(candidate):
     assert candidate([5], 5) is True
 
 ```
--/
+-/