I found the following problem on K. Rustan M. Leino’s puzzles page:

[Carroll Morgan told me this puzzle.]

Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence.

More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n). Prove that for any positive K and natural n, F(n*K) is a multiple of F(K).

This problem caught my attention, because it looks like a good example for using a result that I have derived last year. My result gives a reasonable sufficient condition for showing that a function distributes over the greatest common divisor and shows that the Fibonacci function satisfies the condition.

In fact, using the property that the Fibonacci function distributes over the greatest common divisor, we can solve this problem very easily. Using $\fapp{fib}{n}$ to denote the Fibonacci number $n$, $m{\nabla}n$ to denote the greatest common divisor of $m$ and $n$, and $\setminus$ to denote the division relation, a possible proof is:

\[

\beginproof

\pexp{\text{$\fapp{fib}{(n{\times}k)}$ is a multiple of $\fapp{fib}{k}$}}

\hint{=}{definition}

\pexp{\fapp{fib}{k} \setminus \fapp{fib}{(n{\times}k)}}

\hint{=}{rewrite in terms of $\nabla$}

\pexp{\fapp{fib}{k} ~\nabla~ \fapp{fib}{(n{\times}k)} ~=~ \fapp{fib}{k}}

\hint{=}{$fib$ distributes over $\nabla$}

\pexp{\fapp{fib}{(k{\nabla}(n{\times}k))} = \fapp{fib}{k}}

\hint{=}{$k{\nabla}(n{\times}k) = k$}

\pexp{\fapp{fib}{k} = \fapp{fib}{k}}

\hint{=}{reflexivity}

\pexp{true~~.}

\endproof

\]

The crucial step is clearly the one where we apply the distributivity property. Distributivity properties are very important, because they allow us to rewrite expressions in a way that prioritizes the function that has the most relevant properties. In the example above we could not simplify $\fapp{fib}{k}$ nor $\fapp{fib}{(n{\times}k)}$, but applying the distributivity property prioritised the $\nabla$ operator — and we know how to simplify $k{\nabla}(n{\times}k)$. Furthermore, in practice, distributivity properties reduce to simple syntactic manipulations, thus reducing the introduction of error and simplifying the verification of our arguments.

(Now that I think about it, perhaps it would be a good idea to write a note on distributivity properties, summarizing their importance and their relation with symbol dynamics.)

If you have any corrections, questions, or alternative proofs, please leave a comment!

Can you help me understand your second equality?

Hi Hugo,

If fib.k divides fib.(n*k), then the greatest common divisor of fib.k and fib.(n*k) is fib.k (it divides both, and is the largest divisor of itself).

Also, if fib.k is the greatest common divisor of itself and fib.(n*k), then it clearly divides fib.(n*k).

Do you agree?

Joao

That’s right, I disregarded fib.(n*k) represents a number, thanks for the help. Congratulations! Your work it’s really interesting.

Yes, it’s just the (n*k)th Fibonacci number Thanks for your comments!

I tried to prove it using induction.

for k =1; F(k) = 1; so all F(n*k) are divisible by F(k)

Let’s assume for k, the proposition is true ie F(n*k) is a muliple of F(k)

Now we use the fact(I do not have a proof for it. This is based on observation.) that F(n*(k+1)) = [ F(k+1)]*F(n*k)+ [F(k)]*F(n*k-1)

Which clearly means that F(n*(k+1)) also is divisible by F(k).

-Manish

Th

Dear Manish,

thanks for your comment. First, I don’t know why you say that the property you use is a fact. If you replace n by 2 and k by 1, the lefthand side becomes fib.(2*(1+1)) = fib.4 = 3 . On the other hand, the righthand side becomes fib.(1+1)*fib.(2*1) + fib.(1)*fib.(2*1-1) = fib.2 * fib.2 + fib.1 * fib.1 = 1*1 + 1*1 = 2 . Clearly, the property is not valid.

Second, the nice thing about formulating and using distributivity properties is that the induction is somehow hidden. If you read JFF0 (it’s in the Publications page), you see that the induction process is formulated in terms of loop invariance. Also, by formulating sufficient conditions for a function to distribute over the greatest common divisor, we avoid doing induction everytime.

Joao