Add alphametics exercise

config.json

@@ -722,6 +722,14 @@
         "prerequisites": [],
         "difficulty": 8
       },
+      {
+        "slug": "alphametics",
+        "name": "Alphametics",
+        "uuid": "ac086674-808b-4f36-be70-725174f1caff",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 8
+      },
       {
         "slug": "bank-account",
         "name": "Bank Account",

exercises/practice/alphametics/.docs/instructions.md

@@ -0,0 +1,29 @@
+# Instructions
+
+Given an alphametics puzzle, find the correct solution.
+
+[Alphametics][alphametics] is a puzzle where letters in words are replaced with numbers.
+
+For example `SEND + MORE = MONEY`:
+
+```text
+  S E N D
+  M O R E +
+-----------
+M O N E Y
+```
+
+Replacing these with valid numbers gives:
+
+```text
+  9 5 6 7
+  1 0 8 5 +
+-----------
+1 0 6 5 2
+```
+
+This is correct because every letter is replaced by a different number and the words, translated into numbers, then make a valid sum.
+
+Each letter must represent a different digit, and the leading digit of a multi-digit number must not be zero.
+
+[alphametics]: https://en.wikipedia.org/wiki/Alphametics

exercises/practice/alphametics/.meta/Example.lean

@@ -0,0 +1,82 @@
+namespace Alphametics
+
+private structure Letter where
+  ch : Char
+  leading : Nat
+  rank : Nat
+  weight : Array Int
+
+private def wordSigns (tokens : List String) : List (String × Int) := Id.run do
+  let mut sign : Int := -1
+  let mut result : List (String × Int) := []
+  for tok in tokens do
+    if tok == "==" then
+      sign := 1
+    else if tok != "+" then
+      result := (tok, sign) :: result
+  return result
+
+private def uniqueLetters (puzzle : String) : List Char :=
+  puzzle.toList.filter Char.isAlpha
+    |>.foldl (fun acc c => if acc.contains c then acc else c :: acc) []
+
+private def makeLetter (words : List (String × Int)) (numCols : Nat) (ch : Char) : Letter := Id.run do
+  let mut weight : Array Int := Array.replicate numCols 0
+  let mut leading : Nat := 0
+  for (word, sign) in words do
+    let chars := word.toList.toArray
+    let len := chars.size
+    if len > 1 && chars[0]! == ch then
+      leading := 1
+    for i in [:len] do
+      if chars[len - 1 - i]! == ch then
+        weight := weight.set! i (weight[i]! + sign)
+  let rank :=
+    (List.range numCols).find? (fun col => weight[col]! != 0)
+      |>.getD (numCols - 1)
+  return { ch, leading, rank, weight }
+
+private def columnSum (letters : List Letter) (mapping : List (Char × Nat)) (col : Nat) : Int :=
+  letters.foldl (fun acc l =>
+    acc + l.weight[col]! * (Int.ofNat (mapping.lookup l.ch |>.getD 0))) 0
+
+-- Depth-first search. `remaining` holds letters not yet assigned,
+-- sorted by rank ascending; `col` is the current column (0 = rightmost).
+-- When the next letter's rank exceeds `col`, validate the column sum
+-- (accounting for `carry`) and advance to the next column.
+private partial def search (numCols : Nat) (allLetters : List Letter)
+    (col : Nat) (carry : Int) (remaining : List Letter) (claimed : Nat)
+    (mapping : List (Char × Nat)) : Option (List (Char × Nat)) :=
+  let columnComplete : Bool :=
+    match remaining with
+    | [] => true
+    | entry :: _ => entry.rank > col
+  if columnComplete then
+    let colSum := carry + columnSum allLetters mapping col
+    if colSum % 10 != 0 then
+      none
+    else if col + 1 < numCols then
+      search numCols allLetters (col + 1) (colSum / 10) remaining claimed mapping
+    else if colSum == 0 then
+      some (mapping.mergeSort (fun a b => a.1 ≤ b.1))
+    else
+      none
+  else
+    match remaining with
+    | [] => none
+    | entry :: rest =>
+      ((List.range 10).filter (· ≥ entry.leading)).findSome? (fun digit =>
+        if claimed &&& (1 <<< digit) == 0 then
+          search numCols allLetters col carry rest
+            (claimed ||| (1 <<< digit)) ((entry.ch, digit) :: mapping)
+        else
+          none)
+
+def solve (puzzle : String) : Option (List (Char × Nat)) :=
+  let words := wordSigns ((puzzle.splitOn " ").filter (· != ""))
+  let numCols := (words.map (fun (w, _) => w.length)).foldl max 0
+  let uniq := uniqueLetters puzzle
+  let allLetters := (uniq.map (makeLetter words numCols)).mergeSort (fun a b => a.rank ≤ b.rank)
+  search numCols allLetters 0 0 allLetters 0 []
+
+end Alphametics

exercises/practice/alphametics/.meta/config.json

@@ -0,0 +1,17 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "Alphametics.lean"
+    ],
+    "test": [
+      "AlphameticsTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Given an alphametics puzzle, find the correct solution."
+}

