The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

On Sun, Feb 22, 2009 at 7:52 PM, Samuel E. Moelius III
<moelius AT cis.udel.edu>
 wrote:
> Please let me rephrase my question then.  Consider the following two
> approaches.
>
> (1) What is now done in the library (using the ``Carrier_of'' field).
>
> (2) Doing something similar to what I wrote above, letting U be a
> sigma-type, if necessary.
>
> What are the advantages of (1) over (2)?  Or is it just a matter of taste?

OK I see it's an interesting point. The only real advantage I can
think of (and Id like to have the opinion of others on this list) is
that (1) allows you to relate objects that have different carriers on
the same type U. The typical example would be substructures such as
subgroups, etc. In our case, with partial order, you may want to
define what it means for a PO to be restriction of another PO on a
smaller carrier. You can easily do that with the first method :

Inductive restriction (U : Set) (P : PO U) (Q : PO U) : Prop :=
| mk_restriction : subset (Carrier_of P) (Carrier_of Q) -> (forall x
y, Rel_of P x y -> Rel_of Q x y) -> restriction U P Q.

With the second method, you would have to explicitely mention a
"coercion" function between your two carriers U and U', or you would
have to restrict your definition to sigma types.

It is not something I just "forged" actually, it happened to me once
to have a converging (and increasing) sequence of sets S : nat -> (U
-> Prop), and I had to define a relation by successive refinements
over the (S n), it was very handy to be able to relate relations in a
similar way as above.

> Stéphane: Thanks for your help, BTW.  :)
You're very welcome :) I hope this helps.

Stéphane L.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06