A New Look at Generalized Rewriting in Type Theory

Abstract : Rewriting is an essential tool for computer-based reasoning, both automated and assisted. This is because rewriting is a general notion that permits modeling a wide range of problems and provides a means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. This can be done provided the necessary proofs that functions appearing in goals are congruent with respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof assistant, making essential use of the expressive power of dependent types and the recently implemented type class mechanism. The new rewrite tactic improves on and generalizes previous versions by natively supporting higher-order functions, polymorphism and subrelations. The type class system inspired by Haskell provides a perfect interface between the user and the tactic, making it easily extensible.
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2009, 2 (1), pp.41-62
Liste complète des métadonnées

Contributeur : Matthieu Sozeau <>
Soumis le : mardi 4 octobre 2011 - 14:50:55
Dernière modification le : jeudi 7 février 2019 - 16:29:29


  • HAL Id : inria-00628904, version 1


Matthieu Sozeau. A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning, ASDD-AlmaDL, 2009, 2 (1), pp.41-62. 〈inria-00628904〉



Consultations de la notice