The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 22 Apr 2014 18:45:59 -0400,
Jonathan 
<jonikelee AT gmail.com>
 a écrit :

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

If you can decide of some property, then you have a form of irrelevance.
Any function to the 'bool' type can be converted in a function to
'Prop' by composition with 'conv (fun x => if x then True else False) :
bool -> Prop'. And for any boolean 'b', a term of type 'conv b' is
"irrelevant" (there is only a single habitant to that type).

That is mainly the main reason why we have UIP on decidable equalities.