binary distribution for Leopard (and Snow Leopard)

[Thorsten Altenkirch]

Hi,

I am teaching a course using COQ, see
http://www.cs.nott.ac.uk/~txa/g52mc2/

Many students are using their laptops and a number is using Macs.  
However, currently there is no binary distribution for Leopard and  
Snow Leopard. The only way to install it in the moment seems to be to  
compile it following
http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html

However, this is a lengthy and error prone process.

Is there any chance that a kind soul puts up coq binaries (i.e. dmg)  
for Leopard (and maybe even Snow Leopard)?

Cheers,
Thorsten

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

[Matthieu Sozeau]

Le 5 oct. 09 à 06:46, Thorsten Altenkirch a écrit :

> Hi,

Hi,

> I am teaching a course using COQ, see
> http://www.cs.nott.ac.uk/~txa/g52mc2/
>
> Many students are using their laptops and a number is using Macs.  
> However, currently there is no binary distribution for Leopard and  
> Snow Leopard. The only way to install it in the moment seems to be  
> to compile it following
> http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html
>
> However, this is a lengthy and error prone process.
>
> Is there any chance that a kind soul puts up coq binaries (i.e. dmg)  
> for Leopard (and maybe even Snow Leopard)?

I made binaries for coq-8.2pl1 and lablgtk2 (including gtk2) for 10.5  
using
macports: http://eecs.harvard.edu/~mattam/
I'll make Snow Leopard packages if a kind soul gives me an ssh access :)

Hope this helps,
-- Matthieu

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

[Vladimir Voevodsky]

Hi,


I am trying to understand the way in which Coq treats input texts. To  
some extent it is explained in the first part of the reference manual,  
but I could not find the explanation for what "levels" are (e.g. in


Reserved Notation "x <-> y" (at level 95, no associativity).

from the Coq standard library,)

Also, is there a way to search the reference manual?

Thanks,
Vladimir.

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

[Adam Chlipala-3]

Vladimir Voevodsky wrote:
> I am trying to understand the way in which Coq treats input texts. To
> some extent it is explained in the first part of the reference manual,
> but I could not find the explanation for what "levels" are

This chapter of the manual explains syntax extensions, including levels:
    http://coq.inria.fr/refman/Reference-Manual015.html

> Also, is there a way to search the reference manual?

Google supports an incantation to search only pages on a particular web
site.  Applying that to the Coq site would probably achieve what you want.

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

[harke]

This is a standard trick for reducing the amount of parenthesisation
used by many languages that have user defined infix operators.

You'll also notice the line:

  Reserved Notation "x /\ y" (at level 80, right associativity).

Try the following in coqide/proofgeneral:

  Variables A B C : Prop.
  Check A /\ (B <-> C).
  Check (A /\ B) <-> C.

You'll see the printout of the first shows parentheses while the second
omits them.  This is due to the different levels.  Then try:
       
  Check (A /\ B) /\ C.
  Check A /\ (B /\ C).

Again, the first shows parens, the second omits, due to the right
associativity.

On Tue, Oct 06, 2009 at 01:52:21PM -0400, Vladimir Voevodsky wrote:

> Hi,
>
>
> I am trying to understand the way in which Coq treats input texts. To  
> some extent it is explained in the first part of the reference manual,  
> but I could not find the explanation for what "levels" are (e.g. in
>
>
> Reserved Notation "x <-> y" (at level 95, no associativity).
>
> from the Coq standard library,)
>
> Also, is there a way to search the reference manual?
>
> Thanks,
> Vladimir.

--
Tom Harke

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

[Vladimir Voevodsky]

A related question: does Cow has an "internal representation" language  
with a more rigid syntactic structure?

V.




On Oct 6, 2009, at 2:11 PM, harke@... wrote:

