The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

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,

--
Stéphane