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.

`boundednat k -> nat.`

will be the type, but the `Coercion`

command doesn't take types.

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

is `boundednat`

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.

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?

Exactly.

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

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.

`&`

means it's `sigT`

not `sig`

(not much difference though)

Right. (Is there a reason why we still have both `sig`

and `sigT`

?)

sig probably has better extraction

and possibly better type inference in some cases

Good point. Anything that avoids cumulativity helps with extraction.

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?

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`

.

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`

.

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.

Arpan Agrawal has marked this topic as resolved.

Last updated: Feb 06 2023 at 12:04 UTC