exercises/practice/alphametics/.meta/extra.json

@@ -0,0 +1,20 @@
+[
+  {
+    "description": "puzzle with a colors theme",
+    "property": "solve",
+    "input": {
+      "puzzle": "GREEN + ORANGE == COLORS"
+    },
+    "expected": {
+      "A": 5,
+      "C": 2,
+      "E": 4,
+      "G": 8,
+      "L": 9,
+      "N": 6,
+      "O": 1,
+      "R": 3,
+      "S": 0
+    }
+  }
+]

exercises/practice/alphametics/.meta/tests.toml

@@ -0,0 +1,40 @@
+# 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.
+
+[e0c08b07-9028-4d5f-91e1-d178fead8e1a]
+description = "puzzle with three letters"
+
+[a504ee41-cb92-4ec2-9f11-c37e95ab3f25]
+description = "solution must have unique value for each letter"
+
+[4e3b81d2-be7b-4c5c-9a80-cd72bc6d465a]
+description = "leading zero solution is invalid"
+
+[8a3e3168-d1ee-4df7-94c7-b9c54845ac3a]
+description = "puzzle with two digits final carry"
+
+[a9630645-15bd-48b6-a61e-d85c4021cc09]
+description = "puzzle with four letters"
+
+[3d905a86-5a52-4e4e-bf80-8951535791bd]
+description = "puzzle with six letters"
+
+[4febca56-e7b7-4789-97b9-530d09ba95f0]
+description = "puzzle with seven letters"
+
+[12125a75-7284-4f9a-a5fa-191471e0d44f]
+description = "puzzle with eight letters"
+
+[fb05955f-38dc-477a-a0b6-5ef78969fffa]
+description = "puzzle with ten letters"
+
+[9a101e81-9216-472b-b458-b513a7adacf7]
+description = "puzzle with ten letters and 199 addends"

exercises/practice/alphametics/Alphametics.lean

@@ -0,0 +1,6 @@
+namespace Alphametics
+
+def solve (puzzle : String) : Option (List (Char × Nat)) :=
+  sorry --remove this line and implement the function
+
+end Alphametics

exercises/practice/alphametics/AlphameticsTest.lean

