The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Note that relaxing this constraint also causes Coq to lose subject reduction on the inductive fragment (normally, I believe, it fails on the coinductive fragment but succeeds on the inductive fragment):

Inductive inhabited (X : Set) : Prop := inhabits (_ : X).

Constraint Set = Prop.

Scheme Induction for inhabited Sort Prop.

Fail Scheme Induction for inhabited Sort Set. (*Error: Induction on sort Set is not allowed for inductive definition inhabited.*)

Definition inhabited_rec

  : forall (X : Set) (P : inhabited X -> Set), (forall x : X, P (inhabits X x)) -> forall i : inhabited X, P i

  := inhabited_ind_dep. (* success *)

Definition inhabited_rec'

  : forall (X : Set) (P : inhabited X -> Set), (forall x : X, P (inhabits X x)) -> forall i : inhabited X, P i

  := Eval compute in inhabited_rec. (* Error:

Incorrect elimination of "i" in the inductive type "inhabited":

the return type has sort "Set" while it should be "Prop".

Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set

because proofs can be eliminated only to build proofs. *)

So at the very least, I think it would be tricky to make this change consistently across Coq.

On Sat, Jan 21, 2017 at 1:59 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Matej,

With your branch of Coq:

Set Universe Polymorphism.

Definition foo@{i j} (x : Type@{i}) := x : Type@{j}.

Set Printing Universes.

Section foo.

  Universe i.

  Constraint i = Prop. (* works fine in your branch, fails in standard Coq with Error: Universe inconsistency. Cannot enforce i = Prop because Prop < Set <= i. *)

  Definition bar := foo@{Set i}.

End foo.

Eval compute in bar nat. (* = nat : Prop *)

Definition natP : Prop.

Proof.

  let v := (eval compute in (bar nat)) in exact v.

Defined.

Print natP. (* natP = nat

     : Prop

(*  |= Prop = Set

        *) *)

I had to jump through some hoops to work around other ad-hoc restrictions that prevent collapsing things to Prop (polymorphic universes can't normally be instantiated with [Prop], even when you relax Prop < Set; monomorphic universes are always strictly greater than Set, the subtyping relation must special-case Prop and Set in some places, rather than going through the generic universe comparison algorithm.)

Regarding your question

> I wonder why Coq infers that.

The command [Print Sorted Universes] collapses all universes to the minimal universe they can inhabit.  If you include the prelude and [Print Sorted Universes], all of the universes in the prelude get collapsed to Type.0.  So since you don't have Prop < Set, Coq infers that Set can be collapsed to Prop.

On Sat, Jan 21, 2017 at 1:09 PM Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

On 01/21/2017 06:03 PM, Jason Gross wrote:
> If you write
>   (fun x : Set => (x : Prop))
> Coq will currently reject that.  If you relax Prop < Set to Prop ≤ Set, Coq will add the global constraint that Set ≤ Prop and hence that Prop = Set, just as when you write

I wasn't able to reproduce what you say. In my branch where I relaxed Prop < Set to Prop ≤ Set, this is what I see:

    Welcome to Coq trunk (January 2017)

    Coq < Print Universes.
    Prop <= Set

    Coq < Set Printing Universes.

    Coq < Check fun x : Set => (x : Prop).
    Toplevel input, characters 22-23:
    > Check fun x : Set => (x : Prop).
    >                       ^
    Error:
    In environment
    x : Set
    The term "x" has type "Set" while it is expected to have type
    "Prop" (universe inconsistency: Cannot enforce Set = Prop).

which totally makes sense. The term:

  fun x : Set => (x : Prop)

is not well-typed because Set is not a subtype of Prop.
(this is not the case of neither in the official Coq branches, neither in my experiment).

Relaxing Prop < Set to Prop ≤ Set does not imply Set suddenly becomes a subtype of Prop.

> (fun x : Type@{i} => (x : Type@{j}))
> Coq adds the constraint that i ≤ j.

It may. I fail to see how it is a problem (wrt what I asked).

>
> It might also be the case that you'd get this constraint in more subtle situations, such as if you write
>   Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
> or if you write
>   (forall X : Set, X) : Set

    Welcome to Coq trunk (January 2017)

    Coq < Print Universes.
    Prop <= Set


    Coq < Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
    inhabited is defined
    inhabited_ind is defined

    Coq < Print Universes.
    Prop <= Set

>
> Does this answer your question?

Unfortunatelly, not. But think you (all) for the answers!

However, independently from your concrete arguments, which I wasn't able to reproduce, there is more simple way to see that something is wrong after these changes:

    https://github.com/matej-kosik/coq/commit/2fcbb0ced3bc32210ae9fbf4acc40804841c9200

this:

    Welcome to Coq trunk (January 2017)

    Coq < Print Universes.
    Prop <= Set


    Coq < Print Sorted Universes.
    Prop = Set

shows that Coq, somehow really decides (why?) infers that "Prop = Set"
(regardless whether we add inhabitants to Set or not).

I wonder why Coq infers that.

This is consistent with what Hugo said.

Hm, I guess that the only way to find out is to look at the implementation ...

>
>
> On Sat, Jan 21, 2017, 11:27 AM Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>> wrote:
>
>     Hi Hugo,
>
>     For me, the most surprising parts of you reply are:
>
>     On 01/19/2017 11:58 PM, Hugo Herbelin wrote:
>     >
>     > 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.
>
>     ...
>
>     > (*) 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.
>
>     I wouldn't be surprised if Coq concluded that:
>
>       X ≤ Z      (* all inhabitants of X are also inhabitants of Z *)
>
>     from the following two universe constraints:
>
>       X ≤ Y      (* all inhabitants of X are also inhabitants of Y *)
>
>       Y ≤ Z      (* all inhabitants of Y are also inhabitants of Z *)
>
>
>     Similarly, no surprise when it concludes:
>
>       X = Y      (* X and Y have the same inhabitants *)
>
>     from these constraints:
>
>       X ≤ Y      (* all inhabitants of X are also inhabitants of Y *)
>
>       Y ≤ X      (* all inhabitants of Y are also inhabitants of X *)
>
>
>     However, when you claim that Coq can conclude
>
>       Prop = Set   (* Prop and Set have the same inhabitants *)
>
>     from, and solely from:
>
>       Prop ≤ Set   (* all inhabitants of Prop are also inhabitants of Set *)
>
>     isn't that counterintuitive for the user?
>
>     Did I understand you correctly when you said that this could really happen (if we imagine that "Prop < Set" was relaxed to "Prop ≤ Set") ?
>
>     Would Coq do this only in case of Prop and Set or in general for any two universes?
>


--
Matej Košík