The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Very good point Pierre. And now that you mention this, Matthieu was precisely recently talking about the need for anonymous records (which would probably be made available by creating a syntax for anonymous inductive types, since Coq's record are implemented in terms of inductive types).

Le jeu. 19 janv. 2017 à 17:57, Pierre Courtieu <pierre.courtieu AT gmail.com> a écrit :

Hi,

Something that may confuse Matej is also that the only way of defining
an inductive in Coq is to declare it via a definition. Which Matej
associates to "changing the type Set by adding new inhabitants in it"
but this is a wrong interpretation. All inductive types exists from
the beginning, it is just that the implementation of Coq does not have
a anonymous syntax for them (and maybe other deeper problem I am not
aware of).

You can define anonymous functions like this: (fun x:Prop => Prop).
And everyone will probably admit that this function existed even
before we write it (although we may reach philosophical problems with
this formulation).

But you cannot declare an anonymous inductive in such a way in coq
(say for instance with a binder syntax like this: (Ind nat:Set =>
O:nat | S: nat -> nat). So one could conclude that nat "does not exist
until it is declared".

But actually the underlying theory do have this kind of anonymous
inductive (see constr.ml as suggested by Maxime). So all typable
inductives types always existed as every typable other terms.

Hope this helps,
Pierre




2017-01-19 17:31 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com>:
>
>
> On 01/19/2017 11:20 AM, Matej Kosik wrote:
>>
>> ...
>>    Coq < Check (forall x : Set, x) : Set.
>>    Toplevel input, characters 0-32:
>>    > Check (forall x : Set, x) : Set.
>>    > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>>    Error:
>>    The term "forall x : Set, x" has type "Type@{Set+1}"
>>    while it is expected to have type "Set".
>>
>>
>> So this is not the counter-example that would show that, when I start
>> "coqtop -noinit" it would be the case that:
>>
>>    Set not only has all the inhabitants of Prop, but it also has some such
>> inhabitants, which are not in Prop.
>>
>> (in which case we could relax "Prop < Set" to "Prop ≤ Set").
>>
>> Are there such counter-examples?
>
>
>
> I think you are missing some implications of what Bruno Barras said here:
>
>> The reason why Prop:Set does not hold (although it is consistent in the
>> default settings of Coq: think of Set as Type(0) and Type(i) as Type(i+1))
>> is that Coq allows to make Set impredicative, and we expect this to be an
>> extension of Coq without the option set (all theorems of Coq without the
>> option are theorems of Coq with it).
>> With this option set and Prop:Set, Coq would then contain system U which
>> is inconsistent.
>
>
> (this, by the way, would be a great addition to the FAQ).
>
> Note that when -impredicative-set is used, then
>
> Check (forall x : Set, x) : Set.
>
> succeeds.  I think that plus the design constraint on Coq Bruno mentioned
> above - all theorems without -impredicative-set are theorems with
> -impredicative-set - might imply that Prop can't bet <= Set even without
> -impredicative-set.
>
> -- Jonathan
>
>