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.