Arpan Agrawal (Feb 10 2022 at 11:26): 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.
Paolo Giarrusso (Feb 10 2022 at 11:27):boundednat k -> nat. will be the type, but the Coercion command doesn't take types.
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
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.
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?
Guillaume Melquiond (Feb 10 2022 at 11:39):Exactly.
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
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.
Gaëtan Gilbert (Feb 10 2022 at 12:13):& means it's sigT not sig (not much difference though)
Guillaume Melquiond (Feb 10 2022 at 12:19):Right. (Is there a reason why we still have both sig and sigT?)
Gaëtan Gilbert (Feb 10 2022 at 12:25):sig probably has better extraction
Gaëtan Gilbert (Feb 10 2022 at 12:25):and possibly better type inference in some cases
Guillaume Melquiond (Feb 10 2022 at 12:29):Good point. Anything that avoids cumulativity helps with extraction.
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?
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.
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.
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.
Notification Bot (Feb 10 2022 at 17:35):Arpan Agrawal has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC