From d90b44b1aff5543e89985c26e36804ae3755620c Mon Sep 17 00:00:00 2001 From: jt0202 Date: Tue, 29 Jul 2025 17:39:30 +0200 Subject: [PATCH 1/3] Start --- HumanEvalLean/HumanEval96.lean | 101 ++++++++++++++++++++++++++++++++- 1 file changed, 98 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval96.lean b/HumanEvalLean/HumanEval96.lean index ffbed3f..085c4c8 100644 --- a/HumanEvalLean/HumanEval96.lean +++ b/HumanEvalLean/HumanEval96.lean @@ -1,5 +1,100 @@ -def count_up_to : Unit := - () +import Std.Data.HashSet +import HumanEvalLean.ProvedElsewhere + +set_option grind.warning false + +def Nat.Prime (p : Nat) : Prop := 2 ≤ p ∧ ∀ (m : Nat), m < p → 2 ≤ m → ¬ m ∣ p + +def Nat.relativePrime (p n : Nat) : Prop := 2 ≤ p ∧ ∀ (m : Nat), m < p → m < n → 2 ≤ m → ¬ 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 ∧ p % n ≠ 0 ↔ Nat.relativePrime p (n + 1) := by + simp [relativePrime] + constructor + · intro h + rcases h with ⟨h₁, h₃⟩ + rcases h₁ with ⟨h₁, h₂⟩ + apply And.intro h₁ + intro m hmp hmn h2m + have : m < n ∨ m = n := by grind + cases this with + | inl h' => + apply h₂ m hmp h' h2m + | inr h' => + simp [h', Nat.dvd_iff_mod_eq_zero, h₃] + · intro h + rcases h with ⟨h₁, h₂⟩ + constructor + · apply And.intro h₁ + intro m hmp hmn h2m + apply h₂ m hmp (by omega) h2m + · rw [← Nat.dvd_iff_mod_eq_zero] + sorry + +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 + · admit + · simp only [List.mem_mergeSort, Std.HashSet.mem_toList] + suffices ∀ (n curr : Nat) (sieve : Std.HashSet Nat), (∀ (k : Nat), 2 ≤ k → (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 (fillSieve n) + · intro k hk + simp [mem_fillSieve, Nat.relativePrimeTo2, hk] + · omega + intro n curr sieve h₁ h₂ + fun_induction eratosthenes_sieve.go with + | case1 sieve curr h₄ h₅ ih => + unfold eratosthenes_sieve.go + sorry + | case2 sieve curr h₄ h₅ ih => + sorry + | case3 sieve curr h => + unfold eratosthenes_sieve.go + simp [h] + sorry + +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 +147,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 +-/ From 32018d0e000ac1a5b11809b196e1c87dc27af43d Mon Sep 17 00:00:00 2001 From: jt0202 Date: Tue, 29 Jul 2025 18:58:01 +0200 Subject: [PATCH 2/3] Results on relative primes --- HumanEvalLean/HumanEval96.lean | 77 ++++++++++++++++++++++++++-------- 1 file changed, 60 insertions(+), 17 deletions(-) diff --git a/HumanEvalLean/HumanEval96.lean b/HumanEvalLean/HumanEval96.lean index 085c4c8..6d40d57 100644 --- a/HumanEvalLean/HumanEval96.lean +++ b/HumanEvalLean/HumanEval96.lean @@ -3,37 +3,69 @@ import HumanEvalLean.ProvedElsewhere set_option grind.warning false -def Nat.Prime (p : Nat) : Prop := 2 ≤ p ∧ ∀ (m : Nat), m < p → 2 ≤ m → ¬ m ∣ p +theorem Nat.dvd_def (n m : Nat) : n ∣ m ↔ ∃ c, m = n * c := by rfl -def Nat.relativePrime (p n : Nat) : Prop := 2 ≤ p ∧ ∀ (m : Nat), m < p → m < n → 2 ≤ m → ¬ m ∣ p +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 ∧ p % n ≠ 0 ↔ Nat.relativePrime p (n + 1) := by + Nat.relativePrime p n ∧ (¬ n ∣ p ∨ n = p) ↔ Nat.relativePrime p (n + 1) := by simp [relativePrime] constructor · intro h rcases h with ⟨h₁, h₃⟩ rcases h₁ with ⟨h₁, h₂⟩ apply And.intro h₁ - intro m hmp hmn h2m + intro m hmn h2m hmp have : m < n ∨ m = n := by grind cases this with | inl h' => - apply h₂ m hmp h' h2m + apply h₂ m h' h2m hmp | inr h' => - simp [h', Nat.dvd_iff_mod_eq_zero, h₃] + grind · intro h rcases h with ⟨h₁, h₂⟩ constructor · apply And.intro h₁ - intro m hmp hmn h2m - apply h₂ m hmp (by omega) h2m - · rw [← Nat.dvd_iff_mod_eq_zero] - sorry + intro m hmn h2m hmp + apply h₂ m (by omega) h2m hmp + · by_cases h: n = p + · simp [h] + · simp [h] + 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)) @@ -62,25 +94,36 @@ 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 - · admit + · simp + intro h + have := Nat.Prime_ge_2 m h + grind · simp only [List.mem_mergeSort, Std.HashSet.mem_toList] - suffices ∀ (n curr : Nat) (sieve : Std.HashSet Nat), (∀ (k : Nat), 2 ≤ k → (k ∈ sieve ↔ Nat.relativePrime k curr ∧ k < n)) → curr ≤ n → + suffices ∀ (n curr : Nat) (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 (fillSieve n) - · intro k hk - simp [mem_fillSieve, Nat.relativePrimeTo2, hk] + · intro k + simp only [mem_fillSieve, ge_iff_le, Nat.relativePrime] + grind · omega intro n curr sieve h₁ h₂ fun_induction eratosthenes_sieve.go with | case1 sieve curr h₄ h₅ ih => unfold eratosthenes_sieve.go - sorry + simp [h₄, h₅] + simp at ih + apply ih + · simp [Std.HashSet.get_eq] + admit + · grind | case2 sieve curr h₄ h₅ ih => sorry | case3 sieve curr h => unfold eratosthenes_sieve.go - simp [h] - sorry + 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 From 53f840b09a3e4b561f8cdfe415612ff2254cc03e Mon Sep 17 00:00:00 2001 From: jt0202 Date: Tue, 29 Jul 2025 21:40:18 +0200 Subject: [PATCH 3/3] WIP --- HumanEvalLean/HumanEval96.lean | 69 ++++++++++++++++++++++++++-------- 1 file changed, 53 insertions(+), 16 deletions(-) diff --git a/HumanEvalLean/HumanEval96.lean b/HumanEvalLean/HumanEval96.lean index 6d40d57..7c9e71e 100644 --- a/HumanEvalLean/HumanEval96.lean +++ b/HumanEvalLean/HumanEval96.lean @@ -26,9 +26,8 @@ theorem Nat.relativePrimeTo2 (p : Nat) (hp : 2 ≤ p) : Nat.relativePrime p 2 := simp [Nat.relativePrime, hp] grind -theorem Nat.relativePrime_succ (p n : Nat) (hn₁ : 2 ≤ n) : - Nat.relativePrime p n ∧ (¬ n ∣ p ∨ n = p) ↔ Nat.relativePrime p (n + 1) := by - simp [relativePrime] +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₃⟩ @@ -41,16 +40,16 @@ theorem Nat.relativePrime_succ (p n : Nat) (hn₁ : 2 ≤ n) : apply h₂ m h' h2m hmp | inr h' => grind - · intro h - rcases h with ⟨h₁, h₂⟩ + · 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] - · simp [h] - apply h₂ _ (by omega) hn₁ h + · 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 @@ -85,7 +84,7 @@ where if curr < n then if curr ∈ sieve - then eratosthenes_sieve.go n (sieve.filter (fun x => (x ≤ curr ∨ x % curr != 0))) (curr + 1) + 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 @@ -99,25 +98,63 @@ theorem mem_eratosthenes_sieve_iff_prime_and_less_than (n m : Nat) : have := Nat.Prime_ge_2 m h grind · simp only [List.mem_mergeSort, Std.HashSet.mem_toList] - suffices ∀ (n curr : Nat) (sieve : Std.HashSet Nat), (∀ (k : Nat), (k ∈ sieve ↔ Nat.relativePrime k curr ∧ k < n)) → curr ≤ n → + 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 (fillSieve n) + apply this n 2 (by omega) (fillSieve n) · intro k simp only [mem_fillSieve, ge_iff_le, Nat.relativePrime] grind · omega - intro n curr sieve h₁ h₂ + 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 - · simp [Std.HashSet.get_eq] - admit + · 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 => - sorry + 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₁]