Definitions by Rewriting in the Calculus of Constructions

TL;DR

This paper extends the Calculus of Constructions with rewrite rules for predicates, proving strong normalization under certain conditions, and demonstrating applicability to systems like Coq and Natural Deduction Modulo theories.

Contribution

It introduces predicate definitions via rewrite rules in the Calculus of Constructions and proves strong normalization for the extended system under broad conditions.

Findings

Strong normalization of the extended calculus is proven.

Applicable to Coq's subsystem and Natural Deduction Modulo theories.

Conditions for confluence and syntactic criteria are established.

Abstract

The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prove the strong normalization of the reduction relation generated by the beta-rule and the user-defined rules under some general syntactic conditions including confluence. As examples, we show that two important systems satisfy these conditions: a sub-system of the Calculus of Inductive Constructions which is the basis of the proof assistant Coq, and the Natural Deduction Modulo a large class of equational theories.