Converting Orders.OrderedType to OrderedType.OrderedType?

[b***@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

[Pierre Courtieu]

These modules are already given in the standard library, look in
theories/Structures/OrderedTypeEx.v for Nat_as_OT for example.

P.

Post by b***@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?
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

[b***@yahoo.com]

Post by Pierre Courtieu
These modules are already given in the standard library, look in
theories/Structures/OrderedTypeEx.v for Nat_as_OT for example.

Thanks. That answers the problem of getting a Nat_as_OT suitable for FMap.

It doesn't seem to provide a general conversion functor, which might not be
that useful overall, but would at least be applicable for cases such as Q
(maybe for an FSet).

[Pierre Letouzey]

----- Mail original -----

Post by b***@yahoo.com

Post by Pierre Courtieu
These modules are already given in the standard library, look in
theories/Structures/OrderedTypeEx.v for Nat_as_OT for example.

Thanks. That answers the problem of getting a Nat_as_OT suitable for
FMap.
It doesn't seem to provide a general conversion functor, which might
not be that useful overall, but would at least be applicable for cases such
as Q (maybe for an FSet).

Such conversion functors already exist : in theories/Structures/OrdersAlt.v,
look for Update_OT and Backport_OT.

My apologies for the current situation which is rather complex.
the transition between old-style OrderedType and the new one isn't
finished yet (some work remain to be done on FMaps for instance),
and we cannot simply remove the old-style OrderedType. Moreover,
the documentation of all these structures is clearly not sufficient yet.
Sorry for that...

Best regards,
Pierre Letouzey