Showing two different fibonacci functions are equivalent

Question

I'm trying to learn exactly what it means to prove a program correct. I'm starting from scratch and getting hung up on the first steps/the introduction to the topic.

In this paper on total functional programming, two definitions of the fibonacci function are given. The traditional one:

fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)
--fib (n+2) = fib (n+1) + fib (n+2) --The definition as given in the paper 
                                    --It seems incorrect to me. Typo?

and a tail recursive version I had never seen before:

fib' n = f n 0 1
f 0 a b = a
f n a b = f (n-1) b (a+b)

The paper then claimed that it is "straightforward" to prove by induction that both functions return the same result for all positive Integers n. This is the first time I've thought of analysing programs like this. It's quite interesting to think that you can prove that two programs are equivilent, so I immediately tried to do this proof by induction myself. Either my maths skills are rusty or the task is not actually all that straightforward.

I proved for n = 1

fib' 1 = f 1 0 1
       = f 0 1 1
       = 1
fib 1  = 1 (By definition)
therefore
fib' n = fib n for n = 1

I made the n = k assumption

fib' k  = fib k
f k 0 1 = fib k

I start trying to prove that if the assumption holds true, then the functions are also equivilant for n = k + 1 (and hence they are all equivalent for all n >= 1 QED)

fib' (k+1)  = fib (k+1)
f (k+1) 0 1 = fib k + fib (k-1)

I've tried various manipulations, substituting the assumption in at the right time and so on, but I just can't get LHS to equal RHS and therefore prove that the functions/programs are equivalent. What am I missing? The paper mentions that the task is equivalent to proving

f n (fib p) (fib (p+1)) = fib (p+n)

by induction for arbitrary p. But I don't see how that's true at all. How did the authors arrive at this equation? That's a valid transformation on the equation only if p = 0. I don't see how that means it works for arbitrary p. To prove it for arbitrary p requires you to go through another layer of induction. Surely the correct formula to prove would be

fib' (n+p)  = fib (n+p)
f (n+p) 0 1 = fib (n+p)

So far that hasn't helped either. Can anyone show me how the induction would be done? Or link to a page that shows the proof (I did search, couldn't find anything).

Deka

fib (n+2) = fib (n+1) + fib (n+2) is clearly a typo, they probably meant fib (n+2) = fib (n+1) + fib n which is mathematically correct, but is getting removed from valid Haskell hackage.haskell.org/trac/haskell-prime/wiki/RemoveNPlusK – Materi

You might be interested in this: ats-lang.org/EXAMPLE/#FIBexample -- an example of programming with theorem proving (for a Fibonacci function). Also note that the specification given there for Fib is inductive, but an implementation is tail-recursive and is shown to conform to the spec. – Consult

Answer 1

I couldn't access to the above mentioned paper, but their generalized theorem is a good way to go. Two values 0 and 1 in f n 0 1 sound like magic numbers; however if you generalize them to Fibonacci numbers, a proof is much easier to be conducted.

To avoid confusion when reading the proof, fib k is written as F(k) and some unnecessary parentheses are also removed. We have a generalized theorem: forall k. fib' n F(k) F(k+1) = F(k+n) and prove it by induction on n.

Base case with n=1:

fib' 1 F(k) F(k+1) = F(k+1) // directly deduce from definition of fib'

Inductive step:

We have the induction hypothesis where:

forall k. fib' n F(k) F(k+1) = F(k+n)

And we have to prove:

forall k. fib' (n+1) F(k) F(k+1) = F(k+(n+1))

The proof starts from the left-hand side:

fib' (n+1) F(k) F(k+1)
= fib' n F(k+1) (F(k) + F(k+1)) // definition of fib'
= fib' n F(k+1) F(k+2) // definition of F (or fib)
= F((k+1)+n) // induction hypothesis
= F(k+(n+1)) // arithmetic

We completed the generalized proof. Your example is also proven because it is a specific case of the above theorem with k=0.

As a side note, fib' isn't strange at all; it is a tail-recursive version of fib.

Extracurricular

Answer 2

The machine-checked version of pad's proof in Agda:

