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 :
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : José Grimm <>
Submitted on : Tuesday, December 16, 2014 - 9:11:27 AM
Last modification on : Thursday, January 11, 2018 - 4:23:52 PM
Long-term archiving on : Saturday, April 15, 2017 - 9:13:37 AM


Files produced by the author(s)


  • HAL Id : hal-01093589, version 2



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



Record views


Files downloads