A mathematical proof is generally made of clever deductions and mechanizable computations. However, current proof assistants (Coq, Lego, Nuprl, HOL, etc.) have a rather simple computation mechanism. Although they allow one to express many functions (any function whose existence is provable in intuitionist higher-order arithmetic), definitions can be uneasy and sometimes inefficient (they must follow a very restrictive schema similar to primitive recursion). Therefore, these systems do not allow one to define functions and predicates as one would like, which makes them difficult to use for non-specialists and restrict the use of computations in proofs: some propositions that could be proved automatically, by a simple computation, require complex deductions. Conversely, with a richer computation notion, but such that the equality of two terms remain decidable, it is not necessary to memorize the computation steps. Proofs are then reduced to true deductions. And the size of proofs is a critical problem in current proof assistants.
Definitions with rewrite rules are more general, easier and may be more efficient. However, considering functions or predicates defined by a set of a priori arbitrary rewrite rules raises an important problem: can we check whether a proof is correct? This is the decidability of "type checking".
In this talk, I will present the interest of extending the Calculus of Constructions with function and predicate definitions based on rewrite rules. Then, I will give general conditions ensuring the decidability of type-checking. These conditions generalize all the previous work on the combination lambda-calculus and rewriting, include the Calculus of Inductive Constructions with strong elimination and can also be applied to Natural Deduction Modulo.
(Frédéric comes from LRI, Université Paris-Sud; he is in the Computer Lab doing a postdoc with Larry Paulson.)