The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

Uhm, I'm a little worried about this idea of selective proof
irrelevance and the interaction with an injectivity axiom
for some nat -> Prop constructor.  This is exactly what we
wanted in Ynot, but I didn't see how to do it safely...

Can you say more Jonathan?  

-Greg

On Sep 12, 2014, at 5:36 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:

> On Fri, Sep 12, 2014 at 1:52 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>> But, if one is willing, one can exploit the Prop universe to get such 
>> things
>> erased.  This can complicate things a bit - for example, you would need an
>> alternate definition of Vector - but that is fairly easy (if lengthy) to
>> achieve.  To exploit the Prop universe this way requires adding an axiom -
>> with the usual consistency risks of doing so - but it is a very simple 
>> axiom
>> that, as far as I know, is only incompatible with general proof-irrelevance
>> (among the typical other axioms that are frequently added to Coq), but not
>> with specific proof-irrelevance (defined separately for each Prop one 
>> wishes
>> to be irrelevant, such as equality).  The idea of this axiom is to make a
>> single Prop relevant by adding an injectivity axiom to its sole 
>> constructor,
>> and to use "lifted" (into that single Prop) versions of types and values 
>> you
>> want erased in those spots where you want them erased - and then allow 
>> Coq's
>> normal Prop removal to do its thing.  With careful handling, one can get
>> OCaml output from Coq with this addition that is quite clean.
> 
> And here, all this time, I thought you were using something more like
> a singleton monad: passing an argument of type (nat -> Prop) in place
> of nat which is understood (or maybe even restricted) to be a
> singleton set.  That should probably work along with proof
> irrelevance, maybe with an axiom like Extensionality_Ensembles but
> maybe even without it.
> -- 
> Daniel Schepler