coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop / Type (again)

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Prop / Type (again)
Date: Sat, 14 Dec 2019 14:09:19 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay10.mail.gandi.net
Ironport-phdr: 9a23:TsY8gRBA638NsTijG+mxUyQJP3N1i/DPJgcQr6AfoPdwSPvypcbcNUDSrc9gkEXOFd2Cra4d0KyM6/mrBTxIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfL1/IA+ooQnNq8UajoRvJ6UswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9VvQyvpxJ/zYDXbo+aOvVxcaHBct0VXmdBQsVcWjZdDo+gYYYCDewMNvtYoYnnoFsOqAOzCwi2C+Tz1j9HnHn20rU73eQgFQHJxxIvH8gSsH/Jq9j1O70dXv6pzKbSyzXPdfxW2Tb56IfTbB8hu+2MUKlrccrSyUgvDADFjlSVqYzgITyVzP4Bs26F4Op8TO+ijXMspQJpojW32Msgl4vEipgXx1zY7yl13YQ4KN6iREJlb9OoDINcuzyUOoZ5WM8uXmVltDwnxrAEvZO3ZjYGxZonyhPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq60iv1On8WdO00VpXsiZJiNzMuWoM1xzX8MSHReFy/kG81jaOzQzT7P9LIVwsmaraLZ4u3KIwm4INvUjeHCL6gkf7gLOMekk5+OWl6P7rbqvoq5OAL4N0jxvxMqUqmsyxG+Q4NQ0OUnCU+eumyrLj4Vf2QLNQgv05k6nZtIvVKtoBpq6lGAJVyYUj6hakDzel0dQYmHwHI0xfeB6diYjmJU3OLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g4gZQCeEBrKTGKLUq16BoOw1cMeWY4pAlz9+N/Ej0NHviXU0g0NVKaag0Icebja3H/BsLl+FSWHvk8wCEGIPsxB4SuH23g7RGQVPbmq/CvpvrgowD5irWN+aGtKdxYeZ1SL+JaV4I3hcAwnSQ2zrZp6HWvIJZTjUJMJ9wGRdBOqRDrQ53BTrjzfUjr9uL+7a4Cod7Myxz9tk/O7SkBQ/73pyAtjPijjQHVExpXsBQnoN5I46oUF5zQ3fg7J1h/VJTIQV4vpIVkE1PJjQzqp8BsygAg8=

When you write an inductive Coq will sometimes detect that it can be lowered to Prop without issue

>when singleton_rel is given as
> argument to a function which requires its argument to be (... -> ... ->
> Type), it fails.

cannot reproduce, eg

Check (fun _ : (forall U V _ _ _ _, Type) => _) singleton_rel.

works for me

Gaëtan Gilbert

On 14/12/2019 14:01, Jeremy Dawson wrote:

Hi,

In contrast to my last query on this general topic, when it seemed that
(sometimes) Set, Type and Prop were interchangeable, here coq changes
Type in my definition to Prop, and so when singleton_rel is given as
argument to a function which requires its argument to be (... -> ... ->
Type), it fails.

(* this definition replaces Type by Prop - why?
Inductive singleton_rel U V u v : U -> V -> Type :=
| srI : @singleton_rel U V u v u v : Type.
*)

Thanks for any help

Jeremy

[Coq-Club] Prop / Type (again), Jeremy Dawson, 12/14/2019
- Re: [Coq-Club] Prop / Type (again), Gaëtan Gilbert, 12/14/2019
  - Re: [Coq-Club] Prop / Type (again), Jeremy Dawson, 12/15/2019