The Coq mailing list

[Jeffrey Terrell <jeffrey.terrell AT kcl.ac.uk>]

Thanks for your help. There's a very good primer on pattern matching in sections 2 and 3 of "A New Elimination Rule for the Calculus of Inductive Constructions" by Barras et al. It references what appears to be a primary source on pattern matching, namely Coquand's 1992 paper on "Pattern Matching with Dependent Types". Does anyone know where I can obtain a copy of this paper?

Jeff.

On 17/08/2011 18:01, Stéphane Glondu wrote:

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,