The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 05:36 PM, Daniel Schepler 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.

Here's is all that I do, really:

Inductive Erasable(A : Type) : Prop :=
  erasable: A -> Erasable A.

Arguments erasable [A] _.

Axiom Erasable_inj : forall {A : Type}{a b : A}, erasable a=erasable b -> a=b.

I then use "Erasable nat" (##nat via notation) instead of nat, and "erasable 42" (#42 via notation) instead of 42.

I am not sure I understand the difference you are suggesting.  For instance, are you saying that if I want an erasable constant replacement for 42, I instead use a function from a singleton type based on 42 to Prop?  And then achieve injectivity using some variety of extensionality?  Hmmm.....

-- Jonathan