Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] an inductive types question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] an inductive types question


chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
  • Cc: Adam Chlipala <adamc AT hcoop.net>, Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] an inductive types question
  • Date: Sat, 10 Oct 2009 19:55:38 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Suppose for example that T= Prop. Then, a function from I1 to T should be a triple (P_1, P_2, prf) where P_1, P_2: Prop and prf: P_1 <-> P_2 is a proof of their equivalence.

V.


On Oct 10, 2009, at 7:28 PM, Thorsten Altenkirch wrote:


On 11 Oct 2009, at 00:23, Vladimir Voevodsky wrote:

Excuse me, there was a typo. The correct text is:

Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .

What I want here is a type such that for any type T, a function I1 -> T is given by a triple -- t1:T (its value on x0), t2:T (its value on x1) and e : eq t1 t2 .

Assuming that eq means equals, aren't two values which are the same not the same as one value?

T.



Also, the definition of Impl given below is meaningless.

V.



On Oct 10, 2009, at 5:42 PM, Adam Chlipala wrote:

Vladimir Voevodsky wrote:
Is there a way in Coq to make definitions such as:

Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .

or

Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .

Neither of these fits the spirit of inductive definitions. In each example, you might want to assert the final "constructor" as an [Axiom] instead, but there is almost always a better way to do such things. We can't comment on the better way(s) for your specific situation without more background.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/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





Archive powered by MhonArc 2.6.16.

Top of Page