Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve
Résumé
In this thesis, we are interested in the cooperation of first-order rewriting and constructive type theory to improve the automation of computer-aided proofs. We aim to integrate (simple, conditional or AC) rewriting in the Coq proof assistant by an automatic, safe and efficient means using an external programming environment ELAN. Two different approaches are investigated. In the mixed approach, ELAN is used as an external rewriting engine for normalising terms in a reflexive rewriting tactic in Coq. The normalisation trace generated by ELAN is replayed in Coq to compute the corresponding normal form. In order to improve the performance of this reflexive tactic, we show how to use lazy rewriting for producing compact normalisation traces.The second approach called external is more flexible since it also covers several useful extensions of term rewriting such as conditional rewriting and AC rewriting, and it can be easily adapted to other proof assistants. In this approach, term rewriting is entirely performed in ELAN and proof assistants are only used for checking purpose. We formalise the notion of proof term for ELAN computations in the rewriting calculus with explicit substitutions. We investigate the equivalent properties of the proof terms and translate them into the syntax of proof assistant in order to check the corresponding computations. By this work, non-deterministic ELAN computations can be independently certified and we obtain term rewriting in proof assistant. In order to speed up proof-checking of the computations involving AC rewriting, we also propose an efficient method for proving equalities modulo AC based on the syntacticness of AC theories. These results have been integrated in a new ELAN-based rewriting tactic in Coq.
Nous étudions dans cette thèse une coopération entre la réécriture du premier ordre et la théorie constructive des types pour automatiser les preuves assistées par l'ordinateur. Nous cherchons par ce travail à mettre en oeuvre la réécriture de manière automatique, sûre et efficace dans l'assistant de preuve Coq à l'aide d'un environnement de programmation externe (ELAN). Deux approches différentes sont étudiées.Dans l'approche mixte, ELAN est utilisé comme un moteur de réécriture externe pour la normalisation des termes dans une tactique réflexive de réécriture en Coq. La trace générée par ELAN de la normalisation est rejouée en Coq pour calculer la forme normale. Afin d'améliorer la performance de la tactique réflexive, nous montrons comment utiliser la réécriture paresseuse pour obtenir une meilleure trace de normalisation.La deuxième approche, appelée externe, est plus flexible car d'une part, elle permet d'obtenir également plusieurs extensions utiles de la réécriture telles que la réécriture conditionnelle ou bien la réécriture modulo l'associativité et la commutativité (AC), et d'autre part, elle peut être facilement adaptée pour d'autres assistants de preuve. Dans cette approche, la réécriture est effectuée entièrement en ELAN et les assistants de preuve ne servent qu'à la vérifier. Nous formalisons donc la notion de terme de preuve des calculs ELAN dans le calcul de réécriture avec substitutions explicites. Nous étudions les propriétés des termes de preuve et les traduisons en syntaxe de l'assistant de preuve pour vérifier les calculs correspondants. Par conséquent, les calculs non-déterministes en ELAN peuvent être certifiés indépendamment, et nous disposons de la réécriture dans l'assistant de preuve. Afin d'améliorer la performance de la vérification des calculs concernant la réécriture modulo AC, nous proposons également une méthode de preuve efficace pour les égalités modulo AC en se basant sur la syntaxicité des théories AC. Ces résultats ont été intégrés dans une nouvelle tactique de réécriture ELAN en Coq.