coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] prod is still polymorphic over sort Type/Prop ?

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] prod is still polymorphic over sort Type/Prop ?
Date: Mon, 19 Sep 2016 20:17:11 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f46.google.com
Ironport-phdr: 9a23:TgNslxT6BS15hSG/IdlBSDedLdpsv+yvbD5Q0YIujvd0So/mwa67bBeN2/xhgRfzUJnB7Loc0qyN4vmmCTBLuM3Z+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjYZBwNjz6ga/smJxKv6A7Vq8M+gI14K693xAGf8VVSfOED4Gp0OVKSkgu03cCi8Zd+u3BVsu49/stoVKzmY609C7tCA2J1YCgO+MT3uEybHkO07XwGXzBOnw==

Hi Abhishek,

[prod] is still "template polymorphic", its resulting sort is computed from the inferred sorts of its actual parameters, hence the result, which is consistent with previous Coq versions. A "fully" universe polymorphic prod would not have this behavior but rather the one you expected, where prod stays predicative (in Type) whatever the sorts of its parameters are.
-- Matthieu

On Mon, 19 Sep 2016 at 19:29, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

(* checked in Coq versions 8.5pl1 and 8.5pl2 *)

Variable A:Prop.
Variable B:Prop.
Variable AT:Type.
Variable BT:Type.

Check (prod AT BT).
(* Type *)

Fail Check ((prod AT BT):Prop).

Check (A:Type).

Check ((prod A B)).
(* Prop

How is this justified?
I expected Type.
*)

Check prod.
(*
prod
: Type -> Type -> Type
*)

Fail Check (AT:Prop).

-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] prod is still polymorphic over sort Type/Prop ?, Abhishek Anand, 09/19/2016
- Re: [Coq-Club] prod is still polymorphic over sort Type/Prop ?, Matthieu Sozeau, 09/19/2016