Formally proving FizzBuzz for fun and profit, part 5.

Last time we created a formally proven version of FizzBuzz, but it had some problems. Our proofs weren’t strong enough to prevent us making the version below, where anything divisible by five returns Buzz and everything else returns Normal.

wrongfizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
wrongfizzbuzz x = case (divisbleby3 x, divisbleby5 x) of
   (_,  Just buzz_prf) => Buzz buzz_prf
   (_, _) => Normal

The problem is that we create proofs that a number is divisible but not proofs that a number isn’t.

This is an important lesson. Just because you’ve proved something about your code, doesn’t mean you’ve proved what you need to. Proof types need to be crafted carefully so they actually prove what you think they do.

Proving a negative

Idris has a type to represent something which can’t exist, Void.

data Void : Type where

Void has no constructors, so it is impossible to create values of the type. If a function returns Void then one of its arguments must also be impossible to construct. In other words, if we can create a function which takes a single input and returns Void, then we have a proof that the input is impossible.

For FizzBuzz we want to be able to make proofs that a given number isn’t divisible by three or five. Something like:

DivisiblebyX 3 x -> Void
DivisiblebyX 5 x -> Void

Adding requirements for these negative proofs to our FizzBuzzProofSimple type gives:

data FizzBuzzProof: Nat -> Type where
   Fizz: DivisiblebyX 3 x -> (DivisiblebyX 5 x -> Void) -> FizzBuzzProof x
   Buzz: DivisiblebyX 5 x -> (DivisiblebyX 3 x -> Void) -> FizzBuzzProof x
   FizzBuzz: DivisiblebyX 3 x -> DivisiblebyX 5 x -> FizzBuzzProof x
   Normal: (x: Nat) -> (DivisiblebyX 3 x -> Void) ->(DivisiblebyX 5 x -> Void) -> FizzBuzzProof x

With the addition of these proofs it is impossible to use the wrong FizzBuzz variant for a number. Now we just need a way to make the proofs.

Will it divide?

We need to check each input number to see if it is divisible by three or five. Previously the divisibleby3 and divisibleby5 functions returned Nothing if the input didn’t divide, now we need to return a negative proof instead. Returning either a proof something is true or a proof it isn’t, is common enough pattern Idris provides the Dec wrapper type:

data Dec : Type -> Type where
  Yes : (prf: prop) -> Dec prop
  No : (contra : prop -> Void) -> Dec prop

Dec has a Yes and a No constructor, created with an instance of the wrapped type or a proof that the type is impossible to construct values of.

Adding these new features to our old divisibleby3 function gives:

divisibleby3: (y: Nat) -> Dec (DivisiblebyX 3 y)
divisibleby3 Z = No zeroNotDivisible3
divisibleby3 (S Z) = No oneNotDivisible3
divisibleby3 (S (S Z)) = No twoNotDivisible3
divisibleby3 (S (S (S Z))) = Yes Base
divisibleby3 (S (S (S (S y)))) = case divisibleby3 (S y) of
   Yes prf => Yes (Multiple prf)
   No notdiv => No (threeLessNotDivisible3 notdiv)

Instead of a catchall clause for numbers which aren’t divisible we now have separate clauses for when the input number is:

• 0
• 1
• 2
• 3
• some number in the form (n+3)

Collectively these clauses cover all possible inputs (Idris will tell us if they don’t). If the input is divisible then the code is basically the same as before, each of the other clauses requires their own proof function.

Impossible

The proof functions for zero, one and two are almost identical and Idris will auto-generate most of the code.

zeroNotDivisible3 : DivisiblebyX 3 0 -> Void
zeroNotDivisible3 Base impossible
zeroNotDivisible3 (Multiple _) impossible

oneNotDivisible3 : DivisiblebyX 3 1 -> Void
oneNotDivisible3 Base impossible
oneNotDivisible3 (Multiple _) impossible

twoNotDivisible3 : DivisiblebyX 3 2 -> Void
twoNotDivisible3 Base impossible
twoNotDivisible3 (Multiple _) impossible

The function types are in the form for negative proofs we’ve seen above. To implement the function bodies we split the input argument into the two possible constructors, Base and Multiple. Idris can then determine that inputs of the required form are impossible.

For example, in zeroNotDivisible3 the input argument has to have the type DivisiblebyX 3 0. The Base constructor requires the two type arguments to be the same, which 3 and 0 aren’t. The Multiple constructor would require as an input an instance of DivisiblebyX 3 (0-3). Since natural numbers can’t be negative, this clause is also impossible.

threeLessNotDivisible3 is slightly different.

threeLessNotDivisible3 : (notdiv : DivisiblebyX 3 (S y) -> Void) -> DivisiblebyX 3 (3 + (S y)) -> Void
threeLessNotDivisible3 notdiv (Multiple x) = notdiv x

It is a proof that, given a non-zero number y is not divisible by three, y+3 is also not divisible by three. We split DivisiblebyX 3 (3 + (S y)) into the only applicable constructor, Multiple, which gives us a value of DivisiblebyX 3 (S y), calling notdiv with this value returns Void which completes the functions.

divisibleby5 is the same structure, with extra clauses for values of three and four.

A formally proven FizzBuzz (at last)

We now have functions for creating proofs that a number is or isn’t divisible by three or five. Plugging these functions into our fizzbuzz function gives:

fizzbuzz: (x: Nat) -> FizzBuzzProof x
fizzbuzz x = case (divisibleby3 x, divisibleby5 x) of
   (No not_fizz, No not_buzz) => Normal x not_fizz not_buzz
   (Yes fizz_prf, Yes buzz_prf) => FizzBuzz fizz_prf buzz_prf
   (No not_fizz, Yes buzz_prf) => Buzz buzz_prf not_fizz
   (Yes fizz_prf, No not_buzz) => Fizz fizz_prf not_buzz

Unlike our last attempt at FizzBuzz, there is now no way to return the wrong FizzBuzz variant.

The end?

We have a function for generating FizzBuzz for any single number, but FizzBuzz actually needs to be generated for all numbers between one and one hundred. Next time we’ll look at how to do this in Idris.