# Prove correctness for computing the nth Fibonacci number for the pseudo code

How do we prove the correctness of this pseudo code by induction?

fastfib(integer n)
if n < 0 return 0;
else if n = 0 return 0;
else if n = 1 return 1;
else a ← 1; b ← 0;
for i from 2 to n do
t ← a; a ← a + b; b ← t;
return a;
end

• What did you try? Where did you get stuck? In particular: which induction hypothesis are you using? Are you stuck at the base case, or at the inductive step? We're happy to help you understand the concepts but just solving exercises for you is unlikely to achieve that. You might find this page helpful in improving your question. – Discrete lizard May 23 '17 at 9:16

The idea is that at the end of the $i$th iteration, $a = F_i$ and $b = F_{i-1}$. This is something that you can easily prove by induction. (Usually this sort of condition is called a loop invariant.)

Try to

• simplify the program and
• get it into a more functional form.

So

• Dump the negative case - there is no -3rd Fibonacci number.
• You can do without the explicit $1 \mapsto 1$. No times round the loop gives that result.
• The function applied round the loop is $[a, b] \mapsto [a+b, a]$.
• If you take $b$ instead of $a$, you can get rid of the $0 \mapsto 0$ case too.

You then have something you can reason inductively about.

I find it much more convincing with real than with pseudo code. Translating your pseudo-code into Clojure ...

(defn fast-fib [n]
(case n
0 0
1 1
(first
(nth (iterate
(fn [[a b]]
(let [t a
a (+ a b)
b t]
[a b]))
[1 0])
(- n 1)))))


... which the above transformations turn into the equivalent ...

(defn fast-fib [n]
(second
(nth (iterate
(fn [[a b]] [(+ a b) a])
[1 0])
n)))


... which is much easier to reason about.

Other functionally expressive programming languages are available.

Here's my approach:

First I check that the code is indeed possibly correct by checking that it gives the correct result for say all n ≤ 10. If not then you have your answer.

Second I determine the values of a and b for 2 ≤ i ≤ 10 and see if I can find a pattern. If I can't find a pattern then I ask for help. If I find a pattern, then I use induction to prove the following:

If n ≥ 2, then at the end of the loop the values of a and b will be xxx and yyy.


Obviously with values that immediately prove the code is correct.

It happens quite often that the desired statement cannot be proven by induction directly - in this case giving the correct result fib (n) for some n doesn't imply the correct result fib (n+1) for the next larger n. You need to prove something about a and b.