> This is a standard trick for reducing the amount of parenthesisation
> used by many languages that have user defined infix operators.
>
> You'll also notice the line:
>
>  Reserved Notation "x /\ y" (at level 80, right associativity).
>
> Try the following in coqide/proofgeneral:
>
>  Variables A B C : Prop.
>  Check A /\ (B <-> C).
>  Check (A /\ B) <-> C.
>
> You'll see the printout of the first shows parentheses while the  
> second
> omits them.  This is due to the different levels.  Then try:
>
>  Check (A /\ B) /\ C.
>  Check A /\ (B /\ C).
>
> Again, the first shows parens, the second omits, due to the right
> associativity.
>
> On Tue, Oct 06, 2009 at 01:52:21PM -0400, Vladimir Voevodsky wrote:
>> Hi,
>>
>>
>> I am trying to understand the way in which Coq treats input texts. To
>> some extent it is explained in the first part of the reference  
>> manual,
>> but I could not find the explanation for what "levels" are (e.g. in
>>
>>
>> Reserved Notation "x <-> y" (at level 95, no associativity).
>>
>> from the Coq standard library,)
>>
>> Also, is there a way to search the reference manual?
>>
>> Thanks,
>> Vladimir.
>
> --
> Tom Harke

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

[Adam Chlipala-3]

Vladimir Voevodsky wrote:
> A related question: does Cow has an "internal representation" language
> with a more rigid syntactic structure?

Like pretty much all tools that process programming languages, Coq uses
abstract syntax trees internally.  As far as I know, the "format" isn't
documented, but you can see it in the source code.  The Coq
implementation is pretty modular, so it's not actually that much trouble
to write (and dynamically load) your own modules that manipulate syntax
trees.  You just need to learn the "API details" by reading .mli files
in the source.

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

[Thorsten Altenkirch]

On 6 Oct 2009, at 19:19, Vladimir Voevodsky wrote:

> A related question: does Cow has an "internal representation"  
> language with a more rigid syntactic structure?
>
> V.

Coq is based on the Calculus of Inductive (and Coinductive)  
Constructions. This is a dependently typed lambda calculus with an  
impredicative universe (The Calculus of Constructions) of propositions  
extended by a predicative universe of sets which are closed under  
inductive (and coinductive) definitions. See the reference manual, the  
Coq'Art book and a number of related research papers and PhD theses.

Cheers,
Thorsten

>
>
>
>
> On Oct 6, 2009, at 2:11 PM, harke@... wrote:
>
>> This is a standard trick for reducing the amount of parenthesisation
>> used by many languages that have user defined infix operators.
>>
>> You'll also notice the line:
>>
>> Reserved Notation "x /\ y" (at level 80, right associativity).
>>
>> Try the following in coqide/proofgeneral:
>>
>> Variables A B C : Prop.
>> Check A /\ (B <-> C).
>> Check (A /\ B) <-> C.
>>
>> You'll see the printout of the first shows parentheses while the  
>> second
>> omits them.  This is due to the different levels.  Then try:
>>
>> Check (A /\ B) /\ C.
>> Check A /\ (B /\ C).
>>
>> Again, the first shows parens, the second omits, due to the right
>> associativity.
>>
>> On Tue, Oct 06, 2009 at 01:52:21PM -0400, Vladimir Voevodsky wrote:
>>> Hi,
>>>
>>>
>>> I am trying to understand the way in which Coq treats input texts.  
>>> To
>>> some extent it is explained in the first part of the reference  
>>> manual,
>>> but I could not find the explanation for what "levels" are (e.g. in
>>>
>>>
>>> Reserved Notation "x <-> y" (at level 95, no associativity).
>>>
>>> from the Coq standard library,)
>>>
>>> Also, is there a way to search the reference manual?
>>>
>>> Thanks,
>>> Vladimir.
>>
>> --
>> Tom Harke
>
> --------------------------------------------------------
> 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

[Yves Bertot]

Thorsten Altenkirch wrote:
> On 6 Oct 2009, at 19:19, Vladimir Voevodsky wrote:
>
>> A related question: does Cow has an "internal representation"
>> language with a more rigid syntactic structure?
>>
>> V.
>
I guess your question is more about using a simpler notation than the
one with infix operators and all the special notations.  The answer is
yes.  In principle, there is a very small language in which you can
express all formulas of Coq.  It is basically a lambda calculus, so that
you write:

f a  (representing function application)

