From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

TL;DR

This paper introduces a new version of the Calculus of Inductive Constructions that integrates first-order decision procedures, making proofs more aligned with mathematicians' practices and ensuring soundness through certificate verification.

Contribution

It proposes the Calculus of Congruent Inductive Constructions, extending CIC with first-order decision procedures that maintain soundness via certificate checking.

Findings

The system integrates decision procedures into proof construction.

Proof style becomes closer to traditional mathematical reasoning.

Soundness is guaranteed through certificate verification.

Abstract

We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order decision procedures: deduction is still in charge of the CIC kernel, while computation is outsourced to dedicated first-order decision procedures that can be taken from the shelves provided they deliver a proof certificate. The soundness of the whole system becomes an incremental property following from the soundness of the certificate checkers and that of the kernel. A detailed example shows that the resulting style of proofs becomes closer to that of the working mathematician.