The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/22/2014 01:52 PM, Arnaud Spiwack wrote:
> > 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

But, can this be made to work in Coq, where there is no built-in 
irrelevance of any kind?

-- Jonathan