The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 01/19/2017 02:48 PM, Maxime Dénès wrote:
> Hi Matej,
> 
> There are at least three sources of confusion in this thread.
> 
> 1) < vs : (the difference was clearly explained in previous messages)
> 2) that there is no term of a given type in the current context does not
> mean that the type has no inhabitants
> 3) inductive types *are* part of the core logic, and that's clear from
> both the manual and the basic parts of the implementation (see constr.ml)

Of course, the concept of an inductive type is different from the concept of 
a global assumption or a global definition
and Coq has general mechanisms for dealing with any kind of inductive type we 
decide to define.

If this is what you mean by "inductive types are part of the core logic", 
then I fully agree.
(although I would say it in a different way0

However, I do not see how this fact implies that, when I do:

  coqtop -noinit

either Prop or Set has any inhabitants.

There are none, in my opinion.
Consequently, I am puzzled why we insist on saying "Prop < Set".

I am puzzled because I am trying to attach some meaning to "_ ≤ _" and to "_ 
< _" that I wouldn't be ashamed of explaining to anyone else.
That is (like I said before)

(1) the universe constraint "X < Y" means that Y has all the inhabitants of X 
but we know that there are some inhabitants of Y which are not in X.

(2) the universe constraint "X ≤ Y" means that Y has all the inhabitants of X.

This is extremely simple explanation and the fact that we require "Prop < 
Set" breaks beautifully simple (and sufficient) theory.

Whatever Coq text is just more mysterious about the whole matter and it 
reminds me of me asking a question my religion's teacher:
"How can one and the only one God have three Persons? --- the answer was 
similar "That is a MYSTERY". End of discussion.
(now I would give it a different label)

I do not think that this is the same situation, but I am seriously frustrated 
about me not seeing what you see as obvious.

> 
> Maxime.
> 
> On 01/19/17 13:42, Matej Kosik wrote:
>> On 01/19/2017 12:28 PM, Théo Zimmermann wrote:
>>>
>>>> I guess that you wanted to say "Prop is impredicative" and "Set is 
>>>> predicative".
>>>
>>> Yes, this is what I meant, sorry. I regularly confuse the terminology.
>>>
>>>> after starting the toplevel like this:
>>>>
>>>>  coqtop -noinit
>>>>
>>>> neither Prop nor Set have any inhabitants
>>>
>>> I disagree. Inductive types are part of Coq's logic.
>>
>> Where did you read that?
>> (documentation? source code?)
>>
>>> Even if you didn't declare any inductive type yet, all the inductive 
>>> types that you could declare form part of the various universes. Inductive
>>> types are not like axioms which, as long as you haven't introduced them, 
>>> are not part of the logic.
>>>
>>>> Well, if you claim "Prop < Set", how can you say that "Set" is at the 
>>>> bottom of the type hierarchy?
>>>
>>> I want to retract this. But then it really depends on whether we define 
>>> the hierarchy based on < or on : (having a correspondence between the two 
>>> would ease the reasoning but Bruno explained why we
>>> don't want that).
>>>
>>> Going back to your initial question, Prop and Set are very specific 
>>> universes but if you have some Type@{i} <= Type@{j} universe constraint, 
>>> the constraint resolution algorithm should be able to solve
>>> this by making Type@{i} = Type@{j}. In the case of Prop and Set, we 
>>> clearly don't want that but, as I said, there seem to be other mechanisms 
>>> to prevent it anyways.
>>
>> Provided that you are wrong concerning your claim:
>>
>>   Inductive types are part of Coq's logic.
>>   Even if you didn't declare any inductive type yet, all the inductive 
>> types that you could declare form part of the various universes.
>>   Inductive types are not like axioms which, as long as you haven't 
>> introduced them, are not part of the logic.
>>
>> you make, I think, a wrong conclusion above.
>>


-- 
Matej Košík