Abstract: Proof assistants and rewriting techniques: an experiment with Coq and Elan

Helene Kirchner

We present an approach to combine the Coq proof assistant, based on calculus of constructions, with the Elan deduction system, based on rewriting calculus. Our objective is to implement in Coq a class of decision procedures using rewriting techniques. The approach relies on a normalisation tactic in associative and commutative theories that generates a proof term in rewriting calculus, translated into a proof term in calculus of constructions, that can be checked by Coq to get the proof of the normalisation process.