From 2bd3f7e49451eab14dce4e0df35763bb5b1cd4ec Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 10 Jul 2025 15:35:36 +0200 Subject: [PATCH 01/21] Human eval 75 Formalization of the statement and solution --- HumanEvalLean/HumanEval75.lean | 51 +++++++++++++++++++++++++++++++--- 1 file changed, 47 insertions(+), 4 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 9c17622..9e95012 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,5 +1,48 @@ -def is_multiply_prime : Unit := - () +def isPrimeM (n : Nat) : Id Bool := do + let mut i := 2 + while i * i ≤ n do + if n % i = 0 then + return false + else + i := i + 1 + return 1 < n + +def isPrime (n : Nat) : Bool := isPrimeM n |>.run + +def isMultipleOf2Primes (a : Nat) : Id Bool := do + let mut i := 2 + while i * i ≤ a do + if isPrime i then + return isPrime (a / i) + else + i := i + 1 + return false + +def isMultipleOf3Primes (a : Nat) : Id Bool := do + let mut i := 2 + while i * i * i ≤ a do + if isPrime i then + return isMultipleOf2Primes (a / i) + else + i := i + 1 + return false + +def isMultiplyPrime (a : Nat) : Bool := + -- This solution checks if a number is the multiplication of 3 primes, + -- not necessarily different using O(a^(1/3)) operations. + isMultipleOf3Primes a + +def Nat.IsPrime (n : Nat) : Prop := + n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n + +theorem isPrime_is_correct (n : Nat) : isPrime n ↔ Nat.IsPrime n := by + sorry + +def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := + (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ + +theorem isMultiplyPrime_is_correct : IsMultiplyPrimeIff isMultiplyPrime := by + sorry /-! ## Prompt @@ -9,7 +52,7 @@ def is_multiply_prime : Unit := def is_multiply_prime(a): """Write a function that returns true if the given number is the multiplication of 3 prime numbers and false otherwise. - Knowing that (a) is less then 100. + Knowing that (a) is less then 100. Example: is_multiply_prime(30) == True 30 = 2 * 3 * 5 @@ -52,4 +95,4 @@ def check(candidate): assert candidate(11 * 13 * 7) == True ``` --/ \ No newline at end of file +-/ From 69f7cfc079882e92aa9e2de64d34c4cd5746ce8e Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 10 Jul 2025 15:39:04 +0200 Subject: [PATCH 02/21] add examples and fix solution --- HumanEvalLean/HumanEval75.lean | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 9e95012..bf78f8e 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,7 +1,7 @@ def isPrimeM (n : Nat) : Id Bool := do let mut i := 2 while i * i ≤ n do - if n % i = 0 then + if i ∣ n then return false else i := i + 1 @@ -12,7 +12,7 @@ def isPrime (n : Nat) : Bool := isPrimeM n |>.run def isMultipleOf2Primes (a : Nat) : Id Bool := do let mut i := 2 while i * i ≤ a do - if isPrime i then + if i ∣ a ∧ isPrime i then return isPrime (a / i) else i := i + 1 @@ -21,7 +21,7 @@ def isMultipleOf2Primes (a : Nat) : Id Bool := do def isMultipleOf3Primes (a : Nat) : Id Bool := do let mut i := 2 while i * i * i ≤ a do - if isPrime i then + if i ∣ a ∧ isPrime i then return isMultipleOf2Primes (a / i) else i := i + 1 @@ -32,6 +32,15 @@ def isMultiplyPrime (a : Nat) : Bool := -- not necessarily different using O(a^(1/3)) operations. isMultipleOf3Primes a +example : isMultiplyPrime 5 = false := by native_decide +example : isMultiplyPrime 30 = true := by native_decide +example : isMultiplyPrime 8 = true := by native_decide +example : isMultiplyPrime 10 = false := by native_decide +example : isMultiplyPrime 125 = true := by native_decide +example : isMultiplyPrime (3 * 5 * 7) = true := by native_decide +example : isMultiplyPrime (3 * 6 * 7) = false := by native_decide +example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide + def Nat.IsPrime (n : Nat) : Prop := n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n From bc9cb34387646cccf9a704a61d429c9bd7420435 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 10 Jul 2025 18:50:46 +0200 Subject: [PATCH 03/21] Use Id.run instead of returning Id monad --- HumanEvalLean/HumanEval75.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index bf78f8e..e143486 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,4 +1,4 @@ -def isPrimeM (n : Nat) : Id Bool := do +def isPrime (n : Nat) : Bool := Id.run do let mut i := 2 while i * i ≤ n do if i ∣ n then @@ -7,9 +7,7 @@ def isPrimeM (n : Nat) : Id Bool := do i := i + 1 return 1 < n -def isPrime (n : Nat) : Bool := isPrimeM n |>.run - -def isMultipleOf2Primes (a : Nat) : Id Bool := do +def isMultipleOf2Primes (a : Nat) : Bool := Id.run do let mut i := 2 while i * i ≤ a do if i ∣ a ∧ isPrime i then @@ -18,7 +16,7 @@ def isMultipleOf2Primes (a : Nat) : Id Bool := do i := i + 1 return false -def isMultipleOf3Primes (a : Nat) : Id Bool := do +def isMultipleOf3Primes (a : Nat) : Bool := Id.run do let mut i := 2 while i * i * i ≤ a do if i ∣ a ∧ isPrime i then From ff1a7f2e25935a6995b83c5e381d5b3fee813c68 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 11 Jul 2025 07:32:31 +0200 Subject: [PATCH 04/21] don't need to check if the number is prime --- HumanEvalLean/HumanEval75.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index e143486..cff8f63 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -10,7 +10,7 @@ def isPrime (n : Nat) : Bool := Id.run do def isMultipleOf2Primes (a : Nat) : Bool := Id.run do let mut i := 2 while i * i ≤ a do - if i ∣ a ∧ isPrime i then + if i ∣ a then return isPrime (a / i) else i := i + 1 @@ -19,15 +19,13 @@ def isMultipleOf2Primes (a : Nat) : Bool := Id.run do def isMultipleOf3Primes (a : Nat) : Bool := Id.run do let mut i := 2 while i * i * i ≤ a do - if i ∣ a ∧ isPrime i then + if i ∣ a then return isMultipleOf2Primes (a / i) else i := i + 1 return false def isMultiplyPrime (a : Nat) : Bool := - -- This solution checks if a number is the multiplication of 3 primes, - -- not necessarily different using O(a^(1/3)) operations. isMultipleOf3Primes a example : isMultiplyPrime 5 = false := by native_decide From 0b7831b7d1b7c7fa455810802508469c11a3e530 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 11 Jul 2025 07:34:11 +0200 Subject: [PATCH 05/21] uses lean 4.22 --- HumanEvalLean/HumanEval75.lean | 5 +++-- lean-toolchain | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index cff8f63..9c8ea0c 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,3 +1,5 @@ +import Std.Tactic.Do + def isPrime (n : Nat) : Bool := Id.run do let mut i := 2 while i * i ≤ n do @@ -40,8 +42,7 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide def Nat.IsPrime (n : Nat) : Prop := n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n -theorem isPrime_is_correct (n : Nat) : isPrime n ↔ Nat.IsPrime n := by - sorry +theorem isPrime_is_correct (n : Nat) : isPrime n ↔ Nat.IsPrime n := by sorry def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ diff --git a/lean-toolchain b/lean-toolchain index 980709b..67eefcc 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0 +leanprover/lean4:v4.22.0-rc1 From 9c9ec291c3a26329296aac6249011ef9af3d673f Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Sun, 20 Jul 2025 16:37:12 +0200 Subject: [PATCH 06/21] Simplify algorithm: - Find smallest prime 3 times and check that it was enough --- HumanEvalLean/HumanEval75.lean | 51 +++++++++++++++------------------- 1 file changed, 22 insertions(+), 29 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 9c8ea0c..1969d0a 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,34 +1,26 @@ import Std.Tactic.Do -def isPrime (n : Nat) : Bool := Id.run do - let mut i := 2 - while i * i ≤ n do +def smallestPrimeFactor (n : Nat) : Nat := Id.run do + for i in [2:n] do + if i * i > n then + break if i ∣ n then + return i + n + +def isMultiplyPrime (a : Nat) : Bool := Id.run do + let mut primes := (∅ : Array Nat) + let mut a := a + for _ in [0:3] do + + if a ≤ 1 then return false - else - i := i + 1 - return 1 < n - -def isMultipleOf2Primes (a : Nat) : Bool := Id.run do - let mut i := 2 - while i * i ≤ a do - if i ∣ a then - return isPrime (a / i) - else - i := i + 1 - return false - -def isMultipleOf3Primes (a : Nat) : Bool := Id.run do - let mut i := 2 - while i * i * i ≤ a do - if i ∣ a then - return isMultipleOf2Primes (a / i) - else - i := i + 1 - return false - -def isMultiplyPrime (a : Nat) : Bool := - isMultipleOf3Primes a + + let p := smallestPrimeFactor a + a := a / p + primes := primes.push p + + primes.size == 3 && a == 1 example : isMultiplyPrime 5 = false := by native_decide example : isMultiplyPrime 30 = true := by native_decide @@ -38,12 +30,13 @@ example : isMultiplyPrime 125 = true := by native_decide example : isMultiplyPrime (3 * 5 * 7) = true := by native_decide example : isMultiplyPrime (3 * 6 * 7) = false := by native_decide example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide +example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide +example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide + def Nat.IsPrime (n : Nat) : Prop := n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n -theorem isPrime_is_correct (n : Nat) : isPrime n ↔ Nat.IsPrime n := by sorry - def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ From 773368f45f3479211a2f82e47f04afcc3a1d3f3b Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Sun, 20 Jul 2025 16:46:13 +0200 Subject: [PATCH 07/21] no need for array, since we don't care about the primes --- HumanEvalLean/HumanEval75.lean | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 1969d0a..f27c239 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -8,19 +8,21 @@ def smallestPrimeFactor (n : Nat) : Nat := Id.run do return i n -def isMultiplyPrime (a : Nat) : Bool := Id.run do - let mut primes := (∅ : Array Nat) +def isMultipleOfKPrimes (a : Nat) (k : Nat) : Bool := Id.run do + let mut total := 0 let mut a := a - for _ in [0:3] do + for _ in [0:k] do if a ≤ 1 then return false let p := smallestPrimeFactor a a := a / p - primes := primes.push p + total := total + 1 - primes.size == 3 && a == 1 + total == k && a == 1 + +def isMultiplyPrime (a : Nat) : Bool := isMultipleOfKPrimes a 3 example : isMultiplyPrime 5 = false := by native_decide example : isMultiplyPrime 30 = true := by native_decide @@ -41,7 +43,10 @@ def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ theorem isMultiplyPrime_is_correct : IsMultiplyPrimeIff isMultiplyPrime := by - sorry + intro a + constructor + · sorry + · sorry /-! ## Prompt From c2b8057f50114e0f745d1cea81a2b6ab0c980982 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Mon, 21 Jul 2025 11:02:01 +0200 Subject: [PATCH 08/21] start working on the proof --- HumanEvalLean/HumanEval75.lean | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index f27c239..cffe2d2 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -35,18 +35,39 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide - def Nat.IsPrime (n : Nat) : Prop := n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Defs.html#List.prod +def List.prod {α} [Mul α] [One α] : List α → α := + List.foldr (· * ·) 1 + +structure PrimeDecomposition (n : Nat) where + -- Multiset is only available in mathlib, using List instead + ps : List Nat + all_prime : ∀ p ∈ ps, p.IsPrime + is_decomposition : ps.prod = n + +def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length + +theorem isMultipleOfKPrimes_primeDecompositionLength (n k : Nat) : + isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by + + + sorry + +theorem primeDecomposition_length_3 (n : Nat) : + (∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃) + ↔ ∃ (d : PrimeDecomposition n), d.length = 3 := by + sorry + theorem isMultiplyPrime_is_correct : IsMultiplyPrimeIff isMultiplyPrime := by intro a - constructor - · sorry - · sorry + rw [primeDecomposition_length_3 a] + simp [isMultiplyPrime, isMultipleOfKPrimes_primeDecompositionLength] /-! ## Prompt From f3a22ccd9cf70cef87b78ef4de3a5586c6b6c127 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Wed, 23 Jul 2025 10:02:31 +0200 Subject: [PATCH 09/21] Finish high level proof for isMultiplyPrime - Missing several lemmas - Missing proof for smallestPrimeFactor --- HumanEvalLean/HumanEval75.lean | 179 ++++++++++++++++++++++++++++----- 1 file changed, 156 insertions(+), 23 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index cffe2d2..e8019de 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,29 +1,55 @@ import Std.Tactic.Do +import Init.Data.Nat.Dvd -def smallestPrimeFactor (n : Nat) : Nat := Id.run do - for i in [2:n] do - if i * i > n then - break - if i ∣ n then - return i - n +open Std Do -def isMultipleOfKPrimes (a : Nat) (k : Nat) : Bool := Id.run do - let mut total := 0 - let mut a := a - for _ in [0:k] do +def smallestPrimeFactor (n : Nat) : Nat := + go 2 +where + go (i : Nat) : Nat := + if h : n < i * i then + n + else if h2 : i ∣ n then + i + else + go (i + 1) + termination_by n - i + decreasing_by + have : i < n := by + match i with + | 0 => omega + | 1 => omega + | i + 2 => exact Nat.lt_of_lt_of_le (Nat.lt_mul_self_iff.2 (by omega)) (Nat.not_lt.1 h) + omega - if a ≤ 1 then - return false +def Nat.IsPrime (n : Nat) : Prop := + n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n + +theorem smallestPrimeFactor_div_n (n : Nat) (hn : 1 < n) : smallestPrimeFactor n ∣ n := by sorry - let p := smallestPrimeFactor a - a := a / p - total := total + 1 +theorem smallestPrimeFactor_isPrime {n : Nat} (hn : 1 < n) : Nat.IsPrime $ smallestPrimeFactor n := by sorry - total == k && a == 1 +def isMultipleOfKPrimes (n : Nat) (k : Nat) : Bool := + if hn₀ : n = 0 then + false + else if hk : k = 0 then + n = 1 + else if hn₁ : n = 1 then + false + else + let p := smallestPrimeFactor n + isMultipleOfKPrimes (n / p) (k - 1) + termination_by k + decreasing_by + omega -def isMultiplyPrime (a : Nat) : Bool := isMultipleOfKPrimes a 3 +theorem isMultipleOfKPrimes_zero (k : Nat) : isMultipleOfKPrimes 0 k = false := by + simp [isMultipleOfKPrimes] +def isMultiplyPrime (n : Nat) : Bool := isMultipleOfKPrimes n 3 + +example : isMultiplyPrime 0 = false := by native_decide +example : isMultiplyPrime 1 = false := by native_decide example : isMultiplyPrime 5 = false := by native_decide example : isMultiplyPrime 30 = true := by native_decide example : isMultiplyPrime 8 = true := by native_decide @@ -35,8 +61,7 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide -def Nat.IsPrime (n : Nat) : Prop := - n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n +theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by sorry def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ @@ -45,6 +70,11 @@ def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := def List.prod {α} [Mul α] [One α] : List α → α := List.foldr (· * ·) 1 +theorem List.prod_ne_zero {α} [Mul α] [One α] [Zero α] (l : List α) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by sorry + +theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 := + rfl + structure PrimeDecomposition (n : Nat) where -- Multiset is only available in mathlib, using List instead ps : List Nat @@ -53,16 +83,119 @@ structure PrimeDecomposition (n : Nat) where def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length -theorem isMultipleOfKPrimes_primeDecompositionLength (n k : Nat) : - isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by +def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : PrimeDecomposition (n * p) := + ⟨p :: d.ps, by sorry, by sorry⟩ + +def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : PrimeDecomposition (n / p) := + ⟨d.ps.erase p, by sorry, by sorry⟩ + +theorem PrimeDecomposition.push_length_eq_length_plus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : (d.push p hp).length = d.length + 1 := by sorry + +theorem PrimeDecomposition.push_simp {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by sorry +theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by sorry +def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod_nil])⟩ + +theorem PrimeDecomposition.zero_does_not_exist (d : PrimeDecomposition 0) : False := by + apply List.prod_ne_zero d.ps + · intro x h + exact Nat.isPrime_ne_zero (d.all_prime x h) + exact d.is_decomposition + +theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDecomposition.one := by + simp [PrimeDecomposition.one] sorry +theorem PrimeDecomposition.length_eq_zero_iff (n : Nat) (d : PrimeDecomposition n) : d.length = 0 ↔ n = 1 := by sorry + +theorem PrimeDecomposition.one_length_eq_zero (d : PrimeDecomposition 1) : d.length = 0 := by sorry + +theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : + isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by + if hn₀ : n = 0 then + rw [hn₀] + simp [isMultipleOfKPrimes] + intro x h + exact PrimeDecomposition.zero_does_not_exist x + else + unfold isMultipleOfKPrimes + simp [hn₀] + if hk : k = 0 then + simp [hk] + sorry + else + simp [hk] + constructor + · intro ⟨hn₁, hrec⟩ + let ⟨d, hd⟩ := isMultipleOfKPrimes_primeDecompositionLength.mp hrec + have hn_ge_1 : 1 < n := by sorry + let d₁ := d.push (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) + rw [← Nat.div_mul_cancel (smallestPrimeFactor_div_n n hn_ge_1)] + suffices d₁.length = k by + exact ⟨d₁, by simp [this]⟩ + let x := PrimeDecomposition.push_length_eq_length_plus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) + rw [x, hd] + have hk₀ : 1 ≤ k := by match k with + | 0 => contradiction + | k + 1 => simp + rw [← Nat.sub_add_comm hk₀, Nat.add_sub_cancel] + · intro ⟨d, hd⟩ + have hn_ge_1 : 1 < n := by sorry + constructor + · sorry + · let d2 := d.erase (smallestPrimeFactor n) (by sorry) (by sorry) + suffices d2.length = k - 1 by + exact isMultipleOfKPrimes_primeDecompositionLength.mpr ⟨d2, by simp [this]⟩ + let x := PrimeDecomposition.erase_length_eq_length_minus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1) + rw [x, hd] + +theorem List.prod_3_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by sorry + theorem primeDecomposition_length_3 (n : Nat) : (∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃) ↔ ∃ (d : PrimeDecomposition n), d.length = 3 := by - sorry + constructor + · intro ⟨a, b, c, ⟨h, ha, hb, hc⟩⟩ + let d := PrimeDecomposition.one.push a ha |>.push b hb |>.push c hc + + suffices ∃ d : PrimeDecomposition (1 * a * b * c), d.length = 3 by + have h1 : 1 * a * b * c = n := by simp [h] + rw [h1] at this + exact this + + suffices d.length = 3 by + exact ⟨d, this⟩ + + repeat rw [PrimeDecomposition.push_simp] + rw [PrimeDecomposition.one_length_eq_zero] + · intro ⟨⟨ps, hp, ha⟩, hd⟩ + simp [PrimeDecomposition.length] at hd + match ps with + | [] => contradiction + | a₁ :: rest => match rest with + | [] => simp at hd + | a₂ :: rest => match rest with + | [] => simp at hd + | a₃ :: rest => + simp at hd + rw [hd] at ha + suffices a₁ * a₂ * a₃ = n ∧ a₁.IsPrime ∧ a₂.IsPrime ∧ a₃.IsPrime by + exact ⟨a₁, a₂, a₃, this⟩ + rw [List.prod_3_mul] at ha + constructor + · exact ha + constructor + · let t := hp a₁ + simp at t + trivial + constructor + · let t := hp a₂ + simp at t + trivial + · let t := hp a₃ + simp at t + trivial theorem isMultiplyPrime_is_correct : IsMultiplyPrimeIff isMultiplyPrime := by intro a From 2d6dc1fc04507a57ffd69a5a832c84676e1f3930 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Wed, 23 Jul 2025 11:28:50 +0200 Subject: [PATCH 10/21] close few more sorries --- HumanEvalLean/HumanEval75.lean | 95 +++++++++++++++++++++++++++------- 1 file changed, 75 insertions(+), 20 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index e8019de..07e7d54 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -61,7 +61,13 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide -theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by sorry +theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by + intro h + have h2 : 2 ∣ p := by simp [h] + apply Or.elim (hp.right 2 h2) + trivial + rw [h] + trivial def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ @@ -70,7 +76,17 @@ def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := def List.prod {α} [Mul α] [One α] : List α → α := List.foldr (· * ·) 1 -theorem List.prod_ne_zero {α} [Mul α] [One α] [Zero α] (l : List α) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by sorry +theorem List.prod_head_eq_mul {α} [Mul α] [One α] (a : α) (l : List α) : (a :: l).prod = a * l.prod := by + simp [List.prod] + +theorem List.prod_ne_zero {α} [Mul α] [One α] [Zero α] (l : List α) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by + induction l with + | nil => + simp [List.prod] + intro h + sorry + | cons x xs ih => + sorry theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 := rfl @@ -84,16 +100,26 @@ structure PrimeDecomposition (n : Nat) where def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : PrimeDecomposition (n * p) := - ⟨p :: d.ps, by sorry, by sorry⟩ + ⟨p :: d.ps, + by + intro p1 h + simp at h + apply Or.elim h + · intro t; rw[t]; exact hp + · exact (d.all_prime p1 ·), + by + simp [List.prod_head_eq_mul] + rw [d.is_decomposition, Nat.mul_comm] + ⟩ def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : PrimeDecomposition (n / p) := ⟨d.ps.erase p, by sorry, by sorry⟩ -theorem PrimeDecomposition.push_length_eq_length_plus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : (d.push p hp).length = d.length + 1 := by sorry - -theorem PrimeDecomposition.push_simp {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by sorry +theorem PrimeDecomposition.push_length_eq_length_plus_one {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by + simp [PrimeDecomposition.push, PrimeDecomposition.length] -theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by sorry +theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by + sorry def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod_nil])⟩ @@ -105,11 +131,14 @@ theorem PrimeDecomposition.zero_does_not_exist (d : PrimeDecomposition 0) : Fals theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDecomposition.one := by simp [PrimeDecomposition.one] - sorry - -theorem PrimeDecomposition.length_eq_zero_iff (n : Nat) (d : PrimeDecomposition n) : d.length = 0 ↔ n = 1 := by sorry + if h : d.ps = [] then + sorry + else + sorry -theorem PrimeDecomposition.one_length_eq_zero (d : PrimeDecomposition 1) : d.length = 0 := by sorry +theorem PrimeDecomposition.one_length_eq_zero (d : PrimeDecomposition 1) : d.length = 0 := by + rw [PrimeDecomposition.one_unique d] + simp [PrimeDecomposition.length, PrimeDecomposition.one] theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by @@ -123,34 +152,60 @@ theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : simp [hn₀] if hk : k = 0 then simp [hk] - sorry + constructor + · intro h1 + rw [h1] + exact ⟨PrimeDecomposition.one, by simp [PrimeDecomposition.one_length_eq_zero]⟩ + · intro ⟨d, hd⟩ + simp [PrimeDecomposition.length] at hd + symm + let x := d.is_decomposition + simp [hd, List.prod] at x + trivial else simp [hk] constructor · intro ⟨hn₁, hrec⟩ let ⟨d, hd⟩ := isMultipleOfKPrimes_primeDecompositionLength.mp hrec - have hn_ge_1 : 1 < n := by sorry + have hn_ge_1 : 1 < n := by match n with + | 0 => trivial + | 1 => trivial + | n + 2 => simp let d₁ := d.push (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) rw [← Nat.div_mul_cancel (smallestPrimeFactor_div_n n hn_ge_1)] suffices d₁.length = k by exact ⟨d₁, by simp [this]⟩ - let x := PrimeDecomposition.push_length_eq_length_plus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) - rw [x, hd] + rw [PrimeDecomposition.push_length_eq_length_plus_one, hd] have hk₀ : 1 ≤ k := by match k with | 0 => contradiction | k + 1 => simp rw [← Nat.sub_add_comm hk₀, Nat.add_sub_cancel] · intro ⟨d, hd⟩ - have hn_ge_1 : 1 < n := by sorry + have hn_ge_1 : 1 < n := by match n with + | 0 => trivial + | 1 => + exfalso + rw [PrimeDecomposition.one_length_eq_zero d] at hd + symm at hd + contradiction + | n + 2 => simp constructor - · sorry - · let d2 := d.erase (smallestPrimeFactor n) (by sorry) (by sorry) + · intro h1 + revert hd d + rw [h1] + intro d hd + rw [PrimeDecomposition.one_length_eq_zero d] at hd + symm at hd + contradiction + · let d2 := d.erase (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1) suffices d2.length = k - 1 by exact isMultipleOfKPrimes_primeDecompositionLength.mpr ⟨d2, by simp [this]⟩ let x := PrimeDecomposition.erase_length_eq_length_minus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1) rw [x, hd] -theorem List.prod_3_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by sorry +theorem List.prod_3_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by + simp [List.prod] + rw [Nat.mul_assoc] theorem primeDecomposition_length_3 (n : Nat) : (∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃) @@ -167,7 +222,7 @@ theorem primeDecomposition_length_3 (n : Nat) : suffices d.length = 3 by exact ⟨d, this⟩ - repeat rw [PrimeDecomposition.push_simp] + repeat rw [PrimeDecomposition.push_length_eq_length_plus_one] rw [PrimeDecomposition.one_length_eq_zero] · intro ⟨⟨ps, hp, ha⟩, hd⟩ simp [PrimeDecomposition.length] at hd From bd1684224e4b98d55a19b82ce063569ab4aca329 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 24 Jul 2025 11:13:07 +0200 Subject: [PATCH 11/21] de-sorrying --- HumanEvalLean/HumanEval75.lean | 91 +++++++++++++++++++++++++++++++--- 1 file changed, 83 insertions(+), 8 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 07e7d54..ee8a51a 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -69,6 +69,12 @@ theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by rw [h] trivial +theorem Nat.IsPrime.zero_lt (hp : Nat.IsPrime p) : 0 < p := by match p with + | p + 1 => simp + | 0 => simp [Nat.IsPrime] at hp + +theorem Nat.IsPrime.two_le (hp : Nat.IsPrime p) : 2 ≤ p := by sorry + def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ @@ -79,14 +85,15 @@ def List.prod {α} [Mul α] [One α] : List α → α := theorem List.prod_head_eq_mul {α} [Mul α] [One α] (a : α) (l : List α) : (a :: l).prod = a * l.prod := by simp [List.prod] -theorem List.prod_ne_zero {α} [Mul α] [One α] [Zero α] (l : List α) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by +theorem List.prod_ne_zero (l : List Nat) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by induction l with - | nil => - simp [List.prod] - intro h - sorry + | nil => simp [List.prod] | cons x xs ih => - sorry + have : (x :: xs).prod = x * xs.prod := by simp [List.prod] + rw [this] + apply Nat.mul_ne_zero + · apply h x; simp + · apply ih; intro x1 hx; apply h; simp [hx] theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 := rfl @@ -112,14 +119,82 @@ def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime rw [d.is_decomposition, Nat.mul_comm] ⟩ +theorem List.prod_cons (a : α) (l : List α) [Mul α] [One α] : (a :: l).prod = a * l.prod := by + simp [List.prod] + + +theorem List.dvd_prod {l : List Nat} {n : Nat} (h : n ∈ l) : n ∣ l.prod := by + induction l with + | nil => contradiction + | cons head tail ih => + rw [List.prod_cons] + if hd : head = n then + simp [hd, Nat.dvd_mul_right] + else + have ht : n ∈ tail := by + simp at h + apply Or.elim h + intro x; symm at x; contradiction + simp + exact Nat.dvd_mul_left_of_dvd (ih ht) head + +theorem List.prod_erase (l : List Nat) (p : Nat) (h : p ∈ l) (h1 : 0 < p) : (l.erase p).prod = l.prod / p := by + induction l with + | nil => contradiction + | cons head tail ih => + if hp : head = p then + simp [hp, List.prod, Nat.mul_comm p, Nat.mul_div_cancel _ h1] + else + simp [List.prod_cons, hp] + have ht : p ∈ tail := by + simp at h + apply Or.elim h + intro x; symm at x; contradiction + simp + rw [ih ht, ← Nat.mul_div_assoc] + exact List.dvd_prod ht + +def PrimeDecomposition.erase_cons (d : PrimeDecomposition n) : PrimeDecomposition (n / d.ps.headD 1) := by + match d.ps with + | [] => sorry + | head :: tail => sorry + +theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.IsPrime) (hd : p ∣ n) : p ∈ d.ps := by + let ⟨ps, ha, hb⟩ := d + induction ps generalizing n with + | nil => + simp [List.prod] at hb + symm at hb + rw [hb] at hd + let c := Nat.le_trans (hp.two_le) (Nat.le_of_dvd (by simp) hd) + contradiction + | cons head tail ih => + simp + simp at ih + if hp : p = head then + simp [hp] + else + simp [hp] + have hh : d.ps.headD 1 = head := by sorry + let ih := ih d.erase_cons + rw [hh] at ih + have hd : p ∣ n / head := by sorry + have hpp : ∀ p ∈ tail, p.IsPrime := by sorry + apply ih hd hpp + simp [List.prod_cons] at hb + sorry + def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : PrimeDecomposition (n / p) := - ⟨d.ps.erase p, by sorry, by sorry⟩ + ⟨d.ps.erase p, + fun p1 h1 => d.all_prime p1 (List.mem_of_mem_erase h1), + by rw [List.prod_erase d.ps p (PrimeDecomposition.prime_mem d hp hd) hp.zero_lt]; simp [d.is_decomposition]⟩ theorem PrimeDecomposition.push_length_eq_length_plus_one {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by simp [PrimeDecomposition.push, PrimeDecomposition.length] theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by - sorry + simp [PrimeDecomposition.length, PrimeDecomposition.erase] + rw [List.length_erase_of_mem (PrimeDecomposition.prime_mem d hp hd)] def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod_nil])⟩ From 02480b61c6b1fa938d1bd1ac4598b786e7ff32b0 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 24 Jul 2025 11:36:33 +0200 Subject: [PATCH 12/21] refactor --- HumanEvalLean/HumanEval75.lean | 136 +++++++++++++++++---------------- 1 file changed, 70 insertions(+), 66 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index ee8a51a..1cb849d 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -22,13 +22,6 @@ where | i + 2 => exact Nat.lt_of_lt_of_le (Nat.lt_mul_self_iff.2 (by omega)) (Nat.not_lt.1 h) omega -def Nat.IsPrime (n : Nat) : Prop := - n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n - -theorem smallestPrimeFactor_div_n (n : Nat) (hn : 1 < n) : smallestPrimeFactor n ∣ n := by sorry - -theorem smallestPrimeFactor_isPrime {n : Nat} (hn : 1 < n) : Nat.IsPrime $ smallestPrimeFactor n := by sorry - def isMultipleOfKPrimes (n : Nat) (k : Nat) : Bool := if hn₀ : n = 0 then false @@ -43,9 +36,6 @@ def isMultipleOfKPrimes (n : Nat) (k : Nat) : Bool := decreasing_by omega -theorem isMultipleOfKPrimes_zero (k : Nat) : isMultipleOfKPrimes 0 k = false := by - simp [isMultipleOfKPrimes] - def isMultiplyPrime (n : Nat) : Bool := isMultipleOfKPrimes n 3 example : isMultiplyPrime 0 = false := by native_decide @@ -61,7 +51,12 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide -theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by +-- Section: Is prime + +def Nat.IsPrime (n : Nat) : Prop := + n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n + +theorem Nat.IsPrime.ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by intro h have h2 : 2 ∣ p := by simp [h] apply Or.elim (hp.right 2 h2) @@ -75,16 +70,21 @@ theorem Nat.IsPrime.zero_lt (hp : Nat.IsPrime p) : 0 < p := by match p with theorem Nat.IsPrime.two_le (hp : Nat.IsPrime p) : 2 ≤ p := by sorry -def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := - (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ +-- Section: Smallest prime factor + +theorem Nat.smallestPrimeFactor_dvd (n : Nat) (hn : 1 < n) : smallestPrimeFactor n ∣ n := by sorry + +theorem Nat.smallestPrimeFactor_prime {n : Nat} (hn : 1 < n) : Nat.IsPrime (smallestPrimeFactor n) := by sorry + +theorem isMultipleOfKPrimes_zero (k : Nat) : isMultipleOfKPrimes 0 k = false := by + simp [isMultipleOfKPrimes] + +-- Section: List -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Defs.html#List.prod def List.prod {α} [Mul α] [One α] : List α → α := List.foldr (· * ·) 1 -theorem List.prod_head_eq_mul {α} [Mul α] [One α] (a : α) (l : List α) : (a :: l).prod = a * l.prod := by - simp [List.prod] - theorem List.prod_ne_zero (l : List Nat) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by induction l with | nil => simp [List.prod] @@ -98,31 +98,9 @@ theorem List.prod_ne_zero (l : List Nat) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 := rfl -structure PrimeDecomposition (n : Nat) where - -- Multiset is only available in mathlib, using List instead - ps : List Nat - all_prime : ∀ p ∈ ps, p.IsPrime - is_decomposition : ps.prod = n - -def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length - -def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : PrimeDecomposition (n * p) := - ⟨p :: d.ps, - by - intro p1 h - simp at h - apply Or.elim h - · intro t; rw[t]; exact hp - · exact (d.all_prime p1 ·), - by - simp [List.prod_head_eq_mul] - rw [d.is_decomposition, Nat.mul_comm] - ⟩ - theorem List.prod_cons (a : α) (l : List α) [Mul α] [One α] : (a :: l).prod = a * l.prod := by simp [List.prod] - theorem List.dvd_prod {l : List Nat} {n : Nat} (h : n ∈ l) : n ∣ l.prod := by induction l with | nil => contradiction @@ -154,7 +132,34 @@ theorem List.prod_erase (l : List Nat) (p : Nat) (h : p ∈ l) (h1 : 0 < p) : (l rw [ih ht, ← Nat.mul_div_assoc] exact List.dvd_prod ht -def PrimeDecomposition.erase_cons (d : PrimeDecomposition n) : PrimeDecomposition (n / d.ps.headD 1) := by +theorem List.prod_three_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by + simp [List.prod] + rw [Nat.mul_assoc] + +-- Section: Prime decomposition + +structure PrimeDecomposition (n : Nat) where + -- Multiset is only available in mathlib, using List instead + ps : List Nat + all_prime : ∀ p ∈ ps, p.IsPrime + is_decomposition : ps.prod = n + +def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length + +def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : PrimeDecomposition (n * p) := + ⟨p :: d.ps, + by + intro p1 h + simp at h + apply Or.elim h + · intro t; rw[t]; exact hp + · exact (d.all_prime p1 ·), + by + simp [List.prod_cons] + rw [d.is_decomposition, Nat.mul_comm] + ⟩ + +def PrimeDecomposition.erase_head (d : PrimeDecomposition n) : PrimeDecomposition (n / d.ps.headD 1) := by match d.ps with | [] => sorry | head :: tail => sorry @@ -176,7 +181,7 @@ theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.IsPrime) else simp [hp] have hh : d.ps.headD 1 = head := by sorry - let ih := ih d.erase_cons + let ih := ih d.PrimeDecomposition.erase_head rw [hh] at ih have hd : p ∣ n / head := by sorry have hpp : ∀ p ∈ tail, p.IsPrime := by sorry @@ -189,10 +194,10 @@ def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrim fun p1 h1 => d.all_prime p1 (List.mem_of_mem_erase h1), by rw [List.prod_erase d.ps p (PrimeDecomposition.prime_mem d hp hd) hp.zero_lt]; simp [d.is_decomposition]⟩ -theorem PrimeDecomposition.push_length_eq_length_plus_one {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by +theorem PrimeDecomposition.push_length {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by simp [PrimeDecomposition.push, PrimeDecomposition.length] -theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by +theorem PrimeDecomposition.erase_length (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by simp [PrimeDecomposition.length, PrimeDecomposition.erase] rw [List.length_erase_of_mem (PrimeDecomposition.prime_mem d hp hd)] @@ -201,7 +206,7 @@ def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [L theorem PrimeDecomposition.zero_does_not_exist (d : PrimeDecomposition 0) : False := by apply List.prod_ne_zero d.ps · intro x h - exact Nat.isPrime_ne_zero (d.all_prime x h) + exact Nat.IsPrime.ne_zero (d.all_prime x h) exact d.is_decomposition theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDecomposition.one := by @@ -211,11 +216,11 @@ theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDeco else sorry -theorem PrimeDecomposition.one_length_eq_zero (d : PrimeDecomposition 1) : d.length = 0 := by +theorem PrimeDecomposition.one_length (d : PrimeDecomposition 1) : d.length = 0 := by rw [PrimeDecomposition.one_unique d] simp [PrimeDecomposition.length, PrimeDecomposition.one] -theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : +theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by if hn₀ : n = 0 then rw [hn₀] @@ -230,7 +235,7 @@ theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : constructor · intro h1 rw [h1] - exact ⟨PrimeDecomposition.one, by simp [PrimeDecomposition.one_length_eq_zero]⟩ + exact ⟨PrimeDecomposition.one, by simp [PrimeDecomposition.one_length]⟩ · intro ⟨d, hd⟩ simp [PrimeDecomposition.length] at hd symm @@ -241,16 +246,16 @@ theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : simp [hk] constructor · intro ⟨hn₁, hrec⟩ - let ⟨d, hd⟩ := isMultipleOfKPrimes_primeDecompositionLength.mp hrec + let ⟨d, hd⟩ := isMultipleOfKPrimes_iff_primeDecomposition_length.mp hrec have hn_ge_1 : 1 < n := by match n with | 0 => trivial | 1 => trivial | n + 2 => simp - let d₁ := d.push (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) - rw [← Nat.div_mul_cancel (smallestPrimeFactor_div_n n hn_ge_1)] + let d₁ := d.push (smallestPrimeFactor n) (Nat.smallestPrimeFactor_prime hn_ge_1) + rw [← Nat.div_mul_cancel (Nat.smallestPrimeFactor_dvd n hn_ge_1)] suffices d₁.length = k by exact ⟨d₁, by simp [this]⟩ - rw [PrimeDecomposition.push_length_eq_length_plus_one, hd] + rw [PrimeDecomposition.push_length, hd] have hk₀ : 1 ≤ k := by match k with | 0 => contradiction | k + 1 => simp @@ -260,7 +265,7 @@ theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : | 0 => trivial | 1 => exfalso - rw [PrimeDecomposition.one_length_eq_zero d] at hd + rw [PrimeDecomposition.one_length d] at hd symm at hd contradiction | n + 2 => simp @@ -269,20 +274,16 @@ theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} : revert hd d rw [h1] intro d hd - rw [PrimeDecomposition.one_length_eq_zero d] at hd + rw [PrimeDecomposition.one_length d] at hd symm at hd contradiction - · let d2 := d.erase (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1) + · let d2 := d.erase (smallestPrimeFactor n) (Nat.smallestPrimeFactor_prime hn_ge_1) (Nat.smallestPrimeFactor_dvd n hn_ge_1) suffices d2.length = k - 1 by - exact isMultipleOfKPrimes_primeDecompositionLength.mpr ⟨d2, by simp [this]⟩ - let x := PrimeDecomposition.erase_length_eq_length_minus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1) + exact isMultipleOfKPrimes_iff_primeDecomposition_length.mpr ⟨d2, by simp [this]⟩ + let x := PrimeDecomposition.erase_length d (smallestPrimeFactor n) (Nat.smallestPrimeFactor_prime hn_ge_1) (Nat.smallestPrimeFactor_dvd n hn_ge_1) rw [x, hd] -theorem List.prod_3_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by - simp [List.prod] - rw [Nat.mul_assoc] - -theorem primeDecomposition_length_3 (n : Nat) : +theorem PrimeDecomposition.length_three (n : Nat) : (∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃) ↔ ∃ (d : PrimeDecomposition n), d.length = 3 := by constructor @@ -297,8 +298,8 @@ theorem primeDecomposition_length_3 (n : Nat) : suffices d.length = 3 by exact ⟨d, this⟩ - repeat rw [PrimeDecomposition.push_length_eq_length_plus_one] - rw [PrimeDecomposition.one_length_eq_zero] + repeat rw [PrimeDecomposition.push_length] + rw [PrimeDecomposition.one_length] · intro ⟨⟨ps, hp, ha⟩, hd⟩ simp [PrimeDecomposition.length] at hd match ps with @@ -312,7 +313,7 @@ theorem primeDecomposition_length_3 (n : Nat) : rw [hd] at ha suffices a₁ * a₂ * a₃ = n ∧ a₁.IsPrime ∧ a₂.IsPrime ∧ a₃.IsPrime by exact ⟨a₁, a₂, a₃, this⟩ - rw [List.prod_3_mul] at ha + rw [List.prod_three_mul] at ha constructor · exact ha constructor @@ -327,10 +328,13 @@ theorem primeDecomposition_length_3 (n : Nat) : simp at t trivial -theorem isMultiplyPrime_is_correct : IsMultiplyPrimeIff isMultiplyPrime := by +def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := + (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ + +theorem isMultiplyPrime_correct : IsMultiplyPrimeIff isMultiplyPrime := by intro a - rw [primeDecomposition_length_3 a] - simp [isMultiplyPrime, isMultipleOfKPrimes_primeDecompositionLength] + rw [PrimeDecomposition.length_three a] + simp [isMultiplyPrime, isMultipleOfKPrimes_iff_primeDecomposition_length] /-! ## Prompt From d2e20402523a9a809873c6bc584bbe1aeecfd639 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 24 Jul 2025 11:41:43 +0200 Subject: [PATCH 13/21] continue refactoring code golf and renames --- HumanEvalLean/HumanEval75.lean | 42 ++++++++++++++++------------------ 1 file changed, 20 insertions(+), 22 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 1cb849d..d7dd4ac 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -53,10 +53,10 @@ example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide -- Section: Is prime -def Nat.IsPrime (n : Nat) : Prop := +def Nat.Prime (n : Nat) : Prop := n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n -theorem Nat.IsPrime.ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by +theorem Nat.Prime.ne_zero (hp : Prime p) : p ≠ 0 := by intro h have h2 : 2 ∣ p := by simp [h] apply Or.elim (hp.right 2 h2) @@ -64,17 +64,17 @@ theorem Nat.IsPrime.ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by rw [h] trivial -theorem Nat.IsPrime.zero_lt (hp : Nat.IsPrime p) : 0 < p := by match p with +theorem Nat.Prime.zero_lt (hp : Prime p) : 0 < p := by match p with | p + 1 => simp - | 0 => simp [Nat.IsPrime] at hp + | 0 => simp [Prime] at hp -theorem Nat.IsPrime.two_le (hp : Nat.IsPrime p) : 2 ≤ p := by sorry +theorem Nat.Prime.two_le (hp : Prime p) : 2 ≤ p := by sorry -- Section: Smallest prime factor theorem Nat.smallestPrimeFactor_dvd (n : Nat) (hn : 1 < n) : smallestPrimeFactor n ∣ n := by sorry -theorem Nat.smallestPrimeFactor_prime {n : Nat} (hn : 1 < n) : Nat.IsPrime (smallestPrimeFactor n) := by sorry +theorem Nat.smallestPrimeFactor_prime {n : Nat} (hn : 1 < n) : Prime (smallestPrimeFactor n) := by sorry theorem isMultipleOfKPrimes_zero (k : Nat) : isMultipleOfKPrimes 0 k = false := by simp [isMultipleOfKPrimes] @@ -141,12 +141,12 @@ theorem List.prod_three_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by structure PrimeDecomposition (n : Nat) where -- Multiset is only available in mathlib, using List instead ps : List Nat - all_prime : ∀ p ∈ ps, p.IsPrime + all_prime : ∀ p ∈ ps, p.Prime is_decomposition : ps.prod = n def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length -def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : PrimeDecomposition (n * p) := +def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.Prime) : PrimeDecomposition (n * p) := ⟨p :: d.ps, by intro p1 h @@ -164,7 +164,7 @@ def PrimeDecomposition.erase_head (d : PrimeDecomposition n) : PrimeDecompositio | [] => sorry | head :: tail => sorry -theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.IsPrime) (hd : p ∣ n) : p ∈ d.ps := by +theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.Prime) (hd : p ∣ n) : p ∈ d.ps := by let ⟨ps, ha, hb⟩ := d induction ps generalizing n with | nil => @@ -181,15 +181,15 @@ theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.IsPrime) else simp [hp] have hh : d.ps.headD 1 = head := by sorry - let ih := ih d.PrimeDecomposition.erase_head + let ih := ih d.erase_head rw [hh] at ih have hd : p ∣ n / head := by sorry - have hpp : ∀ p ∈ tail, p.IsPrime := by sorry + have hpp : ∀ p ∈ tail, p.Prime := by sorry apply ih hd hpp simp [List.prod_cons] at hb sorry -def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : PrimeDecomposition (n / p) := +def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.Prime) (hd : p ∣ n) : PrimeDecomposition (n / p) := ⟨d.ps.erase p, fun p1 h1 => d.all_prime p1 (List.mem_of_mem_erase h1), by rw [List.prod_erase d.ps p (PrimeDecomposition.prime_mem d hp hd) hp.zero_lt]; simp [d.is_decomposition]⟩ @@ -197,17 +197,14 @@ def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrim theorem PrimeDecomposition.push_length {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by simp [PrimeDecomposition.push, PrimeDecomposition.length] -theorem PrimeDecomposition.erase_length (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by +theorem PrimeDecomposition.erase_length (d : PrimeDecomposition n) (p : Nat) (hp : p.Prime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by simp [PrimeDecomposition.length, PrimeDecomposition.erase] rw [List.length_erase_of_mem (PrimeDecomposition.prime_mem d hp hd)] def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod_nil])⟩ -theorem PrimeDecomposition.zero_does_not_exist (d : PrimeDecomposition 0) : False := by - apply List.prod_ne_zero d.ps - · intro x h - exact Nat.IsPrime.ne_zero (d.all_prime x h) - exact d.is_decomposition +theorem PrimeDecomposition.zero_not_exist (d : PrimeDecomposition 0) : False := by + exact List.prod_ne_zero d.ps (fun x h => (d.all_prime x h).ne_zero) d.is_decomposition theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDecomposition.one := by simp [PrimeDecomposition.one] @@ -226,7 +223,7 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : rw [hn₀] simp [isMultipleOfKPrimes] intro x h - exact PrimeDecomposition.zero_does_not_exist x + exact PrimeDecomposition.zero_not_exist x else unfold isMultipleOfKPrimes simp [hn₀] @@ -284,7 +281,7 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : rw [x, hd] theorem PrimeDecomposition.length_three (n : Nat) : - (∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃) + (∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ p₁.Prime ∧ p₂.Prime ∧ p₃.Prime) ↔ ∃ (d : PrimeDecomposition n), d.length = 3 := by constructor · intro ⟨a, b, c, ⟨h, ha, hb, hc⟩⟩ @@ -311,7 +308,7 @@ theorem PrimeDecomposition.length_three (n : Nat) : | a₃ :: rest => simp at hd rw [hd] at ha - suffices a₁ * a₂ * a₃ = n ∧ a₁.IsPrime ∧ a₂.IsPrime ∧ a₃.IsPrime by + suffices a₁ * a₂ * a₃ = n ∧ a₁.Prime ∧ a₂.Prime ∧ a₃.Prime by exact ⟨a₁, a₂, a₃, this⟩ rw [List.prod_three_mul] at ha constructor @@ -329,13 +326,14 @@ theorem PrimeDecomposition.length_three (n : Nat) : trivial def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := - (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃ + (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ p₁.Prime ∧ p₂.Prime ∧ p₃.Prime theorem isMultiplyPrime_correct : IsMultiplyPrimeIff isMultiplyPrime := by intro a rw [PrimeDecomposition.length_three a] simp [isMultiplyPrime, isMultipleOfKPrimes_iff_primeDecomposition_length] + /-! ## Prompt From ac922f1da013b4beab851c5a4efaefc5d428803f Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 24 Jul 2025 11:44:57 +0200 Subject: [PATCH 14/21] add references to mathlib --- HumanEvalLean/HumanEval75.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index d7dd4ac..48b03ab 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -53,9 +53,11 @@ example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide -- Section: Is prime +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.Prime def Nat.Prime (n : Nat) : Prop := n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Prime/Defs.html#Prime.ne_zero theorem Nat.Prime.ne_zero (hp : Prime p) : p ≠ 0 := by intro h have h2 : 2 ∣ p := by simp [h] @@ -68,6 +70,7 @@ theorem Nat.Prime.zero_lt (hp : Prime p) : 0 < p := by match p with | p + 1 => simp | 0 => simp [Prime] at hp +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.Prime.two_le theorem Nat.Prime.two_le (hp : Prime p) : 2 ≤ p := by sorry -- Section: Smallest prime factor @@ -85,6 +88,7 @@ theorem isMultipleOfKPrimes_zero (k : Nat) : isMultipleOfKPrimes 0 k = false := def List.prod {α} [Mul α] [One α] : List α → α := List.foldr (· * ·) 1 +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Ring/List.html#List.prod_ne_zero theorem List.prod_ne_zero (l : List Nat) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by induction l with | nil => simp [List.prod] @@ -95,12 +99,15 @@ theorem List.prod_ne_zero (l : List Nat) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ · apply h x; simp · apply ih; intro x1 hx; apply h; simp [hx] +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Defs.html#List.prod_nil theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 := rfl +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Defs.html#List.prod_cons theorem List.prod_cons (a : α) (l : List α) [Mul α] [One α] : (a :: l).prod = a * l.prod := by simp [List.prod] +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Lemmas.html#List.dvd_prod theorem List.dvd_prod {l : List Nat} {n : Nat} (h : n ∈ l) : n ∣ l.prod := by induction l with | nil => contradiction @@ -116,6 +123,7 @@ theorem List.dvd_prod {l : List Nat} {n : Nat} (h : n ∈ l) : n ∣ l.prod := b simp exact Nat.dvd_mul_left_of_dvd (ih ht) head +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Basic.html#List.prod_erase theorem List.prod_erase (l : List Nat) (p : Nat) (h : p ∈ l) (h1 : 0 < p) : (l.erase p).prod = l.prod / p := by induction l with | nil => contradiction @@ -333,7 +341,6 @@ theorem isMultiplyPrime_correct : IsMultiplyPrimeIff isMultiplyPrime := by rw [PrimeDecomposition.length_three a] simp [isMultiplyPrime, isMultipleOfKPrimes_iff_primeDecomposition_length] - /-! ## Prompt From b3cd3f5657e09592a6fbd8e1fa5d25c5d31f9f60 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 24 Jul 2025 15:23:49 +0200 Subject: [PATCH 15/21] finish batch of sorries missing smallestPrimeFactor --- HumanEvalLean/HumanEval75.lean | 157 +++++++++++++++++++++------------ 1 file changed, 103 insertions(+), 54 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 48b03ab..d988331 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -51,27 +51,75 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide --- Section: Is prime +-- Section: Logic + +theorem by_contra {p : Prop} (h : ¬p → False) : p := by + if h1 : p then + exact h1 + else + simp [h1, h] + +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Bool/Basic.html#Bool.not_eq_true_eq_eq_false +theorem Bool.not_eq_true_eq_eq_false {b : Bool} : ¬b = true ↔ b = false := by simp + +-- Section: Prime -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.Prime def Nat.Prime (n : Nat) : Prop := - n > 1 ∧ ∀ m, m ∣ n → m = 1 ∨ m = n + 1 < n ∧ ∀ {a b}, n ∣ a * b → n ∣ a ∨ n ∣ b + + +theorem Nat.Prime.one_lt (hp : Prime p) : 1 < p := hp.left + +theorem Nat.Prime.zero_lt (hp : Prime p) : 0 < p := Nat.lt_trans (by simp) (hp.one_lt) -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Prime/Defs.html#Prime.ne_zero -theorem Nat.Prime.ne_zero (hp : Prime p) : p ≠ 0 := by - intro h - have h2 : 2 ∣ p := by simp [h] - apply Or.elim (hp.right 2 h2) - trivial - rw [h] - trivial - -theorem Nat.Prime.zero_lt (hp : Prime p) : 0 < p := by match p with - | p + 1 => simp - | 0 => simp [Prime] at hp +theorem Nat.Prime.ne_zero (hp : Prime p) : p ≠ 0 := Ne.symm (Nat.ne_of_lt hp.zero_lt) + +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Prime/Defs.html#Prime.ne_one +theorem Nat.Prime.ne_one (hp : Prime p) : p ≠ 1 := Ne.symm (Nat.ne_of_lt hp.one_lt) -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.Prime.two_le -theorem Nat.Prime.two_le (hp : Prime p) : 2 ≤ p := by sorry +theorem Nat.Prime.two_le (hp : Prime p) : 2 ≤ p := by + match p with + | 0 => simp [Prime] at hp + | 1 => simp [Prime] at hp + | n + 2 => simp + +theorem Nat.Prime.eq_one_or_self_of_dvd {a p : Nat} (hb : Prime p) (h : a ∣ p) : a = 1 ∨ a = p := by + let ⟨u, hu⟩ := h + have hd : p ∣ a * u := by simp [hu] + apply Or.elim (hb.right hd) + · intro hr; simp [Nat.dvd_antisymm h hr] + · intro huu + suffices a = 1 by simp [this] + let ⟨v, hv⟩ := huu + rw [hv, Nat.mul_comm p, ← Nat.mul_assoc] at hu + have : a ∣ 1 := by exact ⟨v, Nat.mul_right_cancel hb.zero_lt (by simp; exact hu)⟩ + exact Nat.dvd_one.mp this + +theorem Nat.Prime.not_dvd_of_ne {a b : Nat} (ha : Prime a) (hb : Prime b) (hne : a ≠ b) : ¬a ∣ b := + (fun h => Or.elim (hb.eq_one_or_self_of_dvd h) ha.ne_one hne) + +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Prime/Defs.html#Prime.dvd_mul +theorem Nat.Prime.dvd_mul (hp : Prime p) : p ∣ a * b ↔ p ∣ a ∨ p ∣ b := by + constructor + · exact hp.right + · exact (Or.elim · (Nat.dvd_trans · (Nat.dvd_mul_right _ _)) (Nat.dvd_trans · (Nat.dvd_mul_left _ _))) + +theorem Nat.Prime.dvd_div_of_dvd_mul {p a b : Nat} (hp : Prime p) (ha : p ∣ a) (hb : ¬p ∣ b) (hab : b ∣ a) : p ∣ a / b := by + rcases ha with ⟨u, hu⟩ + suffices a / b = p * (u / b) by exact ⟨u / b, this⟩ + suffices b ∣ u by rw [hu, Nat.mul_div_assoc _ this] + rw [hu] at hab + rcases hab with ⟨v, hv⟩ + suffices u = b * (v / p) by exact ⟨v / p, this⟩ + suffices p ∣ v by rw [← Nat.mul_div_assoc _ this, ← hv, Nat.mul_comm, Nat.mul_div_cancel _ hp.zero_lt] + have : p ∣ b * v := ⟨u, Eq.symm hv⟩ + rw [Nat.Prime.dvd_mul hp] at this + apply Or.elim this + · intro h; contradiction + · exact fun x => x -- Section: Smallest prime factor @@ -116,12 +164,11 @@ theorem List.dvd_prod {l : List Nat} {n : Nat} (h : n ∈ l) : n ∣ l.prod := b if hd : head = n then simp [hd, Nat.dvd_mul_right] else - have ht : n ∈ tail := by - simp at h - apply Or.elim h - intro x; symm at x; contradiction - simp - exact Nat.dvd_mul_left_of_dvd (ih ht) head + suffices n ∈ tail by exact Nat.dvd_mul_left_of_dvd (ih this) head + simp at h + apply Or.elim h + · intro x; symm at x; contradiction + · simp -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Basic.html#List.prod_erase theorem List.prod_erase (l : List Nat) (p : Nat) (h : p ∈ l) (h1 : 0 < p) : (l.erase p).prod = l.prod / p := by @@ -167,10 +214,17 @@ def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.Prime) rw [d.is_decomposition, Nat.mul_comm] ⟩ -def PrimeDecomposition.erase_head (d : PrimeDecomposition n) : PrimeDecomposition (n / d.ps.headD 1) := by - match d.ps with - | [] => sorry - | head :: tail => sorry +def PrimeDecomposition.erase_head (d : PrimeDecomposition n) : PrimeDecomposition (n / d.ps.headD 1) := + let ⟨ps, ha, hb⟩ := d + match ps with + | [] => ⟨[], ha, by simp; exact hb⟩ + | head :: tail => + ⟨tail, + fun p h => ha p (by simp [h]), + by simp + simp [List.prod_cons] at hb + symm at hb + rw [hb, Nat.mul_comm, Nat.mul_div_cancel _ (ha head (by simp)).zero_lt]⟩ theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.Prime) (hd : p ∣ n) : p ∈ d.ps := by let ⟨ps, ha, hb⟩ := d @@ -184,18 +238,22 @@ theorem PrimeDecomposition.prime_mem (d : PrimeDecomposition n) (hp : p.Prime) ( | cons head tail ih => simp simp at ih - if hp : p = head then - simp [hp] + if hh : p = head then + simp [hh] else - simp [hp] - have hh : d.ps.headD 1 = head := by sorry - let ih := ih d.erase_head - rw [hh] at ih - have hd : p ∣ n / head := by sorry - have hpp : ∀ p ∈ tail, p.Prime := by sorry - apply ih hd hpp + simp [hh] + let ih := ih ((⟨head :: tail, ha, hb⟩ : PrimeDecomposition n).erase_head) + simp at ih simp [List.prod_cons] at hb - sorry + symm at hb + apply ih + · apply hp.dvd_div_of_dvd_mul hd (hp.not_dvd_of_ne (ha head (by simp)) hh) + simp [hb, Nat.dvd_mul_right] + · intro p1 ht + specialize ha p1 + simp [ht] at ha + exact ha + · rw [hb, Nat.mul_comm, Nat.mul_div_cancel _ (ha head (by simp)).zero_lt] def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.Prime) (hd : p ∣ n) : PrimeDecomposition (n / p) := ⟨d.ps.erase p, @@ -214,16 +272,17 @@ def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [L theorem PrimeDecomposition.zero_not_exist (d : PrimeDecomposition 0) : False := by exact List.prod_ne_zero d.ps (fun x h => (d.all_prime x h).ne_zero) d.is_decomposition -theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDecomposition.one := by - simp [PrimeDecomposition.one] - if h : d.ps = [] then - sorry - else - sorry - theorem PrimeDecomposition.one_length (d : PrimeDecomposition 1) : d.length = 0 := by - rw [PrimeDecomposition.one_unique d] - simp [PrimeDecomposition.length, PrimeDecomposition.one] + let ⟨ps, hp, hd⟩ := d + simp [PrimeDecomposition.length] + apply by_contra + intro h + rw [← List.isEmpty_iff, Bool.not_eq_true_eq_eq_false, List.isEmpty_eq_false_iff_exists_mem] at h + rcases h with ⟨x, hx⟩ + specialize hp x hx + have : x ∣ 1 := by rw [← hd]; exact List.dvd_prod hx + let e := Nat.le_trans hp.two_le (Nat.le_of_dvd (by simp) this) + contradiction theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by @@ -321,17 +380,7 @@ theorem PrimeDecomposition.length_three (n : Nat) : rw [List.prod_three_mul] at ha constructor · exact ha - constructor - · let t := hp a₁ - simp at t - trivial - constructor - · let t := hp a₂ - simp at t - trivial - · let t := hp a₃ - simp at t - trivial + exact ⟨by simp [hp a₁], by simp [hp a₂], by simp [hp a₃]⟩ def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop := (a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ p₁.Prime ∧ p₂.Prime ∧ p₃.Prime From 3eaa37971fc54c944901d91951041a1f3eb1fb35 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Thu, 24 Jul 2025 15:28:30 +0200 Subject: [PATCH 16/21] similar to mathlib --- HumanEvalLean/HumanEval75.lean | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index d988331..9646a76 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -3,7 +3,8 @@ import Init.Data.Nat.Dvd open Std Do -def smallestPrimeFactor (n : Nat) : Nat := +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac +def minFac (n : Nat) : Nat := go 2 where go (i : Nat) : Nat := @@ -30,7 +31,7 @@ def isMultipleOfKPrimes (n : Nat) (k : Nat) : Bool := else if hn₁ : n = 1 then false else - let p := smallestPrimeFactor n + let p := minFac n isMultipleOfKPrimes (n / p) (k - 1) termination_by k decreasing_by @@ -68,7 +69,6 @@ theorem Bool.not_eq_true_eq_eq_false {b : Bool} : ¬b = true ↔ b = false := by def Nat.Prime (n : Nat) : Prop := 1 < n ∧ ∀ {a b}, n ∣ a * b → n ∣ a ∨ n ∣ b - theorem Nat.Prime.one_lt (hp : Prime p) : 1 < p := hp.left theorem Nat.Prime.zero_lt (hp : Prime p) : 0 < p := Nat.lt_trans (by simp) (hp.one_lt) @@ -123,12 +123,11 @@ theorem Nat.Prime.dvd_div_of_dvd_mul {p a b : Nat} (hp : Prime p) (ha : p ∣ a) -- Section: Smallest prime factor -theorem Nat.smallestPrimeFactor_dvd (n : Nat) (hn : 1 < n) : smallestPrimeFactor n ∣ n := by sorry - -theorem Nat.smallestPrimeFactor_prime {n : Nat} (hn : 1 < n) : Prime (smallestPrimeFactor n) := by sorry +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_dvd +theorem Nat.minFactor_dvd (n : Nat) : minFac n ∣ n := by sorry -theorem isMultipleOfKPrimes_zero (k : Nat) : isMultipleOfKPrimes 0 k = false := by - simp [isMultipleOfKPrimes] +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_prime +theorem Nat.minFactor_prime {n : Nat} (hn : 1 < n) : Prime (minFac n) := by sorry -- Section: List @@ -315,8 +314,8 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : | 0 => trivial | 1 => trivial | n + 2 => simp - let d₁ := d.push (smallestPrimeFactor n) (Nat.smallestPrimeFactor_prime hn_ge_1) - rw [← Nat.div_mul_cancel (Nat.smallestPrimeFactor_dvd n hn_ge_1)] + let d₁ := d.push (minFac n) (Nat.minFactor_prime hn_ge_1) + rw [← Nat.div_mul_cancel (Nat.minFactor_dvd n)] suffices d₁.length = k by exact ⟨d₁, by simp [this]⟩ rw [PrimeDecomposition.push_length, hd] @@ -341,10 +340,10 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : rw [PrimeDecomposition.one_length d] at hd symm at hd contradiction - · let d2 := d.erase (smallestPrimeFactor n) (Nat.smallestPrimeFactor_prime hn_ge_1) (Nat.smallestPrimeFactor_dvd n hn_ge_1) + · let d2 := d.erase (minFac n) (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) suffices d2.length = k - 1 by exact isMultipleOfKPrimes_iff_primeDecomposition_length.mpr ⟨d2, by simp [this]⟩ - let x := PrimeDecomposition.erase_length d (smallestPrimeFactor n) (Nat.smallestPrimeFactor_prime hn_ge_1) (Nat.smallestPrimeFactor_dvd n hn_ge_1) + let x := PrimeDecomposition.erase_length d (minFac n) (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) rw [x, hd] theorem PrimeDecomposition.length_three (n : Nat) : From 9ec711c4cf6a624512293b1d1bda3f691cfa5f3f Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 25 Jul 2025 09:53:29 +0200 Subject: [PATCH 17/21] refactor minFac usage --- HumanEvalLean/HumanEval75.lean | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index 9646a76..b110efe 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -4,7 +4,7 @@ import Init.Data.Nat.Dvd open Std Do -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac -def minFac (n : Nat) : Nat := +def Nat.minFac (n : Nat) : Nat := go 2 where go (i : Nat) : Nat := @@ -31,7 +31,7 @@ def isMultipleOfKPrimes (n : Nat) (k : Nat) : Bool := else if hn₁ : n = 1 then false else - let p := minFac n + let p := n.minFac isMultipleOfKPrimes (n / p) (k - 1) termination_by k decreasing_by @@ -123,11 +123,14 @@ theorem Nat.Prime.dvd_div_of_dvd_mul {p a b : Nat} (hp : Prime p) (ha : p ∣ a) -- Section: Smallest prime factor +theorem Nat.minFac.go_dvd {n : Nat} : Nat.minFac.go n 2 ∣ n := by sorry + -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_dvd -theorem Nat.minFactor_dvd (n : Nat) : minFac n ∣ n := by sorry +theorem Nat.minFactor_dvd (n : Nat) : n.minFac ∣ n := by + simp [Nat.minFac, Nat.minFac.go_dvd] -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_prime -theorem Nat.minFactor_prime {n : Nat} (hn : 1 < n) : Prime (minFac n) := by sorry +theorem Nat.minFactor_prime {n : Nat} (hn : 1 < n) : Prime (n.minFac) := by sorry -- Section: List @@ -314,7 +317,7 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : | 0 => trivial | 1 => trivial | n + 2 => simp - let d₁ := d.push (minFac n) (Nat.minFactor_prime hn_ge_1) + let d₁ := d.push n.minFac (Nat.minFactor_prime hn_ge_1) rw [← Nat.div_mul_cancel (Nat.minFactor_dvd n)] suffices d₁.length = k by exact ⟨d₁, by simp [this]⟩ @@ -340,10 +343,10 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : rw [PrimeDecomposition.one_length d] at hd symm at hd contradiction - · let d2 := d.erase (minFac n) (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) + · let d2 := d.erase n.minFac (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) suffices d2.length = k - 1 by exact isMultipleOfKPrimes_iff_primeDecomposition_length.mpr ⟨d2, by simp [this]⟩ - let x := PrimeDecomposition.erase_length d (minFac n) (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) + let x := PrimeDecomposition.erase_length d n.minFac (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) rw [x, hd] theorem PrimeDecomposition.length_three (n : Nat) : From 17a084c71ce0a410994848df8f97126d0203afb9 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 25 Jul 2025 16:43:32 +0200 Subject: [PATCH 18/21] missing one theorems about primes --- HumanEvalLean/HumanEval75.lean | 119 +++++++++++++++++++++++++++++++-- 1 file changed, 112 insertions(+), 7 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index b110efe..d906291 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -52,6 +52,18 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide +-- Section: Nat + +theorem Nat.mul_lt_sq_imp_lt {a b : Nat} (h : a * b < d * d) : a < d ∨ b < d := by + if hn : a < d then + simp [hn] + else + simp at hn + right + suffices d * b ≤ a * b by + exact Nat.lt_of_mul_lt_mul_left (Nat.lt_of_le_of_lt this h) + exact mul_le_mul_right b hn + -- Section: Logic theorem by_contra {p : Prop} (h : ¬p → False) : p := by @@ -98,6 +110,8 @@ theorem Nat.Prime.eq_one_or_self_of_dvd {a p : Nat} (hb : Prime p) (h : a ∣ p) have : a ∣ 1 := by exact ⟨v, Nat.mul_right_cancel hb.zero_lt (by simp; exact hu)⟩ exact Nat.dvd_one.mp this +theorem Nat.prime_def {p : Nat} : p.Prime ↔ 1 < p ∧ ∀ (m : Nat), m ∣ p → m = 1 ∨ m = p := by sorry + theorem Nat.Prime.not_dvd_of_ne {a b : Nat} (ha : Prime a) (hb : Prime b) (hne : a ≠ b) : ¬a ∣ b := (fun h => Or.elim (hb.eq_one_or_self_of_dvd h) ha.ne_one hne) @@ -123,14 +137,105 @@ theorem Nat.Prime.dvd_div_of_dvd_mul {p a b : Nat} (hp : Prime p) (ha : p ∣ a) -- Section: Smallest prime factor -theorem Nat.minFac.go_dvd {n : Nat} : Nat.minFac.go n 2 ∣ n := by sorry +theorem Nat.minFac.go_dvd {n : Nat} : Nat.minFac.go n 2 ∣ n := by + fun_induction Nat.minFac.go n 2 + case case1 i hni => simp + case case2 => assumption + case case3 => assumption -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_dvd -theorem Nat.minFactor_dvd (n : Nat) : n.minFac ∣ n := by +theorem Nat.minFac_dvd (n : Nat) : n.minFac ∣ n := by simp [Nat.minFac, Nat.minFac.go_dvd] +theorem not_lt_iff_eq_or_lt {a b : Nat} : ¬a < b ↔ a = b ∨ a > b := by + simp + constructor + · intro h + match h with + | Nat.le.refl => simp + | Nat.le.step a => exact Or.inr (Nat.lt_add_one_of_le a) + · intro h + rcases h with ⟨h1, h2⟩ + simp + omega + +theorem minFac_go_prime + {n i : Nat} (hn : 1 < n) (hi : 1 < i): + (∀ k, 1 < k → k < i → ¬ k ∣ n) → + (Nat.minFac.go n i).Prime := by + fun_induction Nat.minFac.go n i + with + | case1 i hlt => + intro h + simp [Nat.prime_def, hn] + intro m hd + if g : m = 1 ∨ m = n then + exact g + else + simp [g] + simp at g + have hm₁ : 1 < m := by match m with + | 0 => rw [Nat.zero_dvd] at hd; rw [hd] at hn; contradiction + | 1 => simp at g + | _ + 2 => simp + + suffices m < i by + specialize h m hm₁ this + exact h hd + + let ⟨m', hm'⟩ := hd + symm at hm' + rw [← hm'] at hlt + apply Or.elim (Nat.mul_lt_sq_imp_lt hlt) + simp + intro hd' + have hm₁' : 1 < m' := by match m' with + | 0 => simp at hm'; rw [hm']; exact hn + | 1 => simp at hm'; rw [hm'] at g; simp at g + | _ + 2 => simp + specialize h m' hm₁' hd' + exfalso + apply h + rw [← hm'] + exact ⟨m, by simp [Nat.mul_comm]⟩ + + | case2 i hlt hdiv => + intro h + simp [Nat.prime_def, hi] + intro m hm + match m with + | 0 => rw [Nat.zero_dvd] at hm; symm at hm; simp [hm] + | 1 => simp + | m' + 2 => + if he : m' + 2 = i then + simp [he] + else + simp [he] + specialize h (m' + 2) (by simp) (Nat.lt_of_le_of_ne (Nat.le_of_dvd (by omega) hm) he) + exact h (Nat.dvd_trans hm hdiv) + | case3 i h1 h2 ih => + intro hk + apply ih (Nat.lt_add_right 1 hi) + intro k h3 h4 + if h5 : k < i then + exact hk k h3 h5 + else if h6 : k = i then + rw [h6]; exact h2 + else + exfalso + rw [not_lt_iff_eq_or_lt] at h5 + apply Or.elim h5 + · exact h6 + · simp [Nat.le_of_lt_add_one, h4] + -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_prime -theorem Nat.minFactor_prime {n : Nat} (hn : 1 < n) : Prime (n.minFac) := by sorry +theorem Nat.minFac_prime {n : Nat} (hn : 1 < n) : Prime (n.minFac) := by + apply minFac_go_prime hn (by simp) + intro k hk1 hk2 + match k with + | 0 => contradiction + | 1 => contradiction + | n + 2 => contradiction -- Section: List @@ -317,8 +422,8 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : | 0 => trivial | 1 => trivial | n + 2 => simp - let d₁ := d.push n.minFac (Nat.minFactor_prime hn_ge_1) - rw [← Nat.div_mul_cancel (Nat.minFactor_dvd n)] + let d₁ := d.push n.minFac (Nat.minFac_prime hn_ge_1) + rw [← Nat.div_mul_cancel (Nat.minFac_dvd n)] suffices d₁.length = k by exact ⟨d₁, by simp [this]⟩ rw [PrimeDecomposition.push_length, hd] @@ -343,10 +448,10 @@ theorem isMultipleOfKPrimes_iff_primeDecomposition_length {n k : Nat} : rw [PrimeDecomposition.one_length d] at hd symm at hd contradiction - · let d2 := d.erase n.minFac (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) + · let d2 := d.erase n.minFac (Nat.minFac_prime hn_ge_1) (Nat.minFac_dvd n) suffices d2.length = k - 1 by exact isMultipleOfKPrimes_iff_primeDecomposition_length.mpr ⟨d2, by simp [this]⟩ - let x := PrimeDecomposition.erase_length d n.minFac (Nat.minFactor_prime hn_ge_1) (Nat.minFactor_dvd n) + let x := PrimeDecomposition.erase_length d n.minFac (Nat.minFac_prime hn_ge_1) (Nat.minFac_dvd n) rw [x, hd] theorem PrimeDecomposition.length_three (n : Nat) : From 6454bc01c2c419fd63c94bc6eb4807cf458fbe06 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 25 Jul 2025 17:11:48 +0200 Subject: [PATCH 19/21] sorry free --- HumanEvalLean/HumanEval75.lean | 47 ++++++++++++++++++++++++---------- 1 file changed, 33 insertions(+), 14 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index d906291..eef6c4a 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,5 +1,6 @@ import Std.Tactic.Do import Init.Data.Nat.Dvd +import Init.Data.Nat.Gcd open Std Do @@ -52,6 +53,17 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide +-- Section: Logic + +theorem by_contra {p : Prop} (h : ¬p → False) : p := by + if h1 : p then + exact h1 + else + simp [h1, h] + +-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Bool/Basic.html#Bool.not_eq_true_eq_eq_false +theorem Bool.not_eq_true_eq_eq_false {b : Bool} : ¬b = true ↔ b = false := by simp + -- Section: Nat theorem Nat.mul_lt_sq_imp_lt {a b : Nat} (h : a * b < d * d) : a < d ∨ b < d := by @@ -64,17 +76,6 @@ theorem Nat.mul_lt_sq_imp_lt {a b : Nat} (h : a * b < d * d) : a < d ∨ b < d : exact Nat.lt_of_mul_lt_mul_left (Nat.lt_of_le_of_lt this h) exact mul_le_mul_right b hn --- Section: Logic - -theorem by_contra {p : Prop} (h : ¬p → False) : p := by - if h1 : p then - exact h1 - else - simp [h1, h] - --- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Bool/Basic.html#Bool.not_eq_true_eq_eq_false -theorem Bool.not_eq_true_eq_eq_false {b : Bool} : ¬b = true ↔ b = false := by simp - -- Section: Prime -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.Prime @@ -98,7 +99,7 @@ theorem Nat.Prime.two_le (hp : Prime p) : 2 ≤ p := by | 1 => simp [Prime] at hp | n + 2 => simp -theorem Nat.Prime.eq_one_or_self_of_dvd {a p : Nat} (hb : Prime p) (h : a ∣ p) : a = 1 ∨ a = p := by +theorem Nat.Prime.eq_one_or_self_of_dvd {p : Nat} (hb : Prime p) (a : Nat) (h : a ∣ p) : a = 1 ∨ a = p := by let ⟨u, hu⟩ := h have hd : p ∣ a * u := by simp [hu] apply Or.elim (hb.right hd) @@ -110,10 +111,28 @@ theorem Nat.Prime.eq_one_or_self_of_dvd {a p : Nat} (hb : Prime p) (h : a ∣ p) have : a ∣ 1 := by exact ⟨v, Nat.mul_right_cancel hb.zero_lt (by simp; exact hu)⟩ exact Nat.dvd_one.mp this -theorem Nat.prime_def {p : Nat} : p.Prime ↔ 1 < p ∧ ∀ (m : Nat), m ∣ p → m = 1 ∨ m = p := by sorry +theorem Nat.prime_def {p : Nat} : p.Prime ↔ 1 < p ∧ ∀ (m : Nat), m ∣ p → m = 1 ∨ m = p := by + refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩ + simp [Nat.Prime, h.1] + let ⟨h1, h2⟩ := h + intro a b hd + apply Or.elim (h2 (Nat.gcd p a) (by simp [Nat.gcd_dvd])) + intro ha + apply Or.elim (h2 (Nat.gcd p b) (by simp [Nat.gcd_dvd])) + intro hb + rw [← Nat.dvd_gcd_mul_iff_dvd_mul, Nat.mul_comm, ← Nat.dvd_gcd_mul_iff_dvd_mul, ha, hb, Nat.mul_one, Nat.dvd_one] at hd + simp [hd] + intro h + rw [← h] + right + simp [Nat.gcd_dvd] + intro h + rw [← h] + left + simp [Nat.gcd_dvd] theorem Nat.Prime.not_dvd_of_ne {a b : Nat} (ha : Prime a) (hb : Prime b) (hne : a ≠ b) : ¬a ∣ b := - (fun h => Or.elim (hb.eq_one_or_self_of_dvd h) ha.ne_one hne) + (fun h => Or.elim (hb.eq_one_or_self_of_dvd _ h) ha.ne_one hne) -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Prime/Defs.html#Prime.dvd_mul theorem Nat.Prime.dvd_mul (hp : Prime p) : p ∣ a * b ↔ p ∣ a ∨ p ∣ b := by From 27ba3b10dfb01b409ea9f2a02a02f8e529f9c949 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 25 Jul 2025 17:14:25 +0200 Subject: [PATCH 20/21] don't need latest lean --- HumanEvalLean/HumanEval75.lean | 4 +--- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index eef6c4a..e86e0aa 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -1,9 +1,6 @@ -import Std.Tactic.Do import Init.Data.Nat.Dvd import Init.Data.Nat.Gcd -open Std Do - -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac def Nat.minFac (n : Nat) : Nat := go 2 @@ -60,6 +57,7 @@ theorem by_contra {p : Prop} (h : ¬p → False) : p := by exact h1 else simp [h1, h] + exact h h1 -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Bool/Basic.html#Bool.not_eq_true_eq_eq_false theorem Bool.not_eq_true_eq_eq_false {b : Bool} : ¬b = true ↔ b = false := by simp diff --git a/lean-toolchain b/lean-toolchain index 67eefcc..980709b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0-rc1 +leanprover/lean4:v4.21.0 From c64036be99244f8066e822378b60a30784b18641 Mon Sep 17 00:00:00 2001 From: Marcelo Fornet Date: Fri, 25 Jul 2025 17:27:59 +0200 Subject: [PATCH 21/21] golfing --- HumanEvalLean/HumanEval75.lean | 25 ++++++------------------- 1 file changed, 6 insertions(+), 19 deletions(-) diff --git a/HumanEvalLean/HumanEval75.lean b/HumanEvalLean/HumanEval75.lean index e86e0aa..68b64c5 100644 --- a/HumanEvalLean/HumanEval75.lean +++ b/HumanEvalLean/HumanEval75.lean @@ -106,8 +106,7 @@ theorem Nat.Prime.eq_one_or_self_of_dvd {p : Nat} (hb : Prime p) (a : Nat) (h : suffices a = 1 by simp [this] let ⟨v, hv⟩ := huu rw [hv, Nat.mul_comm p, ← Nat.mul_assoc] at hu - have : a ∣ 1 := by exact ⟨v, Nat.mul_right_cancel hb.zero_lt (by simp; exact hu)⟩ - exact Nat.dvd_one.mp this + exact Nat.dvd_one.mp ⟨v, Nat.mul_right_cancel hb.zero_lt (by simp; exact hu)⟩ theorem Nat.prime_def {p : Nat} : p.Prime ↔ 1 < p ∧ ∀ (m : Nat), m ∣ p → m = 1 ∨ m = p := by refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩ @@ -120,14 +119,8 @@ theorem Nat.prime_def {p : Nat} : p.Prime ↔ 1 < p ∧ ∀ (m : Nat), m ∣ p intro hb rw [← Nat.dvd_gcd_mul_iff_dvd_mul, Nat.mul_comm, ← Nat.dvd_gcd_mul_iff_dvd_mul, ha, hb, Nat.mul_one, Nat.dvd_one] at hd simp [hd] - intro h - rw [← h] - right - simp [Nat.gcd_dvd] - intro h - rw [← h] - left - simp [Nat.gcd_dvd] + intro h; rw [← h]; right; simp [Nat.gcd_dvd] + intro h; rw [← h]; left; simp [Nat.gcd_dvd] theorem Nat.Prime.not_dvd_of_ne {a b : Nat} (ha : Prime a) (hb : Prime b) (hne : a ≠ b) : ¬a ∣ b := (fun h => Or.elim (hb.eq_one_or_self_of_dvd _ h) ha.ne_one hne) @@ -156,9 +149,7 @@ theorem Nat.Prime.dvd_div_of_dvd_mul {p a b : Nat} (hp : Prime p) (ha : p ∣ a) theorem Nat.minFac.go_dvd {n : Nat} : Nat.minFac.go n 2 ∣ n := by fun_induction Nat.minFac.go n 2 - case case1 i hni => simp - case case2 => assumption - case case3 => assumption + simp; assumption; assumption -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_dvd theorem Nat.minFac_dvd (n : Nat) : n.minFac ∣ n := by @@ -248,7 +239,7 @@ theorem minFac_go_prime -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Defs.html#Nat.minFac_prime theorem Nat.minFac_prime {n : Nat} (hn : 1 < n) : Prime (n.minFac) := by apply minFac_go_prime hn (by simp) - intro k hk1 hk2 + intro k _ _ match k with | 0 => contradiction | 1 => contradiction @@ -271,10 +262,6 @@ theorem List.prod_ne_zero (l : List Nat) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ · apply h x; simp · apply ih; intro x1 hx; apply h; simp [hx] --- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Defs.html#List.prod_nil -theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 := - rfl - -- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/List/Defs.html#List.prod_cons theorem List.prod_cons (a : α) (l : List α) [Mul α] [One α] : (a :: l).prod = a * l.prod := by simp [List.prod] @@ -391,7 +378,7 @@ theorem PrimeDecomposition.erase_length (d : PrimeDecomposition n) (p : Nat) (hp simp [PrimeDecomposition.length, PrimeDecomposition.erase] rw [List.length_erase_of_mem (PrimeDecomposition.prime_mem d hp hd)] -def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod_nil])⟩ +def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod])⟩ theorem PrimeDecomposition.zero_not_exist (d : PrimeDecomposition 0) : False := by exact List.prod_ne_zero d.ps (fun x h => (d.all_prime x h).ne_zero) d.is_decomposition