Library Coq.Structures.OrdersEx
Examples of Ordered Type structures.
Ordered Type for
bool,
nat,
Positive,
N,
Z with the usual order.
An OrderedType can now directly be seen as a DecidableType
(Usual) Decidable Type for bool, nat, positive, N, Z
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 MSetPositive).
Local Open Scope positive.
Module PositiveOrderedTypeBits <:
UsualOrderedType.
Definition t:=
positive.
Include HasUsualEq <+
UsualIsEq.
Definition eqb :=
Pos.eqb.
Definition eqb_eq :=
Pos.eqb_eq.
Include HasEqBool2Dec.
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_antirefl :
forall x :
positive,
~ bits_lt x x.
Lemma bits_lt_trans :
forall x y z :
positive,
bits_lt x y -> bits_lt y z -> bits_lt x z.
Instance lt_compat :
Proper (
eq==>eq==>iff)
lt.
Instance lt_strorder :
StrictOrder lt.
Fixpoint compare x y :=
match x,
y with
|
x~1,
y~1 =>
compare x y
|
x~1,
_ =>
Gt
|
x~0,
y~0 =>
compare x y
|
x~0,
_ =>
Lt
| 1,
y~1 =>
Lt
| 1, 1 =>
Eq
| 1,
y~0 =>
Gt
end.
Lemma compare_spec :
forall x y,
CompSpec eq lt x y (
compare x y).
End PositiveOrderedTypeBits.