DST changes in North Macedonia on the last Sunday of October. It happens to be the 25th of October this year.

What can we do with the previous statement, other than generalize it and try to prove a mathematical fact about it? 🙂

The fact that we will prove is that if a month has days, then there is one Sunday in the range . So for example October has 31 days, but we can be sure that there will be one Sunday in . So **some date from 25th through 31st of October will contain a Sunday**, and this is true for every year.

First, we will prove that there is one Sunday in the range . For this, we can use proof by cases where each case will be a day of the week. Thus, the day is one of:

- Sunday: Thus, is Sunday.
- Saturday: Thus, is Sunday.
- Friday: Thus, is Sunday.
- Thursday: Thus, is Sunday.
- Wednesday: Thus, is Sunday.
- Tuesday: Thus, is Sunday.
- Monday: Thus, is Sunday.

In any case, for any , there is one Sunday in the range . Now, if we replace with , we get that if a month has days, then we can be sure that there is one Sunday in . The proof can be generalized for any day, not just Sunday.

Let’s prove the same in Dafny now.

We start by providing the datatypes for days and naturals (we need to map days to numbers):

datatype Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday datatype Nat = S (Nat) | Z

Now we will provide a neat method that converts a natural number to a day:

function method nat_to_day (n: Nat) : Day decreases n { match n { case Z => Monday case S(Z) => Tuesday case S(S(Z)) => Wednesday case S(S(S(Z))) => Thursday case S(S(S(S(Z)))) => Friday case S(S(S(S(S(Z))))) => Saturday case S(S(S(S(S(S(Z)))))) => Sunday case S(S(S(S(S(S(S(k))))))) => nat_to_day(k) } }

Finally, the proof just uses similar technique to the case analysis we did earlier:

lemma {:induction n} proof (n : Nat) ensures nat_to_day(n) == Sunday ==> nat_to_day(n) == Sunday ensures nat_to_day(n) == Saturday ==> nat_to_day(S(n)) == Sunday ensures nat_to_day(n) == Friday ==> nat_to_day(S(S(n))) == Sunday ensures nat_to_day(n) == Thursday ==> nat_to_day(S(S(S(n)))) == Sunday ensures nat_to_day(n) == Wednesday ==> nat_to_day(S(S(S(S(n))))) == Sunday ensures nat_to_day(n) == Tuesday ==> nat_to_day(S(S(S(S(S(n)))))) == Sunday ensures nat_to_day(n) == Monday ==> nat_to_day(S(S(S(S(S(S(n))))))) == Sunday {}

So we proved that for every natural number , one of will be a Sunday.

Disregarding the usefulness (uselessness) of this proof, the post demonstrates a few things:

- We modeled a simple real-world fact into the world of mathematics, and we proved some stuff about that fact
- We translated the problem from the language of mathematics to the programming language Dafny, and we proved some stuff about it