The Coq mailing list

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

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/