Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proving an induction principle on even numbers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving an induction principle on even numbers


chronological Thread 
  • From: Benjamin Werner <benjamin.werner AT polytechnique.fr>
  • To: Aaron Bohannon <bohannon AT cis.upenn.edu>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] proving an induction principle on even numbers
  • Date: Mon, 4 Apr 2005 16:17:55 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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






Archive powered by MhonArc 2.6.16.

Top of Page