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
Résumé : 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).
Type de document :
Rapport
[Research Report] RR-8654, Inria Sophia Antipolis; INRIA. 2014, pp.76
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01093589
Contributeur : José Grimm <>
Soumis le : mardi 16 décembre 2014 - 09:11:27
Dernière modification le : jeudi 11 janvier 2018 - 16:23:52
Document(s) archivé(s) le : samedi 15 avril 2017 - 09:13:37

Fichier

RR8654-v2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01093589, version 2

Collections

Citation

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

Partager

Métriques

Consultations de la notice

189

Téléchargements de fichiers

473