Thm* n:. CoPrime(fib(n),fib(n+1))

The Fibonacci function is defined recursively like this:

fib(n) == if n=0  n=1 1 else fib(n-1)+fib(n-2) fi.

We prove this by true-for-less induction after eliminating CoPrime(a,b) via the equivalence

Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1).

So under the inductive hypothesis

k:. k<n  (x,y:. fib(k)x+fib(k+1)y = 1)

we must show

a,b:. fib(n)a+fib(n+1)b = 1

(we changed binding variable names to avoid confusion).

Consider the two cases of how fib(n+1) computes.

If it takes the first branch and computes to 1, then our goal is obviously satisfied by using 0 for a and 1 for b.

If fib(n+1) takes the other branch, then we must show that

a,b:. fib(n)a+(fib(n)+fib(n-1))b = 1,

which reduces by algebraic rearrangement to showing

a,b:. fib(n-1)b+fib(n)(a+b) = 1.

But applying our inductive hyp to n-1 (for k<n) we get

fib(n-1)x+fib(n)y = 1, for some x and y,

so using x for b and y-x for a,

fib(n-1)x+fib(n)(y-x+x) = 1 satisfies our goal.

QED

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html