Stream: Coq users

Topic: Quantifying over Type and remaining in Prop


view this post on Zulip Kiran Gopinathan (Nov 25 2022 at 06:29):

This might be a dumb question and I'm blanking on something obvious, but could someone give the justification for why when we quantify over Types but return a prop, the result is still in prop?

Check ((forall (x: Type), 1 = 1) : Prop).

Is this related to the impredicativity of Prop? I thought that was just about quantifying over Prop still being in Prop, rather than quantifying over Type.

view this post on Zulip Kiran Gopinathan (Nov 25 2022 at 06:41):

I guess more specifically I'm asking about the justification for the Prod-Prop typing rule: https://coq.inria.fr/refman/language/cic.html#id6

The manual explains that no values of a term of type Prop are extractable, hence this rule, but I was wondering if there was some more justification for this.

view this post on Zulip Guillaume Melquiond (Nov 25 2022 at 07:31):

No, that is about it. Objects in Prop are non-informational. Quantifying over them does not change that fact. Pretending that they suddenly carry some information due to quantification would just make the system more painful to use.

view this post on Zulip Gaëtan Gilbert (Nov 25 2022 at 09:02):

Is this related to the impredicativity of Prop? I thought that was just about quantifying over Prop still being in Prop, rather than quantifying over Type.

impredicativity of Prop means that we have the Prod-Prop rule
quantifying over Prop is not special

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 02:22):

It's probably fair to say the real reason isn't obvious: (1) you build an appropriate proof that Coq's metatheory has certain good properties (say, it's logically sound) (2) you see this rule isn't a problem. And step (1) isn't trivial.

view this post on Zulip Kiran Gopinathan (Nov 26 2022 at 09:53):

@Gaëtan Gilbert could you clarify what the formal definition of impredicativity is?

view this post on Zulip Gaëtan Gilbert (Nov 26 2022 at 10:44):

a sort s is impredicative when for all product types if the codomain is in s then the product type is also in s

view this post on Zulip Stefan Monnier (Nov 26 2022 at 17:53):

Just to clarify: Gaëtan describes the kind of impredicativity accepted by Coq. Impredicativity itself is a more general notion which can be introduced in a few different ways (some of which will introduce known forms of unsoundness).


Last updated: Jan 28 2023 at 06:30 UTC