Views of Pi: definition and computation

Abstract : We study several formal proofs and algorithms related to the number π in the context of Coq's standard library. In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula). We give a formal description of the arctangent function and its expansion as a power series. We then study other possible descriptions of π, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides. In a third section, we concentrate on techniques to effectively compute approximations of π in the proof assistant by relying on rational numbers and decimal representations.
Keywords : Coq real analysis Pi
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, 7 (1), pp.105-129. 〈10.6092/issn.1972-5787/4343〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01074926
Contributeur : Yves Bertot <>
Soumis le : jeudi 16 octobre 2014 - 05:15:11
Dernière modification le : mercredi 12 septembre 2018 - 01:16:49

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Yves Bertot, Guillaume Allais. Views of Pi: definition and computation. Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, 7 (1), pp.105-129. 〈10.6092/issn.1972-5787/4343〉. 〈hal-01074926〉

Partager

Métriques

Consultations de la notice

254

Téléchargements de fichiers

234