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.
Create HintDb ordered_type.
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.
lia. 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.
lia.
Qed.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Proof.
unfold lt,
eq;
intros;
red;
intros.
subst.
lia.
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 option type is ordered.
Module OrderedOption (
A:
OrderedType) <:
OrderedType.
Definition t :=
option A.t.
Definition eq (
x y:
t) :=
option_rel A.eq x y.
Lemma eq_refl :
forall x,
eq x x.
Proof.
destruct x;
constructor.
apply A.eq_refl. Qed.
Lemma eq_sym :
forall x y,
eq x y ->
eq y x.
Proof.
intros *
EQ;
inv EQ;
constructor.
now apply A.eq_sym.
Qed.
Lemma eq_trans :
forall x y z,
eq x y ->
eq y z ->
eq x z.
Proof.
intros *
EQ1 EQ2;
inv EQ1;
inv EQ2;
constructor.
eapply A.eq_trans;
eauto.
Qed.
Definition lt (
x y:
t) :=
match x,
y with
|
Some x,
Some y =>
A.lt x y
|
None,
Some _ =>
True
| _,
None =>
False
end.
Lemma lt_trans :
forall x y z :
t,
lt x y ->
lt y z ->
lt x z.
Proof.
intros [] [] []
LT1 LT2;
simpl in *;
eauto using A.lt_trans.
now inv LT1.
Qed.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Proof.
intros *
LT EQ;
inv EQ;
simpl in *;
auto.
eapply A.lt_not_eq;
eauto.
Qed.
Lemma compare :
forall x y :
t,
Compare lt eq x y.
Proof.
intros [] [].
-
destruct (
A.compare t0 t1); [
apply LT|
apply EQ|
apply GT];
auto.
now constructor.
-
now apply GT.
-
now apply LT.
-
apply EQ.
constructor.
Defined.
Lemma eq_dec :
forall x y, {
eq x y } + { ~
eq x y }.
Proof.
intros [] [];
simpl.
destruct (
A.eq_dec t0 t1).
1,5:
left;
constructor;
auto.
all:
right;
intros *
CONTRA;
inv CONTRA;
eauto.
Defined.
End OrderedOption.
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 with ordered_type.
Qed.
Lemma eq_sym :
forall x y :
t,
eq x y ->
eq y x.
Proof.
unfold eq;
intros.
intuition auto with ordered_type.
Qed.
Lemma eq_trans :
forall x y z :
t,
eq x y ->
eq y z ->
eq x z.
Proof.
unfold eq;
intros.
intuition eauto with ordered_type.
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.