The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Fri, Aug 01, 2008 at 12:36:22PM +0200, 
Cedric.Auger AT lri.fr
 wrote:
> I want to make very simple enumerated types,
> so I did:
> 
> Inductive enums : nat -> Set :=
> | New : forall n, enums n
> | Old : forall n, enums n -> enums (S n).
> Implicit Arguments New [n].
> Implicit Arguments Old [n].
> 
> Set Printing All.
> 
> Lemma e : forall (e : enums 0), e = New.
> intros.
> (*
> Now I want to destruct e
> *)
> induction e.
> (*
> all occurences of O have been replaced by n,
> so it "generalize" instead of instantiate,
> and our proof cannot succeed this way
> *)
> 
> is there anyway to prove this lemma, or to implement
> enumerated types without using Fsets & co, and without using
> like enums m = {n | m < n}?

You can use dependent inversion:

Lemma e : forall (e : enums 0), e = New.                                    
dependent inversion e.
reflexivity.
Qed.

Edsko