The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/22/2014 04:04 AM, Arnaud Spiwack wrote:
> 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).

Thank you very much for that link!  I was not aware of this.

> 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 ]).

I have had some communications with developers of Idris who are working 
on an implementation of erasability there.  But, I should read Edwin's 
thesis at some point.  I am somewhat familiar with the paper you link 
above.  One of the things that I hope to point out is that Coq's 
separation of Prop from Set and Type does not entail the requirement for 
code duplication in order to get an effective erasure of all 
proof-related terms.  For example, I did not duplicate list or nat in 
rbtree.v.

> 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).

I tried using "difflists" - which are the list implementation of this 
idea, and it did not work.  There were two ways I tried using it.  The 
first was to use difflists as a complete replacement for lists.  This 
failed to work because of requirements for lemmas such as sortedr, which 
states:

forall x y, sorted (x ++ y) -> sorted y.

If x is a difflist, then it is really just a function mapping (normal) 
lists to lists, and append is just a type of function composition.  
However, consider the function reverse, which is also a function mapping 
lists to lists - obviously, the above lemma is false if x is the reverse 
function.

An alternative hybrid use of difflist that I tried was to have just the 
append operator itself be difflist-based, while the rest of the lists 
are normal lists, with the addition of implicit coercion. This did not 
work either, but it is more difficult to explain why.

> 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).

This looks very promising!  Thanks for this link as well!

-- Jonathan