The Coq mailing list

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

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.

Indeed, this is why you need (conversion level) proof irrelevance: you need to restrict to the type of functions from lists to lists which are of the form (λy. l++y) for some list l. Associative laws will be up to conversion only if the proof (essentially the list l) is irrelevant to the conversion.

/Arnaud Spiwack