# hub.darcs.net :: rdockins -> domains -> files

A Coq library for domain theory

## 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.``````