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