Skip to Content.
Sympa Menu

coq-club - RE : Re: [Coq-Club]Type system in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE : Re: [Coq-Club]Type system in Coq


chronological Thread 
  • From: Fabrice Lemercier <nouvid-coq AT yahoo.fr>
  • To: Lionel Elie Mamane <lionel AT mamane.lu>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: RE : Re: [Coq-Club]Type system in Coq
  • Date: Wed, 7 Jun 2006 14:09:52 +0200 (CEST)
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Message-ID:Received:Date:From:Reply-To:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=Qf+c0Oc9YTSuATzoOWPRg48q+JYA9Rrvc80I8DnqlpW0k8fhUe6GIAdzrgp7LDIZht10p/46p5/HRBPvslQC7RkldB10MvUoVBnh96YLNrbhnLBvCJJH0OZpzDtikgCHeMhVRqcr9TLGV+79OArb+9ID+qqry7LtSvF8uHcmNwc= ;
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,

Thank you for the reply. Unfortunately my example was
too simplified compare to the original type system I
am dealing with. Here is a less simplified version.
Can you prove the goal?

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

  Inductive Typ : Trm*nat->Set :=
    axiom : forall n, Typ (trm n, n).

  Goal forall t:Trm, forall n, forall x y:Typ (t,n),
x=y.

Fabrice

P.S. I also found that I can prove the goal in my
previous mail by using dependent equality, but it is
not enough to prove the above goal.

  Require Export Eqdep.

  Inductive Trm : Set :=
    trm : Trm.

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

  Goal forall t:Trm, forall x y:Typ t, x=y.
    induction t.
    intros.
    apply (eq_dep_eq Trm Typ).
    induction x.
    induction y.
    apply eq_dep_intro.


__________________________________________________
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 ;



Archive powered by MhonArc 2.6.16.

Top of Page