The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Personally, I prefer to write comparison operators to be more like Perl's <=> operator.  And I don't really like to use { x < y } + { x = y } + { x > y } as the result of this, as the constructors of the different cases are a bit awkward to look at.  (And even though that could probably be worked around using notations, the extraction would still have the asymmetrical ugliness.)  So I roll my own inductive type "comparison_with_proof" for the result, since I couldn't find any suitable inductive type in the standard library that did exactly what I wanted.

So, this thread inspired me to mock up what proof-carrying comparison operators on ascii and string might look like, in the attached file.  A couple points: First, the proofs of vector_lt_irrefl, vector_lt_trans, string_lt_irrefl would probably get bad marks in one of Prof. Chlipala's classes as insufficiently automated...  And in more general cases, you'd probably want to allow a general equivalence relation in place of eq for those cases where you're using setoids and you don't want to (or can't) define an explicit quotient type of the setoid.
-- 
Daniel Schepler

Attachment: StringCompare.v
Description: Binary data