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 (@
eq_refl t).
Lemma eq_sym :
forall x y :
t,
eq x y ->
eq y x.
Proof (@
eq_sym t).
Lemma eq_trans :
forall x y z :
t,
eq x y ->
eq y z ->
eq x z.
Proof (@
eq_trans 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.
Proof.
Definition eq_dec :
forall x y, {
eq x y } + { ~
eq x y } :=
peq.
End OrderedPositive.
The ordered type of integers
Module OrderedZ <:
OrderedType.
Definition t :=
Z.
Definition eq (
x y:
t) :=
x =
y.
Definition lt :=
Z.lt.
Lemma eq_refl :
forall x :
t,
eq x x.
Proof (@
eq_refl t).
Lemma eq_sym :
forall x y :
t,
eq x y ->
eq y x.
Proof (@
eq_sym t).
Lemma eq_trans :
forall x y z :
t,
eq x y ->
eq y z ->
eq x z.
Proof (@
eq_trans t).
Lemma lt_trans :
forall x y z :
t,
lt x y ->
lt y z ->
lt x z.
Proof Z.lt_trans.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Proof.
unfold lt,
eq,
t;
intros.
omega. Qed.
Lemma compare :
forall x y :
t,
Compare lt eq x y.
Proof.
Definition eq_dec :
forall x y, {
eq x y } + { ~
eq x y } :=
zeq.
End OrderedZ.
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 (@
eq_refl t).
Lemma eq_sym :
forall x y :
t,
eq x y ->
eq y x.
Proof (@
eq_sym t).
Lemma eq_trans :
forall x y z :
t,
eq x y ->
eq y z ->
eq x z.
Proof (@
eq_trans t).
Lemma lt_trans :
forall x y z :
t,
lt x y ->
lt y z ->
lt x z.
Proof.
unfold lt;
intros.
omega.
Qed.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Proof.
unfold lt,
eq;
intros;
red;
intros.
subst.
omega.
Qed.
Lemma compare :
forall x y :
t,
Compare lt eq x y.
Proof.
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 (@
eq_refl t).
Lemma eq_sym :
forall x y :
t,
eq x y ->
eq y x.
Proof (@
eq_sym t).
Lemma eq_trans :
forall x y z :
t,
eq x y ->
eq y z ->
eq x z.
Proof (@
eq_trans t).
Lemma lt_trans :
forall x y z :
t,
lt x y ->
lt y z ->
lt x z.
Proof.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Proof.
Lemma compare :
forall x y :
t,
Compare lt eq x y.
Proof.
Lemma eq_dec :
forall x y, {
eq x y } + { ~
eq x y }.
Proof.
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.
Proof.
intros; split; auto.
Qed.
Lemma eq_sym :
forall x y :
t,
eq x y ->
eq y x.
Proof.
unfold eq;
intros.
intuition auto.
Qed.
Lemma eq_trans :
forall x y z :
t,
eq x y ->
eq y z ->
eq x z.
Proof.
unfold eq;
intros.
intuition eauto.
Qed.
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.
Proof.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Proof.
unfold lt,
eq,
not;
intros.
elim H0;
intros.
elim H;
intro.
apply (@
A.lt_not_eq _ _ H3 H1).
elim H3;
intros.
apply (@
B.lt_not_eq _ _ H5 H2).
Qed.
Lemma compare :
forall x y :
t,
Compare lt eq x y.
Proof.
intros.
case (
A.compare (
fst x) (
fst y));
intro.
apply LT.
red.
left.
auto.
case (
B.compare (
snd x) (
snd y));
intro.
apply LT.
red.
right.
tauto.
apply EQ.
red.
tauto.
apply GT.
red.
right.
split.
apply A.eq_sym.
auto.
auto.
apply GT.
red.
left.
auto.
Defined.
Lemma eq_dec :
forall x y, {
eq x y } + { ~
eq x y }.
Proof.
unfold eq;
intros.
case (
A.eq_dec (
fst x) (
fst y));
intros.
case (
B.eq_dec (
snd x) (
snd y));
intros.
left;
auto.
right;
intuition.
right;
intuition.
Defined.
End OrderedPair.