Stream: Coq users

Topic: ✔ Coercion of boundednat to nat


view this post on Zulip Arpan Agrawal (Feb 10 2022 at 11:26):

I'm reading "A type theory with definitional proof-irrelevance" and as a demonstration of the need for Proof Irrelevance, there is

Definition boundednat (k : nat) : Type := { n : nat & n <= k }.

Followed by

Coercion boundednat_to_nat : boundednat >-> nat.

I am trying to understand how this coercion would work, and my first thought is that the coercion should be from boundednat k to nat.
Am I misunderstanding what the coercion is doing?

I looked at the manual page for Coercions but could not find anything relevant.

view this post on Zulip Paolo Giarrusso (Feb 10 2022 at 11:27):

boundednat k -> nat. will be the type, but the Coercion command doesn't take types.

view this post on Zulip Paolo Giarrusso (Feb 10 2022 at 11:28):

it takes "classes", which are defined in the manual; and the class for boundednat k is boundednat

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 11:34):

Coercion lookup is purely directed by the head symbols of the source and target types. That is why the Coercion command only cares about these head symbols (the so-called "classes"), that is, boundednat for the source type and nat for the target type.

view this post on Zulip Arpan Agrawal (Feb 10 2022 at 11:36):

So to make that work, I would first have to define a function (called boundednat_to_nat, of type boundednat k -> nat) that converts a given element of boundednat k to the corresponding nat?

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 11:39):

Exactly.

view this post on Zulip Arpan Agrawal (Feb 10 2022 at 11:53):

Wouldnt it be better to use a sig instead of Type as the type of boundednat k?
With Type, I am unsure as to how I would define the boundednat_to_nat function

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 12:12):

There seems to be some confusion. boundednat is sig, which is what you want. It just happens that sig itself (and thus boundednat too) is of type Type, but this is irrelevant.

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 12:13):

& means it's sigT not sig (not much difference though)

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 12:19):

Right. (Is there a reason why we still have both sig and sigT?)

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 12:25):

sig probably has better extraction

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 12:25):

and possibly better type inference in some cases

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 12:29):

Good point. Anything that avoids cumulativity helps with extraction.

view this post on Zulip Arpan Agrawal (Feb 10 2022 at 12:37):

Definition boundednat_to_nat (boundednat k: Type) : nat
:= projT1 (A:= nat) (le _ k).

Why does Coq think k is of type Type instead of nat?

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 12:39):

If you write (boundednat k: Type), you are telling Coq that boundednat_to_nat takes two arguments named boundednt and k, both of type Type.

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 12:40):

What you want is (k:nat) (b:boundednat k), which tells Coq that the function takes two arguments named k and b, the latter being of type boundednat k.

view this post on Zulip Arpan Agrawal (Feb 10 2022 at 12:53):

Right, yes, I dont know what I was thinking there.
Thanks for all your help!
I managed to make it work with:

Definition boundednat (k : nat) : Type := {n : nat & n <= k}.

Definition boundednat_to_nat (k: nat) (bn: boundednat k) : nat
:= projT1 bn.

Coercion boundednat_to_nat : boundednat >-> nat.

view this post on Zulip Notification Bot (Feb 10 2022 at 17:35):

Arpan Agrawal has marked this topic as resolved.


Last updated: Feb 06 2023 at 12:04 UTC