The Coq mailing list

[Benjamin Werner <Benjamin.werner AT inria.fr>]

Hi,


Le 9 janv. 06 à 13:46, Adam Chlipala a écrit :

> I know that the Calculus of Inductive Constructions was created  
> because the Calculus of Constructions was insufficient to represent  
> some inductive types.  Can anyone on this list give a short  
> characterization of which types require this extension, and/or  
> perhaps the simplest example of such a type?

It is not so much the question of "which types" but rather what you  
can do with them. Without inductive types, i.e. in raw CC, you :

* cannot prove 0 \neq 1

* cannot prove the induction scheme (or dependent matching for the  
matter)

* do not have constant-time reduction for the matching, and matching  
only works for closed terms.

You can get back some of the results in CC through mere axioms. But  
not the reduction behavior.

Cheers,


Benjamin



> I'm interested in this in the context of trying to minimize the  
> trusted code base needed to use results proved with Coq.  If  
> compiled developments can be translated to the Calculus of  
> Constructions, then I imagine it's possible to use a significantly  
> simpler checker.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club