The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

To recenter on the initial question, let us first notice that the
"Prop < Set" mentioned by Matej is printed by the command "Print
Universes". It does not reflect the definition of the logic of Coq but
instead the internal state of the universe-acyclicity algorithm that
Coq uses to ensure that the different occurrences of the anonymous
"Type" in a development can be interpreted within the linear hierarchy
Type(n). (The Type(n) hierarchy is the one which serves as reference
in papers and in particular in Chapter 4 of the reference manual.)

The "Prop < Set" is technical: the universe-acyclicity algorithm
internally needs to consider Prop <> Set to ensure that Prop is not
accidentally equated to Set (*). Matthieu, who introduced this for the
polymorphism of universes, confirmed.

However, at the logical level, there is no constraint that Prop should
be different from Set.

By looking at the rules of the logic of Coq, i.e. at the rules of the
Calculus of Inductive Constructions, one can check that all rules
involving subtyping (Section 4.4 of the reference manual) are
insensitive to whether one sets "Prop < Set" or "Prop <= Set", so why
not to start from "Prop <= Set" which is easier to manipulate since
the general subtyping relation has to be reflexive, hence large, and
that using explicitly a different relation < would just make things
more complicated.

Moreover, not only no rules of the logic is able to state Prop <> Set
but every rule about Prop also remains valid when interpreted in
impredicative Set and every rule about predicative Set remains
derivable as well when interpreted in impredicative Set. This gives
place for models where Set is interpreted impredicatively and Prop is
equated with Set. Thus, thinking at Prop subtype of Set in terms of
the large relation "<=" is the natural expectation in order to support
these models.

The above should be enough to answer yes to Matej's questions about <
vs <= but let me now generalize the discussion and show the basic
different possible models of the universe hierarchy of Coq. Let me
first remind the full hierarchy for typing and subtyping (**):

  Prop               }
  predicative Set    } : Type(1) : Type(2) : ...
  impredicative Set  }

  Prop <= { predicative Set   } <= Type(1) <= Type(2) <= ...  (***)
          { impredicative Set }

This hierarchy is designed so that it can basically support three
models, leading to five models if we distinguish between the theory
with or without option -impredicative-set, the three models depending
on whether Prop is taken proof-relevant or not and whether predicative
Set is "small" or not. In particular, one of the three models
identifies Prop with Set impredicative.

Let me give these "interesting" models. In the set-theoretic view at
them, "<=" is inclusion, "<" is strict inclusion, ":" is belonging and
Type(i) is the i-th inaccessible cardinal, except in the third model
where it is the (i+1)-ith inaccessible cardinal.

1. The "standard" interpretation of option -impredicative-set with
Prop a (two-element) proof-irrelevant universe:

  Prop < (impr) Set < Type(1) < Type(2) < ...
  Prop, (impr) Set  : Type(1) : Type(2) : ...

2. The Prop-relevant interpretation of option -impredicative-set (as
mentioned above):

  Prop = (impr) Set < Type(1) < Type(2) < ...
  Prop = (impr) Set : Type(1) : Type(2) : ...

3. The "standard" interpretation with Prop irrelevant and Set seen as an
extra Type(0) at the bottom of the predicative hierarchy of Type (as
implicitly expected by Abhishek):

  Prop < (pred) Set = Type(0) < Type(1) < Type(2) < ...
  Prop : (pred) Set = Type(0) : Type(1) : Type(2) : ...

4. The interpretation with Prop irrelevant and predicative Set as a
small universe, i.e. as a universe of subsets of terms like
impredicative Set would be; this is basically the equivalent of 1.
without -impredicative-set:

  Prop < (pred-as-impr) Set < Type(1) < Type(2) < ...
  Prop, (pred-as-impr) Set  : Type(1) : Type(2) : ...

5. The Prop-relevant interpretation with predicative Set being
interpreted within impredicative Set; this is the equivalent of 2.
without -impredicative-set:

  Prop = (pred-as-impr) Set < Type(1) < Type(2) < ...
  Prop = (pred-as-impr) Set : Type(1) : Type(2) : ...

Then, regarding the various issues raised in the discusion, we can
state the following properties of the hierarchy:

- Prop and Set are indeed both at the bottom of the typing hierarchy;
- Prop is at the bottom of the subtyping hierarchy;
- impredicative Set is allowed to be thought at the bottom of the
  subtyping hierarchy together with Prop even though the logic does
  not enforce it (thanks to subtyping not being strict);
