Library Ordered
Constructions of ordered types, for use with the
FSet functors
for finite sets and the FMap functors for finite maps.
Require Import FSets.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
The ordered type of positive numbers
Module OrderedPositive <: OrderedType.
Definition t := positive.
Definition eq (x y: t) := x = y.
Definition lt := Plt.
Lemma eq_refl : forall x : t, eq x x.
Proof (@refl_equal t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@sym_equal t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@trans_equal t).
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof Plt_trans.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof Plt_ne.
Lemma compare : forall x y : t, Compare lt eq x y.
Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
End OrderedPositive.
The ordered type of machine integers
Module OrderedInt <: OrderedType.
Definition t := int.
Definition eq (x y: t) := x = y.
Definition lt (x y: t) := Int.unsigned x < Int.unsigned y.
Lemma eq_refl : forall x : t, eq x x.
Proof (@refl_equal t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@sym_equal t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@trans_equal t).
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.
Lemma compare : forall x y : t, Compare lt eq x y.
Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec.
End OrderedInt.
Indexed types (those that inject into
positive) are ordered.
Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType.
Definition t := A.t.
Definition eq (x y: t) := x = y.
Definition lt (x y: t) := Plt (A.index x) (A.index y).
Lemma eq_refl : forall x : t, eq x x.
Proof (@refl_equal t).
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@sym_equal t).
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@trans_equal t).
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.
Lemma compare : forall x y : t, Compare lt eq x y.
Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
End OrderedIndexed.
The product of two ordered types is ordered.
Module OrderedPair (A B: OrderedType) <: OrderedType.
Definition t := (A.t * B.t)%type.
Definition eq (x y: t) :=
A.eq (fst x) (fst y) /\ B.eq (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.
Definition lt (x y: t) :=
A.lt (fst x) (fst y) \/
(A.eq (fst x) (fst y) /\ B.lt (snd x) (snd y)).
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.
Lemma compare : forall x y : t, Compare lt eq x y.
Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
End OrderedPair.