Add perfect numbers (#55)

Author: oxe-i

config.json

@@ -289,6 +289,14 @@
         "prerequisites": [],
         "difficulty": 4
       },
+      {
+        "slug": "perfect-numbers",
+        "name": "Perfect Numbers",
+        "uuid": "1e2d1960-e71d-48b7-8e65-cc9498daa713",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 4
+      },
       {
         "slug": "prime-factors",
         "name": "Prime Factors",

exercises/practice/perfect-numbers/.docs/instructions.append.md

@@ -0,0 +1,32 @@
+# Instructions append
+
+## Defining an inductive type
+
+This exercise expects the return value to be an [inductive type][inductive] `Classification` that you must define.
+
+This type must have a [BEq][beq] instance, i.e., it admits a Boolean equality test, and a [Repr][repr] instance, i.e., values of the type can be formatted for display.
+
+You can refer to [this page][instance] on instance declarations.
+Lean can automatically [generate instances][deriving] for many classes.
+
+## Subtypes
+
+The argument to the `classify` function is a [subtype][subtype] called `Positive`: 
+
+```
+def Positive := { x : Nat // x > 0 }
+```
+
+Subtypes represent elements of a particular type that satisfy a predicate.
+`Positive` represents elements of `Nat` that are greater than `0`.
+
+Any element of a subtype can be thought of as a pair consisting of a value of the underlying type and a proof, in the mathematical sense, that this value satisfies the corresponding predicate.
+
+Subtypes enforce invariants at the type level,ensuring that ill-formed values cannot be constructed.
+
+[inductive]: https://lean-lang.org/functional_programming_in_lean/Getting-to-Know-Lean/Datatypes-and-Patterns/#datatypes-and-patterns
+[beq]: https://lean-lang.org/doc/reference/latest/Type-Classes/Basic-Classes/#BEq___mk
+[repr]: https://lean-lang.org/doc/reference/4.26.0/Interacting-with-Lean/?terms=Repr#repr
+[instance]: https://lean-lang.org/doc/reference/latest/Type-Classes/Deriving-Instances/#deriving-instances
+[deriving]: https://lean-lang.org/doc/reference/latest/Type-Classes/Deriving-Instances/#deriving-instances
+[subtype]: https://lean-lang.org/doc/reference/latest/Basic-Types/Subtypes/#Subtype___mk

exercises/practice/perfect-numbers/.docs/instructions.md

@@ -0,0 +1,39 @@
+# Instructions
+
+Determine if a number is perfect, abundant, or deficient based on Nicomachus' (60 - 120 CE) classification scheme for positive integers.
+
+The Greek mathematician [Nicomachus][nicomachus] devised a classification scheme for positive integers, identifying each as belonging uniquely to the categories of [perfect](#perfect), [abundant](#abundant), or [deficient](#deficient) based on their [aliquot sum][aliquot-sum].
+The _aliquot sum_ is defined as the sum of the factors of a number not including the number itself.
+For example, the aliquot sum of `15` is `1 + 3 + 5 = 9`.
+
+## Perfect
+
+A number is perfect when it equals its aliquot sum.
+For example:
+
+- `6` is a perfect number because `1 + 2 + 3 = 6`
+- `28` is a perfect number because `1 + 2 + 4 + 7 + 14 = 28`
+
+## Abundant
+
+A number is abundant when it is less than its aliquot sum.
+For example:
+
+- `12` is an abundant number because `1 + 2 + 3 + 4 + 6 = 16`
+- `24` is an abundant number because `1 + 2 + 3 + 4 + 6 + 8 + 12 = 36`
+
+## Deficient
+
+A number is deficient when it is greater than its aliquot sum.
+For example:
+
+- `8` is a deficient number because `1 + 2 + 4 = 7`
+- Prime numbers are deficient
+
+## Task
+
+Implement a way to determine whether a given number is [perfect](#perfect).
+Depending on your language track, you may also need to implement a way to determine whether a given number is [abundant](#abundant) or [deficient](#deficient).
+
+[nicomachus]: https://en.wikipedia.org/wiki/Nicomachus
+[aliquot-sum]: https://en.wikipedia.org/wiki/Aliquot_sum

exercises/practice/perfect-numbers/.meta/Example.lean

@@ -0,0 +1,27 @@
+namespace PerfectNumbers
+
+def Positive := { x : Nat // x > 0 }
+
+inductive Classification where
+  | abundant  : Classification
+  | perfect   : Classification
+  | deficient : Classification
+  deriving BEq, Repr
+
+def getFactors (number : Nat) (factor : Nat) (acc : List Nat) : List Nat :=
+  if factor < number then
+    if number % factor == 0 then
+      getFactors number (factor + 1) (factor :: acc)
+    else
+      getFactors number (factor + 1) acc
+  else acc
+
+def classify (number : Positive) : Classification :=
+  let factors := getFactors number.val 1 []
+  let sum := factors.foldl (· + ·) 0
+  match compare sum number.val with
+  | .lt => .deficient
+  | .gt => .abundant
+  | .eq => .perfect
+
+end PerfectNumbers

exercises/practice/perfect-numbers/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "PerfectNumbers.lean"
+    ],
+    "test": [
+      "PerfectNumbersTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Determine if a number is perfect, abundant, or deficient based on Nicomachus' (60 - 120 CE) classification scheme for positive integers.",
+  "source": "Taken from Chapter 2 of Functional Thinking by Neal Ford.",
+  "source_url": "https://www.oreilly.com/library/view/functional-thinking/9781449365509/"
+}

exercises/practice/perfect-numbers/.meta/tests.toml

@@ -0,0 +1,51 @@
+# 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.
+
+[163e8e86-7bfd-4ee2-bd68-d083dc3381a3]
+description = "Perfect numbers -> Smallest perfect number is classified correctly"
+
+[169a7854-0431-4ae0-9815-c3b6d967436d]
+description = "Perfect numbers -> Medium perfect number is classified correctly"
+
+[ee3627c4-7b36-4245-ba7c-8727d585f402]
+description = "Perfect numbers -> Large perfect number is classified correctly"
+
+[80ef7cf8-9ea8-49b9-8b2d-d9cb3db3ed7e]
+description = "Abundant numbers -> Smallest abundant number is classified correctly"
+
+[3e300e0d-1a12-4f11-8c48-d1027165ab60]
+description = "Abundant numbers -> Medium abundant number is classified correctly"
+
+[ec7792e6-8786-449c-b005-ce6dd89a772b]
+description = "Abundant numbers -> Large abundant number is classified correctly"
+
+[e610fdc7-2b6e-43c3-a51c-b70fb37413ba]
+description = "Deficient numbers -> Smallest prime deficient number is classified correctly"
+
+[0beb7f66-753a-443f-8075-ad7fbd9018f3]
+description = "Deficient numbers -> Smallest non-prime deficient number is classified correctly"
+
+[1c802e45-b4c6-4962-93d7-1cad245821ef]
+description = "Deficient numbers -> Medium deficient number is classified correctly"
+
+[47dd569f-9e5a-4a11-9a47-a4e91c8c28aa]
+description = "Deficient numbers -> Large deficient number is classified correctly"
+
+[a696dec8-6147-4d68-afad-d38de5476a56]
+description = "Deficient numbers -> Edge case (no factors other than itself) is classified correctly"
+
+[72445cee-660c-4d75-8506-6c40089dc302]
+description = "Invalid inputs -> Zero is rejected (as it is not a positive integer)"
+include = false
+
+[2d72ce2c-6802-49ac-8ece-c790ba3dae13]
+description = "Invalid inputs -> Negative integer is rejected (as it is not a positive integer)"
+include = false

exercises/practice/perfect-numbers/PerfectNumbers.lean

@@ -0,0 +1,12 @@
+namespace PerfectNumbers
+
+def Positive := { x : Nat // x > 0 }
+
+/-
+  You should define Classification here
+-/
+
+def classify (number : Positive) : Classification :=
+  sorry
+
+end PerfectNumbers

exercises/practice/perfect-numbers/PerfectNumbersTest.lean

@@ -0,0 +1,32 @@
+import LeanTest
+import PerfectNumbers
+
+open LeanTest
+
+def perfectNumbersTests : TestSuite :=
+  (TestSuite.empty "PerfectNumbers")
+  |>.addTest "Perfect numbers -> Smallest perfect number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.perfect (PerfectNumbers.classify ⟨6, (by decide)⟩))
+  |>.addTest "Perfect numbers -> Medium perfect number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.perfect (PerfectNumbers.classify ⟨28, (by decide)⟩))
+  |>.addTest "Perfect numbers -> Large perfect number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.perfect (PerfectNumbers.classify ⟨33550336, (by decide)⟩))
+  |>.addTest "Abundant numbers -> Smallest abundant number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.abundant (PerfectNumbers.classify ⟨12, (by decide)⟩))
+  |>.addTest "Abundant numbers -> Medium abundant number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.abundant (PerfectNumbers.classify ⟨30, (by decide)⟩))
+  |>.addTest "Abundant numbers -> Large abundant number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.abundant (PerfectNumbers.classify ⟨33550335, (by decide)⟩))
+  |>.addTest "Deficient numbers -> Smallest prime deficient number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.deficient (PerfectNumbers.classify ⟨2, (by decide)⟩))
+  |>.addTest "Deficient numbers -> Smallest non-prime deficient number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.deficient (PerfectNumbers.classify ⟨4, (by decide)⟩))
+  |>.addTest "Deficient numbers -> Medium deficient number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.deficient (PerfectNumbers.classify ⟨32, (by decide)⟩))
+  |>.addTest "Deficient numbers -> Large deficient number is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.deficient (PerfectNumbers.classify ⟨33550337, (by decide)⟩))
+  |>.addTest "Deficient numbers -> Edge case (no factors other than itself) is classified correctly" (do
+      return assertEqual PerfectNumbers.Classification.deficient (PerfectNumbers.classify ⟨1, (by decide)⟩))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [perfectNumbersTests]

exercises/practice/perfect-numbers/lakefile.toml

@@ -0,0 +1,15 @@
+name = "perfect-numbers"
+version = "0.1.0"
+defaultTargets = ["PerfectNumbersTest"]
+testDriver = "PerfectNumbersTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "PerfectNumbers"
+
+[[lean_exe]]
+name = "PerfectNumbersTest"
+root = "PerfectNumbersTest"

exercises/practice/perfect-numbers/lean-toolchain

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