TY - JOUR AU - Sozeau, Matthieu PY - 2009/01/01 Y2 - 2024/03/29 TI - A New Look at Generalized Rewriting in Type Theory JF - Journal of Formalized Reasoning JA - JFR VL - 2 IS - 1 SE - Articles DO - 10.6092/issn.1972-5787/1574 UR - https://jfr.unibo.it/article/view/1574 SP - 41-62 AB - 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. ER -