The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 19.05.2013 20:33, schrieb Daniel Schepler:
> 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

Hi Daniel,

Why not have something like this (which is the natural extension of + to 
three types):

Inductive threesum A B C : Type :=
  | introA : A -> threesum
  | introB : B -> threesum
  | introC : C -> threesum
  .

You don't have the asymmetry and it is general enough to support, e.g., 
other ordering relations.
Nevertheless, I think that a ternary elimination operator (like if for 
binary types) is really missing.
Nobody wants to write "match ... with introA _ => ...  | ... " or "match 
... with left (inleft _) => | left (inright _) => ... | _ => ...". 
Writing "{ lt_eq_lt_dec a b ? e1 | e2 | e3 }" or something would be nicer.