Add twelve-days exercise

config.json

@@ -419,6 +419,14 @@
         "prerequisites": [],
         "difficulty": 4
       },
+      {
+        "slug": "twelve-days",
+        "name": "Twelve Days",
+        "uuid": "4c407000-255a-44c9-a7ef-549580a2ccb8",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 4
+      },
       {
         "slug": "word-count",
         "name": "Word Count",

exercises/practice/twelve-days/.docs/instructions.md

@@ -0,0 +1,36 @@
+# Instructions
+
+Your task in this exercise is to write code that returns the lyrics of the song: "The Twelve Days of Christmas."
+
+"The Twelve Days of Christmas" is a common English Christmas carol.
+Each subsequent verse of the song builds on the previous verse.
+
+The lyrics your code returns should _exactly_ match the full song text shown below.
+
+## Lyrics
+
+```text
+On the first day of Christmas my true love gave to me: a Partridge in a Pear Tree.
+
+On the second day of Christmas my true love gave to me: two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the third day of Christmas my true love gave to me: three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the fourth day of Christmas my true love gave to me: four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the fifth day of Christmas my true love gave to me: five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the sixth day of Christmas my true love gave to me: six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the seventh day of Christmas my true love gave to me: seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the eighth day of Christmas my true love gave to me: eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the ninth day of Christmas my true love gave to me: nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the tenth day of Christmas my true love gave to me: ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the eleventh day of Christmas my true love gave to me: eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+
+On the twelfth day of Christmas my true love gave to me: twelve Drummers Drumming, eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.
+```

exercises/practice/twelve-days/.meta/Example.lean

@@ -0,0 +1,30 @@
+namespace TwelveDays
+
+abbrev VerseIndex := { x : Nat // 1 ≤ x ∧ x ≤ 12 }
+
+def ordinal (verse : Nat) : String :=
+  let ordinals := "firstsecondthirdfourthfifthsixthseventheighthninthtentheleventhtwelfth"
+  let ordinalsTable := #[0, 0, 5, 11, 16, 22, 27, 32, 39, 45, 50, 55, 63, 70]
+  ordinals
+      |> (·.toSlice)
+      |> (·.drop ordinalsTable[verse]!)
+      |> (·.take (ordinalsTable[verse + 1]! - ordinalsTable[verse]!))
+      |> (·.copy)
+
+def gift (verse : Nat) : String :=
+  let gifts := "twelve Drummers Drumming, eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+  let giftsTable := #[262, 235, 213, 194, 174, 157, 137, 113, 90, 69, 48, 26, 0]
+  gifts
+      |> (·.toSlice)
+      |> (·.drop giftsTable[verse]!)
+      |> (·.take (giftsTable[0]! - giftsTable[verse]!))
+      |> (·.copy)
+
+def lyrics (verse : Nat) : String :=
+  s!"On the {ordinal verse} day of Christmas my true love gave to me: {gift verse}"
+
+def recite (startVerse endVerse : VerseIndex) : List String :=
+  List.range' startVerse.val (endVerse.val + 1 - startVerse.val)
+      |> (·.map lyrics)
+
+end TwelveDays

exercises/practice/twelve-days/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "TwelveDays.lean"
+    ],
+    "test": [
+      "TwelveDaysTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Output the lyrics to 'The Twelve Days of Christmas'.",
+  "source": "Wikipedia",
+  "source_url": "https://en.wikipedia.org/wiki/The_Twelve_Days_of_Christmas_(song)"
+}

exercises/practice/twelve-days/.meta/tests.toml

@@ -0,0 +1,55 @@
+# 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.
+
+[c0b5a5e6-c89d-49b1-a6b2-9f523bff33f7]
+description = "verse -> first day a partridge in a pear tree"
+
+[1c64508a-df3d-420a-b8e1-fe408847854a]
+description = "verse -> second day two turtle doves"
+
+[a919e09c-75b2-4e64-bb23-de4a692060a8]
+description = "verse -> third day three french hens"
+
+[9bed8631-ec60-4894-a3bb-4f0ec9fbe68d]
+description = "verse -> fourth day four calling birds"
+
+[cf1024f0-73b6-4545-be57-e9cea565289a]
+description = "verse -> fifth day five gold rings"
+
+[50bd3393-868a-4f24-a618-68df3d02ff04]
+description = "verse -> sixth day six geese-a-laying"
+
+[8f29638c-9bf1-4680-94be-e8b84e4ade83]
+description = "verse -> seventh day seven swans-a-swimming"
+
+[7038d6e1-e377-47ad-8c37-10670a05bc05]
+description = "verse -> eighth day eight maids-a-milking"
+
+[37a800a6-7a56-4352-8d72-0f51eb37cfe8]
+description = "verse -> ninth day nine ladies dancing"
+
+[10b158aa-49ff-4b2d-afc3-13af9133510d]
+description = "verse -> tenth day ten lords-a-leaping"
+
+[08d7d453-f2ba-478d-8df0-d39ea6a4f457]
+description = "verse -> eleventh day eleven pipers piping"
+
+[0620fea7-1704-4e48-b557-c05bf43967f0]
+description = "verse -> twelfth day twelve drummers drumming"
+
+[da8b9013-b1e8-49df-b6ef-ddec0219e398]
+description = "lyrics -> recites first three verses of the song"
+
+[c095af0d-3137-4653-ad32-bfb899eda24c]
+description = "lyrics -> recites three verses from the middle of the song"
+
+[20921bc9-cc52-4627-80b3-198cbbfcf9b7]
+description = "lyrics -> recites the whole song"

exercises/practice/twelve-days/TwelveDays.lean

@@ -0,0 +1,8 @@
+namespace TwelveDays
+
+abbrev VerseIndex := { x : Nat // 1 ≤ x ∧ x ≤ 12 }
+
+def recite (startVerse endVerse : VerseIndex) : List String :=
+  sorry
+
+end TwelveDays

exercises/practice/twelve-days/TwelveDaysTest.lean

@@ -0,0 +1,85 @@
+import LeanTest
+import TwelveDays
+
+open LeanTest
+
+def twelveDaysTests : TestSuite :=
+  (TestSuite.empty "TwelveDays")
+  |>.addTest "verse -> first day a partridge in a pear tree" (do
+      return assertEqual [
+        "On the first day of Christmas my true love gave to me: a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨1, by decide⟩ ⟨1, by decide⟩))
+  |>.addTest "verse -> second day two turtle doves" (do
+      return assertEqual [
+        "On the second day of Christmas my true love gave to me: two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨2, by decide⟩ ⟨2, by decide⟩))
+  |>.addTest "verse -> third day three french hens" (do
+      return assertEqual [
+        "On the third day of Christmas my true love gave to me: three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨3, by decide⟩ ⟨3, by decide⟩))
+  |>.addTest "verse -> fourth day four calling birds" (do
+      return assertEqual [
+        "On the fourth day of Christmas my true love gave to me: four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨4, by decide⟩ ⟨4, by decide⟩))
+  |>.addTest "verse -> fifth day five gold rings" (do
+      return assertEqual [
+        "On the fifth day of Christmas my true love gave to me: five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨5, by decide⟩ ⟨5, by decide⟩))
+  |>.addTest "verse -> sixth day six geese-a-laying" (do
+      return assertEqual [
+        "On the sixth day of Christmas my true love gave to me: six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨6, by decide⟩ ⟨6, by decide⟩))
+  |>.addTest "verse -> seventh day seven swans-a-swimming" (do
+      return assertEqual [
+        "On the seventh day of Christmas my true love gave to me: seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨7, by decide⟩ ⟨7, by decide⟩))
+  |>.addTest "verse -> eighth day eight maids-a-milking" (do
+      return assertEqual [
+        "On the eighth day of Christmas my true love gave to me: eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨8, by decide⟩ ⟨8, by decide⟩))
+  |>.addTest "verse -> ninth day nine ladies dancing" (do
+      return assertEqual [
+        "On the ninth day of Christmas my true love gave to me: nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨9, by decide⟩ ⟨9, by decide⟩))
+  |>.addTest "verse -> tenth day ten lords-a-leaping" (do
+      return assertEqual [
+        "On the tenth day of Christmas my true love gave to me: ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨10, by decide⟩ ⟨10, by decide⟩))
+  |>.addTest "verse -> eleventh day eleven pipers piping" (do
+      return assertEqual [
+        "On the eleventh day of Christmas my true love gave to me: eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨11, by decide⟩ ⟨11, by decide⟩))
+  |>.addTest "verse -> twelfth day twelve drummers drumming" (do
+      return assertEqual [
+        "On the twelfth day of Christmas my true love gave to me: twelve Drummers Drumming, eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨12, by decide⟩ ⟨12, by decide⟩))
+  |>.addTest "lyrics -> recites first three verses of the song" (do
+      return assertEqual [
+        "On the first day of Christmas my true love gave to me: a Partridge in a Pear Tree.",
+        "On the second day of Christmas my true love gave to me: two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the third day of Christmas my true love gave to me: three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨1, by decide⟩ ⟨3, by decide⟩))
+  |>.addTest "lyrics -> recites three verses from the middle of the song" (do
+      return assertEqual [
+        "On the fourth day of Christmas my true love gave to me: four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the fifth day of Christmas my true love gave to me: five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the sixth day of Christmas my true love gave to me: six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨4, by decide⟩ ⟨6, by decide⟩))
+  |>.addTest "lyrics -> recites the whole song" (do
+      return assertEqual [
+        "On the first day of Christmas my true love gave to me: a Partridge in a Pear Tree.",
+        "On the second day of Christmas my true love gave to me: two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the third day of Christmas my true love gave to me: three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the fourth day of Christmas my true love gave to me: four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the fifth day of Christmas my true love gave to me: five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the sixth day of Christmas my true love gave to me: six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the seventh day of Christmas my true love gave to me: seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the eighth day of Christmas my true love gave to me: eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the ninth day of Christmas my true love gave to me: nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the tenth day of Christmas my true love gave to me: ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the eleventh day of Christmas my true love gave to me: eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree.",
+        "On the twelfth day of Christmas my true love gave to me: twelve Drummers Drumming, eleven Pipers Piping, ten Lords-a-Leaping, nine Ladies Dancing, eight Maids-a-Milking, seven Swans-a-Swimming, six Geese-a-Laying, five Gold Rings, four Calling Birds, three French Hens, two Turtle Doves, and a Partridge in a Pear Tree."
+      ] (TwelveDays.recite ⟨1, by decide⟩ ⟨12, by decide⟩))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [twelveDaysTests]

exercises/practice/twelve-days/lakefile.toml

@@ -0,0 +1,15 @@
+name = "twelve-days"
+version = "0.1.0"
+defaultTargets = ["TwelveDaysTest"]
+testDriver = "TwelveDaysTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "TwelveDays"
+
+[[lean_exe]]
+name = "TwelveDaysTest"
+root = "TwelveDaysTest"

exercises/practice/twelve-days/lean-toolchain

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

exercises/practice/twelve-days/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