Library Coq.FSets.OrderedTypeEx
Require Import OrderedType.
Require Import ZArith.
Require Import Omega.
Require Import NArith Ndec.
Require Import Compare_dec.
First, a particular case of OrderedType where
the equality is the usual one of Coq.
Module Type UsualOrderedType.
Parameter Inline t : Type.
Definition eq := @eq t.
Parameter Inline lt : t -> t -> Prop.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Parameter compare : forall x y : t, Compare lt eq x y.
Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End UsualOrderedType.
a UsualOrderedType is in particular an OrderedType.
nat is an ordered type with respect to the usual order on natural numbers.
Module Nat_as_OT <: UsualOrderedType.
Definition t := nat.
Definition eq := @eq nat.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Definition lt := lt.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Definition compare : forall x y : t, Compare lt eq x y.
Definition eq_dec := eq_nat_dec.
End Nat_as_OT.
Z is an ordered type with respect to the usual order on integers.
Open Local Scope Z_scope.
Module Z_as_OT <: UsualOrderedType.
Definition t := Z.
Definition eq := @eq Z.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Definition lt (x y:Z) := (x<y).
Lemma lt_trans : forall x y z, x<y -> y<z -> x<z.
Lemma lt_not_eq : forall x y, x<y -> ~ x=y.
Definition compare : forall x y, Compare lt eq x y.
Definition eq_dec := Z_eq_dec.
End Z_as_OT.
positive is an ordered type with respect to the usual order on natural numbers.
Open Local Scope positive_scope.
Module Positive_as_OT <: UsualOrderedType.
Definition t:=positive.
Definition eq:=@eq positive.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Definition lt p q:= (p ?= q) Eq = Lt.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Definition compare : forall x y : t, Compare lt eq x y.
Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
End Positive_as_OT.
N is an ordered type with respect to the usual order on natural numbers.
Open Local Scope positive_scope.
Module N_as_OT <: UsualOrderedType.
Definition t:=N.
Definition eq:=@eq N.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Definition lt p q:= Nleb q p = false.
Definition lt_trans := Nltb_trans.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Definition compare : forall x y : t, Compare lt eq x y.
Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
End N_as_OT.
From two ordered types, we can build a new OrderedType
over their cartesian product, using the lexicographic order.
Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
Module MO1:=OrderedTypeFacts(O1).
Module MO2:=OrderedTypeFacts(O2).
Definition t := prod O1.t O2.t.
Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y).
Definition lt x y :=
O1.lt (fst x) (fst y) \/
(O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)).
Lemma eq_refl : forall x : t, eq x x.
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Definition compare : forall x y : t, Compare lt eq x y.
Defined.
Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
End PairOrderedType.