@@ -0,0 +1,43 @@
+import LeanTest
+import Alphametics
+
+open LeanTest
+
+def alphameticsTests : TestSuite :=
+  (TestSuite.empty "Alphametics")
+  |>.addTest "puzzle with three letters" (do
+      return assertEqual (some [('B', 9), ('I', 1), ('L', 0)])
+          (Alphametics.solve "I + BB == ILL"))
+  |>.addTest "solution must have unique value for each letter" (do
+      return assertEqual none
+          (Alphametics.solve "A == B"))
+  |>.addTest "leading zero solution is invalid" (do
+      return assertEqual none
+          (Alphametics.solve "ACA + DD == BD"))
+  |>.addTest "puzzle with two digits final carry" (do
+      return assertEqual (some [('A', 9), ('B', 1), ('C', 0)])
+          (Alphametics.solve "A + A + A + A + A + A + A + A + A + A + A + B == BCC"))
+  |>.addTest "puzzle with four letters" (do
+      return assertEqual (some [('A', 9), ('M', 1), ('O', 0), ('S', 2)])
+          (Alphametics.solve "AS + A == MOM"))
+  |>.addTest "puzzle with six letters" (do
+      return assertEqual (some [('A', 0), ('E', 2), ('L', 1), ('N', 7), ('O', 4), ('T', 9)])
+          (Alphametics.solve "NO + NO + TOO == LATE"))
+  |>.addTest "puzzle with seven letters" (do
+      return assertEqual (some [('E', 4), ('G', 2), ('H', 5), ('I', 0), ('L', 1), ('S', 9), ('T', 7)])
+          (Alphametics.solve "HE + SEES + THE == LIGHT"))
+  |>.addTest "puzzle with eight letters" (do
+      return assertEqual (some [('D', 7), ('E', 5), ('M', 1), ('N', 6), ('O', 0), ('R', 8), ('S', 9), ('Y', 2)])
+          (Alphametics.solve "SEND + MORE == MONEY"))
+  |>.addTest "puzzle with ten letters" (do
+      return assertEqual (some [('A', 5), ('D', 3), ('E', 4), ('F', 7), ('G', 8), ('N', 0), ('O', 2), ('R', 1), ('S', 6), ('T', 9)])
+          (Alphametics.solve "AND + A + STRONG + OFFENSE + AS + A + GOOD == DEFENSE"))
+  |>.addTest "puzzle with ten letters and 199 addends" (do
+      return assertEqual (some [('A', 1), ('E', 0), ('F', 5), ('H', 8), ('I', 7), ('L', 2), ('O', 6), ('R', 3), ('S', 4), ('T', 9)])
+          (Alphametics.solve "THIS + A + FIRE + THEREFORE + FOR + ALL + HISTORIES + I + TELL + A + TALE + THAT + FALSIFIES + ITS + TITLE + TIS + A + LIE + THE + TALE + OF + THE + LAST + FIRE + HORSES + LATE + AFTER + THE + FIRST + FATHERS + FORESEE + THE + HORRORS + THE + LAST + FREE + TROLL + TERRIFIES + THE + HORSES + OF + FIRE + THE + TROLL + RESTS + AT + THE + HOLE + OF + LOSSES + IT + IS + THERE + THAT + SHE + STORES + ROLES + OF + LEATHERS + AFTER + SHE + SATISFIES + HER + HATE + OFF + THOSE + FEARS + A + TASTE + RISES + AS + SHE + HEARS + THE + LEAST + FAR + HORSE + THOSE + FAST + HORSES + THAT + FIRST + HEAR + THE + TROLL + FLEE + OFF + TO + THE + FOREST + THE + HORSES + THAT + ALERTS + RAISE + THE + STARES + OF + THE + OTHERS + AS + THE + TROLL + ASSAILS + AT + THE + TOTAL + SHIFT + HER + TEETH + TEAR + HOOF + OFF + TORSO + AS + THE + LAST + HORSE + FORFEITS + ITS + LIFE + THE + FIRST + FATHERS + HEAR + OF + THE + HORRORS + THEIR + FEARS + THAT + THE + FIRES + FOR + THEIR + FEASTS + ARREST + AS + THE + FIRST + FATHERS + RESETTLE + THE + LAST + OF + THE + FIRE + HORSES + THE + LAST + TROLL + HARASSES + THE + FOREST + HEART + FREE + AT + LAST + OF + THE + LAST + TROLL + ALL + OFFER + THEIR + FIRE + HEAT + TO + THE + ASSISTERS + FAR + OFF + THE + TROLL + FASTS + ITS + LIFE + SHORTER + AS + STARS + RISE + THE + HORSES + REST + SAFE + AFTER + ALL + SHARE + HOT + FISH + AS + THEIR + AFFILIATES + TAILOR + A + ROOFS + FOR + THEIR + SAFE == FORTRESSES"))
+  |>.addTest "puzzle with a colors theme" (do
+      return assertEqual (some [('A', 5), ('C', 2), ('E', 4), ('G', 8), ('L', 9), ('N', 6), ('O', 1), ('R', 3), ('S', 0)])
+          (Alphametics.solve "GREEN + ORANGE == COLORS"))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [alphameticsTests]

exercises/practice/alphametics/lakefile.toml

@@ -0,0 +1,15 @@
+name = "alphametics"
+version = "0.1.0"
+defaultTargets = ["AlphameticsTest"]
+testDriver = "AlphameticsTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Alphametics"
+
+[[lean_exe]]
+name = "AlphameticsTest"
+root = "AlphameticsTest"

exercises/practice/alphametics/lean-toolchain

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

exercises/practice/alphametics/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