The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Mon, Jun 22, 2009 at 11:34:03AM +0100, Neil Ghani wrote:

> 2. What are the principles underlying the induction principles Coq
>    generates?

In the end, it is the "structurally smaller" criterion of recursive
definitions (fixpoints).

See
http://coq.inria.fr/coq/distrib/current/refman/Reference-Manual006.html#htoc101
for a partial presentation of it.

> I believe they are added as axioms every time an inductive data type
> is declared.

That is not correct. They are just automatically generated
definitions. They are as much axioms as proofs generated with "auto."
:)

You can see them like any definition with the "Print" command:
 Print YourType_rect.
 Print YourType_rec.
 Print YourType_ind.

Other schemes can be generated (still as definitions, not axioms) with
the "Scheme" command, see
http://coq.inria.fr/coq/distrib/current/refman/Reference-Manual011.html#@default679

> Do they just look right or are they proven to be correct in a
> mathematical sense? If the later, could I get a response with a
> reference please?

Well, they are "proven correct" in the sense that they are definitions
/ proofs in the pCIC, which is supposed to accept only valid
proofs. pCIC might be inconsistent, or the Coq implementation may have
a bug leading to its accepting a proof/definition it should not. The
Reference Manual used to have pointers to papers explaining some
aspects of (a calculus related to) pCIC, at least some of which spoke
about the positivity criterion for inductive definitions and fixpoint
acceptance condition, but they seem to be gone now. For hints that
pCIC might be approximately as consistent as other "well-known"
foundations to mathematics, probably somebody else will have better
pointers, but I remember papers by Alexandre Miquel and at least one
by Benjamin Werner.

-- 
Lionel