The Coq mailing list

[Santiago Zanella B�guelin <szanella AT fceia.unr.edu.ar>]

Fabrice,

I think the problem is that the induction principle Coq generates for your 
definiton of Typ cannot be used to prove your goal:

Typ_ind
    : forall P : forall t : Trm, Typ t -> Prop,
      P trm axiom -> forall (t : Trm) (t0 : Typ t), P t t0

In order to apply this induction principle in your goal, a predicate of the 
form (fun (t:Trm)(x:Typ t) => x = axiom) may eventually have to be 
constructed. Such a predicate cannot be typed because the Coq type system is 
not able to determine that x must have type Typ trm (although it can be 
proved). You may either (1) restate your definition of Typ, (2) use 
dependent equality, or (3) assume an ad hoc induction principle. It seems 
you should go for (1).

(1)

Inductive Typ : Trm->Set :=
 axiom : forall t:Trm, Typ t.

Goal forall t:Trm, forall x y:Typ t, x=y.
destruct x;  induction y; trivial.

(2) See the Coq.Logic.Eqdep library.

Require Import Eqdep.

Inductive Trm : Set :=
 trm : Trm.

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

Lemma dep_eq : forall t:Trm, forall x y:Typ t, eq_dep Trm Typ t x t y.
destruct x; destruct y; trivial.
Qed.

Goal forall t:Trm, forall x y:Typ t, x = y.
intros t x y; exact (eq_dep_eq Trm Typ t x y (dep_eq t x y)).

(3)

Axiom Typ_trm_ind :
forall P : Typ trm -> Prop,
      P axiom -> forall (x : Typ trm), P x.

Goal forall t:Trm, forall x y:Typ t, x=y.
destruct x; apply Typ_trm_ind; trivial.

Hope this helps,

--
Santiago Zanella Béguelin

----- Original Message ----- 
From: "Fabrice Lemercier" <nouvid-coq AT yahoo.fr>
To: 
<coq-club AT pauillac.inria.fr>
Sent: Tuesday, June 06, 2006 10:16 PM
Subject: [Coq-Club]Type system in Coq


> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club