The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Adam Chlipala wrote:

> Adam Chlipala wrote:
>
> > Benjamin Werner wrote:
> >
> > > 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 :
> >
> >
> >
> > I think I've below defined True, False, eq, and nat without using 
> > inductive definitions or axioms.  I'm able to prove 0 \neq 1, and the 
> > induction scheme follows trivially from my definition of nat. 
>
>
> Oops.  I see that only the non-dependently-typed recursion principle 
> follows trivially, which I think is enough for "programming" but not 
> "proving" with nats.  It still looks to me like I have a faithful 
> encoding of nat in some sense, and I'm able to prove 0 \neq 1 about it.

Hi,
 Notice that your definitions make False, True, 0 <> 1 being 
inhabitants of Type (with some index >0), and
not plain propositions (i.e. of type Prop( at its turn of type Type(0)). 

Check (True:Prop).
Toplevel input, characters 837-841
> Check (True:Prop).
>        ^^^^
Error: The term "True" has type "Type" while it is expected to have type
"Prop"


Pierre


> --------------------------------------------------------
> 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