Kiran Gopinathan (Nov 25 2022 at 06:29): 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.
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.
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.
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
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.
Kiran Gopinathan (Nov 26 2022 at 09:53):@Gaëtan Gilbert could you clarify what the formal definition of impredicativity is?
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
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: Oct 13 2024 at 01:02 UTC