Add armstrong-numbers exercise (#54)

Author: keiravillekode

config.json

@@ -73,6 +73,14 @@
         "prerequisites": [],
         "difficulty": 2
       },
+      {
+        "slug": "armstrong-numbers",
+        "name": "Armstrong Numbers",
+        "uuid": "c33aa0db-3c1e-4511-ad3e-0123ab8005a9",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 2
+      },
       {
         "slug": "bob",
         "name": "Bob",

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

@@ -0,0 +1,14 @@
+# Instructions
+
+An [Armstrong number][armstrong-number] is a number that is the sum of its own digits each raised to the power of the number of digits.
+
+For example:
+
+- 9 is an Armstrong number, because `9 = 9^1 = 9`
+- 10 is _not_ an Armstrong number, because `10 != 1^2 + 0^2 = 1`
+- 153 is an Armstrong number, because: `153 = 1^3 + 5^3 + 3^3 = 1 + 125 + 27 = 153`
+- 154 is _not_ an Armstrong number, because: `154 != 1^3 + 5^3 + 4^3 = 1 + 125 + 64 = 190`
+
+Write some code to determine whether a number is an Armstrong number.
+
+[armstrong-number]: https://en.wikipedia.org/wiki/Narcissistic_number

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

@@ -0,0 +1,15 @@
+namespace ArmstrongNumbers
+
+def extractDigits (measure : Nat) (number : Nat) (acc : List Nat) : List Nat :=
+  match measure with
+  | 0 => acc
+  | .succ measure2 =>
+      if number < 10 then number :: acc
+      else extractDigits measure2 (number / 10) ((number % 10) :: acc)
+
+def isArmstrongNumber (number : Nat) : Bool :=
+  let digits := extractDigits number number []
+  let exponent := List.length digits
+  (List.foldl (· + ·) 0 (List.map (Nat.pow · exponent) digits)) == number
+
+end ArmstrongNumbers

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

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "ArmstrongNumbers.lean"
+    ],
+    "test": [
+      "ArmstrongNumbersTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Determine if a number is an Armstrong number.",
+  "source": "Wikipedia",
+  "source_url": "https://en.wikipedia.org/wiki/Narcissistic_number"
+}

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

@@ -0,0 +1,43 @@
+# 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.
+
+[c1ed103c-258d-45b2-be73-d8c6d9580c7b]
+description = "Zero is an Armstrong number"
+
+[579e8f03-9659-4b85-a1a2-d64350f6b17a]
+description = "Single-digit numbers are Armstrong numbers"
+
+[2d6db9dc-5bf8-4976-a90b-b2c2b9feba60]
+description = "There are no two-digit Armstrong numbers"
+
+[509c087f-e327-4113-a7d2-26a4e9d18283]
+description = "Three-digit number that is an Armstrong number"
+
+[7154547d-c2ce-468d-b214-4cb953b870cf]
+description = "Three-digit number that is not an Armstrong number"
+
+[6bac5b7b-42e9-4ecb-a8b0-4832229aa103]
+description = "Four-digit number that is an Armstrong number"
+
+[eed4b331-af80-45b5-a80b-19c9ea444b2e]
+description = "Four-digit number that is not an Armstrong number"
+
+[f971ced7-8d68-4758-aea1-d4194900b864]
+description = "Seven-digit number that is an Armstrong number"
+
+[7ee45d52-5d35-4fbd-b6f1-5c8cd8a67f18]
+description = "Seven-digit number that is not an Armstrong number"
+
+[5ee2fdf8-334e-4a46-bb8d-e5c19c02c148]
+description = "Armstrong number containing seven zeroes"
+
+[12ffbf10-307a-434e-b4ad-c925680e1dd4]
+description = "The largest and last Armstrong number"

exercises/practice/armstrong-numbers/ArmstrongNumbers.lean

@@ -0,0 +1,6 @@
+namespace ArmstrongNumbers
+
+def isArmstrongNumber (number : Nat) : Bool :=
+  sorry
+
+end ArmstrongNumbers

exercises/practice/armstrong-numbers/ArmstrongNumbersTest.lean

@@ -0,0 +1,32 @@
+import LeanTest
+import ArmstrongNumbers
+
+open LeanTest
+
+def armstrongNumbersTests : TestSuite :=
+  (TestSuite.empty "ArmstrongNumbers")
+  |>.addTest "Zero is an Armstrong number" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 0))
+  |>.addTest "Single-digit numbers are Armstrong numbers" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 5))
+  |>.addTest "There are no two-digit Armstrong numbers" (do
+      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 10))
+  |>.addTest "Three-digit number that is an Armstrong number" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 153))
+  |>.addTest "Three-digit number that is not an Armstrong number" (do
+      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 100))
+  |>.addTest "Four-digit number that is an Armstrong number" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 9474))
+  |>.addTest "Four-digit number that is not an Armstrong number" (do
+      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 9475))
+  |>.addTest "Seven-digit number that is an Armstrong number" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 9926315))
+  |>.addTest "Seven-digit number that is not an Armstrong number" (do
+      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 9926314))
+  |>.addTest "Armstrong number containing seven zeroes" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 186709961001538790100634132976990))
+  |>.addTest "The largest and last Armstrong number" (do
+      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 115132219018763992565095597973971522401))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [armstrongNumbersTests]

exercises/practice/armstrong-numbers/lakefile.toml

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

exercises/practice/armstrong-numbers/lean-toolchain

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

exercises/practice/armstrong-numbers/vendor/LeanTest/LeanTest.lean

@@ -0,0 +1,4 @@
+-- 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