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
101
102
103
104
105
106
107
108
109
110
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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: Cpo.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Export Ensembles.
Require Export Relations_1.
Require Export Partial_Order.
Section Bounds.
Variable U : Type.
Variable D : PO U.
Let C := Carrier_of U D.
Let R := Rel_of U D.
Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
Upper_Bound_definition :
In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
Lower_Bound_definition :
In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
Inductive Lub (B:Ensemble U) (x:U) : Prop :=
Lub_definition :
Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
Inductive Glb (B:Ensemble U) (x:U) : Prop :=
Glb_definition :
Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
Inductive Bottom (bot:U) : Prop :=
Bottom_definition :
In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
Inductive Totally_ordered (B:Ensemble U) : Prop :=
Totally_ordered_definition :
(Included U B C ->
forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
Totally_ordered B.
Definition Compatible : Relation U :=
fun x y:U =>
In U C x ->
In U C y -> exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
Inductive Directed (X:Ensemble U) : Prop :=
Definition_of_Directed :
Included U X C ->
Inhabited U X ->
(forall x1 x2:U,
Included U (Couple U x1 x2) X ->
exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
Directed X.
Inductive Complete : Prop :=
Definition_of_Complete :
(exists bot : _, Bottom bot) ->
(forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) ->
Complete.
Inductive Conditionally_complete : Prop :=
Definition_of_Conditionally_complete :
(forall X:Ensemble U,
Included U X C ->
(exists maj : _, Upper_Bound X maj) ->
exists bsup : _, Lub X bsup) -> Conditionally_complete.
End Bounds.
Hint Resolve Totally_ordered_definition Upper_Bound_definition
Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
Definition_of_Complete Definition_of_Complete
Definition_of_Conditionally_complete.
Section Specific_orders.
Variable U : Type.
Record Cpo : Type := Definition_of_cpo
{PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
Record Chain : Type := Definition_of_chain
{PO_of_chain : PO U;
Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
End Specific_orders.
|
