Hal will be stopped for maintenance from friday on june 10 at 4pm until monday june 13 at 9am. More information
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 metadata

https://hal.inria.fr/hal-01093589
Contributor : José Grimm Connect in order to contact the contributor
Submitted on : Wednesday, December 10, 2014 - 6:32:58 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 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

214

Files downloads

579