The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Dear Jonathan,

This is a nice example. Note that this precise idea has been explored before (see for instance http://www.pps.univ-paris-diderot.fr/~letouzey/download/Letouzey_Spitters_05.pdf ).

As you elegantly notice, there is a use for a proof relevant (so that you can discriminate between annotations) yet static/erasable sort. Erasing proof irrelevant things is, by the way, one of the key points of Edwin Brady's thesis (see for instance [ http://eb.host.cs.st-andrews.ac.uk/writings/types2003.pdf ]).

For unification/conversion up to monoid laws, there is a solution which uses proof irrelevance in conversion (!). It's been found by Alan Jeffrey in Agda [ https://lists.chalmers.se/pipermail/agda/2011/003420.html ]. The idea is that every monoid is a submonoid of a function monoid (with identity and composition). This is a classic result, a variant of Cayley's theorem [ http://en.wikipedia.org/wiki/Cayley%27s_theorem ]: specifically for a monoid M, it is a submonoid of the functions M⟶M, each element x being interpreted as (λy. x⋆y). The above link contains the details, but this lemma allows to turn any monoid in a monoid where associativity is up to conversion (provided we have a way to do some conversion level proof irrelevance like in Agda).

Another tool is Pierre-Yves Strub CoqMT [ http://pierre-yves.strub.nu/coqmt/ ], which allows to plug in decision procedures inside the conversion of Coq (the current prototype has Presburger's arithmetic if I'm not mistaken).

Both proof irrelevance and CoqMT are considered for integration with Coq (CoqMT will most likely be first).

/Arnaud Spiwack

On 21 April 2014 21:02, Jonathan <jonikelee AT gmail.com> wrote:

To all,

If you're interested in a way to get full erasability in Coq, or yet another encoding of Red/Black trees in Coq, have a look at:

https://github.com/jonleivent/mindless-coding

Erasability is accomplished by adding a single injectivity axiom to a single wrapper Prop type (Erasable).  The readme explains things, and the Coq file is fairly well commented.

Any comments and/or criticisms are welcome!

-- Jonathan