Add meetup exercise

config.json

@@ -466,6 +466,14 @@
         "prerequisites": [],
         "difficulty": 5
       },
+      {
+        "slug": "meetup",
+        "name": "Meetup",
+        "uuid": "c88786b1-d953-49c0-b4ce-dac5137087bf",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 5
+      },
       {
         "slug": "nth-prime",
         "name": "Nth Prime",

exercises/practice/meetup/.docs/instructions.append.md

@@ -0,0 +1,10 @@
+# Instructions append
+
+## Subtypes
+
+This exercise defines a Subtype called `Month`, for natural numbers 1 through 12.
+A Subtype can be thought of as a pair `⟨x, h⟩`, where x is the value and h is the proof of its validity.
+
+The value inside a Subtype (x, in this case) can be accessed by using .val, for example, `x.val`.
+Its proof can be accessed by using .property, for example, `x.property`.
+Both can also be accessed by pattern matching, as usual.

exercises/practice/meetup/.docs/instructions.md

@@ -0,0 +1,34 @@
+# Instructions
+
+Your task is to find the exact date of a meetup, given a month, year, weekday and week.
+
+There are six week values to consider: `first`, `second`, `third`, `fourth`, `last`, `teenth`.
+
+For example, you might be asked to find the date for the meetup on the first Monday in January 2018 (January 1, 2018).
+
+Similarly, you might be asked to find:
+
+- the third Tuesday of August 2019 (August 20, 2019)
+- the teenth Wednesday of May 2020 (May 13, 2020)
+- the fourth Sunday of July 2021 (July 25, 2021)
+- the last Thursday of November 2022 (November 24, 2022)
+- the teenth Saturday of August 1953 (August 15, 1953)
+
+## Teenth
+
+The teenth week refers to the seven days in a month that end in '-teenth' (13th, 14th, 15th, 16th, 17th, 18th and 19th).
+
+If asked to find the teenth Saturday of August, 1953, we check its calendar:
+
+```plaintext
+    August 1953
+Su Mo Tu We Th Fr Sa
+                   1
+ 2  3  4  5  6  7  8
+ 9 10 11 12 13 14 15
+16 17 18 19 20 21 22
+23 24 25 26 27 28 29
+30 31
+```
+
+From this we find that the teenth Saturday is August 15, 1953.

exercises/practice/meetup/.docs/introduction.md

@@ -0,0 +1,29 @@
+# Introduction
+
+Every month, your partner meets up with their best friend.
+Both of them have very busy schedules, making it challenging to find a suitable date!
+Given your own busy schedule, your partner always double-checks potential meetup dates with you:
+
+- "Can I meet up on the first Friday of next month?"
+- "What about the third Wednesday?"
+- "Maybe the last Sunday?"
+
+In this month's call, your partner asked you this question:
+
+- "I'd like to meet up on the teenth Thursday; is that okay?"
+
+Confused, you ask what a "teenth" day is.
+Your partner explains that a teenth day, a concept they made up, refers to the days in a month that end in '-teenth':
+
+- 13th (thirteenth)
+- 14th (fourteenth)
+- 15th (fifteenth)
+- 16th (sixteenth)
+- 17th (seventeenth)
+- 18th (eighteenth)
+- 19th (nineteenth)
+
+As there are also seven weekdays, it is guaranteed that each day of the week has _exactly one_ teenth day each month.
+
+Now that you understand the concept of a teenth day, you check your calendar.
+You don't have anything planned on the teenth Thursday, so you happily confirm the date with your partner.

exercises/practice/meetup/.meta/Example.lean

@@ -0,0 +1,96 @@
+namespace Meetup
+
+inductive DayOfWeek where
+  | Monday : DayOfWeek
+  | Tuesday : DayOfWeek
+  | Wednesday : DayOfWeek
+  | Thursday : DayOfWeek
+  | Friday : DayOfWeek
+  | Saturday : DayOfWeek
+  | Sunday : DayOfWeek
+  deriving BEq, Repr
+
+def Month := { m : Nat // m ≥ 1 ∧ m ≤ 12 }
+
+inductive Week where
+  | first : Week
+  | second : Week
+  | third : Week
+  | fourth : Week
+  | teenth : Week
+  | last : Week
+  deriving BEq, Repr
+
+def leapYear (year : Nat) : Bool :=
+  (year % 4 == 0) && ((year % 100 != 0) || (year % 400 == 0))
+
+def daysInMonth (month : Month) (year : Nat) : Nat :=
+  match month.val with
+  | 1 => 31
+  | 2 => if leapYear year then 29 else 28
+  | 3 => 31
+  | 4 => 30
+  | 5 => 31
+  | 6 => 30
+  | 7 => 31
+  | 8 => 31
+  | 9 => 30
+  | 10 => 31
+  | 11 => 30
+  | 12 => 31
+  | _ => panic "impossible month"
+
+def monthOffset (month : Month) : Nat :=
+  match month.val with
+  | 1 => 307  -- offset from the end of February
+  | 2 => 338
+  | 3 => 1
+  | 4 => 32
+  | 5 => 62
+  | 6 => 93
+  | 7 => 123
+  | 8 => 154
+  | 9 => 185
+  | 10 => 215
+  | 11 => 246
+  | 12 => 276
+  | _ => panic "impossible month"
+
+def weekConcludes (month : Month) (week : Week) (year : Nat) : Nat :=
+  match week with
+  | .first => 7
+  | .second => 14
+  | .third => 21
+  | .fourth => 28
+  | .teenth => 19
+  | .last => daysInMonth month year
+
+def dayOfWeekIndex (dayOfWeek : DayOfWeek) : Nat :=
+  match dayOfWeek with
+  | .Monday => 1
+  | .Tuesday => 2
+  | .Wednesday => 3
+  | .Thursday => 4
+  | .Friday => 5
+  | .Saturday => 6
+  | .Sunday => 7
+
+def dayOfWeekIndexCalculated (dayInMonth : Nat) (month : Month) (year : Nat) : Nat :=
+  let year1 := if month.val < 3 then year - 1 else year
+  ((year1 + (year1 / 400) + (year1 / 4) - (year1 / 100)) + (monthOffset month) + dayInMonth) % 7 + 1
+
+def meetupDay (dayOfWeek : DayOfWeek) (month : Month) (week : Week) (year : Nat) : Nat :=
+  let dayWeekConcludes := weekConcludes month week year
+  let concludingDayIndex := dayOfWeekIndexCalculated dayWeekConcludes month year
+  let requiredDayIndex := dayOfWeekIndex dayOfWeek
+  let adjustment := if concludingDayIndex < requiredDayIndex then 7 else 0
+  (dayWeekConcludes + requiredDayIndex) - (concludingDayIndex + adjustment)
+
+def twoDigit (n : Nat) : String :=
+  if n >= 10 then s!"{n}" else s!"0{n}"
+
+def meetup (dayOfWeek : DayOfWeek) (month : Month) (week : Week) (year : Nat) : String :=
+  let day := meetupDay dayOfWeek month week year
+  s!"{year}-{twoDigit month.val}-{twoDigit day}"
+
+end Meetup

exercises/practice/meetup/.meta/config.json

@@ -0,0 +1,18 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "Meetup.lean"
+    ],
+    "test": [
+      "MeetupTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Calculate the date of meetups.",
+  "source": "Jeremy Hinegardner mentioned a Boulder meetup that happens on the Wednesteenth of every month"
+}

exercises/practice/meetup/.meta/extra.json

@@ -0,0 +1,24 @@
+[
+    {
+        "description": "when last Thursday in February in a non-leap year is not the 29th",
+        "property": "meetup",
+        "input": {
+            "year": 2300,
+            "month": 2,
+            "week": "last",
+            "dayofweek": "Thursday"
+        },
+        "expected": "2300-02-22"
+    },
+    {
+        "description": "when fourth Monday is the 23nd, the second day of the fourth week",
+        "property": "meetup",
+        "input": {
+            "year": 2468,
+            "month": 1,
+            "week": "fourth",
+            "dayofweek": "Monday"
+        },
+        "expected": "2468-01-23"
+    }
+]