The Coq mailing list

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

[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/