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.
Module Ascii_as_OT <:
UsualOrderedType.
Definition t :=
ascii.
Definition eq := @
eq ascii.
Definition eq_refl := @
eq_refl t.
Definition eq_sym := @
eq_sym t.
Definition eq_trans := @
eq_trans t.
Definition cmp (
a b :
ascii) :
comparison :=
N.compare (
N_of_ascii a) (
N_of_ascii b).
Lemma cmp_eq (
a b :
ascii):
cmp a b = Eq <-> a = b.
Lemma cmp_lt_nat (
a b :
ascii):
cmp a b = Lt <-> (
nat_of_ascii a < nat_of_ascii b)%
nat.
Lemma cmp_antisym (
a b :
ascii):
cmp a b = CompOpp (
cmp b a).
Definition lt (
x y :
ascii) := (
N_of_ascii x < N_of_ascii y)%
N.
Lemma lt_trans (
x y z :
ascii):
lt x y -> lt y z -> lt x z.
Lemma lt_not_eq (
x y :
ascii):
lt x y -> x <> y.
Definition compare (
a b :
ascii) :
Compare lt eq a b :=
match cmp a b as z return _ = z -> _ with
|
Lt =>
fun E =>
LT E
|
Gt =>
fun E =>
GT (
compare_helper_gt E)
|
Eq =>
fun E =>
EQ (
compare_helper_eq E)
end Logic.eq_refl.
Definition eq_dec (
x y :
ascii):
{x = y} + { ~ (x = y)} :=
ascii_dec x y.
End Ascii_as_OT.
String is an ordered type with respect to the usual lexical order.
Module String_as_OT <:
UsualOrderedType.
Definition t :=
string.
Definition eq := @
eq string.
Definition eq_refl := @
eq_refl t.
Definition eq_sym := @
eq_sym t.
Definition eq_trans := @
eq_trans t.
Inductive lts :
string -> string -> Prop :=
|
lts_empty :
forall a s,
lts EmptyString (
String a s)
|
lts_tail :
forall a s1 s2,
lts s1 s2 -> lts (
String a s1) (
String a s2)
|
lts_head :
forall (
a b :
ascii)
s1 s2,
lt (
nat_of_ascii a) (
nat_of_ascii b)
->
lts (
String a s1) (
String b s2).
Definition lt :=
lts.
Lemma nat_of_ascii_inverse a b :
nat_of_ascii a = nat_of_ascii b -> a = b.
Lemma lts_tail_unique a s1 s2 :
lt (
String a s1) (
String a s2)
->
lt s1 s2.
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.
Fixpoint cmp (
a b :
string) :
comparison :=
match a,
b with
|
EmptyString,
EmptyString =>
Eq
|
EmptyString,
_ =>
Lt
|
String _ _,
EmptyString =>
Gt
|
String a_head a_tail,
String b_head b_tail =>
match Ascii_as_OT.cmp a_head b_head with
|
Lt =>
Lt
|
Gt =>
Gt
|
Eq =>
cmp a_tail b_tail
end
end.
Lemma cmp_eq (
a b :
string):
cmp a b = Eq <-> a = b.
Lemma cmp_antisym (
a b :
string):
cmp a b = CompOpp (
cmp b a).
Lemma cmp_lt (
a b :
string):
cmp a b = Lt <-> lt a b.
Definition compare (
a b :
string) :
Compare lt eq a b :=
match cmp a b as z return _ = z -> _ with
|
Lt =>
fun E =>
LT (
compare_helper_lt E)
|
Gt =>
fun E =>
GT (
compare_helper_gt E)
|
Eq =>
fun E =>
EQ (
compare_helper_eq E)
end Logic.eq_refl.
Definition eq_dec (
x y :
string):
{x = y} + { ~ (x = y)} :=
string_dec x y.
End String_as_OT.