HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:55:09 PM
Last modification on : Friday, February 4, 2022 - 3:32:52 AM


  • HAL Id : inria-00101055, version 1



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⟩



Record views