Library Coq.Sets.Partial_Order
Require
Export
Ensembles
.
Require
Export
Relations_1
.
Section
Partial_orders
.
Variable
U
:
Type
.
Definition
Carrier
:=
Ensemble
U
.
Definition
Rel
:=
Relation
U
.
Record
PO
:
Type
:=
Definition_of_PO
{
Carrier_of
:
Ensemble
U
;
Rel_of
:
Relation
U
;
PO_cond1
:
Inhabited
U
Carrier_of
;
PO_cond2
:
Order
U
Rel_of
}.
Variable
p
:
PO
.
Definition
Strict_Rel_of
:
Rel
:=
fun
x
y
:
U
=>
Rel_of
p
x
y
/\
x
<>
y
.
Inductive
covers
(
y
x
:
U
) :
Prop
:=
Definition_of_covers
:
Strict_Rel_of
x
y
->
~
(
exists
z
:
_
,
Strict_Rel_of
x
z
/\
Strict_Rel_of
z
y
)
->
covers
y
x
.
End
Partial_orders
.
Hint Unfold
Carrier_of
Rel_of
Strict_Rel_of
:
sets
v62
.
Hint Resolve
Definition_of_covers
:
sets
v62
.
Section
Partial_order_facts
.
Variable
U
:
Type
.
Variable
D
:
PO
U
.
Lemma
Strict_Rel_Transitive_with_Rel
:
forall
x
y
z
:
U
,
Strict_Rel_of
U
D
x
y
->
Rel_of
U
D
y
z
->
Strict_Rel_of
U
D
x
z
.
Lemma
Strict_Rel_Transitive_with_Rel_left
:
forall
x
y
z
:
U
,
Rel_of
U
D
x
y
->
Strict_Rel_of
U
D
y
z
->
Strict_Rel_of
U
D
x
z
.
Lemma
Strict_Rel_Transitive
:
Transitive
U
(
Strict_Rel_of
U
D
).
End
Partial_order_facts
.