Fibonacci numbers and the Stern-Brocot tree in Coq
Résumé
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).
Dans ce papier nous étudions les représentations d'un nombre au moyen d'autres nombres. Par exemple un entier peut être représenté de façon unique par une somme de puissances de deux, si chaque puissance de deux peut être utilisée au plus deux fois, le nombre de possibilités est $s_n$, une suite étudiée par Dijkstra, et qui possède de nombreuses propriétés intéressantes, prouvées formellement avec l'assistant de preuve Coq. Il s'avère que tout nombre rationnel s'écrit manière unique comme quotient $s_n/s_{n+1}$, ansi que l'a remarqué Stern; l'entier $n$ est relié au développement en fraction continue du rational $x$. Si l'on prend la représentation binaire de $n$ dans le sens opposé, on obtient une suite de nombres rationnels allant de 1 à $x$, en approchant de mieux en mieux $x$; ceci a été étudié par Brocot, d'où le nom d'arbre de Stern-Brocot. Un entier peut également être représenté comme somme de nombres de Fibonacci; nous étudions les propriétés de $R(n)$, le nombre de telles décompositions. Il y a unicité pour les prédécesseurs des nombre de Fibonacci; il y a également unicité si l'on rajoute des contraintes (il y a unicité deux nombres de Fibonacci consécutifs sont exclus, ou si la distance entre deux nombres est au maximum deux).
Domaines
Logiciel mathématique [cs.MS]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...