add all-your-base exercise

config.json

@@ -336,6 +336,14 @@
         "practices": [],
         "prerequisites": [],
         "difficulty": 7
+      },
+      {
+        "slug": "all-your-base",
+        "name": "All Your Base",
+        "uuid": "da51714a-5399-40ed-9fd7-787cb1bcb925",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 8
       }
     ]
   },

exercises/practice/all-your-base/.docs/instructions.md

@@ -0,0 +1,28 @@
+# Instructions
+
+Convert a sequence of digits in one base, representing a number, into a sequence of digits in another base, representing the same number.
+
+~~~~exercism/note
+Try to implement the conversion yourself.
+Do not use something else to perform the conversion for you.
+~~~~
+
+## About [Positional Notation][positional-notation]
+
+In positional notation, a number in base **b** can be understood as a linear combination of powers of **b**.
+
+The number 42, _in base 10_, means:
+
+`(4 × 10¹) + (2 × 10⁰)`
+
+The number 101010, _in base 2_, means:
+
+`(1 × 2⁵) + (0 × 2⁴) + (1 × 2³) + (0 × 2²) + (1 × 2¹) + (0 × 2⁰)`
+
+The number 1120, _in base 3_, means:
+
+`(1 × 3³) + (1 × 3²) + (2 × 3¹) + (0 × 3⁰)`
+
+_Yes. Those three numbers above are exactly the same. Congratulations!_
+
+[positional-notation]: https://en.wikipedia.org/wiki/Positional_notation

exercises/practice/all-your-base/.docs/introduction.md

@@ -0,0 +1,8 @@
+# Introduction
+
+You've just been hired as professor of mathematics.
+Your first week went well, but something is off in your second week.
+The problem is that every answer given by your students is wrong!
+Luckily, your math skills have allowed you to identify the problem: the student answers _are_ correct, but they're all in base 2 (binary)!
+Amazingly, it turns out that each week, the students use a different base.
+To help you quickly verify the student answers, you'll be building a tool to translate between bases.

exercises/practice/all-your-base/.meta/Example.lean

@@ -0,0 +1,36 @@
+namespace AllYourBase
+
+def ValidBase := { x : Nat // x >= 2 }
+
+def rebase (inputBase : ValidBase) (digits : List (Fin inputBase.val)) (outputBase : ValidBase) : List (Fin outputBase.val) := Id.run do
+  /-
+    Nat.lt_of_lt_of_le = n < m -> m <= k -> n < k
+    decide proves that 0 < 2 (0 is n and 2 is m in the theorem)
+    outputBase.property = outputBase.val >= 2 (outputBase.val is k in the theorem)
+    so: 0 < 2 -> 2 <= outputBase.val -> 0 < outputBase.val
+  -/
+  have hpos : 0 < outputBase.val :=
+    Nat.lt_of_lt_of_le (by decide : 0 < 2) outputBase.property
+  let mut base10 :=
+    digits.reverse.mapIdx (inputBase.val ^ · * ·.val)
+    |> (List.foldl (· + ·) 0 .)
+  match base10 with
+  | 0 => return [⟨0, hpos⟩] /- have already proved that 0 < outputBase.val, so 0 "fits" in Fin outputBase.val -/
+  | _ =>
+    let mut result : List (Fin outputBase.val) := []
+    while base10 > 0 do
+      let digit := base10 % outputBase.val
+      /-
+        Nat.mod_lt = x, y ∈ Nat -> 0 < y -> x % y < y
+        digit = base10 % outputBase.val
+        base10, outputBase.val ∈ Nat
+        so, to prove that digit < outputBase.val, we can prove that 0 < outputBase.val
+        which was already proved by hpos
+      -/
+      have hmod : digit < outputBase.val :=
+        Nat.mod_lt base10 hpos
+      result := ⟨digit, hmod⟩ :: result /- hmod proves that digit < outputBase.val, so digit "fits" in Fin outputBase.val -/
+      base10 := base10 / outputBase.val
+    return result
+
+end AllYourBase

exercises/practice/all-your-base/.meta/config.json

@@ -0,0 +1,17 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "AllYourBase.lean"
+    ],
+    "test": [
+      "AllYourBaseTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Convert a number, represented as a sequence of digits in one base, to any other base."
+}

exercises/practice/all-your-base/.meta/tests.toml

