The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/25/2016 10:18 PM, roux cody wrote:
> ...
> > As for building-in proof irrelevance (while having a separate HoTT mode)
> > that might not bother anyone but me: I (ab)use proof *relevance* in Coq as
> > a way to get really good erasability.
> I'm confused about this. Could you elaborate? Proof-irrelevance and proof
> erasure seem to go rather well together, in my mind.

Coq's standard erasures of Prop, type-like things, and the ability to do 
Extraction Implicit don't erase everything that could be erased.  For 
example, they don't erase non-Prop data (in Set) that is passed around 
and used only "uninformatively" - meaning only by Props.  Consider, for 
example, the height of a binary tree used in invariants in dependent 
types defining the tree and its functions, but which one doesn't want to 
be a field of the extracted binary tree or args in the extracted 
functions.  So, I do this:

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

Arguments erasable [A] _.
...
Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a= erasable b 
-> a=b.

Adding this erasable injectivity axiom makes proofs relevant. However, 
it gives me the ability to pass around and use (in Props) all manner of 
things wrapped in the erasable constructor that Coq will then end up 
erasing at extraction time.  This trick works great, especially when one 
is embedding many complex invariants into dependent types.  But I still 
wish I didn't have to use it.

If you're interested in how nicely erased the extracted results are, you 
can take a look at my github projects:

https://github.com/jonleivent/mindless-coding (stale, slightly bit-rotted)
https://github.com/jonleivent/mindless-coding-phase2 (up-to-date for Coq 
8.5)

The best comparison would be in mindless-coding-phase2, between files 
wavl.v and its extraction wavl.ml - or, if you'd prefer the 
non-proof-mode version: wavl-noninter.v and wavl-noninter.ml.

-- Jonathan