diff --git a/HumanEvalLean/HumanEval96.lean b/HumanEvalLean/HumanEval96.lean index ffbed3f..7c9e71e 100644 --- a/HumanEvalLean/HumanEval96.lean +++ b/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] ``` --/ \ No newline at end of file +-/