add nth-prime

Author: oxe-i

config.json

@@ -117,6 +117,14 @@
         "practices": [],
         "prerequisites": [],
         "difficulty": 4
+      },
+      {
+        "slug": "nth-prime",
+        "name": "Nth Prime",
+        "uuid": "5ff6afa5-aaca-4cdb-84cf-844f4ef64591",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 5
       }
     ]
   },

exercises/practice/nth-prime/.docs/instructions.md

@@ -0,0 +1,7 @@
+# Instructions
+
+Given a number n, determine what the nth prime is.
+
+By listing the first six prime numbers: 2, 3, 5, 7, 11, and 13, we can see that the 6th prime is 13.
+
+If your language provides methods in the standard library to deal with prime numbers, pretend they don't exist and implement them yourself.

exercises/practice/nth-prime/.meta/Example.lean

@@ -0,0 +1,27 @@
+namespace NthPrime
+
+def updateTable (index : Nat) (increment : Nat) (table : Array Bool) : Array Bool :=
+  if positiveIncrement : increment > 0 then
+    if validIndex : index < table.size then
+      updateTable (index + increment) increment (table.set index false)
+    else table
+  else table
+
+def prime' (remaining : Nat) (index : Nat) (table : Array Bool) : Option Nat :=
+  if valuesLeft : remaining > 0 then
+    if validIndex : index < table.size then
+      if table[index] then
+        if remaining == 1 then some index
+        else prime' (remaining - 1) (index + 1) (updateTable (index * index) index table)
+      else prime' remaining (index + 1) table
+    else none
+  else none
+
+def prime (n : Nat) : Option Nat :=
+  let logn := n.log2
+  let loglogn := logn.log2
+  let upperBound := n * (logn + loglogn) + 3
+  let firstPrime := 2
+  prime' n firstPrime (Array.replicate upperBound true)
+
+end NthPrime

exercises/practice/nth-prime/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "NthPrime.lean"
+    ],
+    "test": [
+      "NthPrimeTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Given a number n, determine what the nth prime is.",
+  "source": "A variation on Problem 7 at Project Euler",
+  "source_url": "https://projecteuler.net/problem=7"
+}

exercises/practice/nth-prime/.meta/tests.toml

@@ -0,0 +1,25 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[75c65189-8aef-471a-81de-0a90c728160c]
+description = "first prime"
+
+[2c38804c-295f-4701-b728-56dea34fd1a0]
+description = "second prime"
+
+[56692534-781e-4e8c-b1f9-3e82c1640259]
+description = "sixth prime"
+
+[fce1e979-0edb-412d-93aa-2c744e8f50ff]
+description = "big prime"
+
+[bd0a9eae-6df7-485b-a144-80e13c7d55b2]
+description = "there is no zeroth prime"

exercises/practice/nth-prime/NthPrime.lean

@@ -0,0 +1,6 @@
+namespace NthPrime
+
+def prime (n : Nat) : Option Nat :=
+  sorry
+
+end NthPrime

exercises/practice/nth-prime/NthPrimeTest.lean

@@ -0,0 +1,22 @@
+import LeanTest
+import NthPrime
+
+open LeanTest
+
+def nthPrimeTests : TestSuite :=
+  (TestSuite.empty "NthPrime")
+  |>.addTest "first prime" (do
+      return assertEqual (some 2) (NthPrime.prime 1))
+  |>.addTest "second prime" (do
+      return assertEqual (some 3) (NthPrime.prime 2))
+  |>.addTest "sixth prime" (do
+      return assertEqual (some 13) (NthPrime.prime 6))
+  |>.addTest "big prime" (do
+      return assertEqual (some 104743) (NthPrime.prime 10001))
+  |>.addTest "there is no zeroth prime" (do
+      return assertEqual none (NthPrime.prime 0))
+  |>.addTest "very big prime" (do
+      return assertEqual (some 821647) (NthPrime.prime 65537))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [nthPrimeTests]

exercises/practice/nth-prime/lakefile.toml

@@ -0,0 +1,15 @@
+name = "nth-prime"
+version = "0.1.0"
+defaultTargets = ["NthPrimeTest"]
+testDriver = "NthPrimeTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "NthPrime"
+
+[[lean_exe]]
+name = "NthPrimeTest"
+root = "NthPrimeTest"

exercises/practice/nth-prime/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2

exercises/practice/nth-prime/vendor/LeanTest/LeanTest.lean

@@ -0,0 +1,5 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test
+import LeanTest.Basic