The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.fr>]

Hi,


The main reason your definition is difficult to handle, is that an 
object of type even_nat contains not only a natural number, but also a 
proof that it is even. But obviously, you want the predicates over 
even_nat do depend only upon the number and not the proof.

In order to prove even_nat_ind, you would therefore first need to prove 
something like:

 forall n:nat , forall p p' : (even n) , (exist_even n p)=(exist_even n 
p').

which should be feasible but a little tedious. Then you could prove 
your principle by induction over the natural number.

All in all, I am however afraid that for the moment, you will be better 
of by using properties over the full type nat, even when you prove 
facts about natural numbers. This involves droping your even_nat type.


Things would change if the conversion rule of Coq would include 
proof-irrelevance (that is identify all proof of a same proposition). I 
tend to advocate this change, but there are no imminent plans to 
perform it.


Best wishes,


Benjamin


Le 3 avr. 05, à 22:53, Aaron Bohannon a écrit :

> [I sent this a couple of days ago, but it didn't show up on the list, 
> so I'm resending it.]
>
> I'm just a beginner with Coq, and I'd like to see how I can prove an 
> induction principle on the even numbers to get a feel for working with 
> the weak sum types.  Here's what I've got:
>
> Inductive even : nat -> Prop :=
>   | zero_even : even O
>   | ss_even : forall n : nat, even n -> even (S (S n)).
>
> Definition even_nat := {n : nat | even n}.
> Definition exist_even := exist (fun x : nat => even x).
>
> Definition even_O : even_nat := exist_even O zero_even.
> Definition even_SS (en : even_nat) : even_nat :=
>   match en with
>   exist n p => exist_even (S (S n)) (ss_even n p)
>   end.
>
> Lemma even_nat_ind :
>   forall P : even_nat -> Prop,
>   P even_O ->
>   (forall en : even_nat, P en -> P (even_SS en)) ->
>   forall en : even_nat, P en.
> Proof.
> ...
>
>
> How does this proof go?  The furthest I could get is "intros; case en; 
> intros."  After that I would expect to do induction over the 
> definition of the "even" predicate, but I can't seem to make headway 
> due to unification problems.  I have tried to read all relevant 
> sections of Coq'Art but can't seem to apply its advice to this 
> particular situation.  And I'm really curious to find out the right 
> way to do it.
>
> --
> 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