blob: 759cf4e270c7c84ecc335deaa086deb09106d992 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(****************************************************************************)
(* *)
(* Naive Set Theory in Coq *)
(* *)
(* INRIA INRIA *)
(* Rocquencourt Sophia-Antipolis *)
(* *)
(* Coq V6.1 *)
(* *)
(* Gilles Kahn *)
(* Gerard Huet *)
(* *)
(* *)
(* *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
(* to the Newton Institute for providing an exceptional work environment *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
(*i $Id: Partial_Order.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*)
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 := [x, y: U] (Rel_of p x y) /\ ~ x == y.
Inductive covers [y, x:U]: Prop :=
Definition_of_covers:
(Strict_Rel_of x y) ->
~ (EXT z | (Strict_Rel_of x z) /\ (Strict_Rel_of z y)) ->
(covers y x).
End Partial_orders.
Hints Unfold Carrier_of Rel_of Strict_Rel_of : sets v62.
Hints Resolve Definition_of_covers : sets v62.
Section Partial_order_facts.
Variable U:Type.
Variable D:(PO U).
Lemma Strict_Rel_Transitive_with_Rel:
(x:U) (y:U) (z:U) (Strict_Rel_of U D x y) -> (Rel_of U D y z) ->
(Strict_Rel_of U D x z).
Unfold 1 Strict_Rel_of.
Red.
Elim D; Simpl.
Intros C R H' H'0; Elim H'0.
Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
Apply H'2 with y := y; Tauto.
Red; Intro H'6.
Elim H'4; Intros H'7 H'8; Apply H'8; Clear H'4.
Apply H'3; Auto.
Rewrite H'6; Tauto.
Qed.
Lemma Strict_Rel_Transitive_with_Rel_left:
(x:U) (y:U) (z:U) (Rel_of U D x y) -> (Strict_Rel_of U D y z) ->
(Strict_Rel_of U D x z).
Unfold 1 Strict_Rel_of.
Red.
Elim D; Simpl.
Intros C R H' H'0; Elim H'0.
Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
Apply H'2 with y := y; Tauto.
Red; Intro H'6.
Elim H'5; Intros H'7 H'8; Apply H'8; Clear H'5.
Apply H'3; Auto.
Rewrite <- H'6; Auto.
Qed.
Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)).
Red.
Intros x y z H' H'0.
Apply Strict_Rel_Transitive_with_Rel with y := y;
[ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ].
Qed.
End Partial_order_facts.
|
