The Coq mailing list

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

Hello, Aaron

 What you can do at a first step is to assume proof irrelevance on
even-ness:

 Theorem proof_irrelevance_for_even :
   forall n:nat , forall p p' : (even n) , (exist_even n p)=
                                           (exist_even n  p').
 Proof.
 Admitted.

 Then prove your induction scheme.


 If (and only if :-) ) you want to go further, have a look at Coq's FAQ, at
http://coq.inria.fr/doc-eng.html.

 You will find a proof in section 12 :"Case studies" that any pair of proofs 
of
  n<=m are equal.

 The possibility of proving such a theorem comes from the "determinism"
 on the predicate n<=m (for each pair n,m, there is  a unique constructor
 to apply). Since even seems to have the same property, you can adapt
 Hugo's proof.

 Please read also the subsection
 "Is there an axiom-free proof of Streicher's axiom K for the equality on 
nat?"
          and the following ones (in section 5.2 "Axioms")

  What standard axioms are inconsistent with Coq?
  What is Streicher's axiom K?
  What is proof-irrelevance?



Cheers,

Pierre

Selon 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
> >
>
> --------------------------------------------------------
> 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
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.