Skip to Main content Skip to Navigation
Reports

Fibonacci numbers and the Stern-Brocot tree in Coq

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In this paper, we study the representation of a number by some other numbers. For instance, an integer may be represented uniquely as a sum of powers of two; if each power of two is allowed to appear at most twice, the number of representations is $s_n$, a sequence studied by Dijkstra, that has many nice properties proved here with the use of the proof assistant Coq. It happens that every rational number $x$ is uniquely the quotient $s_n/s_{n+1}$ as noticed by Stern, and that the integer $n$ is related to the continued fraction expansion of $x$. It happens that by reverting the bits on $n$, one gets a sequence of rational numbers with increasing denominators that goes from 1 to $x$ and becomes nearer at each iteration; this was studied by Brocot, whence the name Stern-Brocot tree. An integer can also be represented as a sum of Fibonacci numbers; we study $R(n)$ the number of such representations; there is uniqueness for the predecessors of Fibonacci numbers; there is also uniqueness under additional constraints (for instance, no two consecutive Fibonacci numbers can be used, or no two consecutive numbers can be omitted).
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-01093589
Contributor : José Grimm <>
Submitted on : Wednesday, December 10, 2014 - 6:32:58 PM
Last modification on : Friday, December 19, 2014 - 2:56:39 PM
Long-term archiving on: : Saturday, April 15, 2017 - 7:12:27 AM

File

RR8654.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01093589, version 1

Citation

José Grimm. Fibonacci numbers and the Stern-Brocot tree in Coq. [Research Report] RR-8654, Inria Sophia Antipolis. 2014, pp.76. ⟨hal-01093589v1⟩

Share

Metrics

Record views

25

Files downloads

43