The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

On Fri, Oct 09, 2009 at 10:57:20PM +0200, André Hirschowitz wrote:
> > I interprete this mistake as the violation of the typing rules, because
> > Nat is probably of higher Type level as the X of its definition.
> >
> > Is this true ? Does a means exist for circumventing this problem ?
> 
> Since "they" do not comment, let me say that I like the question, that I 
> agree with your understanding of the error, and that I do not see any 
> way around. So, this could eventually increase my interest in  the 
> impredicative Set option.

One of "them" can try to comment...

With Nat defined polymorphically in Type, you get the logical strength
of arithmetic and in particular 0<>1 (see Alexandre Miquel's PhD) but
a weak computational expressiveness (a priori Schwichtenberg-Statman
representability result for the type (X->X)->(X->X) applies and only
the functions built from addition, multiplication and if-zero will be
representable as lambda-terms; the other functions will only be
definable as logical relations of the form "forall n m, IsNat n ->
IsNat m -> exists p, IsNat p /\ [a relational specification of the
function]" where "IsNat m" expresses that n satisfies induction on Nat).

On the other side, with Nat defined polymorphically in impredicative
Set (with option -impredicative-set), you get a full recursor
"Nat_rec" and at least the computational expressiveness of system T
but you cannot derive 0<>1 (and the recursor has a bad complexity due
to the linear complexity of the predecessor).

Hence, unless we are concerned by theoretical investigations, there is
no reason in practice not to prefer the inductive definition (i.e. the
definition of the standard library) which has all the good properties
we expect.

Hugo Herbelin

On Thu, Oct 08, 2009 at 10:24:32AM +0200, Jean-Francois Dufourd wrote:
> Hi,
>
> I'm trying to (impredicatively) define the type Nat in Coq
> (without the option - impredicative-set, which works well).
>
> I write:
>
> Definition Nat:=forall X:Type,(X->X)->X-> X.
>
> Definition succ(n:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => (f (n X f z)).
>
> Definition add(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X f (n X f z).
>
> Definition mult(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X (n X f) z.
>
> All that is OK. But, when I write an other version of mult:
>
> Definition mult1(n m:Nat):Nat:=
> n Nat (add m) zero.
>
> Coq answers "Universe inconsistency".