The Coq mailing list

[brandon_m_moore AT yahoo.com]

I had hoped to make a module type of maps over nat keys by applying

Module Type Sfun (E : OrderedType).

from FMapInterface to

Module Nat_as_OT <: OrderedTypeFull.

from NatOrderedType, but unfortunately one is Orders.OrderedType and the other
OrderedType.OrderedType.

Is there a standard way to convert between them?
I resorted to this:

Require Import Structures.Orders.
Require Import Structures.OrderedType.

Module OT_TO_OT(O : Orders.OrderedType)
  : OrderedType.OrderedType
      with Definition t := O.t
      with Definition eq := O.eq
      with Definition lt := O.lt.
  Definition t := O.t.
  Definition eq := O.eq.
  Definition eq_refl := Equivalence_Reflexive.
  Definition eq_sym := Equivalence_Symmetric.
  Definition eq_trans := Equivalence_Transitive.
  Definition eq_dec := O.eq_dec.
  Definition lt := O.lt.
  Definition lt_trans := StrictOrder_Transitive.
  Definition lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
    intros. contradict H.
    rewrite <- (O.lt_compat (Equivalence_Reflexive x) H).
    apply StrictOrder_Irreflexive.
  Qed.
  Definition compare : forall x y, Compare lt eq x y.
    intros. pose proof (O.compare_spec x y).
    destruct (O.compare x y);
      [apply EQ|apply LT|apply GT];
      inversion H; apply H0.
  Qed.
End OT_TO_OT.

I hoped tried to use Include, but the signatures
have different types for compare and I didn't see any way
to shadow or avoid including it.

Type classes worked pleasantly for the relation properties.

Brandon