Formally proving FizzBuzz for fun and profit, part 4.

Last time we created the data type FizzBuzzProofSimple, which represents possible FizzBuzz values and created a few instances of it by hand. The next step is to write a function for generating FizzBuzzProofSimple instances from any number automatically.

Making Proofs

First we’re going to need functions to make DivisiblebyX instances. These functions need to:

  1. Take a natural number as an input
  2. If the number is divisible then return a proof that it is
  3. Else return nothing.

Before we get to defining these functions some groundwork.

Representing nothing

Not all numbers are divisible by three or five, so we won’t be able to generate DivisiblebyX instances for all inputs. The way to repesent something or nothing in Idris is with the Maybe type.

data Maybe : (a : Type) -> Type
    Nothing : Maybe a
    Just : (x : a) -> Maybe a

Maybe is a wrapper around any type and can either be Nothing or Just x where x is a value of the wrapped type. In our case, if the input number is divisible then we’ll return a DivisiblebyX wrapped in a Just, otherwise we’ll return Nothing.

Peano Numbers

To write our functions we’re going to need to work more closely with natural numbers. Previously we’ve used integer literals, but under the hood Idris has been converting these to Peano numbers, which are simple way of representing natural numbers.

data Peano = Z | S Peano

A Peano number is defined as either zero, Z, or the successor, n+1, of another Peano number, S n. So the number one is the successor to zero, S Z, two is the successor to one, S (S Z)), and so on.

In lots of places, Idris lets use integer literals in place of writing out the Peano number in full, but not everywhere.

But will it divide?

We’re now ready to make some proofs.

divisbleby3: (y: Nat) -> Maybe (DivisiblebyX 3 y)
divisbleby3  (S (S (S Z))) = Just Base
divisbleby3 (S (S (S x))) = case divisbleby3 x of
   Nothing => Nothing
   Just y => Just (Multiple y)
divisbleby3 _ = Nothing

Unsurprisingly the function to generate a DivisiblebX proof follows the same recursive pattern as the type definition. Let’s go through each clause:

  1. If the input is 3 (remember Peano numbers) then we can just use the Base variant of DivisiblebyX.
  2. If the input can be represented as 3 more than some number x, then recursively call divisbleby3 with x. If x is divisible by 3 then we can construct an instance DivisiblebyX for our original number using the proof for x we just calculated and the Multiple constructor. Otherwise our input isn’t divisible and we return Nothing.
  3. If none of the other function clauses matched, (Idris checks clauses from top to bottom), then we return Nothing.

divisibleby5 is almost identical:

divisbleby5: (y: Nat) -> Maybe (DivisiblebyX 5 y)
divisbleby5 (S (S (S (S (S Z))))) = Just(Base)
divisbleby5 (S (S (S (S (S x))))) = case divisbleby5 x of
   Nothing => Nothing
   Just y => Just (Multiple y)
divisbleby5 _ = Nothing

Putting it all together

We can now generate proofs of divisibility by 3 or 5 programmatically. So here is what you’ve been waiting for, a formally proven FizzBuzz.

fizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
fizzbuzz x = case (divisbleby3 x, divisbleby5 x) of
   (Nothing, Nothing) => Normal
   (Just fizz_prf, Just buzz_prf) => FizzBuzz fizz_prf buzz_prf
   (Nothing, Just buzz_prf) => Buzz buzz_prf
   (Just fizz_prf, Nothing) => Fizz fizz_prf

For the given number we attempt to generate proofs that it is divisible by three and five. If it isn’t divisible by either then we return Normal if it divides by three but not five we return Fizz etc.

Assuming we’ve defined DivisiblebyX correctly, there is no way to return Fizz, Buzz or FizzBuzz without knowing that the input number is divisible by what it is supposed to.

The last step is to update our Show interface from before.

Show (FizzBuzzProofSimple x) where
   show (Fizz x) = "fizz"
   show (Buzz x) = "buzz"
   show (FizzBuzz x y) = "fizzbuzz"
   show (Normal {x}) = show x

Nothing much has changed except for the Normal clause. The actual value that the type is wrapping is now part of the type instead of being associated with Normal directly. Idris let’s us pull the value in the type into a clause with curly brackets.

The end?

So we’ve got a formally proven version of FizzBuzz. If we implement it wrongly the compiler will tell us. Right? Not quite, the function below also compiles but definitely doesn’t do what we want. Next time we’ll look at fixing the escape hatch in our proof.

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