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:

- Take a natural number as an input
- If the number is divisible then return a proof that it is
- 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:

- If the input is 3 (remember Peano numbers) then we can just use the
**Base**variant of**DivisiblebyX**. - 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**. - 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
```