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!
Related Posts:
