External rewriting for skeptical proof assistants (extended version)

Quang-Huy Nguyen 1 Claude Kirchner 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents the design, the implementation and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external since it consists in performing term rewriting in a specific and efficient environment and to check the computations later in a proof assistant. Two typical systems are considered in this work, \elan, based on the rewriting calculus, as the term rewriting based environment, and \coq, based on the calculus of inductive constructions as the proof assistant. We first formalize the proof terms for deduction by rewriting and strategies in \elan\ using the rewriting calculus with explicit substitutions. We then show how these proof terms can soundly be translated into \coq-syntax where they can be directly type checked. For the method to be applicable for proving equalities modulo an equational theory that contains associativity and commutativity, we provide an effective method to prove equalities modulo associativity and commutativity in \coq\ using \elan. These results have been integrated into an {\elan} based rewriting tactic in \coq.
Type de document :
Rapport
[Intern report] A02-R-099 || nguyen02a, 2002, 45 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00101055
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:55:09
Dernière modification le : vendredi 25 mai 2018 - 01:40:29

Identifiants

  • HAL Id : inria-00101055, version 1

Citation

Quang-Huy Nguyen, Claude Kirchner, Hélène Kirchner. External rewriting for skeptical proof assistants (extended version). [Intern report] A02-R-099 || nguyen02a, 2002, 45 p. 〈inria-00101055〉

Partager

Métriques

Consultations de la notice

157