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.