fun (x : type) => a (representing abstraction)

for expressions,

and :

forall (x : type), type

for types.  Of course, function applications and abstractions can occur
in types.

To be complete, you also need to understand the syntax of
pattern-matching constructs:

match e as x in e' return e'' with p1 => e1 | ... end

the patterns p1, ..., mostly look like symbols and function applications.

For inputing data into Coq, this is basically all the syntax you need to
know for terms.  All the rest is decoration, and is defined using Notation.

There is one special treatment with numerals, but even them can be
entered using a function notation.
For example,  when understood as an integer (i.e., in Z_scope)  3 stands
for Zpos (xO xH)

If you use only the syntax described here, you don't need to understand
the notion of levels...

To know what function is hidden behind a notation, you can use Locate,
as in the following example:

Locate "_ /\ _".
The answer that the function is actually named 'and', so that A /\ B  
can also be written (and A B).

I hope this helps.

Yves


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

[Jean-Francois Dufourd]

Hi,

I'm trying to (impredicatively) define the type Nat in Coq
(without the option - impredicative-set, which works well).

I write:

Definition Nat:=forall X:Type,(X->X)->X-> X.

Definition succ(n:Nat):Nat:=
fun(X:Type)(f:X->X)(z:X) => (f (n X f z)).

Definition add(n m:Nat):Nat:=
fun(X:Type)(f:X->X)(z:X) => m X f (n X f z).

Definition mult(n m:Nat):Nat:=
fun(X:Type)(f:X->X)(z:X) => m X (n X f) z.

All that is OK. But, when I write an other version of mult:

Definition mult1(n m:Nat):Nat:=
n Nat (add m) zero.

Coq answers "Universe inconsistency".

I interprete this mistake as the violation of the typing rules, because
Nat is probably of higher Type level as the X of its definition.

Is this true ? Does a means exist for circumventing this problem ?

Thank you !

Jean-Franc,ois Dufourd

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

[Lionel Elie Mamane-2]

On Wed, Oct 07, 2009 at 01:58:38PM +0200, Yves Bertot wrote:
> Thorsten Altenkirch wrote:
>> On 6 Oct 2009, at 19:19, Vladimir Voevodsky wrote:

>>> A related question: does Cow has an "internal representation"
>>> language with a more rigid syntactic structure?


> I guess your question is more about using a simpler notation than
> the one with infix operators and all the special notations.  The
> answer is yes.  In principle, there is a very small language in
> which you can express all formulas of Coq.  It is basically a lambda
> calculus, so that you write:

> f a  (representing function application)

> fun (x : type) => a (representing abstraction)

> forall (x : type), type

> for types.  Of course, function applications and abstractions can
> occur in types.

> To be complete, you also need to understand the syntax of
> pattern-matching constructs:

> match e as x in e' return e'' with p1 => e1 | ... end

> For inputing data into Coq, this is basically all the syntax you
> need to know for terms.  All the rest is decoration, and is defined
> using Notation.

It would seem to me that inductives and fixpoints are another "atomic"
constructs whose syntax is part of that "minimal rigid structure".

--
Lionel

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

[André Hirschowitz]

>  
>
> I interprete this mistake as the violation of the typing rules, because
> Nat is probably of higher Type level as the X of its definition.
>
> Is this true ? Does a means exist for circumventing this problem ?
>

Hello,

Since "they" do not comment, let me say that I like the question, that I
agree with your understanding of the error, and that I do not see any
way around. So, this could eventually increase my interest in  the
impredicative Set option.

ah

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

[Randy Pollack]

Quoting Jean-Francois Dufourd <dufourd@...>:
>
> I'm trying to (impredicatively) define the type Nat in Coq
> (without the option - impredicative-set, which works well).
>
> Definition Nat:=forall X:Type,(X->X)->X-> X.

Type is not impredicative, so how could you expect the impredicative  
definition of Nat to work?  Perhaps you are asking "why do some basic  
definitions work?" or "what is the limit?"

If you could define exponentiation then you could define a Godel  
numbering scheme and prove consistency of arithmetic, which is  
stronger than predicative type theory.

