Library Coq.FSets.OrderedType
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).
Lemma lt_antirefl :
forall x, ~
lt x x.
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.
Lemma le_eq :
forall x y z, ~lt
x y ->
eq y z -> ~lt
x z.
Lemma eq_le :
forall x y z,
eq x y -> ~lt
y z -> ~lt
x z.
Lemma neq_eq :
forall x y z, ~eq
x y ->
eq y z -> ~eq
x z.
Lemma eq_neq :
forall x y z,
eq x y -> ~eq
y z -> ~eq
x z.
Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
Lemma le_lt_trans :
forall x y z, ~lt
y x ->
lt y z ->
lt x z.
Lemma lt_le_trans :
forall x y z,
lt x y -> ~lt
z y ->
lt x z.
Lemma le_neq :
forall x y, ~lt
x y -> ~eq
x y ->
lt y x.
Lemma neq_sym :
forall x y, ~eq
x y -> ~eq
y x.
Ltac abstraction :=
match goal with
|
H :
False |-
_ =>
elim H
|
H :
lt ?x ?x |-
_ =>
elim (
lt_antirefl H)
|
H : ~eq ?x ?x |-
_ =>
elim (
H (
eq_refl x))
|
H :
eq ?x ?x |-
_ =>
clear H;
abstraction
|
H : ~lt ?x ?x |-
_ =>
clear H;
abstraction
| |-
eq ?x ?x =>
exact (
eq_refl x)
| |-
lt ?x ?x =>
elimtype False;
abstraction
| |- ~
_ =>
intro;
abstraction
|
H1: ~lt ?x ?y,
H2: ~eq ?x ?y |-
_ =>
generalize (
le_neq H1 H2);
clear H1 H2;
intro;
abstraction
|
H1: ~lt ?x ?y,
H2: ~eq ?y ?x |-
_ =>
generalize (
le_neq H1 (
neq_sym H2));
clear H1 H2;
intro;
abstraction
|
H : ~eq ?x ?y |-
_ =>
revert H;
abstraction
|
H : ~lt ?x ?y |-
_ =>
revert H;
abstraction
|
H :
lt ?x ?y |-
_ =>
revert H;
abstraction
|
H :
eq ?x ?y |-
_ =>
revert H;
abstraction
|
_ =>
idtac
end.
Ltac do_eq a b EQ :=
match goal with
| |-
lt ?x ?y ->
_ =>
let H :=
fresh "H"
in
(
intro H;
(
generalize (
eq_lt (
eq_sym EQ)
H);
clear H;
intro H) ||
(
generalize (
lt_eq H EQ);
clear H;
intro H) ||
idtac);
do_eq a b EQ
| |- ~lt ?x ?y ->
_ =>
let H :=
fresh "H"
in
(
intro H;
(
generalize (
eq_le (
eq_sym EQ)
H);
clear H;
intro H) ||
(
generalize (
le_eq H EQ);
clear H;
intro H) ||
idtac);
do_eq a b EQ
| |-
eq ?x ?y ->
_ =>
let H :=
fresh "H"
in
(
intro H;
(
generalize (
eq_trans (
eq_sym EQ)
H);
clear H;
intro H) ||
(
generalize (
eq_trans H EQ);
clear H;
intro H) ||
idtac);
do_eq a b EQ
| |- ~eq ?x ?y ->
_ =>
let H :=
fresh "H"
in
(
intro H;
(
generalize (
eq_neq (
eq_sym EQ)
H);
clear H;
intro H) ||
(
generalize (
neq_eq H EQ);
clear H;
intro H) ||
idtac);
do_eq a b EQ
| |-
lt a ?y =>
apply eq_lt with b; [
exact EQ|]
| |-
lt ?y
a =>
apply lt_eq with b; [|exact (
eq_sym EQ)]
| |-
eq a ?y =>
apply eq_trans with b; [
exact EQ|]
| |-
eq ?y
a =>
apply eq_trans with b; [|exact (
eq_sym EQ)]
|
_ =>
idtac
end.
Ltac propagate_eq :=
abstraction;
clear;
match goal with
| |-
eq ?a ?b ->
_ =>
let EQ :=
fresh "EQ"
in (
intro EQ;
do_eq a b EQ;
clear EQ);
propagate_eq
|
_ =>
idtac
end.
Ltac do_lt x y LT :=
match goal with
| |-
lt x y ->
_ =>
intros _;
do_lt x y LT
| |-
lt y ?z ->
_ =>
let H :=
fresh "H"
in
(
intro H;
generalize (
lt_trans LT H);
intro);
do_lt x y LT
| |-
lt ?z
x ->
_ =>
let H :=
fresh "H"
in
(
intro H;
generalize (
lt_trans H LT);
intro);
do_lt x y LT
| |-
lt _ _ ->
_ =>
intro;
do_lt x y LT
| |- ~lt
y x ->
_ =>
intros _;
do_lt x y LT
| |- ~lt
x ?z ->
_ =>
let H :=
fresh "H"
in
(
intro H;
generalize (
le_lt_trans H LT);
intro);
do_lt x y LT
| |- ~lt ?z
y ->
_ =>
let H :=
fresh "H"
in
(
intro H;
generalize (
lt_le_trans LT H);
intro);
do_lt x y LT
| |- ~lt
_ _ ->
_ =>
intro;
do_lt x y LT
|
_ =>
idtac
end.
Definition hide_lt :=
lt.
Ltac propagate_lt :=
abstraction;
match goal with
| |-
lt ?x ?y ->
_ =>
let LT :=
fresh "LT"
in (
intro LT;
do_lt x y LT;
change (
hide_lt x y)
in LT);
propagate_lt
|
_ =>
unfold hide_lt in *
end.
Ltac order :=
intros;
propagate_eq;
propagate_lt;
auto;
propagate_lt;
eauto.
Ltac false_order :=
elimtype False;
order.
Lemma gt_not_eq :
forall x y,
lt y x -> ~
eq x y.
Lemma eq_not_lt :
forall x y :
t,
eq x y -> ~
lt x y.
Hint Resolve gt_not_eq eq_not_lt.
Lemma eq_not_gt :
forall x y :
t,
eq x y -> ~
lt y x.
Lemma lt_not_gt :
forall x y :
t,
lt x y -> ~
lt y x.
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 solve [
intros;
false_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.
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.