The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I have an Ordered class:

Class Ordered (A : Set) :=
{
  lt : A -> A -> Prop;
  lt_strict :> StrictOrder lt
}.

and I want to declare a class that Ordered based on keys, like:

Class KeyOrdered (A K : Set)(OK : Ordered K) :=
{
  getkey : A -> K
}.

but I also want to arrange things so that every "KeyOrdered A K OK" is
also considered "Ordered A", and to do so using the obvious ordering of
A's based on their keys via getkey: "a1 < a2" iff "lt (getkey a1)
(getkey a2)".  I can add "Ordered A" as s substructure, like this:

Class KeyOrdered (A K : Set)(OK : Ordered K) :=
{
  getkey : A -> K;
  OA :> Ordered A
}.

but that places the obligation on each instance of KeyOrdered to
demonstrate that it is Ordered A.  How do I remove this obligation with
a single general mapping?

Is it sufficient to leave out the "OA :> Ordered A", and instead
define an instance like this?:

Instance KOO(A Key : Set)(OK : Ordered K)(KO : KeyOrdered A K OK)
: Ordered A.

If I add this instance (which is easy to fully define), will every
"KeyOrdered A K OK" be considered an "Ordered A"?