coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Type hierarchy, (continued)
- Re: [Coq-Club] Type hierarchy, André Hirschowitz
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Adam Chlipala
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Jean-Francois Dufourd
- [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Thorsten Altenkirch
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- Re: [Coq-Club] an inductive types question, AUGER Cédric
- Re: [Coq-Club] an inductive types question, André Hirschowitz
- Re: [Coq-Club] an inductive types question, AUGER Cédric
- Re: [Coq-Club] an inductive types question, André Hirschowitz
- Re: [Coq-Club] an inductive types question, AUGER Cédric
- Re: [Coq-Club] an inductive types question, André Hirschowitz
- Re: [Coq-Club] an inductive types question, Dan Doel
- [Coq-Club] another question (Prop as a subtype of Set), Vladimir Voevodsky
- [Coq-Club] another question (cont.), Vladimir Voevodsky
Archive powered by MhonArc 2.6.16.