Universes

[Zimmi48]

This discussion is bound to happen at some point, so we might just as well start a new thread now, with this quote from @HuStmpHrrr on Coq-Club:

I am not sure if stdlib2 plans to make things primarily in Type and make use of sProp whenever necessary. If that's the case, it would make the future much brighter.

I'm not really expecting any answer now, just recording this for later.

[HuStmpHrrr]

thank you for opening this issue.

It seems stdlib2 is getting started and there are some Prop's around already. I think this is a very important design decision and is probably not straightforward to revert. not sure how should this be organized.

[SkySkimmer]

I'm not clear on what the issue with using Prop is.

[HuStmpHrrr]

the issue with Prop is if a property relies on elimination on another definition, and if that definition is Prop, it will pretty much force all related definitions to be Prop too.

I find Prop is so hard to use and very unnecessary. for example, Exists for lists is so strange to be defined in Prop: https://coq.inria.fr/library/Coq.Lists.List.html#Exists

the situation here, is Exists is so weak that I don't even know which index the target proposition is witnessed, despite the fact that all lists are finite. why I wouldn't want to know about the index provided the information has already been here? figuring out which index is the witness pretty much requires power to decide all propositions, and therefore LEM or Choice.

I think there can be more examples. I hope I am not too shallow but I am fairly scared of Prop now. defining in Prop is really a design decision that "there will not be any users in the future who need to inspect the internal language", but how can that be true in general? all the questions I posted the other days on coq-club can all be resolved in trivial ways, if all my dependencies were not operating in Prop.

after all, there are so many problems that can be defined in proof relevant way, so why they need to be made irrelevant with no obvious advantage? I find it very strange.

[spitters]

Prop is an artifact from the time that Coq was geared towards program extraction. HoTT's hProp (i.e. with unique choice and propositional extensionality) would be closer to the usual intuition. Alternatively, one could use propositions as types. Using sProp gives an interesting new alternative.

…

On Mon, Mar 25, 2019 at 3:24 PM Jason Hu ***@***.***> wrote: the issue with Prop is if a property relies on elimination on another definition, and if that definition is Prop, it will pretty much force all related definitions to be Prop too. I find Prop is so hard to use and very unnecessary. for example, Exists for lists is so strange to be defined in Prop: https://coq.inria.fr/library/Coq.Lists.List.html#Exists the situation here, is Exists is so weak that I don't even know which index the target proposition is witnessed, despite the fact that all lists are finite. why I wouldn't want to know about the index provided the information has already been here? figuring out which index is the witness pretty much requires power to decide all propositions, and therefore LEM or Choice. I think there can be more examples. I hope I am not too shallow but I am fairly scared of Prop now. defining in Prop is really a design decision that "there will not be any users in the future who need to inspect the internal language", but how can that be true in general? there are situations where irrelevance can be proven, but that's not always possible. all the questions I posted the other days on coq-club can all be resolved in trivial ways, if all my dependencies were not operating in Prop. after all, there are so many problems that can be defined in proof relevant way, so why they need to be made irrelevant with no obvious advantage? I find it very strange. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[gmalecha]

Are types exposed by stdlib2 universe polymorphic? I didn't notice any Set Universe Polymorphism, but I did see Global Unset Auto Template Polymorphism. Does that make everything universe polymorphic?

[gmalecha]

@spitters Prop has the "benefit" of being impredicative. That might factor into things as well.

[Zimmi48]

I didn't notice any Set Universe Polymorphism, but I did see Global Unset Auto Template Polymorphism. Does that make everything universe polymorphic?

It doesn't but I would expect this to be the objective (or at least some attempt to be made).

[spitters]

@gmalecha I wonder who is using Prop without wanting to use UIP too.

[ppedrot]

@spitters do you mean proof-irrelevance rather than UIP? In that case there are some use-cases for impredicative set (which is still part of the kernel of Coq AFAIK) geared towards programming. At some point we relied on this to extract the tactic monad, an actually case of bootstrapping. Stuff like Mendler's encoding is another example from the top of my head.

[spitters]

@ppedrot Yes, I meant PI.
Indeed, I use impredicative set in some of my programming exercises for Fw, but I wouldn't put it in stdlib2.