The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

M. Scott Doerrie wrote:
> I suppose I have assumed that since everything is complete, decidable, 
> deterministic, and finite, that the result of union_sort and add_sort 
> would be identical structures when union and add produced identical 
> structures.  Why can I talk about having identical resulting 
> structures over union and add and not union_sort and add_sort?

The latter return proofs.  Coq's type system _intentionally_ blocks some 
"obvious" computational equivalences over proofs, so that extraction to 
OCaml is sound.  Extraction erases proofs, so it's important that some 
kinds of computations over proofs are impossible, since the proofs won't 
be around "at runtime" to compute with.

Also, even ignoring this (which I'm not sure is fair to give as the 
culprit for your problem), imagine that we encode proofs in [Set] 
instead.  You _can_ talk about having identical structures here, but you 
don't automatically get that every possible comparison type has exactly 
one member.  This depends on the details of individual notions of 
comparison.