The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Dear Michael,

> "Soegtrop, Michael" 
> <michael.soegtrop AT intel.com>
>  writes:

> My larger goal is to create order structures (like TotalOrder) from
> user supplied types and boolean comparison operators in a reasonably
> efficient way. Using Nat.eqb was just an example. I am interested in
> elegant proof techniques for such kind of goals, but not so much in
> this specific goal.

You may be interested in Cyril's Cohen recent work.

https://github.com/Barbichu/finmap (see order.v) there.

The approach followed there (as well as in most of math-comp) is to
provide Canonical Structures for your orders and let Coq infer them when
needed, which is almost the same as type classes. Depending on what
you'd like to do this may work better or worse, as you've seen there are
many different styles.

"Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 writes:

> Say I have some type class structure T for a relation R, I know that
> relation R and S are equivalent (forall x y, R x y <-> S x y) and I
> want to derive structure T for S. Is there a generic way to do this
> for any structure T?

The way it is done in math-comp/ssreflect is indeed to provide
"builders" that take some proof of equivalence and indeed build the new
structure for S.

Quoting an example from the documentation:

(* PcanFinMixin fK == the Finite mixin for T, given f : T -> fT and g with fT 
*)
(*                    a finType and fK : pcancel f g.                         
*)

So if you have a (partial) embedding from T to a finite type, then you
can equiv T with a finite type structure. Note that this approach may
not be the best if you still need to compute with the transported class.

Best regards,
Emilio