Building decision procedures in the Calculus of Inductive Constructions. F. Blanqui, J.-P. Jouannaud and P.-Y. Strub. CSL'07. LNCS 4646.
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deductions in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P' obtained from P thanks to possibly complex calculations.
In this paper, we investigate a new version of the calculus of constructions which incorporates arbitrary decision procedures into deductions via the conversion rule of the calculus. Besides the novelty of the problem itself in the context of the calculus of constructions, a major technical innovation of this work lies in the fact that the computation mechanism varies along proof-checking: goals are sent to the decision procedure together with the set of user hypotheses available from the current context.
Our main result shows that this extension of the calculus of constructions does not compromise its main properties: confluency, strong normalization and decidability of proof-checking are all preserved. We also show in detail how a goal to be proved in the calculus of constructions is actually transformed into a goal in a decidable first-order theory. Based on this transformation, we are currently developping a new version of Coq implementing this calculus, taking linear arithmetic and the theory of lists as targets combined via Shostak's algorithm.