Library Coq.Structures.OrdersFacts
Require
Import
Basics
OrdersTac
.
Require
Export
Orders
.
Properties of
OrderedTypeFull
Module
OrderedTypeFullFacts
(
Import
O
:
OrderedTypeFull'
).
Module
OrderTac
:=
OTF_to_OrderTac
O
.
Ltac
order
:=
OrderTac.order
.
Ltac
iorder
:=
intuition
order
.
Instance
le_compat
:
Proper
(
eq
==>
eq
==>
iff
)
le
.
Instance
le_preorder
:
PreOrder
le
.
Instance
le_order
:
PartialOrder
eq
le
.
Instance
le_antisym
:
Antisymmetric
_
eq
le
.
Lemma
le_not_gt_iff
:
forall
x
y
,
x
<=
y
<->
~
y
<
x
.
Lemma
lt_not_ge_iff
:
forall
x
y
,
x
<
y
<->
~
y
<=
x
.
Lemma
le_or_gt
:
forall
x
y
,
x
<=
y
\/
y
<
x
.
Lemma
lt_or_ge
:
forall
x
y
,
x
<
y
\/
y
<=
x
.
Lemma
eq_is_le_ge
:
forall
x
y
,
x
==
y
<->
x
<=
y
/\
y
<=
x
.
End
OrderedTypeFullFacts
.
Properties of
OrderedType
Module
OrderedTypeFacts
(
Import
O
:
OrderedType'
).
Module
OrderTac
:=
OT_to_OrderTac
O
.
Ltac
order
:=
OrderTac.order
.
Notation
"
x <= y" := (
~
lt
y
x
) :
order
.
Infix
"
?=" :=
compare
(
at
level
70,
no
associativity
) :
order
.
Local
Open
Scope
order
.
Tactic Notation
"elim_compare"
constr
(
x
)
constr
(
y
) :=
destruct
(
compare_spec
x
y
).
Tactic Notation
"elim_compare"
constr
(
x
)
constr
(
y
) "as"
ident
(
h
) :=
destruct
(
compare_spec
x
y
)
as
[
h
|
h
|
h
].
The following lemmas are either re-phrasing of
eq_equiv
and
lt_strorder
or immediately provable by
order
. Interest: compatibility, test of order, etc
Definition
eq_refl
(
x
:
t
) :
x
==
x
:=
Equivalence_Reflexive
x
.
Definition
eq_sym
(
x
y
:
t
) :
x
==
y
->
y
==
x
:=
Equivalence_Symmetric
x
y
.
Definition
eq_trans
(
x
y
z
:
t
) :
x
==
y
->
y
==
z
->
x
==
z
:=
Equivalence_Transitive
x
y
z
.
Definition
lt_trans
(
x
y
z
:
t
) :
x
<
y
->
y
<
z
->
x
<
z
:=
StrictOrder_Transitive
x
y
z
.
Definition
lt_irrefl
(
x
:
t
) :
~
x
<
x
:=
StrictOrder_Irreflexive
x
.
Some more about
compare
Lemma
compare_eq_iff
:
forall
x
y
,
(
x
?=
y
)
=
Eq
<->
x
==
y
.
Lemma
compare_lt_iff
:
forall
x
y
,
(
x
?=
y
)
=
Lt
<->
x
<
y
.
Lemma
compare_gt_iff
:
forall
x
y
,
(
x
?=
y
)
=
Gt
<->
y
<
x
.
Lemma
compare_ge_iff
:
forall
x
y
,
(
x
?=
y
)
<>
Lt
<->
y
<=
x
.
Lemma
compare_le_iff
:
forall
x
y
,
(
x
?=
y
)
<>
Gt
<->
x
<=
y
.
Hint
Rewrite
compare_eq_iff
compare_lt_iff
compare_gt_iff
:
order
.
Instance
compare_compat
:
Proper
(
eq
==>
eq
==>
Logic.eq
)
compare
.
Lemma
compare_refl
:
forall
x
,
(
x
?=
x
)
=
Eq
.
Lemma
compare_antisym
:
forall
x
y
,
(
y
?=
x
)
=
CompOpp
(
x
?=
y
).
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
if_eq_dec
:
forall
x
y
(
B
:
Type
)(
b
b'
:
B
),
(
if
eq_dec
x
y
then
b
else
b'
)
=
(
match
compare
x
y
with
Eq
=>
b
|
_
=>
b'
end
)
.
Lemma
eqb_alt
:
forall
x
y
,
eqb
x
y
=
match
compare
x
y
with
Eq
=>
true
|
_
=>
false
end
.
Instance
eqb_compat
:
Proper
(
eq
==>
eq
==>
Logic.eq
)
eqb
.
End
OrderedTypeFacts
.
Tests of the order tactic
Is it at least capable of proving some basic properties ?
Module
OrderedTypeTest
(
Import
O
:
OrderedType'
).
Module
Import
MO
:=
OrderedTypeFacts
O
.
Local
Open
Scope
order
.
Lemma
lt_not_eq
x
y
:
x
<
y
->
~
x
==
y
.
Lemma
lt_eq
x
y
z
:
x
<
y
->
y
==
z
->
x
<
z
.
Lemma
eq_lt
x
y
z
:
x
==
y
->
y
<
z
->
x
<
z
.
Lemma
le_eq
x
y
z
:
x
<=
y
->
y
==
z
->
x
<=
z
.
Lemma
eq_le
x
y
z
:
x
==
y
->
y
<=
z
->
x
<=
z
.
Lemma
neq_eq
x
y
z
:
~
x
==
y
->
y
==
z
->
~
x
==
z
.
Lemma
eq_neq
x
y
z
:
x
==
y
->
~
y
==
z
->
~
x
==
z
.
Lemma
le_lt_trans
x
y
z
:
x
<=
y
->
y
<
z
->
x
<
z
.
Lemma
lt_le_trans
x
y
z
:
x
<
y
->
y
<=
z
->
x
<
z
.
Lemma
le_trans
x
y
z
:
x
<=
y
->
y
<=
z
->
x
<=
z
.
Lemma
le_antisym
x
y
:
x
<=
y
->
y
<=
x
->
x
==
y
.
Lemma
le_neq
x
y
:
x
<=
y
->
~
x
==
y
->
x
<
y
.
Lemma
neq_sym
x
y
:
~
x
==
y
->
~
y
==
x
.
Lemma
lt_le
x
y
:
x
<
y
->
x
<=
y
.
Lemma
gt_not_eq
x
y
:
y
<
x
->
~
x
==
y
.
Lemma
eq_not_lt
x
y
:
x
==
y
->
~
x
<
y
.
Lemma
eq_not_gt
x
y
:
x
==
y
->
~
y
<
x
.
Lemma
lt_not_gt
x
y
:
x
<
y
->
~
y
<
x
.
Lemma
eq_is_nlt_ngt
x
y
:
x
==
y
<->
~
x
<
y
/\
~
y
<
x
.
End
OrderedTypeTest
.
Reversed OrderedTypeFull.
we can switch the orientation of the order. This is used for example when deriving properties of
min
out of the ones of
max
(see
GenericMinMax
).
Module
OrderedTypeRev
(
O
:
OrderedTypeFull
) <:
OrderedTypeFull
.
Definition
t
:=
O.t
.
Definition
eq
:=
O.eq
.
Instance
eq_equiv
:
Equivalence
eq
.
Definition
eq_dec
:=
O.eq_dec
.
Definition
lt
:=
flip
O.lt
.
Definition
le
:=
flip
O.le
.
Instance
lt_strorder
:
StrictOrder
lt
.
Instance
lt_compat
:
Proper
(
eq
==>
eq
==>
iff
)
lt
.
Lemma
le_lteq
:
forall
x
y
,
le
x
y
<->
lt
x
y
\/
eq
x
y
.
Definition
compare
:=
flip
O.compare
.
Lemma
compare_spec
:
forall
x
y
,
CompSpec
eq
lt
x
y
(
compare
x
y
).
End
OrderedTypeRev
.