*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.

## 11 comments:

Thanks for the very nice example.

For comparison, this is how you would do the same in F*

module Fib

val fibExp: nat -> nat

let rec fibExp = function

| 0 -> 0

| 1 -> 1

| n -> fibExp (n - 1) + fibExp (n - 2)

val fibLin': nat -> nat -> nat -> nat

let rec fibLin' n a b =

match n with

| 0 -> b

| _ -> fibLin' (n - 1) (a + b) a

val fibLin: nat -> nat

let fibLin n = fibLin' n 1 0

val fibLinInvariant: d:nat -> u:nat ->

Lemma (fibLin' d (fibExp (1 + u)) (fibExp u) == fibExp (d + u))

let rec fibLinInvariant d u =

match d with

| 0 -> ()

| _ -> fibLinInvariant (d - 1) (u + 1)

val fibEq: n:nat -> Lemma (fibLin n == fibExp n)

let rec fibEq n = fibLinInvariant n 0

Apologies for the shameless plug.

Santiago, plug most welcome! In F*, how are the arithmetic lemmas been discharged? Is that something F* does automatically? Or is there some theory with normalisation of arithmetic?

We encode verification conditions to the Z3 SMT solver, using Z3's primitive arithmetic theory. Here's a paper that explains in some detail how it's done: http://prosecco.gforge.inria.fr/personal/hritcu/publications/fstar-to-smt-hatt2016.pdf.

There is a tactic language in the works (https://github.com/FStarLang/FStar/wiki/F%2A-tactics). Our ultimate goal is to generate proof terms like in Idris, by integrating with the Lean theorem prover.

Nice examples! Its easy to port these proofs (Idris, F*) to (Liquid) Haskell:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1495491514_730.hs

Ranjit: Thanks for the example. Can you say what Liquid Haskell is doing? Is it just translating it to a theorem prover? Is it proved inductively, or just for a bound of Nat in terms of bits? Are we limited to proofs on Nat, or can we prove things about lists (more than just properties about list size)?

I solved this problem myself without looking at your post, and I ended up using the fact that fibLin' satisfies the Fibonacci recurrence as my invariant (although I used a slightly different definition of fibLin' which makes this easier).

fibLin' : Nat -> Nat -> Nat -> Nat

fibLin' a b Z = a

fibLin' a b (S n) = fibLin' b (a + b) n

lemma : (a : Nat) -> (b : Nat) -> (n : Nat) -> fibLin' a b (2 + n) = fibLin' a b (1 + n) + fibLin' a b n

lemma a b Z = plusCommutative a b

lemma a b (S k) = lemma b (a + b) k

@Sean - elegant, but if you defined fibLin' a b c = 0, I think your proof still holds, so not sure how strong the proof is.

@Neil Mitchell it is just a simple induction to the full proof:

fibEq : (n : Nat) -> fibLin n = fibExp n

fibEq Z = Refl

fibEq (S Z) = Refl

fibEq (S (S k)) =

rewrite sym (fibEq (S k)) in

rewrite sym (fibEq k) in

lemma 0 1 k

Although I was wrong that my fibLin' makes the proof easier, it is actually slightly shorter with the original definition.

Neat, a very nice definition.

Thhanks for this

Post a Comment