Library Coq.Structures.OrderedType
NB: This file is here only for compatibility with earlier version of
FSets and FMap. Please use Structures/Orders.v directly now.
A eq_dec can be deduced from compare below. But adding this
redundant field allows to see an OrderedType as a DecidableType.
Additional properties that can be derived from signature
OrderedType.
Module OrderedTypeFacts (
Import O:
OrderedType).
Instance eq_equiv :
Equivalence eq.
Lemma lt_antirefl :
forall x,
~ lt x x.
Instance lt_strorder :
StrictOrder lt.
Lemma lt_eq :
forall x y z,
lt x y ->
eq y z ->
lt x z.
Lemma eq_lt :
forall x y z,
eq x y ->
lt y z ->
lt x z.
Instance lt_compat :
Proper (
eq==>eq==>iff)
lt.
Lemma lt_total :
forall x y,
lt x y \/ eq x y \/ lt y x.
Module OrderElts <:
Orders.TotalOrder.
Definition t :=
t.
Definition eq :=
eq.
Definition lt :=
lt.
Definition le x y :=
lt x y \/ eq x y.
Definition eq_equiv :=
eq_equiv.
Definition lt_strorder :=
lt_strorder.
Definition lt_compat :=
lt_compat.
Definition lt_total :=
lt_total.
Lemma le_lteq :
forall x y,
le x y <-> lt x y \/ eq x y.
End OrderElts.
Module OrderTac := !
MakeOrderTac OrderElts.
Ltac order :=
OrderTac.order.
Lemma le_eq x y z :
~lt x y ->
eq y z ->
~lt x z.
Lemma eq_le x y z :
eq x y ->
~lt y z ->
~lt x z.
Lemma neq_eq x y z :
~eq x y ->
eq y z ->
~eq x z.
Lemma eq_neq x y z :
eq x y ->
~eq y z ->
~eq x z.
Lemma le_lt_trans x y z :
~lt y x ->
lt y z ->
lt x z.
Lemma lt_le_trans x y z :
lt x y ->
~lt z y ->
lt x z.
Lemma le_neq x y :
~lt x y ->
~eq x y ->
lt y x.
Lemma le_trans x y z :
~lt y x ->
~lt z y ->
~lt z x.
Lemma le_antisym x y :
~lt y x ->
~lt x y ->
eq x y.
Lemma neq_sym x y :
~eq x y ->
~eq y x.
Lemma lt_le x y :
lt x y ->
~lt y x.
Lemma gt_not_eq x y :
lt y x ->
~ eq x y.
Lemma eq_not_lt x y :
eq x y ->
~ lt x y.
Lemma eq_not_gt x y :
eq x y ->
~ lt y x.
Lemma lt_not_gt x y :
lt x y ->
~ lt y x.
Hint Resolve gt_not_eq eq_not_lt.
Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
Lemma elim_compare_eq :
forall x y :
t,
eq x y ->
exists H : eq x y, compare x y = EQ _ H.
Lemma elim_compare_lt :
forall x y :
t,
lt x y ->
exists H : lt x y, compare x y = LT _ H.
Lemma elim_compare_gt :
forall x y :
t,
lt y x ->
exists H : lt y x, compare x y = GT _ H.
Ltac elim_comp :=
match goal with
| |- ?
e =>
match e with
|
context ctx [
compare ?
a ?
b ] =>
let H :=
fresh in
(
destruct (
compare a b)
as [
H|
H|
H];
try order)
end
end.
Ltac elim_comp_eq x y :=
elim (
elim_compare_eq (
x:=
x) (
y:=
y));
[
intros _1 _2;
rewrite _2;
clear _1 _2 |
auto ].
Ltac elim_comp_lt x y :=
elim (
elim_compare_lt (
x:=
x) (
y:=
y));
[
intros _1 _2;
rewrite _2;
clear _1 _2 |
auto ].
Ltac elim_comp_gt x y :=
elim (
elim_compare_gt (
x:=
x) (
y:=
y));
[
intros _1 _2;
rewrite _2;
clear _1 _2 |
auto ].
For compatibility reasons
Definition eq_dec :=
eq_dec.
Lemma lt_dec :
forall x y :
t,
{lt x y} + {~ lt x y}.
Definition eqb x y :
bool :=
if eq_dec x y then true else false.
Lemma eqb_alt :
forall x y,
eqb x y = match compare x y with EQ _ =>
true |
_ =>
false end.
Section ForNotations.
Notation In:=(
InA eq).
Notation Inf:=(
lelistA lt).
Notation Sort:=(
sort lt).
Notation NoDup:=(
NoDupA eq).
Lemma In_eq :
forall l x y,
eq x y ->
In x l ->
In y l.
Lemma ListIn_In :
forall l x,
List.In x l ->
In x l.
Lemma Inf_lt :
forall l x y,
lt x y ->
Inf y l ->
Inf x l.
Lemma Inf_eq :
forall l x y,
eq x y ->
Inf y l ->
Inf x l.
Lemma Sort_Inf_In :
forall l x a,
Sort l ->
Inf a l ->
In x l ->
lt a x.
Lemma ListIn_Inf :
forall l x, (
forall y,
List.In y l ->
lt x y) ->
Inf x l.
Lemma In_Inf :
forall l x, (
forall y,
In y l ->
lt x y) ->
Inf x l.
Lemma Inf_alt :
forall l x,
Sort l -> (
Inf x l <-> (forall y,
In y l ->
lt x y)).
Lemma Sort_NoDup :
forall l,
Sort l ->
NoDup l.
End ForNotations.
Hint Resolve ListIn_In Sort_NoDup Inf_lt.
Hint Immediate In_eq Inf_lt.
End OrderedTypeFacts.
Module KeyOrderedType(
O:
OrderedType).
Import O.
Module MO:=
OrderedTypeFacts(
O).
Import MO.
Section Elt.
Variable elt :
Type.
Notation key:=
t.
Definition eqk (
p p':
key*elt) :=
eq (
fst p) (
fst p').
Definition eqke (
p p':
key*elt) :=
eq (
fst p) (
fst p')
/\ (snd p) = (snd p').
Definition ltk (
p p':
key*elt) :=
lt (
fst p) (
fst p').
Hint Unfold eqk eqke ltk.
Hint Extern 2 (
eqke ?
a ?
b) =>
split.
Lemma eqke_eqk :
forall x x',
eqke x x' ->
eqk x x'.
Lemma ltk_right_r :
forall x k e e',
ltk x (k,e) ->
ltk x (k,e').
Lemma ltk_right_l :
forall x k e e',
ltk (k,e) x ->
ltk (k,e') x.
Hint Immediate ltk_right_r ltk_right_l.
Lemma eqk_refl :
forall e,
eqk e e.
Lemma eqke_refl :
forall e,
eqke e e.
Lemma eqk_sym :
forall e e',
eqk e e' ->
eqk e' e.
Lemma eqke_sym :
forall e e',
eqke e e' ->
eqke e' e.
Lemma eqk_trans :
forall e e' e'',
eqk e e' ->
eqk e' e'' ->
eqk e e''.
Lemma eqke_trans :
forall e e' e'',
eqke e e' ->
eqke e' e'' ->
eqke e e''.
Lemma ltk_trans :
forall e e' e'',
ltk e e' ->
ltk e' e'' ->
ltk e e''.
Lemma ltk_not_eqk :
forall e e',
ltk e e' ->
~ eqk e e'.
Lemma ltk_not_eqke :
forall e e',
ltk e e' ->
~eqke e e'.
Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
Hint Immediate eqk_sym eqke_sym.
Global Instance eqk_equiv :
Equivalence eqk.
Global Instance eqke_equiv :
Equivalence eqke.
Global Instance ltk_strorder :
StrictOrder ltk.
Global Instance ltk_compat :
Proper (
eqk==>eqk==>iff)
ltk.
Global Instance ltk_compat' :
Proper (
eqke==>eqke==>iff)
ltk.
Lemma eqk_not_ltk :
forall x x',
eqk x x' ->
~ltk x x'.
Lemma ltk_eqk :
forall e e' e'',
ltk e e' ->
eqk e' e'' ->
ltk e e''.
Lemma eqk_ltk :
forall e e' e'',
eqk e e' ->
ltk e' e'' ->
ltk e e''.
Hint Resolve eqk_not_ltk.
Hint Immediate ltk_eqk eqk_ltk.
Lemma InA_eqke_eqk :
forall x m,
InA eqke x m ->
InA eqk x m.
Hint Resolve InA_eqke_eqk.
Definition MapsTo (
k:
key)(
e:
elt):=
InA eqke (k,e).
Definition In k m :=
exists e:elt, MapsTo k e m.
Notation Sort := (
sort ltk).
Notation Inf := (
lelistA ltk).
Hint Unfold MapsTo In.
Lemma In_alt :
forall k l,
In k l <-> exists e, InA eqk (k,e) l.
Lemma MapsTo_eq :
forall l x y e,
eq x y ->
MapsTo x e l ->
MapsTo y e l.
Lemma In_eq :
forall l x y,
eq x y ->
In x l ->
In y l.
Lemma Inf_eq :
forall l x x',
eqk x x' ->
Inf x' l ->
Inf x l.
Lemma Inf_lt :
forall l x x',
ltk x x' ->
Inf x' l ->
Inf x l.
Hint Immediate Inf_eq.
Hint Resolve Inf_lt.
Lemma Sort_Inf_In :
forall l p q,
Sort l ->
Inf q l ->
InA eqk p l ->
ltk q p.
Lemma Sort_Inf_NotIn :
forall l k e,
Sort l ->
Inf (k,e) l ->
~In k l.
Lemma Sort_NoDupA:
forall l,
Sort l ->
NoDupA eqk l.
Lemma Sort_In_cons_1 :
forall e l e',
Sort (
e::l) ->
InA eqk e' l ->
ltk e e'.
Lemma Sort_In_cons_2 :
forall l e e',
Sort (
e::l) ->
InA eqk e' (
e::l) ->
ltk e e' \/ eqk e e'.
Lemma Sort_In_cons_3 :
forall x l k e,
Sort (
(k,e)::l) ->
In x l ->
~eq x k.
Lemma In_inv :
forall k k' e l,
In k (
(k',e) :: l) ->
eq k k' \/ In k l.
Lemma In_inv_2 :
forall k k' e e' l,
InA eqk (k, e) (
(k', e') :: l) ->
~ eq k k' ->
InA eqk (k, e) l.
Lemma In_inv_3 :
forall x x' l,
InA eqke x (
x' :: l) ->
~ eqk x x' ->
InA eqke x l.
End Elt.
Hint Unfold eqk eqke ltk.
Hint Extern 2 (
eqke ?
a ?
b) =>
split.
Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
Hint Immediate eqk_sym eqke_sym.
Hint Resolve eqk_not_ltk.
Hint Immediate ltk_eqk eqk_ltk.
Hint Resolve InA_eqke_eqk.
Hint Unfold MapsTo In.
Hint Immediate Inf_eq.
Hint Resolve Inf_lt.
Hint Resolve Sort_Inf_NotIn.
Hint Resolve In_inv_2 In_inv_3.
End KeyOrderedType.