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

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

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

Unknown 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

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