The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

M. Scott Doerrie wrote:
> You are correct that I've been assuming FSetLists as my structure.  I 
> had not considered the AVL structure, for which this wouldn't hold.
> I do not understand where proof-irrelevance would enter for 
> FSetLists.  I had thought that with identical representations, the 
> proofs of sorting would also be identical.  What did I miss here?

A proof of sortedness can involve arbitrary mathematical machinery.  
What is it that makes you think that any two such proofs can be shown 
equal in Coq?  This would require showing that, modulo the definitional 
equality, the proofs have the same syntax.  There can be many proofs of 
the same proposition that use very different proof strategies and so 
have very different syntax.