The Coq mailing list

[Fabrice Lemercier <nouvid-coq AT yahoo.fr>]

Hello,

I am formalizing a language and its type system in
Coq. Follow a simple example which is sufficient to
exhibit my problem.

The syntax of my language (consisting of just one
constant) is given by the following inductive
definition:

  Inductive Trm : Set :=
    trm : Trm.

There is only one typing rules (stating that my
constant is well typed) given by:

  Inductive Typ : Trm->Set :=
    axiom : Typ trm.

Now, I'd like to prove a fundamental property of my
type system which is that for each term there is a
unique type derivation:

  Goal forall t:Trm, forall x y:Typ t, x=y.

I know that if I put Typ in Prop instead of Set, then
I can prove the above statement by using proof
irrelevance in classical logic. But I put them in Set
because I want them to be extracted. What can I do?

Thanks,

Fabrice




__________________________________________________
Do You Yahoo!?
En finir avec le spam? Yahoo! Mail vous offre la meilleure protection 
possible contre les messages non sollicités 
http://mail.yahoo.fr Yahoo! Mail ;