Multiples in the Fibonacci series

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:

\pexp{\text{$\fapp{fib}{(n{\times}k)}$ is a multiple of $\fapp{fib}{k}$}}
\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}}

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!

Related Posts:

New domain name (

Some people were complaining about the domain, because it was a bit long and they never got the number of r’s in Ferreira right. From today, they can’t complain anymore!

The new and official URL of this website is now shorter and r’s-free: .

If you don’t like it and prefer the old one, please let me know!

Related Posts:

A reward check from Donald Knuth

The other day I went to my pigeon-hole to collect my snail mail, and I had a letter from Donald E. Knuth, Professor Emeritus of the Art of Computer Programming!

Cover of the letter that Knuth sent to Joao

Inside, there was a check for a correction I sent him some months ago. In fact, it was not really a correction; it was more like a comment. And it was so obvious (he even said that) that he just sent $\$$0.32, instead of the usual $\$$2.56. But hey, who cares? I’ve got Knuth’s autograph now :-)

A reward check from Donald Knuth

Perhaps I should set as one of my goals to find a proper error, so that I can receive a $\$$2.56 check :) By the way, the errata of the Concrete Mathematics is available online and this particular omission is documented as follows:

page 338, line 2 from the bottom
change “for $z$” to “for $z$ and multiplying by $a$”

Related Posts:

Calculational proofs are usually direct

jd2718 asked in his blog if anyone knew a direct proof of the irrationality of $\sqrt{2}$. In this post I present a proof that, even if some don’t consider it direct, is a nice example of the effectiveness of calculational proof. But first, there are two concepts that need to be clarified: direct proof and irrational number.

Direct proofs

The concept of direct proof can vary slightly from person to person. For instance, Wikipedia defines it as:

In mathematics and logic, a direct proof is a way of showing the truth or falsehood of a given statement by a straightforward combination of established facts, usually existing lemmas and theorems, without making any further assumptions.

Alternatively, in Larry W. Cusick’s website we can read:

A direct poof [sic] should be thought of as a flow of implications beginning with “P” and ending with “Q”.

P -> … -> Q

Most proofs are (and should be) direct proofs. Always try direct proof first, unless you have a good reason not to.

I consider the wording ‘without making any further assumptions‘ in the first definition ambiguous and I don’t understand why the second definition only applies to implications. But anyway, with these definitions in mind, a direct proof for the irrationality of $\sqrt{2}$ can be something like:

\pexp{\text{$\sqrt{2}$ is irrational}}

Or, alternatively, we can also use a proof of the following shape:

\pexp{\text{$\sqrt{2}$ is irrational}}

Irrational numbers

An irrational number is a real number that can’t be expressed as a simple fraction. Therefore, the number $\sqrt{2}$ is irrational because for all integers $m$ and $n$, with $n$ non-negative, we have that:

\sqrt{2} \neq \frac{m}{n} ~~.

A direct proof for the irrationality of $\sqrt{2}$

Now that we have clarified the concepts above, we prove that $\sqrt{2}$ is irrational. For all integers $m$ and $n$, with $n$ non-negative, we have:

\pexp{\sqrt{2} \neq \frac{m}{n}}
\hint{=}{Use arithmetic to eliminate the square root operator.}
\hintf{\Leftarrow}{Two values are different if applying the same function to them}
\hintl{yields different values.}
\pexp{\fapp{exp}{(n^2{\times}2)} \neq \fapp{exp}{m^2}}
\hintf{=}{Now we choose the function $exp$.}
\hintm{Let $\fapp{exp}{k}$ be the number of times that $2$ divides $k$.}
\hintm{The function $exp$ has two important properties:}
\hintm{$~~~\fapp{exp}{2}=1$ and}
\hintm{$~~~\fapp{exp}{k{\times}l} = \fapp{exp}{k} + \fapp{exp}{l}$}
\hintl{We apply these properties to simplify the left and right sides.}
\pexp{1{\,+\,}2{\times}\fapp{exp}{n} ~\neq~ 2{\times}\fapp{exp}{m}}
\hintf{=}{The left side is an odd number and the right side is an even}
\hintl{number. Odd numbers and even numbers are different.}
\pexp{true ~~.}

Note that, unlike traditional proofs, we don’t assume that $m$ and $n$ are co-prime, nor that $\sqrt{2}$ is a rational number. We simply derive the boolean value of the expression $\sqrt{2}~{\neq}~{\frac{m}{n}}$.

If you have any suggestions or corrections, please leave a comment. I’d be more than happy to hear from you.

Note: I learnt the contrapositive of this proof from Roland Backhouse (page 38, Program Construction — Calculating Implementations from Specifications).

Related Posts:

In Defense Of Computer Science

Very good post from Paper Trail:

So why study computer science? The job prospects at the end are usually pretty good – because, if nothing else, you can become a pretty good software developer fairly quickly – but they are unknown. My argument is that the study of computer science is enough of an incentive enough to make it worthwhile.

Related Posts: