Stream: Coq users

Topic: Potentially superfluous universe constraints


view this post on Zulip Janno (Apr 06 2021 at 09:38):

Coq introduces a universe constraint Set < u in the definition below and I don't understand why it adds this constraint. Is it not implied by u0 < u (which is the second constraint Coq generates)? Both u := Prop and u := Set suffice to conclude u >= Set+1, AFAICT.

Definition type_or_prop@{u u0} (b : bool) : Type@{u} :=
  if b then Prop else Type@{u0}.
(* {type_or_prop.u0 type_or_prop.u} |= Set < type_or_prop.u
                                       type_or_prop.u0 < type_or_prop.u *)

view this post on Zulip Gaëtan Gilbert (Apr 06 2021 at 10:03):

monomorphic univs are always declared > Set

view this post on Zulip Janno (Apr 06 2021 at 10:03):

u0 is not > Set, is it?

view this post on Zulip Gaëtan Gilbert (Apr 06 2021 at 10:04):

actually it is, but the implicit > Set is not listed (being implicit)

view this post on Zulip Gaëtan Gilbert (Apr 06 2021 at 10:05):

also Coq does not especially try to remove redundant constraints

view this post on Zulip Janno (Apr 06 2021 at 10:06):

Hm. So what decides whether a > Set constraint is implicit or explicit, i.e. printed?

view this post on Zulip Gaëtan Gilbert (Apr 06 2021 at 10:09):

some magic
I recommend not caring

view this post on Zulip Janno (Apr 06 2021 at 10:14):

Okay, I'll try to not care about that. :)


Last updated: Jan 29 2023 at 01:02 UTC