coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Type system in Coq

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Fabrice Lemercier <nouvid-coq AT yahoo.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Type system in Coq
Date: Wed, 7 Jun 2006 07:57:11 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Jun 07, 2006 at 03:16:07AM +0200, Fabrice Lemercier wrote:

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

>   Inductive Trm : Set :=
>     trm : Trm.

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

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

Definition canon : forall (t:Trm), Typ t.
intros [].
exact axiom.
Defined.

Lemma a: forall x:Typ trm, x= (canon trm).
intros [].
reflexivity.
Qed.

Lemma b:forall t:Trm, forall x y:Typ t, x=y.
intros [] [] y.
rewrite (a y).
reflexivity.
Qed.

--
Lionel

[Coq-Club]Type system in Coq, Fabrice Lemercier
- Re: [Coq-Club]Type system in Coq, Santiago Zanella B�guelin
- Re: [Coq-Club]Type system in Coq, Lionel Elie Mamane
  - RE : Re: [Coq-Club]Type system in Coq, Fabrice Lemercier
    - Re: RE : Re: [Coq-Club]Type system in Coq, Roland Zumkeller
    - Re: RE : Re: [Coq-Club]Type system in Coq, Lionel Elie Mamane
    - Re: RE : Re: [Coq-Club]Type system in Coq, Frederic Blanqui