module fibs where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

fib : ℕ → ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = fib n + fib (suc n)

f : ℕ → ℕ → ℕ → ℕ
f 0 a b = a
f (suc n) a b = f n b (a + b)

fib' : ℕ → ℕ
fib' n = f n 0 1

-- Exactly the theorem the user `pad` proposed:
Theorem : ℕ → Set
Theorem n = ∀ k → f n (fib k) (fib (suc k)) ≡ fib (k + n)

-- Helper theorems about natural numbers:
right-identity : ∀ k → k ≡ k + 0
right-identity zero = refl
right-identity (suc n) = cong suc (right-identity n)

1+m+n≡m+1+n : ∀ n k → suc (n + k) ≡ n + suc k
1+m+n≡m+1+n zero k = refl
1+m+n≡m+1+n (suc n) k = cong suc (1+m+n≡m+1+n n k)

-- The base case. 
-- Theorem 0 by definition expands to (∀ k → fib k ≡ fib (k + 0))
-- and we prove that using the right-identity theorem.
th-base : Theorem 0
th-base k = cong fib (right-identity k)

-- The inductive step.
-- The definitions are expanded automatically, so (Theorem (suc n)) is
--   (∀ k → f n (fib (suc k)) (fib (suc (suc k))) ≡ fib (k + suc n))
-- We can apply the induction hypothesis to rewrite the LHS to 
--   (fib (suc k + n))
-- which is equal to the RHS by the 1+m+n≡m+1+n theorem.
th-step : ∀ n → Theorem n → Theorem (suc n)
th-step n hyp k = trans (hyp (suc k)) (cong fib (1+m+n≡m+1+n k n))

-- The inductive proof of Theorem using th-base and th-step.
th : ∀ n → Theorem n
th zero = th-base
th (suc n) = th-step n (th n)

-- And the final proof:
fibs-equal : ∀ n → fib' n ≡ fib n
fibs-equal n = th n 0

Written

Answer 3

I believe your proof would be easier to recognize with Strong Induction:

... in the second step we may assume not only that the statement holds for n = m but also that it is true for all n less than or equal to m.

You were getting stuck here:

fib' (k+1)  = fib (k+1)
f (k+1) 0 1 = fib k + fib (k-1)

.. in part because you need to have both the steps from k+1 to k but also k+1 to k-1.

Sorry this isn't more convincing, it's been years since I've done real proofs.

Subtorrid

Answer 4

If the paper says it is equivalent to

Lemma:
f n (fib p) (fib (p+1)) = fib (p+n)

we should start by proving that. The key here is use generalized induction, that is, keep track of your forall quantifiers.

First we show

forall p, f 0 (fib p) (fib (p+1)) = fib p = fib (p + 0)

Now, we assume the inductive hypothesis

forall p, f n (fib p) (fib (p+1)) = fib (p + n)

and show

forall p, f (n+1) (fib p) (fib (p+1)) = f n (fib (p+1)) (fib (p+1) + fib p)
                                      = f n (fib (p+1)) (fib (p + 2)) --By def of fib
                                      = fib ((p + 1) + n) --By induction hypothesis
                                      = fib (p + (n+1))

So, that shows the lemma.

That makes it easy to prove your goal. If you have

fib' n = f n 0 1
       = f n (fib 0) (fib (0 + 1)) --by def of fib
       = fib (n + 1) --by lemma

Btw, if you are interested in this kind of thing, I suggest you check out Benjamin Pierce's free book on "Software Foundations." It is the textbook for a course on programming languages that uses the Coq proof assistant. Coq is like an uglier, meaner, and more powerful Haskell that lets you prove properties of your functions. It is good enough to do real math (prove of four color theorem), but the most natural thing to do in it is proven correct functional programs. I find it nice to have a computer check my work. And, all functions in Coq are total...

Materi

Answer 5

It is sometimes a good idea to not start out too formal. I think as soon as you see that the tail recursive version simply passes F(n-2) and F(n-1) around to avoid recalculation in each step, this gives you a proof idea, which you then formalize.

Cottar