- all rules about Prop are valid for impredicative Set; in particular,
  any judgement of Coq can be turned into a judgement where Prop and
  impredicative Set are equated;
- all rules about predicative Set are derivable when Set is
  interpreted impredicatively; in particular, even without the option
  -impredicative-set, one can interpret Coq in a model where both Prop
  and Set are impredicative and equated;
- predicative Set is also allowed to be thought at the bottom of the
  subtyping hierarchy together with Prop, both being embedded into the
  same impredicative set, even though the logic does not enforce it;
- as emphasized by Bruno, that Prop is not directly of type Set but of
  type Type(1) is to have a way to ensure that Set can remain small
  enough; this allows to support models 1, 2, 4 and 5.

Anyway, coming back to the initial issue, removing "Prop < Set" from
the display of "Print Universes" would certainly be better to avoid
that such confusion arise again.

This is what I can think of so far.

Hugo

(*) In particular, changing the line "enforce_univ_lt Level.prop
Level.set empty" into "enforce_univ_le Level.prop Level.set empty"
would be incorrect, unless other means are used to ensure that the
algorithm does not eventually incorrectly conclude that Prop = Set is
part of the logic.

(**) Depending on terminology. For instance, at the time of the
Coq'Art, the hierarchy started to number Type from 0 (i.e. 
Prop,Set : Type(0) : Type(1) etc.).

(***) One can certainly also contemplate having both predicative Set
and impredicative Set living together in the same system. In this
case, we would have had predicative-set <= impredicative-set, but with
model 3 being excluded.

