The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sun, May 19, 2013 at 2:03 PM, Jonas Oberhauser <s9joober AT gmail.com> wrote:

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.

Well, in the case that you want to do something different in each of the three cases, I think it's very readable to have
match compare x y with
| IsLt _ => less_than_case
| IsEq _ => equal_case
| IsGt _ => greater_than_case
end
and the proposed { lt_eq_lt_dec a b ? e1 | e2 | e3 } doesn't seem as nice to me.  And for the cases where you really want one case for <= and a different case for > it would be easy enough to define le_dec x y.

Also, by the way, in a later version of my StringCompare.v I introduced a notation
Notation "x ||| y" :=
  match x with
  | IsLt _ => IsLt _ _ _ _
  | IsGt _ => IsGt _ _ _ _
  | IsEq _ => y
  end
  (right associativity, at level 51).
which allows for writing very Perl-like compound comparisons like "ascii_compare a1 a2 ||| ReduceCmp (string_compare s1' s2')".  This kind of notation wouldn't make much sense for the more general three-way sum.
-- 
Daniel Schepler