The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 17 Aug 2011 19:01:26 +0200,
Stéphane Glondu 
<steph AT glondu.net>
 a écrit :

> Le 17/08/2011 18:26, Jeffrey Terrell a écrit :
> > In f, are X and X0 the same set?
> >
> > Inductive T : Set -> Type :=
> > Build_T : forall X : Set, T X.
> >
> > Definition f (X : Set) (t : T X) (x : X) :=
> > match t with Build_T X0 => forall x0 : X0, x = x0 end.
> 
> It depends on what you mean by "the same". They are not convertible,
> but you can prove that they are equal. If you need to keep some
> relation between dependencies of the type of the matched item, and
> the arguments of constructors in branches, you have to use "as ...
> in ... return ..." annotations (see the "Extended pattern-matching"
> chapter of the manual).
> 
> In you case, by carefully taking care of dependencies, you can
> directly write:
> 
> Definition f (X : Set) (t : T X) :=
>    match t in T X return X -> _ with
>      Build_T X0 => fun x => forall x0 : X0, x = x0
>    end.
> 
> 
> Cheers,
> 

Or even better (if your real inductive allows it):
 Inductive T (X : Set): Type :=
 Build_T : T X.

Whith that there is no dependency to manage as X becomes a parameter
and is no more an index (the place of X from the colon has its
importance).