Task 96

HumanEvalLean/HumanEval96.lean

@@ -1,5 +1,180 @@
-def count_up_to : Unit :=
-  ()
+import Std.Data.HashSet
+import HumanEvalLean.ProvedElsewhere
+
+set_option grind.warning false
+
+theorem Nat.dvd_def (n m : Nat) : n ∣ m ↔ ∃ c, m = n * c := by rfl
+
+theorem Nat.not_dvd_of_lt_and_pos (n m : Nat) (h : n < m) (h' : 0 < n): ¬ m ∣ n := by
+  simp [Nat.dvd_def]
+  intro x
+  cases x with
+  | zero => grind
+  | succ y =>
+    have : m * (y + 1) = m*y + m := by rfl
+    grind
+
+def Nat.Prime (p : Nat) : Prop := 2 ≤ p ∧ ∀ (m : Nat), 2 ≤ m → m ≠ p → ¬ m ∣ p
+
+def Nat.Prime_ge_2 (p : Nat) (hp : Nat.Prime p) : 2 ≤ p := by
+  simp [Nat.Prime] at hp
+  grind
+
+def Nat.relativePrime (p n : Nat) : Prop := 2 ≤ p ∧ ∀ (m : Nat), m < n → 2 ≤ m → m ≠ p → ¬ m ∣ p
+
+theorem Nat.relativePrimeTo2 (p : Nat) (hp : 2 ≤ p) : Nat.relativePrime p 2 := by
+  simp [Nat.relativePrime, hp]
+  grind
+
+theorem Nat.relativePrime_succ (p n : Nat) (hn : 2 ≤ n):
+  Nat.relativePrime p n ∧ (¬ n ∣ p ∨ p = n) ↔ Nat.relativePrime p (n + 1) := by
+  constructor
+  · intro h
+    rcases h with ⟨h₁, h₃⟩
+    rcases h₁ with ⟨h₁, h₂⟩
+    apply And.intro h₁
+    intro m hmn h2m hmp
+    have : m < n ∨ m = n := by grind
+    cases this with
+    | inl h' =>
+      apply h₂ m h' h2m hmp
+    | inr h' =>
+      grind
+  · intro h'
+    rcases h' with ⟨h₁, h₂⟩
+    constructor
+    · apply And.intro h₁
+      intro m hmn h2m hmp
+      apply h₂ m (by omega) h2m hmp
+    · by_cases h' : n = p
+      · simp [h']
+      · left
+        apply h₂ _ (by omega) hn h'
+
+theorem Nat.prime_iff_relative_prime_of_le (p n : Nat) (h : p ≤ n) :
+    Nat.Prime p ↔ Nat.relativePrime p n := by
+  simp only [Prime, relativePrime]
+  constructor
+  · grind
+  · intro h'
+    rcases h' with ⟨h₁, h₂⟩
+    apply And.intro h₁
+    intro m h2m hmp
+    by_cases h' : m < p
+    · grind
+    · apply not_dvd_of_lt_and_pos
+      · grind
+      · grind
+
+def fillSieve (n : Nat) : Std.HashSet Nat := Std.HashSet.ofList (List.range' 2 (n-2))
+
+theorem mem_fillSieve {n m : Nat} : m ∈ fillSieve n ↔ m ≥ 2 ∧ m < n := by
+  simp only [fillSieve, Std.HashSet.mem_ofList, List.contains_eq_mem, List.mem_range'_1,
+    Bool.decide_and, Bool.and_eq_true, decide_eq_true_eq, ge_iff_le, and_congr_right_iff]
+  omega
+
+def eratosthenes_sieve (n : Nat) : List Nat :=
+  if n < 2
+  then []
+  else
+    let sieve := fillSieve n
+    (eratosthenes_sieve.go n sieve 2).toList.mergeSort
+where
+  go (n : Nat) (sieve : Std.HashSet Nat) (curr : Nat) :=
+    if curr < n
+    then
+      if curr ∈ sieve
+      then eratosthenes_sieve.go n (sieve.filter (fun x => (x = curr ∨ x % curr != 0))) (curr + 1)
+      else eratosthenes_sieve.go n sieve (curr + 1)
+    else
+      sieve
+
+theorem mem_eratosthenes_sieve_iff_prime_and_less_than (n m : Nat) :
+    m ∈ eratosthenes_sieve n ↔ m.Prime ∧ m < n := by
+  simp only [eratosthenes_sieve]
+  split
+  · simp
+    intro h
+    have := Nat.Prime_ge_2 m h
+    grind
+  · simp only [List.mem_mergeSort, Std.HashSet.mem_toList]
+    suffices ∀ (n curr : Nat) (hcurr : 2 ≤ curr) (sieve : Std.HashSet Nat), (∀ (k : Nat), (k ∈ sieve ↔ Nat.relativePrime k curr ∧ k < n)) → curr ≤ n →
+    (m ∈ eratosthenes_sieve.go n sieve curr ↔ m.Prime ∧ m < n) by
+      apply this n 2 (by omega) (fillSieve n)
+      · intro k
+        simp only [mem_fillSieve, ge_iff_le, Nat.relativePrime]
+        grind
+      · omega
+    intro n curr hcurr sieve h₁ h₂
+    fun_induction eratosthenes_sieve.go with
+    | case1 sieve curr h₄ h₅ ih =>
+      unfold eratosthenes_sieve.go
+      simp [h₄, h₅]
+      simp at ih
+      apply ih
+      · omega
+      · simp only [Std.HashSet.get_eq, exists_prop]
+        intro k
+        rw [h₁, ← Nat.relativePrime_succ _ _ hcurr, Nat.dvd_iff_mod_eq_zero]
+        grind
+      · grind
+    | case2 sieve curr h₄ h₅ ih =>
+      unfold eratosthenes_sieve.go
+      simp [h₄, h₅]
+      have hcurr' := h₁ curr
+      simp [h₄] at hcurr'
+      simp [hcurr', Nat.relativePrime, hcurr] at h₅
+      rw [ih (by omega)]
+      · intro k
+        rw [h₁]
+        simp
+        intro hk
+        simp [Nat.relativePrime]
+        intro h2k
+        constructor
+        · intro h
+          intro m hmcurr
+          have : m = curr ∨ m < curr := by grind
+          cases this with
+          | inl h' =>
+            rcases h₅ with ⟨x, hx₁, h2x, hx₂, hx₃⟩
+            intro _ _
+            false_or_by_contra
+            rename_i p
+            rw [Nat.dvd_def, h'] at p
+            rcases p with ⟨y, hy⟩
+            specialize h x hx₁ h2x
+            have : ¬ x = k := by
+              false_or_by_contra
+              rename_i q
+              rw [q, Nat.dvd_def] at hx₃
+              sorry
+            sorry
+          | inr h' =>
+            apply h
+            exact h'
+        · grind
+      · grind
+    | case3 sieve curr h =>
+      unfold eratosthenes_sieve.go
+      simp [h, h₁]
+      intro hmn
+      rw [Nat.prime_iff_relative_prime_of_le m curr]
+      grind
+
+theorem testCase1 : eratosthenes_sieve 5 = [2, 3] := by native_decide
+theorem testCase2 : eratosthenes_sieve 6 = [2, 3, 5] := by native_decide
+theorem testCase3 : eratosthenes_sieve 7 = [2, 3, 5] := by native_decide
+theorem testCase4 : eratosthenes_sieve 10 = [2, 3, 5, 7] := by native_decide
+theorem testCase5 : eratosthenes_sieve 0 = [] := by native_decide
+theorem testCase6 : eratosthenes_sieve 22 = [2, 3, 5, 7, 11, 13, 17, 19] := by native_decide
+theorem testCase7 : eratosthenes_sieve 1 = [] := by native_decide
+theorem testCase8 : eratosthenes_sieve 18 = [2, 3, 5, 7, 11, 13, 17] := by native_decide
+theorem testCase9 : eratosthenes_sieve 47 = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43] := by
+    native_decide
+theorem testCase10 : eratosthenes_sieve 101 = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43,
+        47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97] := by
+    native_decide
 
 /-!
 ## Prompt
@@ -52,4 +227,4 @@ def check(candidate):
     assert candidate(101) == [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]
 
 ```
--/
+-/