## Sunday, May 21, 2017

### Proving fib equivalence

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.

Santiago Zanella said...

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.

Neil Mitchell said...

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?

Santiago Zanella said...

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.

Ranjit Jhala said...

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

Neil Mitchell said...

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)?

Sean Burton said...

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

Neil Mitchell said...

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

Sean Burton said...

@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

Sean Burton said...

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

Neil Mitchell said...

Neat, a very nice definition.