A Coq library for domain theory (http://rwd.rdockins.name/domains/)

root / directed.v

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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
(* Copyright (c) 2014, Robert Dockins *)

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import effective.

(**  * Conditionally-inhabited sets and h-directed sets.
  *)

(**  A finite set is conditionally-inhabited for hf
     whenever hf is false; or when hf is true, the set
     is inhabited.

     This very odd little definition is the key to
     providing a uniform presentation of pointed and
     unpointed domains.
  *)
Definition inh {A:preord} (hf:bool) (X:finset A) := 
  if hf then exists x, x ∈ X else True.

Lemma inh_dec A hf (X:finset A) : { inh hf X } + {~inh hf X}.
Proof.
  destruct hf; simpl; auto.
  destruct X. right.
  intro. destruct H. apply nil_elem in H. auto.
  left. exists c. apply cons_elem; auto.
Qed.

Lemma inh_image A B hf (X:finset A) (f:A → B) :
  inh hf X <-> inh hf (image f X).
Proof.
  destruct hf; simpl; intuition.
  destruct H as [x ?].
  exists (f#x). apply image_axiom1. auto.
  destruct H as [x ?].
  apply image_axiom2 in H.
  destruct H as [y [??]].
  exists y. auto.
Qed.

Lemma inh_sub A hf (X Y:finset A) :
  X ⊆ Y -> inh hf X -> inh hf Y.
Proof.
  destruct hf; simpl; auto.
  intros. destruct H0 as [x ?].
  exists x. apply H; auto.
Qed.

Lemma inh_eq A hf (X Y:finset A) :
  X ≈ Y -> inh hf X -> inh hf Y. 
Proof.
  intros. apply inh_sub with X; auto.
  destruct H; auto.
Qed.

Lemma elem_inh A hf (X:finset A) x : x ∈ X -> inh hf X.
Proof.
  intros. destruct hf; simpl; eauto.
Qed.

Hint Resolve inh_sub elem_inh.

(**  A subset of the image of a function is equal to the image
     of some subset of the set X.
  *)
Lemma finset_sub_image (A B:preord) (T:set.theory) 
  (f:A → B) (X:set T A) (M:finset B) :
  M ⊆ image f X ->
  exists M', M ≈ image f M' /\ M' ⊆ X.
Proof.
  induction M; intros.
  exists nil. split; simpl; auto.
  hnf; simpl; intros. apply nil_elem in H0. elim H0.
  destruct IHM as [M' [??]].
  hnf; intros. apply H. apply cons_elem; auto.
  assert (a ∈ image f X). apply H. apply cons_elem. auto.
  apply image_axiom2 in H2.
  destruct H2 as [y [??]].
  exists (y::M')%list.
  split.
  split. hnf. simpl. intros.
  apply cons_elem in H4. destruct H4.
  apply cons_elem. left.
  rewrite H4; auto.
  apply cons_elem. right.
  rewrite H0 in H4. auto.
  hnf. simpl; intros.
  unfold image in H4. simpl in H4.
  apply cons_elem in H4.
  apply cons_elem.
  destruct H4.
  left. rewrite H4; auto.
  right. rewrite H0. auto.
  hnf; simpl; intros.
  apply cons_elem in H4.
  destruct H4.
  rewrite H4; auto.
  apply H1; auto.
Qed.


(**  A directed preorder is an effective preorder where every finite set
     has an upper bound (that may be found constructively).
  *)
Record directed_preord :=
  DirPreord
  { dir_preord :> preord
  ; dir_effective : effective_order dir_preord
  ; choose_ub_set : forall M:finset dir_preord, { k | upper_bound k M }
  }.
Arguments dir_preord _.
Arguments dir_effective _.
Arguments choose_ub_set _ _.

Lemma choose_ub (I:directed_preord) (i j:I) :
  { k | i ≤ k /\ j ≤ k }.
Proof.
  destruct (choose_ub_set I (i::j::nil)%list).
  exists x. split; apply u.
  apply cons_elem; auto.
  apply cons_elem; right.
  apply cons_elem; auto.
Qed.


(** A set X is h-directed when every h-inhabited finite
    subset has an upper bound in X.
  *)
Definition directed {T:set.theory} {A:preord} (hf:bool) (X:set T A) :=
  forall (M:finset A) (Hinh:inh hf M),
    M ⊆ X -> exists x, upper_bound x M /\ x ∈ X.

(**  To prove a set X is directed, it suffices (and is necessary)
     that every pair of elements in X has an upper bound in X; and that
     X is inhabited when b = false.
  *)
Lemma prove_directed (T:set.theory) (A:preord) (b:bool) (X:set T A) :
  (if b then True else exists x, x ∈ X) ->
  (forall x y, x ∈ X -> y ∈ X -> exists z, x ≤ z /\ y ≤ z /\ z ∈ X) ->
  directed b X.
Proof.
  intros. intro M.
  induction M.
  simpl; intros.
  destruct b; simpl in *.
  destruct Hinh. apply nil_elem in H2. elim H2.
  destruct H as [x ?]. exists x. split; auto.
  hnf. simpl; intros. apply nil_elem in H2. elim H2.
  intros.
  destruct M.
  exists a. split; auto.
  hnf; simpl; intros.
  apply cons_elem in H2. destruct H2.
  rewrite H2. auto.
  apply nil_elem in H2. elim H2.
  apply H1. apply cons_elem. auto.
  destruct IHM as [q [??]].
  destruct b; auto.
  hnf. exists c. apply cons_elem; auto.
  hnf; intros. apply H1; auto.
  apply cons_elem; auto.
  destruct (H0 a q) as [z [?[??]]]; auto.
  apply H1; auto. apply cons_elem; auto.
  exists z. split; auto.
  hnf; intros.
  apply cons_elem in H7.
  destruct H7. rewrite H7; auto.
  transitivity q; auto.
Qed.

(**  Directeness forms a set color.
  *)
Program Definition directed_hf_cl (hf:bool) : color :=
  Color (fun SL A X => @directed SL A hf X) _ _ _ _.
Next Obligation.    
  repeat intro.
  destruct (H0 M) as [x [??]]; auto.
  rewrite H; auto.
  exists x. split.
  hnf; intros.
  apply H2; auto.
  rewrite <- H; auto.
Qed.
Next Obligation.
  repeat intro.
  exists a. split; auto.
  hnf; intros. apply H in H0.
  apply single_axiom in H0. auto.
  apply single_axiom; auto.
Qed.
Next Obligation.
  repeat intro.
  destruct (finset_sub_image A B T f X M H0) as [M' [??]].
  destruct (H M') as [x [??]]; auto.
  rewrite (inh_image A B hf M' f).
  apply inh_eq with M; auto.
  exists (f#x); split; auto.
  hnf; intros.
  rewrite H1 in H5.
  apply image_axiom2 in H5.
  destruct H5 as [y [??]].
  rewrite H6.
  apply Preord.axiom.
  apply H3. auto.
  apply image_axiom1. auto.
Qed.
Next Obligation.
  intros.
  apply prove_directed.
  case_eq hf; auto. intros.
  destruct (H nil) as [X [??]].
  rewrite H1; hnf; auto.
  hnf; intros. apply nil_elem in H2. elim H2.
  destruct (H0 X H3 nil) as [x [??]].
  rewrite H1; hnf; auto.
  hnf; intros. apply nil_elem in H4. elim H4.
  exists x. apply union_axiom; eauto.
  intros.
  apply union_axiom in H1.
  apply union_axiom in H2.
  destruct H1 as [X1 [??]].
  destruct H2 as [X2 [??]].
  destruct (H (X1::X2::nil)%list) as [X [??]]; auto.
  apply elem_inh with X1; auto.
  apply cons_elem; auto.
  hnf; intros.
  apply cons_elem in H5. destruct H5.
  rewrite H5; auto.
  apply cons_elem in H5. destruct H5.
  rewrite H5; auto.
  apply nil_elem in H5; elim H5.
  destruct (H0 X H6 (x::y::nil)%list) as [z [??]]; auto.
  apply elem_inh with x; auto.
  apply cons_elem; auto.
  hnf; intros.
  apply cons_elem in H7. destruct H7.
  rewrite H7; auto.
  assert (X1 ≤ X).
  apply H5. apply cons_elem; auto.
  apply H8. auto.
  apply cons_elem in H7. destruct H7.
  rewrite H7; auto.
  assert (X2 ≤ X).
  apply H5.
  apply cons_elem; right.
  apply cons_elem; auto.
  apply H8. auto.
  apply nil_elem in H7. elim H7.
  exists z. split.
  apply H7. apply cons_elem; auto.
  split.
  apply H7.
  apply cons_elem; right.
  apply cons_elem; auto.
  apply union_axiom.
  exists X; split; auto.
Qed.

Definition semidirected_cl := directed_hf_cl true.
Definition directed_cl := directed_hf_cl false.


(**  The preorder of natural numbers with their arithmetic ordering
     is an effective, directed preorder.
  *)
Require Import Arith.
Require Import NArith.

Program Definition nat_ord := Preord.Pack nat (Preord.Mixin nat le _ _).
Solve Obligations using eauto with arith.
  
Program Definition nat_eff : effective_order nat_ord :=
  EffectiveOrder nat_ord le_dec (fun x => Some (N.to_nat x)) _.
Next Obligation.
  intros. exists (N.of_nat x).
  rewrite Nat2N.id. auto.
Qed.

Program Definition nat_dirord : directed_preord :=
  DirPreord nat_ord nat_eff _.
Next Obligation.  
  induction M.
  exists 0. hnf; intros. apply nil_elem in H. elim H.
  destruct IHM as [k ?].
  exists (max a k).
  hnf; intros.
  apply cons_elem in H. destruct H.
  rewrite H.
  red; simpl.
  apply Max.le_max_l.
  transitivity k.
  apply u. auto.
  red; simpl.
  apply Max.le_max_r.
Qed.