The Coq mailing list

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

Aaron Bohannon wrote:

> 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



Hi Aaron,

It seems you don't need these axioms

> Axiom discriminate_zero_succ : zero <> succ n.
> Axiom injective_succ : succ m = succ n -> m = n.

since you can derive them from N_rect.

N_rect (and the axioms N_rec_zero and N_rec_succ) are enough to build a 
predicate is_Zero (for proving
0 <> succ n) and the predecessor function (for proving that succ is 
injective).

Please find attached this version of your development (without modules, 
but it should be easy to write some
functors).

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



  Parameter N : Set.
  Parameter zero : N.
  Parameter succ : N -> N.

  Section Properties.

  Axiom N_rect :
     forall P : N -> Type,
      P zero ->
      (forall n : N, P n -> P (succ n)) ->
      forall n : N, P n.


  Section N_rect_axioms.

  Variables m n : N.

     
    Variable F : N -> Type.
    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 N_rect_axioms.


    Definition is_Zero := N_rect (fun _ => Prop) True (fun _ H => False).
   
    Remark R1 : is_Zero zero.
     unfold is_Zero.   
     rewrite N_rec_zero.
     trivial.
    Qed.

    Remark R2 : forall n, ~is_Zero (succ n).
     unfold is_Zero.
     red;intros.
     rewrite N_rec_succ in H.
     auto.
    Qed.  

    Lemma discriminate_zero_succ : forall n, zero <> succ n.
    Proof.
     intros n H.
     apply (R2 n).
     case H.
     apply R1.
    Qed.


   Definition pred := N_rect (fun _ => N) zero (fun p q => p).

   Lemma pred_of_zero : pred zero = zero.
   Proof.
    unfold pred.
    rewrite N_rec_zero;trivial.
   Qed.

   Lemma pred_of_succ : forall n, pred (succ n) = n.
   Proof.
    intros.
    unfold pred;rewrite N_rec_succ.
    trivial.
   Qed.

   Lemma N_inj : forall n p, succ n = succ p -> n = p.
   Proof.
    intros.
    assert (pred (succ n) = pred (succ p)).
    rewrite H;trivial.
    do 2 rewrite pred_of_succ in H0.
    trivial.
   Qed.

  End Properties.