On Thu, Jan 19, 2017 at 11:42:30AM +0100, Matej Kosik wrote:
> Hi Théo,
> 
> Thank you for the reply!
> 
> On 01/18/2017 05:39 PM, Théo Zimmermann wrote:
> > Hi,
> > 
> > Disclaimer: there are people so much more qualified than me on this list 
> > who can answer this question. But as they did not wake up yet (maybe they 
> > are too engrossed in some POPL presentations) I will
> > try to give a few hints.
> > 
> > My personal, very limited, understanding of the universes was also that 
> > Prop : Set : Type 1 : Type 2 : ...
> > But actually Check Prop : Set. fails both in Coq 8.6 and in your branch. 
> > I am not sure I understand why.
> > 
> > Coq < Check Prop:Set.
> >> ^^^^^^^^^^^^^^^
> > Error:
> > The term "Prop" has type "Type" while it is expected to have type "Set".
> 
> I wonder, why did you think that this might make sense?
> (Personally, I do not find the above error message surprising.)
> 
> > 
> > However, we can see that the constraint allows one to give type Set to 
> > something of type Prop:
> > 
> > Coq < Check False : Prop.
> > False : Prop
> >      : Prop
> > 
> > Coq < Check False : Set.
> > False : Set
> >      : Set
> 
> The above behavior is fully consistent with the fact that Prop is declared 
> to be a subtype of Set.
> (Reference Manual, Section 4.4, Point 4).
> This makes sense.
> 
> > 
> > As for weakening the constraint to Prop <= Set do you have any reasons in 
> > mind?
> 
> 
> If there is a good reason for that restriction, we should document it.
> 
> If there is no good reason for that restriction:
> - it is strange to insist on it
> - it inflates the theory
> - it creates unnecessary confusion and raises unnecessary questions
> 
> > This kind of weakening should allow in particular a constraint resolution 
> > where Prop = Set. But Prop and Set are
> > supposed to be different!
> 
> The strangeness of the "Prop < Set" universe depends directly on how you 
> interpret "_ < _".
> If we accept the sloppy definition ("Whatever works, man!"), then there is 
> nothing strange about this.
> If we are fussy about it we can interpret it like:
> 
>   If X and Y are two universes then "X < Y" means that "Y" has strictly 
> more inhabitants than "X"
>                                 and "X ≤ Y" means that "Y" has at least as 
> many inhabitants as "X".
> 
> In the "fussy interpretation" of "<" and "≤", the restriction "Prop < Set" 
> is surprising because after starting the toplevel like this:
> 
>   coqtop -noinit
> 
> neither Prop nor Set have any inhabitants and thus it is not the case that 
> "Prop < Set".
> The only thing that we can claim is "Prop ≤ Set".
> 
> > Because one is predicative and the other is impredicative.
> 
> Are you saying that relaxing "Prop < Set" to "Prop ≤ Set" would prevent us 
> from keeping impredicativity of Prop and predicativity of Set?
> Why?
> 
> > And also to help with extraction.
> 
> Are you saying that relaxing "Prop < Set" to "Prop ≤ Set" would somehow 
> make the extraction more difficult?
> Why?
> 
> > 
> > However, even in your branch where you are supposed to have relaxed the 
> > constraint, it seems that there is still something preventing Set and 
> > Prop to be considered equal:
> > Coq < Check nat : Prop.
> >> Check nat : Prop.
> >>       ^^^
> > Error:
> > The term "nat" has type "Set" while it is expected to have type
> > "Prop" (universe inconsistency).
> 
> As soon as you an inhabitant of "Set" which is not an inhabitant of "Prop" 
> (such as "nat"), then "Prop ≠ Set".
> In this special case, we can really claim that "Prop < Set" (wrt. to "fussy 
> interpretation" of "_ < _").
> This does not imply that it makes sense in general.
> 
> > 
> > Théo
> > 
> > 
> > Le mer. 18 janv. 2017 à 17:20, Matej Kosik 
> > <5764c029b688c1c0d24a2e97cd764f AT gmail.com
> >  
> > <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>>
> >  a écrit :
> > 
> >     Hi,
> > 
> >     On 01/18/2017 05:10 PM, Abhishek Anand wrote:
> >     > Going by the general rule that Ui:Uj if i<j, I suspect that Prop < 
> > Set would allow the following:
> >     > Check (Prop:Set)
> >     > which fails in Coq 8.5pl3.
> > 
> >     AFAIK this:
> > 
> >       Check Prop:Set.
> > 
> >     in all versions of Coq (8.5, 8.6, trunk).
> >     That makes sense.
> > 
> >     And precisely for that, the current version of the constraint:
> > 
> >       Prop < Set
> > 
> >     does not make sense (to me).
> > 
> >     >
> >     > So the stronger constraint may allow some new well-typed terms and 
> > potentially complicate arguments about normalization/consistency etc.
> >     >
> >     >
> >     >
> >     > -- Abhishek
> >     > http://www.cs.cornell.edu/~aa755/ 
> > <http://www.cs.cornell.edu/~aa755/>
> >     >
> >     > On Wed, Jan 18, 2017 at 9:27 AM, Matej Kosik 
> > <5764c029b688c1c0d24a2e97cd764f AT gmail.com
> >  
> > <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>
> >  
> > <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com
> >     
> > <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>>>
> >  wrote:
> >     >
> >     >     Hi,
> >     >
> >     >     I have noticed that in Coq, we have the following universe 
> > constraint:
> >     >
> >     >       Prop < Set
> >     >
> >     >     I am wondering what is the reason for that?
> >     >     Wouldn't
> >     >
> >     >       Prop <= Set
> >     >
> >     >     suffice in this case?
> >     >
> >     >     The code that makes the decision is here:
> >     >
> >     >       https://github.com/coq/coq/blob/trunk/kernel/uGraph.ml#L716 
> > <https://github.com/coq/coq/blob/trunk/kernel/uGraph.ml#L716>
> >     >
> >     >     I wonder whether it is necessary to do:
> >     >
> >     >       enforce_univ_lt Level.prop Level.set empty
> >     >
> >     >     as now, or we could simply do
> >     >
> >     >       enforce_univ_leq Level.prop Level.set empty
> >     >
> >     >     I've created an experimental branch where I did the change:
> >     >
> >     >       
> > https://github.com/matej-kosik/coq/commit/2fcbb0ced3bc32210ae9fbf4acc40804841c9200
> >  
> > <https://github.com/matej-kosik/coq/commit/2fcbb0ced3bc32210ae9fbf4acc40804841c9200>
> >     >
> >     >     ran some tests:
> >     >
> >     >       
> > https://ci.inria.fr/coq/view/coq-contribs/job/coq-contribs/653/console 
> > <https://ci.inria.fr/coq/view/coq-contribs/job/coq-contribs/653/console>
> >     >       https://ci.inria.fr/coq/view/opam/job/opam-install/22/console 
> > <https://ci.inria.fr/coq/view/opam/job/opam-install/22/console>
> >     >
> >     >     and I do not see any breakage but the major question is, would 
> > this kind of change make Coq inconsistent
> >     >     (enable us to prove False)
> >     >     or not?
> >     >
> >     >     Thank you in advance for any insight on this.
> >     >     --
> >     >     Matej Košík
> >     >
> >     >
> > 
> > 
> >     --
> >     Matej Košík
> > 
> 
> 
> -- 
> Matej Košík