*Summary: Using Idris I proved the exponential and linear time fib functions are equivalent.*

The Haskell wiki proclaims that Implementing the Fibonacci sequence is considered the "Hello, world!" of Haskell programming. It also provides multiple versions of `fib`

- an exponential version and a linear version. We can translate these into Idris fairly easily:

```
fibExp : Nat -> Nat
fibExp Z = 0
fibExp (S Z) = 1
fibExp (S (S n)) = fibExp (S n) + fibExp n
fibLin' : Nat -> Nat -> Nat -> Nat
fibLin' Z a b = b
fibLin' (S n) a b = fibLin' n (a + b) a
fibLin : Nat -> Nat
fibLin n = fibLin' n 1 0
```

We've made the intermediate `go`

function in `fibLin`

top-level, named it `fibLib'`

and untupled the accumulator - but it's still fundamentally the same. Now we've got the power of Idris, it would be nice to prove that `fibExp`

and `fibLin`

are equivalent. To do that, it's first useful to think about why `fibLib'`

works at all. In essence we're decrementing the first argument, and making the next two arguments be `fib`

of increasingly large values. If we think more carefully we can come up with the invariant:

```
fibLinInvariant : (d : Nat) -> (u : Nat) ->
fibLin' d (fibExp (1+u)) (fibExp u) = fibExp (d+u)
```

Namely that at all recursive calls we must have the `fib`

of two successive values (`u`

and `u+1`

), and after `d`

additional loops we end up with `fib (d+u)`

. Actually proving this invariant isn't too hard:

```
fibLinInvariant Z u = Refl
fibLinInvariant (S d) u =
rewrite fibLinInvariant d (S u) in
rewrite plusSuccRightSucc d u in
Refl
```

Idris simplifies the base case away for us. For the recursive case we apply the induction hypothesis to leave us with:

```
fibExp (plus d (S u)) = fibExp (S (plus d u))
```

Ignoring the `fibExp`

we just need to prove `d+(u+1) = (d+u)+1`

. That statement is obviously true because `+`

is associative, but in our particular case, we use `plusSuccRightSucc`

which is the associative lemma where `+1`

is the special `S`

constructor. After that, everything has been proven.

Armed with the fundamental correctness invariant for `fibLib`

, we can prove the complete equivalence.

```
fibEq : (n : Nat) -> fibLin n = fibExp n
fibEq n =
rewrite fibLinInvariant n 0 in
rewrite plusZeroRightNeutral n in
Refl
```

We appeal to the invariant linking `fibLin'`

and `finExp`

, do some minor arithmetic manipulation (`x+0 = x`

), and are done. Note that depending on exactly how you define the `fibLinInvariant`

you require different arithmetic lemmas, e.g. if you write `d+u`

or `u+d`

. Idris is equipped with everything required.

I was rather impressed that proving `fib`

equivalence wasn't all that complicated, and really just requires figuring out what fundamental property makes `fibLin`

actually work. In many ways the proof makes things clearer.