To see some thinking about this area look at Daniel Leivant's paper  
"Finitely stratified polymorphism" in Information and Computation,  
Volume 93, Issue 1 (July 1991).

Randy
--

>
> Definition succ(n:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => (f (n X f z)).
>
> Definition add(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X f (n X f z).
>
> Definition mult(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X (n X f) z.
>
> All that is OK. But, when I write an other version of mult:
>
> Definition mult1(n m:Nat):Nat:=
> n Nat (add m) zero.
>
> Coq answers "Universe inconsistency".
>
> I interprete this mistake as the violation of the typing rules, because
> Nat is probably of higher Type level as the X of its definition.
>
> Is this true ? Does a means exist for circumventing this problem ?
>
> Thank you !
>
> Jean-Franc,ois Dufourd
>
> --------------------------------------------------------
> 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

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.




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

[hugo.herbelin]

Hi,

On Fri, Oct 09, 2009 at 10:57:20PM +0200, André Hirschowitz wrote:
> > I interprete this mistake as the violation of the typing rules, because
> > Nat is probably of higher Type level as the X of its definition.
> >
> > Is this true ? Does a means exist for circumventing this problem ?
>
> Since "they" do not comment, let me say that I like the question, that I
> agree with your understanding of the error, and that I do not see any
> way around. So, this could eventually increase my interest in  the
> impredicative Set option.

One of "them" can try to comment...

With Nat defined polymorphically in Type, you get the logical strength
of arithmetic and in particular 0<>1 (see Alexandre Miquel's PhD) but
a weak computational expressiveness (a priori Schwichtenberg-Statman
representability result for the type (X->X)->(X->X) applies and only
the functions built from addition, multiplication and if-zero will be
representable as lambda-terms; the other functions will only be
definable as logical relations of the form "forall n m, IsNat n ->
IsNat m -> exists p, IsNat p /\ [a relational specification of the
function]" where "IsNat m" expresses that n satisfies induction on Nat).

On the other side, with Nat defined polymorphically in impredicative
Set (with option -impredicative-set), you get a full recursor
"Nat_rec" and at least the computational expressiveness of system T
but you cannot derive 0<>1 (and the recursor has a bad complexity due
to the linear complexity of the predecessor).

Hence, unless we are concerned by theoretical investigations, there is
no reason in practice not to prefer the inductive definition (i.e. the
definition of the standard library) which has all the good properties
we expect.

Hugo Herbelin

On Thu, Oct 08, 2009 at 10:24:32AM +0200, Jean-Francois Dufourd wrote:

> Hi,
>
> I'm trying to (impredicatively) define the type Nat in Coq
> (without the option - impredicative-set, which works well).
>
> I write:
>
> Definition Nat:=forall X:Type,(X->X)->X-> X.
>
> Definition succ(n:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => (f (n X f z)).
>
> Definition add(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X f (n X f z).
>
> Definition mult(n m:Nat):Nat:=
> fun(X:Type)(f:X->X)(z:X) => m X (n X f) z.
>
> All that is OK. But, when I write an other version of mult:
>
> Definition mult1(n m:Nat):Nat:=
> n Nat (add m) zero.
>
> Coq answers "Universe inconsistency".

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

[Adam Chlipala-3]

hugo.herbelin@... wrote:
> On the other side, with Nat defined polymorphically in impredicative
> Set (with option -impredicative-set), you get a full recursor
> "Nat_rec" and at least the computational expressiveness of system T
> but you cannot derive 0<>1 (and the recursor has a bad complexity due
> to the linear complexity of the predecessor).
>  

Doesn't the unprovability of [0 <> 1] only arise from doing away with
inductive types altogether?  If we just single out [nat] to be defined
with impredicative polymorphism, then [0 <> 1] seems to reduce simply to
[false <> true], which [discriminate] proves.

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

[Vladimir Voevodsky]

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 .

?

V.

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

[Adam Chlipala-3]

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

[Vladimir Voevodsky]

>> 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 a1 a2 .



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

[Vladimir Voevodsky]

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 .

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

[Thorsten Altenkirch]

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