@@ -0,0 +1,82 @@
+# 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.
+
+[5ce422f9-7a4b-4f44-ad29-49c67cb32d2c]
+description = "single bit one to decimal"
+
+[0cc3fea8-bb79-46ac-a2ab-5a2c93051033]
+description = "binary to single decimal"
+
+[f12db0f9-0d3d-42c2-b3ba-e38cb375a2b8]
+description = "single decimal to binary"
+
+[2c45cf54-6da3-4748-9733-5a3c765d925b]
+description = "binary to multiple decimal"
+
+[65ddb8b4-8899-4fcc-8618-181b2cf0002d]
+description = "decimal to binary"
+
+[8d418419-02a7-4824-8b7a-352d33c6987e]
+description = "trinary to hexadecimal"
+
+[d3901c80-8190-41b9-bd86-38d988efa956]
+description = "hexadecimal to trinary"
+
+[5d42f85e-21ad-41bd-b9be-a3e8e4258bbf]
+description = "15-bit integer"
+
+[d68788f7-66dd-43f8-a543-f15b6d233f83]
+description = "empty list"
+
+[5e27e8da-5862-4c5f-b2a9-26c0382b6be7]
+description = "single zero"
+
+[2e1c2573-77e4-4b9c-8517-6c56c5bcfdf2]
+description = "multiple zeros"
+
+[3530cd9f-8d6d-43f5-bc6e-b30b1db9629b]
+description = "leading zeros"
+
+[a6b476a1-1901-4f2a-92c4-4d91917ae023]
+description = "input base is one"
+include = false
+
+[e21a693a-7a69-450b-b393-27415c26a016]
+description = "input base is zero"
+include = false
+
+[54a23be5-d99e-41cc-88e0-a650ffe5fcc2]
+description = "input base is negative"
+include = false
+
+[9eccf60c-dcc9-407b-95d8-c37b8be56bb6]
+description = "negative digit"
+include = false
+
+[232fa4a5-e761-4939-ba0c-ed046cd0676a]
+description = "invalid positive digit"
+include = false
+
+[14238f95-45da-41dc-95ce-18f860b30ad3]
+description = "output base is one"
+include = false
+
+[73dac367-da5c-4a37-95fe-c87fad0a4047]
+description = "output base is zero"
+include = false
+
+[13f81f42-ff53-4e24-89d9-37603a48ebd9]
+description = "output base is negative"
+include = false
+
+[0e6c895d-8a5d-4868-a345-309d094cfe8d]
+description = "both bases are negative"
+include = false

exercises/practice/all-your-base/AllYourBase.lean

@@ -0,0 +1,8 @@
+namespace AllYourBase
+
+def ValidBase := { x : Nat // x >= 2 }
+
+def rebase (inputBase : ValidBase) (digits : List (Fin inputBase.val)) (outputBase : ValidBase) : List (Fin outputBase.val) :=
+  sorry
+
+end AllYourBase

exercises/practice/all-your-base/AllYourBaseTest.lean

@@ -0,0 +1,34 @@
+import LeanTest
+import AllYourBase
+
+open LeanTest
+
+def allYourBaseTests : TestSuite :=
+  (TestSuite.empty "AllYourBase")
+  |>.addTest "single bit one to decimal" (do
+      return assertEqual [1] (AllYourBase.rebase ⟨2, (by decide)⟩ [1] ⟨10, (by decide)⟩))
+  |>.addTest "binary to single decimal" (do
+      return assertEqual [5] (AllYourBase.rebase ⟨2, (by decide)⟩ [1, 0, 1] ⟨10, (by decide)⟩))
+  |>.addTest "single decimal to binary" (do
+      return assertEqual [1, 0, 1] (AllYourBase.rebase ⟨10, (by decide)⟩ [5] ⟨2, (by decide)⟩))
+  |>.addTest "binary to multiple decimal" (do
+      return assertEqual [4, 2] (AllYourBase.rebase ⟨2, (by decide)⟩ [1, 0, 1, 0, 1, 0] ⟨10, (by decide)⟩))
+  |>.addTest "decimal to binary" (do
+      return assertEqual [1, 0, 1, 0, 1, 0] (AllYourBase.rebase ⟨10, (by decide)⟩ [4, 2] ⟨2, (by decide)⟩))
+  |>.addTest "trinary to hexadecimal" (do
+      return assertEqual [2, 10] (AllYourBase.rebase ⟨3, (by decide)⟩ [1, 1, 2, 0] ⟨16, (by decide)⟩))
+  |>.addTest "hexadecimal to trinary" (do
+      return assertEqual [1, 1, 2, 0] (AllYourBase.rebase ⟨16, (by decide)⟩ [2, 10] ⟨3, (by decide)⟩))
+  |>.addTest "15-bit integer" (do
+      return assertEqual [6, 10, 45] (AllYourBase.rebase ⟨97, (by decide)⟩ [3, 46, 60] ⟨73, (by decide)⟩))
+  |>.addTest "empty list" (do
+      return assertEqual [0] (AllYourBase.rebase ⟨2, (by decide)⟩ [] ⟨10, (by decide)⟩))
+  |>.addTest "single zero" (do
+      return assertEqual [0] (AllYourBase.rebase ⟨10, (by decide)⟩ [0] ⟨2, (by decide)⟩))
+  |>.addTest "multiple zeros" (do
+      return assertEqual [0] (AllYourBase.rebase ⟨10, (by decide)⟩ [0, 0, 0] ⟨2, (by decide)⟩))
+  |>.addTest "leading zeros" (do
+      return assertEqual [4, 2] (AllYourBase.rebase ⟨7, (by decide)⟩ [0, 6, 0] ⟨10, (by decide)⟩))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [allYourBaseTests]

exercises/practice/all-your-base/lakefile.toml

@@ -0,0 +1,15 @@
+name = "all-your-base"
+version = "0.1.0"
+defaultTargets = ["AllYourBaseTest"]
+testDriver = "AllYourBaseTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "AllYourBase"
+
+[[lean_exe]]
+name = "AllYourBaseTest"
+root = "AllYourBaseTest"

exercises/practice/all-your-base/lean-toolchain

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

exercises/practice/all-your-base/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