Modules in Coq are and will be correct

Abstract

The paper presents the system of named modules implemented in Coq version 7.4 and shows that this extension is conservative. It is also shown that the implemented module system is ready for the future planned extension of Coq with definitions of functions by means of rewrite rules. More precisely, the impact of the module system on the acceptance criterion for rewrite rules is carefully studied, leading to the formulation of four closure properties that have to be satisfied by the acceptance criterion in order to validate the conservativity proof. It turns out that syntactic termination criteria such as Higher Order Recursive Path Ordering or the General Schema can be adapted to satisfy these closure properties. © Springer - Verlag 2004.