Add yacht exercise

config.json

@@ -409,6 +409,14 @@
         "prerequisites": [],
         "difficulty": 5
       },
+      {
+        "slug": "yacht",
+        "name": "Yacht",
+        "uuid": "ffc5678e-12da-4a69-996d-93ab1ede6dbc",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 5
+      },
       {
         "slug": "affine-cipher",
         "name": "Affine Cipher",

exercises/practice/yacht/.docs/instructions.md

@@ -0,0 +1,30 @@
+# Instructions
+
+Given five dice and a category, calculate the score of the dice for that category.
+
+~~~~exercism/note
+You'll always be presented with five dice.
+Each dice's value will be between one and six inclusively.
+The dice may be unordered.
+~~~~
+
+## Scores in Yacht
+
+| Category        | Score                  | Description                              | Example             |
+| --------------- | ---------------------- | ---------------------------------------- | ------------------- |
+| Ones            | 1 × number of ones     | Any combination                          | 1 1 1 4 5 scores 3  |
+| Twos            | 2 × number of twos     | Any combination                          | 2 2 3 4 5 scores 4  |
+| Threes          | 3 × number of threes   | Any combination                          | 3 3 3 3 3 scores 15 |
+| Fours           | 4 × number of fours    | Any combination                          | 1 2 3 3 5 scores 0  |
+| Fives           | 5 × number of fives    | Any combination                          | 5 1 5 2 5 scores 15 |
+| Sixes           | 6 × number of sixes    | Any combination                          | 2 3 4 5 6 scores 6  |
+| Full House      | Total of the dice      | Three of one number and two of another   | 3 3 3 5 5 scores 19 |
+| Four of a Kind  | Total of the four dice | At least four dice showing the same face | 4 4 4 4 6 scores 16 |
+| Little Straight | 30 points              | 1-2-3-4-5                                | 1 2 3 4 5 scores 30 |
+| Big Straight    | 30 points              | 2-3-4-5-6                                | 2 3 4 5 6 scores 30 |
+| Choice          | Sum of the dice        | Any combination                          | 2 3 3 4 6 scores 18 |
+| Yacht           | 50 points              | All five dice showing the same face      | 4 4 4 4 4 scores 50 |
+
+If the dice do **not** satisfy the requirements of a category, the score is zero.
+If, for example, _Four Of A Kind_ is entered in the _Yacht_ category, zero points are scored.
+A _Yacht_ scores zero if entered in the _Full House_ category.

exercises/practice/yacht/.docs/introduction.md

@@ -0,0 +1,11 @@
+# Introduction
+
+Each year, something new is "all the rage" in your high school.
+This year it is a dice game: [Yacht][yacht].
+
+The game of Yacht is from the same family as Poker Dice, Generala and particularly Yahtzee, of which it is a precursor.
+The game consists of twelve rounds.
+In each, five dice are rolled and the player chooses one of twelve categories.
+The chosen category is then used to score the throw of the dice.
+
+[yacht]: https://en.wikipedia.org/wiki/Yacht_(dice_game)

exercises/practice/yacht/.meta/Example.lean

@@ -0,0 +1,36 @@
+namespace Yacht
+
+inductive Category where
+  | ones | twos | threes | fours | fives | sixes
+  | choice | fourOfAKind | fullHouse | yacht
+  | littleStraight | bigStraight
+  deriving BEq, Repr
+
+abbrev Die   := { x : Nat // 1 ≤ x ∧ x ≤ 6 }
+abbrev Throw := Vector Die 5
+
+def sortedDice : Throw -> List Nat :=
+  List.mergeSort ∘ List.map (λ (d : Die) => d.val) ∘ Vector.toList -- composition is like in Haskell, right to left
+
+def score (dice : Throw) : Category -> Nat
+  | .ones           => 1 * dice.count ⟨1, by decide⟩
+  | .twos           => 2 * dice.count ⟨2, by decide⟩
+  | .threes         => 3 * dice.count ⟨3, by decide⟩
+  | .fours          => 4 * dice.count ⟨4, by decide⟩
+  | .fives          => 5 * dice.count ⟨5, by decide⟩
+  | .sixes          => 6 * dice.count ⟨6, by decide⟩
+  | .yacht          => if dice.all (λ x => dice[0] == x) then 50 else 0
+  | .choice         => dice.foldl (λ acc ⟨d, _⟩ => acc + d) 0
+  | .littleStraight => if sortedDice dice == [1, 2, 3, 4, 5] then 30 else 0
+  | .bigStraight    => if sortedDice dice == [2, 3, 4, 5, 6] then 30 else 0
+  | .fourOfAKind    => (do
+      let ⟨d, _⟩ ← dice.find? (λ x => dice.count x >= 4)
+      some (4 * d)
+    ).getD 0
+  | .fullHouse      => (do
+      let ⟨d1, _⟩ ← dice.find? (λ x => dice.count x == 3)
+      let ⟨d2, _⟩ ← dice.find? (λ x => dice.count x == 2)
+      some (3 * d1 + 2 * d2)
+    ).getD 0
+
+end Yacht

exercises/practice/yacht/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "Yacht.lean"
+    ],
+    "test": [
+      "YachtTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Score a single throw of dice in the game Yacht.",
+  "source": "James Kilfiger, using Wikipedia",
+  "source_url": "https://en.wikipedia.org/wiki/Yacht_(dice_game)"
+}

exercises/practice/yacht/.meta/tests.toml

@@ -0,0 +1,97 @@
+# 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.
+
+[3060e4a5-4063-4deb-a380-a630b43a84b6]
+description = "Yacht"
+
+[15026df2-f567-482f-b4d5-5297d57769d9]
+description = "Not Yacht"
+
+[36b6af0c-ca06-4666-97de-5d31213957a4]
+description = "Ones"
+
+[023a07c8-6c6e-44d0-bc17-efc5e1b8205a]
+description = "Ones, out of order"
+
+[7189afac-cccd-4a74-8182-1cb1f374e496]
+description = "No ones"
+
+[793c4292-dd14-49c4-9707-6d9c56cee725]
+description = "Twos"
+
+[dc41bceb-d0c5-4634-a734-c01b4233a0c6]
+description = "Fours"
+
+[f6125417-5c8a-4bca-bc5b-b4b76d0d28c8]
+description = "Yacht counted as threes"
+
+[464fc809-96ed-46e4-acb8-d44e302e9726]
+description = "Yacht of 3s counted as fives"
+
+[d054227f-3a71-4565-a684-5c7e621ec1e9]
+description = "Fives"
+
+[e8a036e0-9d21-443a-8b5f-e15a9e19a761]
+description = "Sixes"
+
+[51cb26db-6b24-49af-a9ff-12f53b252eea]
+description = "Full house two small, three big"
+
+[1822ca9d-f235-4447-b430-2e8cfc448f0c]
+description = "Full house three small, two big"
+
+[b208a3fc-db2e-4363-a936-9e9a71e69c07]
+description = "Two pair is not a full house"
+
+[b90209c3-5956-445b-8a0b-0ac8b906b1c2]
+description = "Four of a kind is not a full house"
+
+[32a3f4ee-9142-4edf-ba70-6c0f96eb4b0c]
+description = "Yacht is not a full house"
+
+[b286084d-0568-4460-844a-ba79d71d79c6]
+description = "Four of a Kind"
+
+[f25c0c90-5397-4732-9779-b1e9b5f612ca]
+description = "Yacht can be scored as Four of a Kind"
+
+[9f8ef4f0-72bb-401a-a871-cbad39c9cb08]
+description = "Full house is not Four of a Kind"
+
+[b4743c82-1eb8-4a65-98f7-33ad126905cd]
+description = "Little Straight"
+
+[7ac08422-41bf-459c-8187-a38a12d080bc]
+description = "Little Straight as Big Straight"
+
+[97bde8f7-9058-43ea-9de7-0bc3ed6d3002]
+description = "Four in order but not a little straight"
+
+[cef35ff9-9c5e-4fd2-ae95-6e4af5e95a99]
+description = "No pairs but not a little straight"
+
+[fd785ad2-c060-4e45-81c6-ea2bbb781b9d]
+description = "Minimum is 1, maximum is 5, but not a little straight"
+
+[35bd74a6-5cf6-431a-97a3-4f713663f467]
+description = "Big Straight"
+
+[87c67e1e-3e87-4f3a-a9b1-62927822b250]
+description = "Big Straight as little straight"
+
+[c1fa0a3a-40ba-4153-a42d-32bc34d2521e]
+description = "No pairs but not a big straight"
+
+[207e7300-5d10-43e5-afdd-213e3ac8827d]
+description = "Choice"
+
+[b524c0cf-32d2-4b40-8fb3-be3500f3f135]
+description = "Yacht as choice"

exercises/practice/yacht/Yacht.lean

@@ -0,0 +1,15 @@
+namespace Yacht
+
+inductive Category where
+  | ones | twos | threes | fours | fives | sixes
+  | choice | fourOfAKind | fullHouse | yacht
+  | littleStraight | bigStraight
+  deriving BEq, Repr
+
+abbrev Die   := { x : Nat // 1 ≤ x ∧ x ≤ 6 }
+abbrev Throw := Vector Die 5
+
+def score (dice : Throw) (category: Category) : Nat :=
+  sorry
+
+end Yacht

exercises/practice/yacht/YachtTest.lean

@@ -0,0 +1,68 @@
+import LeanTest
+import Yacht
+
+open LeanTest
+
+def yachtTests : TestSuite :=
+  (TestSuite.empty "Yacht")
+  |>.addTest "Yacht" (do
+      return assertEqual 50 (Yacht.score ⟨#[⟨5, by decide⟩, ⟨5, by decide⟩, ⟨5, by decide⟩, ⟨5, by decide⟩, ⟨5, by decide⟩], by decide⟩ .yacht))
+  |>.addTest "Not Yacht" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨2, by decide⟩, ⟨5, by decide⟩], by decide⟩ .yacht))
+  |>.addTest "Ones" (do
+      return assertEqual 3 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨1, by decide⟩, ⟨1, by decide⟩, ⟨3, by decide⟩, ⟨5, by decide⟩], by decide⟩ .ones))
+  |>.addTest "Ones, out of order" (do
+      return assertEqual 3 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨1, by decide⟩, ⟨1, by decide⟩, ⟨5, by decide⟩, ⟨1, by decide⟩], by decide⟩ .ones))
+  |>.addTest "No ones" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨4, by decide⟩, ⟨3, by decide⟩, ⟨6, by decide⟩, ⟨5, by decide⟩, ⟨5, by decide⟩], by decide⟩ .ones))
+  |>.addTest "Twos" (do
+      return assertEqual 2 (Yacht.score ⟨#[⟨2, by decide⟩, ⟨3, by decide⟩, ⟨4, by decide⟩, ⟨5, by decide⟩, ⟨6, by decide⟩], by decide⟩ .twos))
+  |>.addTest "Fours" (do
+      return assertEqual 8 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨4, by decide⟩, ⟨1, by decide⟩, ⟨4, by decide⟩, ⟨1, by decide⟩], by decide⟩ .fours))
+  |>.addTest "Yacht counted as threes" (do
+      return assertEqual 15 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩], by decide⟩ .threes))
+  |>.addTest "Yacht of 3s counted as fives" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩], by decide⟩ .fives))
+  |>.addTest "Fives" (do
+      return assertEqual 10 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨5, by decide⟩, ⟨3, by decide⟩, ⟨5, by decide⟩, ⟨3, by decide⟩], by decide⟩ .fives))
+  |>.addTest "Sixes" (do
+      return assertEqual 6 (Yacht.score ⟨#[⟨2, by decide⟩, ⟨3, by decide⟩, ⟨4, by decide⟩, ⟨5, by decide⟩, ⟨6, by decide⟩], by decide⟩ .sixes))
+  |>.addTest "Full house two small, three big" (do
+      return assertEqual 16 (Yacht.score ⟨#[⟨2, by decide⟩, ⟨2, by decide⟩, ⟨4, by decide⟩, ⟨4, by decide⟩, ⟨4, by decide⟩], by decide⟩ .fullHouse))
+  |>.addTest "Full house three small, two big" (do
+      return assertEqual 19 (Yacht.score ⟨#[⟨5, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨5, by decide⟩, ⟨3, by decide⟩], by decide⟩ .fullHouse))
+  |>.addTest "Two pair is not a full house" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨2, by decide⟩, ⟨2, by decide⟩, ⟨4, by decide⟩, ⟨4, by decide⟩, ⟨5, by decide⟩], by decide⟩ .fullHouse))
+  |>.addTest "Four of a kind is not a full house" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨4, by decide⟩, ⟨4, by decide⟩, ⟨4, by decide⟩, ⟨4, by decide⟩], by decide⟩ .fullHouse))
+  |>.addTest "Yacht is not a full house" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨2, by decide⟩, ⟨2, by decide⟩, ⟨2, by decide⟩, ⟨2, by decide⟩, ⟨2, by decide⟩], by decide⟩ .fullHouse))
+  |>.addTest "Four of a Kind" (do
+      return assertEqual 24 (Yacht.score ⟨#[⟨6, by decide⟩, ⟨6, by decide⟩, ⟨4, by decide⟩, ⟨6, by decide⟩, ⟨6, by decide⟩], by decide⟩ .fourOfAKind))
+  |>.addTest "Yacht can be scored as Four of a Kind" (do
+      return assertEqual 12 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩], by decide⟩ .fourOfAKind))
+  |>.addTest "Full house is not Four of a Kind" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨3, by decide⟩, ⟨3, by decide⟩, ⟨5, by decide⟩, ⟨5, by decide⟩], by decide⟩ .fourOfAKind))
+  |>.addTest "Little Straight" (do
+      return assertEqual 30 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨5, by decide⟩, ⟨4, by decide⟩, ⟨1, by decide⟩, ⟨2, by decide⟩], by decide⟩ .littleStraight))
+  |>.addTest "Little Straight as Big Straight" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨2, by decide⟩, ⟨3, by decide⟩, ⟨4, by decide⟩, ⟨5, by decide⟩], by decide⟩ .bigStraight))
+  |>.addTest "Four in order but not a little straight" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨1, by decide⟩, ⟨2, by decide⟩, ⟨3, by decide⟩, ⟨4, by decide⟩], by decide⟩ .littleStraight))
+  |>.addTest "No pairs but not a little straight" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨2, by decide⟩, ⟨3, by decide⟩, ⟨4, by decide⟩, ⟨6, by decide⟩], by decide⟩ .littleStraight))
+  |>.addTest "Minimum is 1, maximum is 5, but not a little straight" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨1, by decide⟩, ⟨1, by decide⟩, ⟨3, by decide⟩, ⟨4, by decide⟩, ⟨5, by decide⟩], by decide⟩ .littleStraight))
+  |>.addTest "Big Straight" (do
+      return assertEqual 30 (Yacht.score ⟨#[⟨4, by decide⟩, ⟨6, by decide⟩, ⟨2, by decide⟩, ⟨5, by decide⟩, ⟨3, by decide⟩], by decide⟩ .bigStraight))
+  |>.addTest "Big Straight as little straight" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨6, by decide⟩, ⟨5, by decide⟩, ⟨4, by decide⟩, ⟨3, by decide⟩, ⟨2, by decide⟩], by decide⟩ .littleStraight))
+  |>.addTest "No pairs but not a big straight" (do
+      return assertEqual 0 (Yacht.score ⟨#[⟨6, by decide⟩, ⟨5, by decide⟩, ⟨4, by decide⟩, ⟨3, by decide⟩, ⟨1, by decide⟩], by decide⟩ .bigStraight))
+  |>.addTest "Choice" (do
+      return assertEqual 23 (Yacht.score ⟨#[⟨3, by decide⟩, ⟨3, by decide⟩, ⟨5, by decide⟩, ⟨6, by decide⟩, ⟨6, by decide⟩], by decide⟩ .choice))
+  |>.addTest "Yacht as choice" (do
+      return assertEqual 10 (Yacht.score ⟨#[⟨2, by decide⟩, ⟨2, by decide⟩, ⟨2, by decide⟩, ⟨2, by decide⟩, ⟨2, by decide⟩], by decide⟩ .choice))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [yachtTests]

exercises/practice/yacht/lakefile.toml

@@ -0,0 +1,15 @@
+name = "yacht"
+version = "0.1.0"
+defaultTargets = ["YachtTest"]
+testDriver = "YachtTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Yacht"
+
+[[lean_exe]]
+name = "YachtTest"
+root = "YachtTest"

exercises/practice/yacht/lean-toolchain

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

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