The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Adam's posts reminded me that, of course, such an axiomatization cannot 
do everything the built-in type nat can.  In particular, we cannot 
supply them as arguments to dependent types in a generally useful way 
because type equality is intensional in Coq.

Also, I don't know why I thought recursion should only be allowed at 
sort Set.  It works fine at Type.

Other than this, are there any other improvement for my axiomatization 
or any more comments about additional techniques?

Aaron

On Jan 13, 2006, at 5:44 PM, Aaron Bohannon wrote:

> I know that one of the great things about Coq is that inductive 
> datatypes are built into the language.  However, in trying to 
> understand the theory of inductive datatypes better, I would like to 
> know how one might axiomatize the natural numbers in such a way that 
> the axiomatized theory is equivalently powerful to the inductive type 
> nat.
>
> I have included my first attempt below, written as a module signature. 
>  I essentially just added two axioms about recursion to the usual 
> Peano axioms.  It appears to be sound because I can implement such a 
> module based upon the type nat.  (See further below.)  However, can 
> someone tell me if my axioms are powerful enough to do everything with 
> the natural numbers that I can do with Coq's built-in type?
>
> Also, are there other reasonable ways to axiomatize inductive types?  
> Are there some good papers or references on this topic that someone 
> can point me to?
>
> Thanks,
> Aaron
>
>
> Module Type NAT.
>   Parameter N : Set.
>   Parameter zero : N.
>   Parameter succ : N -> N.
>
>   Section Properties.
>     Variables m n : N.
>
>     Axiom discriminate_zero_succ : zero <> succ n.
>     Axiom injective_succ : succ m = succ n -> m = n.
>
>     Axiom N_rect :
>       forall P : N -> Type,
>       P zero ->
>       (forall n : N, P n -> P (succ n)) ->
>       forall n : N, P n.
>
>     Variable F : N -> Set.
>     Variable f_zero : F zero.
>     Variable f_succ : forall n : N, F n -> F (succ n).
>     Let f := N_rect F f_zero f_succ.
>
>     Axiom N_rec_zero : f zero = f_zero.
>     Axiom N_rec_succ : f (succ n) = f_succ n (f n).
>
>   End Properties.
> End NAT.
>
> Module Nat : NAT.
>   Definition N := nat.
>   Definition zero := O.
>   Definition succ := S.
>   Definition discriminate_zero_succ := O_S.
>   Definition injective_succ := eq_add_S.
>   Definition N_rect := nat_rect.
>   Section Recursion.
>     Variable n : N.
>     Variable P : N -> Set.
>     Variable f_zero : P zero.
>     Variable f_succ : forall n : N, P n -> P (succ n).
>     Let f := N_rect P f_zero f_succ.
>
>     Lemma N_rec_zero : f zero = f_zero.
>     Proof refl_equal (f_zero).
>
>     Lemma N_rec_succ : f (succ n) = f_succ n (f n).
>     Proof refl_equal (f_succ n (f n)).
>
>   End Recursion.
> End Nat.
>
>
> --
> Aaron Bohannon
> http://www.cis.upenn.edu/~bohannon/
>
> --------------------------------------------------------
> 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

--
Aaron Bohannon
http://www.cis.upenn.edu/~bohannon/