From 93e0432f997db7602ff06a2c490a23146f29e51b Mon Sep 17 00:00:00 2001 From: Ondanaoto Date: Mon, 1 Jul 2024 23:15:16 +0900 Subject: [PATCH 1/4] solve 41 and 46 --- Src/Problem41.lean | 37 +++++++++++++++++++++++++++++++++++++ Src/Problem46.lean | 20 ++++++++++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 Src/Problem41.lean create mode 100644 Src/Problem46.lean diff --git a/Src/Problem41.lean b/Src/Problem41.lean new file mode 100644 index 0000000..5c59396 --- /dev/null +++ b/Src/Problem41.lean @@ -0,0 +1,37 @@ +/- # Problem 40 + +(Intermediate ๐ŸŒŸ๐ŸŒŸ) A list of even numbers and their Goldbach compositions in a given range. +-/ + +def Nat.isPrime (n : Nat) : Bool := + if n == 0 || n == 1 then + false + else + let properDivisors := List.range n + |>.drop 2 + |>.filter (n % ยท == 0) + properDivisors.length == 0 + +def goldbach (n : Nat) : Nat ร— Nat := Id.run do + -- sorry + for cand in (List.range n) do + if not cand.isPrime then + continue + let rest := n - cand + if not rest.isPrime then + continue + return (cand, rest) + + panic! "we've found a counter example of goldbach conjecture!! ๐ŸŽ‰" + + +def goldbachList (lower upper : Nat) (primeLower : Nat := 2) : List (Nat ร— Nat) := + List.range (upper + 1) + |>.filter (ยท โ‰ฅ lower) + |>.filter (ยท % 2 == 0) + |>.map (fun n => (goldbach n)) + |>.filter ( fun t => t.fst > primeLower) + +#guard goldbachList 9 20 == [(3, 7), (5, 7), (3, 11), (3, 13), (5, 13), (3, 17)] + +#guard goldbachList 4 2000 50 == [(73,919),(61,1321),(67,1789),(61,1867)] diff --git a/Src/Problem46.lean b/Src/Problem46.lean new file mode 100644 index 0000000..f76b2f2 --- /dev/null +++ b/Src/Problem46.lean @@ -0,0 +1,20 @@ +/- # Problem 46 +(Intermediate ๐ŸŒŸ๐ŸŒŸ) Truth tables for logical expressions. +-/ + + +def table (p : Bool โ†’ Bool โ†’ Bool) : List (List Bool) := + [ + [true, true, p true true], + [true, false, p true false], + [false, true, p false true], + [false, false, p false false] + ] + +#guard table (fun a b => And a (Or a b)) == + [ + [true, true, true], + [true, false, true], + [false, true, false], + [false, false, false] + ] From 394df8a09b4cbaed7c31379545cc9ce3ab8e16db Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 3 Jul 2024 13:53:56 +0900 Subject: [PATCH 2/4] edit TOC --- md/SUMMARY.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/md/SUMMARY.md b/md/SUMMARY.md index 1b0f7c4..708b87e 100644 --- a/md/SUMMARY.md +++ b/md/SUMMARY.md @@ -51,4 +51,9 @@ * [37: Euler's totient improved](./build/Problem37.md) * [38: Compare totient calculations]() * [39: Prime numbers in a range](./build/Problem39.md) -* [40: Goldbach's conjecture](./build/Problem40.md) \ No newline at end of file +* [40: Goldbach's conjecture](./build/Problem40.md) +* [41: Goldbach's list](./build/Problem41.md) + +# 46-50: Logic and codes + +* [46: Truth table](./build/Problem46.md) \ No newline at end of file From 22a4b4c041b9cc60670f48ae34199755ef3eaa7d Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 3 Jul 2024 13:56:33 +0900 Subject: [PATCH 3/4] modify P40 and P41 --- Src/Problem40.lean | 25 +++++++++++++++++-------- Src/Problem41.lean | 29 +++++++++++++++++------------ 2 files changed, 34 insertions(+), 20 deletions(-) diff --git a/Src/Problem40.lean b/Src/Problem40.lean index 7d60fdf..6d84c23 100644 --- a/Src/Problem40.lean +++ b/Src/Problem40.lean @@ -3,17 +3,24 @@ (Intermediate ๐ŸŒŸ๐ŸŒŸ) Goldbach's conjecture says that every positive even number greater than `2` is the sum of two prime numbers. Example: `28 = 5 + 23`. It is one of the most famous facts in number theory that has not been proved to be correct in the general case. It has been numerically confirmed up to very large numbers (much larger than we can go with our Prolog system). Write a predicate to find the two prime numbers that sum up to a given even integer. -/ -def Nat.isPrime (n : Nat) : Bool := - if n == 0 || n == 1 then - false - else - let properDivisors := List.range n - |>.drop 2 - |>.filter (n % ยท == 0) - properDivisors.length == 0 +def Nat.isPrime (n : Nat) : Bool := Id.run do + if n โ‰ค 2 then + return false + for d in [2:n] do + if n % d = 0 then + return false + if d ^ 2 > n then + break + return true + +-- You can use this! +#check Nat.isPrime def goldbach (n : Nat) : Nat ร— Nat := Id.run do -- sorry + if n % 2 โ‰  0 then + panic! "n must be an even number" + for cand in (List.range n) do if not cand.isPrime then continue @@ -41,3 +48,5 @@ def goldbachTest (n : Nat) : IO Unit := #eval goldbachTest 308 #eval goldbachTest 308000 + +#eval goldbachTest 19278020 diff --git a/Src/Problem41.lean b/Src/Problem41.lean index 5c59396..06a13b4 100644 --- a/Src/Problem41.lean +++ b/Src/Problem41.lean @@ -3,18 +3,18 @@ (Intermediate ๐ŸŒŸ๐ŸŒŸ) A list of even numbers and their Goldbach compositions in a given range. -/ -def Nat.isPrime (n : Nat) : Bool := - if n == 0 || n == 1 then - false - else - let properDivisors := List.range n - |>.drop 2 - |>.filter (n % ยท == 0) - properDivisors.length == 0 +def Nat.isPrime (n : Nat) : Bool := Id.run do + if n โ‰ค 2 then + return false + for d in [2:n] do + if n % d = 0 then + return false + if d ^ 2 > n then + break + return true def goldbach (n : Nat) : Nat ร— Nat := Id.run do - -- sorry - for cand in (List.range n) do + for cand in [2:n] do if not cand.isPrime then continue let rest := n - cand @@ -24,14 +24,19 @@ def goldbach (n : Nat) : Nat ร— Nat := Id.run do panic! "we've found a counter example of goldbach conjecture!! ๐ŸŽ‰" - def goldbachList (lower upper : Nat) (primeLower : Nat := 2) : List (Nat ร— Nat) := + -- sorry List.range (upper + 1) |>.filter (ยท โ‰ฅ lower) |>.filter (ยท % 2 == 0) |>.map (fun n => (goldbach n)) - |>.filter ( fun t => t.fst > primeLower) + |>.filter (fun t => t.fst > primeLower) + -- sorry + +-- The following codes are for test and you should not edit these. #guard goldbachList 9 20 == [(3, 7), (5, 7), (3, 11), (3, 13), (5, 13), (3, 17)] +#guard goldbachList 9 20 3 == [(5, 7), (5, 13)] + #guard goldbachList 4 2000 50 == [(73,919),(61,1321),(67,1789),(61,1867)] From 612ad00777d8175dc2ff063675d12b7dc9d26809 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 3 Jul 2024 14:00:55 +0900 Subject: [PATCH 4/4] modify P46 --- Src/Problem46.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Src/Problem46.lean b/Src/Problem46.lean index f76b2f2..0b99345 100644 --- a/Src/Problem46.lean +++ b/Src/Problem46.lean @@ -4,12 +4,16 @@ def table (p : Bool โ†’ Bool โ†’ Bool) : List (List Bool) := + -- sorry [ [true, true, p true true], [true, false, p true false], [false, true, p false true], [false, false, p false false] ] + -- sorry + +-- The following codes are for test and you should not edit these. #guard table (fun a b => And a (Or a b)) == [