Proof: One Sunday every 7 days

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 $K$ days, then there is one Sunday in the range $[K - 6, K]$ . So for example October has 31 days, but we can be sure that there will be one Sunday in $[31 - 6, 31] = [25, 31]$ . 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 $[N, N + 6]$ . For this, we can use proof by cases where each case will be a day of the week. Thus, the day $N$ is one of:

Sunday: Thus, $N$ is Sunday.
Saturday: Thus, $N + 1$ is Sunday.
Friday: Thus, $N + 2$ is Sunday.
Thursday: Thus, $N + 3$ is Sunday.
Wednesday: Thus, $N + 4$ is Sunday.
Tuesday: Thus, $N + 5$ is Sunday.
Monday: Thus, $N + 6$ is Sunday.

In any case, for any $N$ , there is one Sunday in the range $[N, N + 6]$ . Now, if we replace $N$ with $K-6$ , we get that if a month has $K$ days, then we can be sure that there is one Sunday in $[K - 6, K]$ . 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 $n$ , one of $(n, n+1, n+2, n+3, n+4, n+5, n+6)$ 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