Contributions à la certification des calculs dans R : théorie, preuves, programmation
Institution:
NiceDisciplines:
Directors:
Abstract EN:
The Coq system is a proof assistant based on the Calculus of Inductive Constructions. In this work, we propose to enhance the automation of this system by providing a reflexive and complete decision procedure for the first order theory of real numbers. The Type Theory implemented by the Coq system comprises a typed functional programming language, which we have used to implement a Cylindrical Algebraic Decomposition algorithm (CAD). This algorithm computes a partition of the space into sign-invariant, semi-algebraic cells for the polynomials of a given family. Hence it allows deciding all the formulae of this theory. Then we have to prove formally the corrections of the algorithm and of the related decision procedure, using the Coq proof assistant. This work includes a library for certified polynomial arithmetic and a significant part of the format proof of correctness of the sub-resultants algorithm. This last algorithm allows computing efficiently the greatest common divisor of polynomials with coefficients in a ring, and in particular of multivariate polynomials. We also propose a reflexive tactic for deciding equalities in ring and semi-ring structures, which enhances the performances of the tool previously available in the system by taking benefit of the computational abilities of the system. In a last part, we study the computational content of a constructive proof of an elementary lemma of real analysis, called principle of open induction.
Abstract FR:
Le logiciel Coq est un assistant à la preuve basé sur le Calcul des Constructions Inductives. Dans cette thèse, nous proposons d’améliorer l’automatisation de ce système en le dotant d’une procédure de décision réflexive et complète pour la théorie du premier ordre de l’arithmétique réelle. La théorie des types implémentée par le système Coq comprend un langage fonctionnel typé dans lequel nous avons programmé un algorithme de Décomposition Algébrique Cylindrique (CAD). Cet algorithme calcule une partition de l’espace en cellules semi-algébriques sur lesquelles tous les polynômes d’une famille donnée ont un signe constant et permet ainsi de décider les formules de cette théorie. Il s’agit ensuite de prouver la correction de l’algorithme et de la procédure de décision associée avec l’assistant de la preuve Coq. Ce travail comprend en particulier une librairie d’arithmétique polynomiale certifiée et une partie significative de la preuve formelle de correction de l’algorithme des sous-résultants. Ce dernier algorithme permet de calculer efficacement le plus grand commun diviseur de polynômes à coefficients dans un anneau, en particulier à plusieurs variables. Nous proposons également une tactique réflexive de décision des égalités dans les structures d’anneaux et de semi-anneaux qui améliore les performances de l’outil déjà disponible et augmente son spectre d’action en exploitant les possibilités de calcul du système. Dans une dernière partie, nous étudions le contenu calculatoire d’une preuve constructive d’un lemme élémentaire d’analyse réelle, le principe d’induction ouverte.