The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 2 août 08 à 11:37, Edsko de Vries a écrit :

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


Hello,

Beware that this works only because you are in a very favorable case  
where
the goal can actually be generalized before doing induction, like this:
<<
Lemma e : forall (e : enums 0), e = New.
intros.
(*
Now I want to destruct e
*)
generalize (refl_equal 0). set(t:=0) at 1.
generalize 0 e. subst t. destruct e0. intros. reflexivity.
intros. discriminate.
Qed.
>>

Indeed, one can generalize the [n] argument of [New] in this case,  
transforming
the goal 
[@eq
 (enums 0) e (@New 0)] into a
[forall n (e : enums n), @eq (enums n) e (@New n)]

Provided you keep information on [n] on the side (the [generalize  
(refl_equal 0)]
trick) it will work.

Alas, this is not possible in general, consider:
<<
Inductive vector : nat -> Set := vnil : vector 0.

Lemma e' : forall (v : vector 0), v = vnil.
Proof.
  intros. dependent inversion v.
>>

Here there is no way to generalize [vnil] into a [vector n] so inversion
fails. The technique used by the [dependent destruction] tactic avoids  
this
by not attempting any generalization of the goal and so works in both  
cases, e.g:

<<
Require Import Equality.
Lemma e' : forall (v : vector 0), v = vnil.
Proof.
  intros. dependent destruction v.
  reflexivity.
Qed.
>>

Hope this helps,
--
Matthieu Sozeau
http://www.lri.fr/~sozeau