The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

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

P.


2011/12/2  
<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