Library Coq.Structures.OrderedTypeEx
Examples of Ordered Type structures.
First, a particular case of
OrderedType where
the equality is the usual one of Coq.
a UsualOrderedType is in particular an OrderedType.
nat is an ordered type with respect to the usual order on natural numbers.
Z is an ordered type with respect to the usual order on integers.
positive is an ordered type with respect to the usual order on natural numbers.
N is an ordered type with respect to the usual order on natural numbers.
From two ordered types, we can build a new OrderedType
over their cartesian product, using the lexicographic order.
Even if positive can be seen as an ordered type with respect to the
usual order (see above), we can also use a lexicographic order over bits
(lower bits are considered first). This is more natural when using
positive as indexes for sets or maps (see FSetPositive and FMapPositive.
Module PositiveOrderedTypeBits <:
UsualOrderedType.
Definition t:=
positive.
Definition eq:=@
eq positive.
Definition eq_refl := @
eq_refl t.
Definition eq_sym := @
eq_sym t.
Definition eq_trans := @
eq_trans t.
Fixpoint bits_lt (
p q:
positive) :
Prop :=
match p,
q with
|
xH,
xI _ =>
True
|
xH,
_ =>
False
|
xO p,
xO q =>
bits_lt p q
|
xO _,
_ =>
True
|
xI p,
xI q =>
bits_lt p q
|
xI _,
_ =>
False
end.
Definition lt:=
bits_lt.
Lemma bits_lt_trans :
forall x y z :
positive,
bits_lt x y ->
bits_lt y z ->
bits_lt x z.
Lemma lt_trans :
forall x y z :
t,
lt x y ->
lt y z ->
lt x z.
Lemma bits_lt_antirefl :
forall x :
positive,
~ bits_lt x x.
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.
Lemma eq_dec (
x y:
positive):
{x = y} + {x <> y}.
End PositiveOrderedTypeBits.