127 (#215)

This solves problem 127.

Author: datokrat

HumanEvalLean/Common/IsPrime.lean

@@ -0,0 +1,79 @@
+module
+
+import Std.Data.Iterators
+import Std.Tactic.Do
+
+open Std
+
+public def isPrime (n : Nat) : Bool :=
+  let divisors := (2...<n).iter.takeWhile (fun i => i * i ≤ n) |>.filter (· ∣ n)
+  2 ≤ n ∧ divisors.fold (init := 0) (fun count _ => count + 1) = 0
+
+public def IsPrime (n : Nat) : Prop :=
+  2 ≤ n ∧ ∀ d : Nat, d ∣ n → d = 1 ∨ d = n
+
+public theorem isPrime_iff {n : Nat} :
+    IsPrime n ↔ (2 ≤ n ∧ ∀ d : Nat, d ∣ n → d = 1 ∨ d = n) :=
+  Iff.rfl
+
+public theorem two_le_of_isPrime {n : Nat} (h : IsPrime n) :
+    2 ≤ n := by
+  grind [isPrime_iff]
+
+public theorem isPrime_eq_true_iff {n : Nat} :
+    isPrime n = true ↔ 2 ≤ n ∧
+        (List.filter (· ∣ n) (List.takeWhile (fun i => i * i ≤ n) (2...n).toList)).length = 0 := by
+  simp [isPrime, ← Iter.foldl_toList]
+
+public theorem isPrime_iff_mul_self {n : Nat} :
+    IsPrime n ↔ (2 ≤ n ∧ ∀ (a : Nat), 2 ≤ a ∧ a < n → a ∣ n → n < a * a) := by
+  rw [IsPrime]
+  by_cases hn : 2 ≤ n; rotate_left; grind
+  apply Iff.intro
+  · grind
+  · rintro ⟨hn, h⟩
+    refine ⟨hn, fun d hd => ?_⟩
+    have : 0 < d := Nat.pos_of_dvd_of_pos hd (by grind)
+    have : d ≤ n := Nat.le_of_dvd (by grind) hd
+    false_or_by_contra
+    by_cases hsq : d * d ≤ n
+    · specialize h d
+      grind
+    · replace h := h (n / d) ?_ ?_; rotate_left
+      · have : d ≥ 2 := by grind
+        refine ⟨?_, Nat.div_lt_self (n := n) (k := d) (by grind) (by grind)⟩
+        false_or_by_contra; rename_i hc
+        have : n / d * d ≤ 1 * d := Nat.mul_le_mul_right d (Nat.le_of_lt_succ (Nat.lt_of_not_ge hc))
+        grind [Nat.dvd_iff_div_mul_eq]
+      · exact Nat.div_dvd_of_dvd hd
+      simp only [Nat.not_le] at hsq
+      have := Nat.mul_lt_mul_of_lt_of_lt h hsq
+      replace : n * n < ((n / d) * d) * ((n / d) * d) := by grind
+      rw [Nat.dvd_iff_div_mul_eq] at hd
+      rw [hd] at this
+      grind
+
+theorem List.takeWhile_eq_filter {P : α → Bool} {xs : List α}
+    (h : xs.Pairwise (fun x y => P y → P x)) :
+    xs.takeWhile P = xs.filter P := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [takeWhile_cons, filter_cons]
+    simp only [pairwise_cons] at h
+    split
+    · simp [*]
+    · simpa [*] using h
+
+public theorem isPrime_eq_true_iff_isPrime {n : Nat} :
+    isPrime n ↔ IsPrime n := by
+  simp only [isPrime_eq_true_iff]
+  by_cases hn : 2 ≤ n; rotate_left
+  · grind [IsPrime]
+  rw [List.takeWhile_eq_filter]; rotate_left
+  · apply Std.Rco.pairwise_toList_le.imp
+    intro a b hab hb
+    have := Nat.mul_self_le_mul_self hab
+    grind
+  -- `mem_toList_iff_mem` and `mem_iff` should be simp lemmas
+  simp [hn, isPrime_iff_mul_self, Std.Rco.mem_toList_iff_mem, Std.Rco.mem_iff]

HumanEvalLean/HumanEval127.lean

@@ -1,5 +1,146 @@
-def intersection : Unit :=
-  ()
+module
+
+import HumanEvalLean.Common.IsPrime
+meta import HumanEvalLean.Common.IsPrime -- for `native_decide`
+
+/-!
+## Implementation
+-/
+
+def intersection (p : Int × Int) (q : Int × Int) : String :=
+  let l := max p.1 q.1
+  let r := min p.2 q.2
+  let length := r - l
+  if length > 0 ∧ isPrime length.toNat then "YES" else "NO"
+
+/-!
+## Tests
+-/
+
+example : intersection (1, 2) (2, 3) = "NO" := by native_decide
+example : intersection (-1, 1) (0, 4) = "NO" := by native_decide
+example : intersection (-3, -1) (-5, 5) = "YES" := by native_decide
+example : intersection (-2, 2) (-4, 0) = "YES" := by native_decide
+example : intersection (-11, 2) (-1, -1) = "NO" := by native_decide
+example : intersection (1, 2) (3, 5) = "NO" := by native_decide
+example : intersection (1, 2) (1, 2) = "NO" := by native_decide
+example : intersection (-2, -2) (-3, -2) = "NO" := by native_decide
+
+/-!
+## Missing API
+-/
+
+-- stolen from Init.Data.Range.Polymorphic.Lemmas, which is private
+private theorem eq_of_pairwise_lt_of_mem_iff_mem {lt : α → α → Prop} [asymm : Std.Asymm lt]
+    {l l' : List α} (hl : l.Pairwise lt) (hl' : l'.Pairwise lt)
+    (h : ∀ a, a ∈ l ↔ a ∈ l') : l = l' := by
+  induction l generalizing l'
+  · cases l'
+    · rfl
+    · rename_i x xs
+      specialize h x
+      simp at h
+  · rename_i x xs ih
+    cases l'
+    · specialize h x
+      simp at h
+    · have hx := (h x).mp (List.mem_cons_self)
+      cases List.mem_cons.mp hx
+      · rename_i y ys heq
+        cases heq
+        simp only [List.cons.injEq, true_and]
+        apply ih hl.tail hl'.tail
+        intro a
+        specialize h a
+        constructor
+        · intro haxs
+          replace h := h.mp (List.mem_cons_of_mem _ haxs)
+          cases List.mem_cons.mp h
+          · rename_i heq
+            cases heq
+            simp only [List.pairwise_cons] at hl
+            have := hl.1 x haxs
+            cases Std.Asymm.asymm _ _ this this
+          · simp [*]
+        · intro hays
+          replace h := h.mpr (List.mem_cons_of_mem _ hays)
+          cases List.mem_cons.mp h
+          · rename_i heq
+            cases heq
+            simp only [List.pairwise_cons] at hl'
+            have := hl'.1 x hays
+            cases Std.Asymm.asymm _ _ this this
+          · simp [*]
+      · rename_i y ys hx
+        simp only [List.pairwise_cons] at hl'
+        have hlt := hl'.1 _ hx
+        have hmem : y ∈ x :: xs := (h y).mpr List.mem_cons_self
+        cases List.mem_cons.mp hmem
+        · rename_i heq
+          cases heq
+          cases Std.Asymm.asymm _ _ hlt hlt
+        · simp only [List.pairwise_cons] at hl
+          have hgt := hl.1 y ‹_›
+          cases Std.Asymm.asymm _ _ hlt hgt
+
+deriving instance DecidableEq for Std.Rcc
+
+/-!
+## Verification
+-/
+
+theorem intersection_swap {p q} :
+    intersection p q = intersection q p := by
+  grind [intersection]
+
+theorem intersection_mem {p q} :
+    intersection p q ∈ ["YES", "NO"] := by
+  grind [intersection]
+
+/--
+According to the problem description, the length of a range is the difference of its bounds.
+Caution: This is different from the size of the range, a.k.a. `r.size` and `r.toList.length`.
+-/
+def intervalLength (r : Std.Rcc Int) : Nat :=
+  (r.upper - r.lower).toNat
+
+example : intervalLength (2...=3) = 1 := by decide -- example from the problem description
+example : intervalLength (2...=2) = 0 := by decide
+example : intervalLength (5...=0) = 0 := by decide
+
+section IntervalIntersection
+
+def intervalIntersection (r s : Std.Rcc Int) : Std.Rcc Int :=
+  (max r.lower s.lower)...=(min r.upper s.upper)
+
+example : intervalIntersection (1...=3) (2...=4) = (2...=3) := by native_decide
+
+/-! The following three lemmas justify the name `intervalIntersection`. -/
+
+theorem mem_intervalIntersection_iff {l₁ r₁ l₂ r₂ x} :
+    x ∈ intervalIntersection (l₁...=r₁) (l₂...=r₂) ↔ x ∈ (l₁...=r₁) ∧ x ∈ (l₂...=r₂) := by
+  grind [intervalIntersection, Std.Rcc.mem_iff]
+
+theorem intervalIntersection_swap {r s} :
+    intervalIntersection r s = intervalIntersection s r := by
+  grind [intervalIntersection]
+
+theorem toList_intervalIntersection_eq_filter_mem_rcc_toList_rcc {l₁ r₁ l₂ r₂} :
+    (intervalIntersection (l₁...=r₁) (l₂...=r₂)).toList = (l₁...=r₁).toList.filter (· ∈ l₂...=r₂) := by
+  apply eq_of_pairwise_lt_of_mem_iff_mem (lt := LT.lt)
+  · apply Std.Rcc.pairwise_toList_lt
+  · apply List.Pairwise.filter
+    apply Std.Rcc.pairwise_toList_lt
+  · grind [mem_intervalIntersection_iff, Std.Rcc.mem_toList_iff_mem]
+
+end IntervalIntersection
+
+theorem intersection_spec {p q} :
+    intersection p q = "YES" ↔ IsPrime (intervalLength (intervalIntersection (p.1...=p.2) (q.1...=q.2))) := by
+  simp only [intersection, isPrime_eq_true_iff_isPrime, ite_eq_left_iff]
+  suffices h : (min p.2 q.2 - max p.1 q.1).toNat = intervalLength (intervalIntersection (p.1...=p.2) (q.1...=q.2))  by
+    grind [isPrime_iff]
+  grind [intervalLength, intervalIntersection]
 
 /-!
 ## Prompt
@@ -12,7 +153,7 @@ def intersection(interval1, interval2):
     The given intervals are closed which means that the interval (start, end)
     includes both start and end.
     For each given interval, it is assumed that its start is less or equal its end.
-    Your task is to determine whether the length of intersection of these two 
+    Your task is to determine whether the length of intersection of these two
     intervals is a prime number.
     Example, the intersection of the intervals (1, 3), (2, 4) is (2, 3)
     which its length is 1, which not a prime number.
@@ -67,4 +208,4 @@ def check(candidate):
     assert candidate((-2, -2), (-3, -2)) == "NO"
 
 ```
--/
+-/

HumanEvalLean/HumanEval150.lean

@@ -1,7 +1,12 @@
+module
+
 import Std.Data.Iterators
 import Init.Notation
 import Std.Tactic.Do
 
+import HumanEvalLean.Common.IsPrime
+meta import HumanEvalLean.Common.IsPrime -- for `native_decide`
+
 open Std
 
 set_option mvcgen.warning false
@@ -10,10 +15,6 @@ set_option mvcgen.warning false
 ## Implementation
 -/
 
-def isPrime (n : Nat) : Bool :=
-  let divisors := (2...<n).iter.takeWhile (fun i => i * i ≤ n) |>.filter (· ∣ n)
-  2 ≤ n ∧ divisors.fold (init := 0) (fun count _ => count + 1) = 0
-
 def x_or_y (n : Int) (x y : α) : α := Id.run do
   let some n := n.toNat? | return y
   if isPrime n then
@@ -43,71 +44,10 @@ example : x_or_y 2 2 0 = 2 := by native_decide
 ## Verification
 -/
 
-def IsPrime (n : Nat) : Prop :=
-  2 ≤ n ∧ ∀ d : Nat, d ∣ n → d = 1 ∨ d = n
-
-theorem isPrime_eq_true_iff {n : Nat} :
-    isPrime n = true ↔ 2 ≤ n ∧
-        (List.filter (· ∣ n) (List.takeWhile (fun i => i * i ≤ n) (2...n).toList)).length = 0 := by
-  simp [isPrime, ← Iter.foldl_toList]
-
 example {n d : Nat} (h : n / d * d = n) (h' : n * n < n / d * d * (n / d * d)) : False := by
   rw [h] at h' -- Why do we need this?
   grind
 
-theorem isPrime_iff_mul_self {n : Nat} :
-    IsPrime n ↔ (2 ≤ n ∧ ∀ (a : Nat), 2 ≤ a ∧ a < n → a ∣ n → n < a * a) := by
-  rw [IsPrime]
-  by_cases hn : 2 ≤ n; rotate_left; grind
-  apply Iff.intro
-  · grind
-  · rintro ⟨hn, h⟩
-    refine ⟨hn, fun d hd => ?_⟩
-    have : 0 < d := Nat.pos_of_dvd_of_pos hd (by grind)
-    have : d ≤ n := Nat.le_of_dvd (by grind) hd
-    false_or_by_contra
-    by_cases hsq : d * d ≤ n
-    · specialize h d
-      grind
-    · replace h := h (n / d) ?_ ?_; rotate_left
-      · have : d ≥ 2 := by grind
-        refine ⟨?_, Nat.div_lt_self (n := n) (k := d) (by grind) (by grind)⟩
-        false_or_by_contra; rename_i hc
-        have : n / d * d ≤ 1 * d := Nat.mul_le_mul_right d (Nat.le_of_lt_succ (Nat.lt_of_not_ge hc))
-        grind [Nat.dvd_iff_div_mul_eq]
-      · exact Nat.div_dvd_of_dvd hd
-      simp only [Nat.not_le] at hsq
-      have := Nat.mul_lt_mul_of_lt_of_lt h hsq
-      replace : n * n < ((n / d) * d) * ((n / d) * d) := by grind
-      rw [Nat.dvd_iff_div_mul_eq] at hd
-      rw [hd] at this
-      grind
-
-theorem List.takeWhile_eq_filter {P : α → Bool} {xs : List α}
-    (h : xs.Pairwise (fun x y => P y → P x)) :
-    xs.takeWhile P = xs.filter P := by
-  induction xs with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [takeWhile_cons, filter_cons]
-    simp only [pairwise_cons] at h
-    split
-    · simp [*]
-    · simpa [*] using h
-
-theorem isPrime_eq_true_iff_isPrime {n : Nat} :
-    isPrime n ↔ IsPrime n := by
-  simp only [isPrime_eq_true_iff]
-  by_cases hn : 2 ≤ n; rotate_left
-  · grind [IsPrime]
-  rw [List.takeWhile_eq_filter]; rotate_left
-  · apply Std.Rco.pairwise_toList_le.imp
-    intro a b hab hb
-    have := Nat.mul_self_le_mul_self hab
-    grind
-  -- `mem_toList_iff_mem` and `mem_iff` should be simp lemmas
-  simp [hn, isPrime_iff_mul_self, Std.Rco.mem_toList_iff_mem, Std.Rco.mem_iff]
-
 open Classical in
 theorem x_or_y_of_isPrime {n : Int} {x y : α} :
     x_or_y n x y = if n ≥ 0 ∧ IsPrime n.toNat then x else y := by