It is commonly agreed that the success of future proof assistants will
rely in 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 in which computations are based on Shostak's congruence
closure algorithm. Besides the novelty of the problem itself, a major
technical innovation of this work lies in the fact that the
computation mecanism varies along the proof-checking. This is so
because the computation operating on propositions is based upon the
set of user hypotheses at hand, and therefore evolves with the proof
context.
Our main result shows that proof-checking remains decidable when
considering the congruence closure of the user equational hypotheses
on algebraic terms. We also discuss various possible extensions
opening quite new interesting perspectives from a theorem proving
point of view. In particular, we discuss in more details how the
present work can be generalized to the case where the notion of
computation is based on Shostak's algorithm for combining decision
procedures for convex theories.