Proof by computation in the Coq system

AbstractIn informal mathematics, statements involving computations are seldom proved. Instead, it is assumed that readers of the proof can carry out the computations on their own. However, when using an automated proof development system based on type theory, the user is forced to find proofs for all claimed propositions, including computational statements. This paper presents a method to automatically prove statements from primitive recursive arithmetic. The method replaces logical formulas by boolean expressions. A correctness proof is constructed, which states that the original formula is derivable, if and only if the boolean expression equals true. Because the boolean expression reduces to true, the conversion rule yields a trivial proof of the equality. By combining this proof with the correctness proof, we get a proof for the original statement