Construction des nombres algébriques réels en Coq

• exposé

février 2012 Journées Francophones des Langages Applicatifs JFLA12 Construction des nombres algébriques réels en Coq Cyril Cohen INRIA Saclay–Île-de-France Laboratoire d'Informatique de l'École polytechnique, 91128 Palaiseau CEDEX, France Résumé Cet article présente une construction en Coq de l'ensemble des nombres algébriques réels, ainsi qu'une preuve formelle que cet ensemble est muni d'une structure de corps réel clos discret archimédien. Cette construction vient ainsi implémenter une interface de corps réel clos réalisée dans un travail antérieur et bénéficie alors de la propriété d'élimination des quantificateurs, formellement prouvée pour toute instance de l'interface.

• réels en coq
• librairie ssreflect
• structure de corps réel
• bibliothèque ssreflect sur les structures de choix
• structures de la hiérarchie algébriques
• polynômes
• polynôme
• propriété
• propriétés
• réelle
• réel
• réels
• réelles
• preuve
• preuves
• égalités
• egalité
• égalité