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

root / discrete.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
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
(* Copyright (c) 2014, Robert Dockins *)

Require Import Setoid.
Require Import List.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import cpo.
Require Import profinite.

(**  * Discrete unpointed domains

     Every finite type can be turned into a discrete profinite domain.
     These are useful for representing base types.
  *)

Module fintype.
  Record fintype :=
  Fintype
  { carrier :> Type
  ; fintype_list : list carrier
  ; fintype_complete : forall x, In x fintype_list
  ; fintype_dec : forall x y:carrier, {x=y}+{x<>y}
  }.

  Definition eq_mixin (X:fintype) : Eq.mixin_of (carrier X) :=
    Eq.Mixin (carrier X) (@eq _) 
    (@Logic.refl_equal _) (@Logic.eq_sym _) (@Logic.eq_trans _).

  Definition preord_mixin (X:fintype) : Preord.mixin_of (carrier X) :=
    Preord.Mixin (carrier X) (@eq _) (@Logic.refl_equal _) (@Logic.eq_trans _).

  Canonical Structure setoid (X:fintype) : Eq.type :=
    Eq.Pack X (eq_mixin X).
  Canonical Structure ord (X:fintype) : preord :=
    Preord.Pack X (preord_mixin X).

  Lemma order_discrete (X:fintype) (x y:X) : x ≤ y -> x = y.
  Proof (fun H => H).
 
  Lemma strong_eq (X:fintype) (x y:X) : x ≈ y -> x = y.
  Proof (fun H => H).

  Program Definition fintype_effective X : effective_order (ord X) :=
    EffectiveOrder (ord X) (fintype_dec X) (elist (fintype_list X)) _.
  Next Obligation.
    intros. apply elist_elem. exists x. split; auto. apply fintype_complete.
  Qed.

  Program Definition fintype_has_normals hf (X:fintype) : 
    has_normals (ord X) (fintype_effective X) hf.
  Proof.  
    hnf; intros. exists (fintype_list X). split.
    hnf; intros. exists a; split; auto. apply fintype_complete.
    hnf; simpl; intros. split.
    destruct hf.
    destruct Hinh. exists x.
    exists x. split; auto. apply fintype_complete.
    hnf; auto.
    repeat intro. exists z.
    split; repeat intro.
    apply H in H0. apply finsubset_elem in H0.
    destruct H0; auto.
    intros. hnf in H1, H2. destruct H1.
    hnf. hnf in H3. rewrite H3; auto.
    apply finsubset_elem. intros.
    destruct H0. rewrite H2. auto.
    split; auto.
    exists z; split; auto. apply fintype_complete.
  Qed.

  Definition fintype_plotkin hf (X:fintype) : plotkin_order hf (ord X) :=
    norm_plt (ord X) (fintype_effective X) hf (@fintype_has_normals hf X).
End fintype.

Notation fintype := fintype.fintype.
Notation Fintype := fintype.Fintype.

Canonical Structure fintype.setoid.
Canonical Structure fintype.ord.
Coercion fintype.carrier : fintype >-> Sortclass.

Canonical Structure disc (X:fintype) : PLT :=
    PLT.Ob false (fintype.carrier X)
      (PLT.Class _ _
        (fintype.preord_mixin X)
        (fintype.fintype_effective X)
        (fintype.fintype_plotkin false X)).

Program Definition disc_elem (Y:fintype) (y:Y) : 1 → disc Y :=
  PLT.Hom false (PLT.unit false) (disc Y) (single (tt,y)) _ _.
Next Obligation.
  intros. destruct x'. destruct x.
  apply single_axiom in H1.
  apply single_axiom.
  destruct H1. destruct H1. simpl in *.
  split; split; simpl; auto.
  rewrite H0; auto.
  hnf in H0. subst y'. hnf in H3. hnf. auto.
Qed.
Next Obligation.
  repeat intro. exists y.
  split. repeat intro.
  apply H in H0. apply erel_image_elem in H0.
  apply single_axiom in H0.
  destruct H0 as [[??][??]]; auto.
  apply erel_image_elem.
  apply single_axiom. destruct x. auto.
Qed.

Lemma disc_elem_inj Y : forall y1 y2,
  disc_elem Y y1 ≈ disc_elem Y y2 -> y1 = y2.
Proof.
  intros. destruct H.
  assert ((tt,y1) ∈ PLT.hom_rel (disc_elem Y y2)).
  apply H. apply single_axiom. auto.
  simpl in H1. apply single_axiom in H1.
  destruct H1 as [[??][??]]; auto.
Qed.

Arguments disc_elem [Y] y.

Section disc_cases.
  Variable X:fintype.
  Variables (A B:PLT).
  Variable f : X -> (A → B).

  Program Definition insert_index (x:X) : Preord.hom (A×B) ((A×disc X)×B) :=
    Preord.Hom (A×B) ((A×disc X)×B) (fun ab => ((fst ab, x), snd ab)) _.
  Next Obligation.
    intros x [??] [??] [??]; simpl in *; auto.
    split; simpl; auto. split; auto.
  Qed.

  Fixpoint mk_disc_cases_rel (ls:list X) : eset ((PLT.ord A×disc X)×B)%cat_ob :=
    match ls with
    | nil => ∅
    | x::xs => union2 (image (insert_index x) (PLT.hom_rel (f x)))
                      (mk_disc_cases_rel xs)
    end.

  Lemma mk_disc_cases_elem : forall ls x a b, (In x ls) ->
    ((a,b) ∈ PLT.hom_rel (f x) <-> (a,x,b) ∈ mk_disc_cases_rel ls).
  Proof.
    induction ls; simpl; intros. elim H.
    destruct H. subst a.
    split; intros.
    apply union2_elem. left.
    apply image_axiom1'.
    exists (a0,b); split; auto.
    apply union2_elem in H.
    destruct H. apply image_axiom2 in H.
    destruct H as [[p q] [??]].
    simpl in H0.
    revert H. apply member_eq.
    destruct H0 as [[??][??]]. simpl in *.
    destruct H; destruct H1; simpl in *.
    split; split; auto.
    destruct (In_dec (fintype.fintype_dec X) x ls).
    apply IHls; auto.
    elim n. clear IHls. clear n.
    induction ls; simpl in *.
    apply empty_elem in H. auto.
    apply union2_elem in H. destruct H.
    apply image_axiom2 in H.
    destruct H as [[p q] [??]].
    simpl in H0.
    destruct H0 as [[??][??]]. simpl in *.
    destruct H0. simpl in *. hnf in H4. auto.
    right; auto.
    split; intros.
    apply union2_elem. right. apply IHls; auto.
    apply union2_elem in H0. destruct H0.
    apply image_axiom2 in H0.
    destruct H0 as [[p q] [??]]. simpl in H1.
    destruct H1 as [[??][??]]. simpl in *.
    destruct H1. simpl in *. destruct H3. simpl in *.
    hnf in H5. subst a.
    revert H0. apply member_eq.
    split; split; auto.
    apply IHls; auto.
  Qed.

  Program Definition disc_cases : (A × (disc X))%plt → B :=
    PLT.Hom false (PLT.prod A (disc X)) B
       (mk_disc_cases_rel (fintype.fintype_list X)) _ _.
  Next Obligation.
    generalize (fintype.fintype_list X).
    induction l; simpl; intros.
    apply empty_elem in H1. elim H1.
    apply union2_elem in H1. apply union2_elem.
    destruct H1. left.
    apply image_axiom2 in H1. apply image_axiom1'.
    destruct H1 as [[p q] ?]. destruct H1.
    simpl in H2.
    destruct x; destruct x'. simpl.
    destruct H. simpl in *. hnf in H3. subst c0.
    exists (c1,y'). simpl. split.
    destruct H2 as [[??][??]]. simpl in *.
    destruct H2; destruct H4; simpl in *.
    hnf in H6. subst c2. auto.
    destruct H2 as [[??][??]]. simpl in *.
    destruct H2; destruct H4; simpl in *.
    revert H1. apply PLT.hom_order.
    rewrite H4. auto.
    rewrite H0; auto.   
    right. eapply IHl; eauto.
  Qed.
  Next Obligation.
    repeat intro.
    destruct x as [a x].
    destruct (PLT.hom_directed _ _ _ (f x) a M); auto.
    red; simpl; intros. apply H in H0.
    apply erel_image_elem in H0.
    apply erel_image_elem.    
    apply (mk_disc_cases_elem (fintype.fintype_list X) x a a0).
    apply fintype.fintype_complete. auto.
    destruct H0.    
    apply erel_image_elem in H1.
    exists x0. split; auto.
    apply erel_image_elem.    
    apply (mk_disc_cases_elem (fintype.fintype_list X) x a x0).
    apply fintype.fintype_complete. auto.
  Qed.

  Lemma disc_cases_elem x h : disc_cases ∘ 〈 h, disc_elem x 〉 ≈ f x ∘ h.
  Proof.
    split; intros a H. destruct a.
    apply PLT.compose_hom_rel in H.
    apply PLT.compose_hom_rel.
    destruct H as [q [??]].
    destruct q.
    apply (mk_disc_cases_elem (fintype.fintype_list X)) in H0.
    simpl in H.
    rewrite (PLT.pair_hom_rel _ _ _ _ _ _ c c1 c2) in H. destruct H.
    exists c1. split; auto.
    simpl in H1.
    apply single_axiom in H1.
    destruct H1 as [[??][??]]. simpl in *.
    hnf in H2. subst c2. auto.
    apply fintype.fintype_complete.
    destruct a.
    apply PLT.compose_hom_rel in H.
    apply PLT.compose_hom_rel.
    destruct H as [q [??]].
    exists (q,x). split.
    apply PLT.pair_hom_rel. split; auto.
    simpl. apply single_axiom.
    destruct c. auto.
    apply (mk_disc_cases_elem (fintype.fintype_list X)).
    apply fintype.fintype_complete.
    auto.   
  Qed.

End disc_cases.
Arguments disc_cases [X A B] f.

Program Definition finbool : fintype :=
  Fintype bool (true::false::nil) _ _.
Next Obligation.
  intros. destruct x; simpl; auto.
Qed.
Next Obligation.
  decide equality.
Qed.

Canonical Structure finbool.

Lemma disc_cases_elem'
     : forall (X : fintype) (A B C : PLT) 
       (f : X -> A → B) (g: C → 1) (x : X) (h : C → A),
       disc_cases f ∘ PLT.pair h (disc_elem x ∘ g) ≈ f x ∘ h.
Proof.
  split; intros a H. destruct a.
  apply PLT.compose_hom_rel in H.
  apply PLT.compose_hom_rel.
  destruct H as [q [??]].
  destruct q.
  apply (mk_disc_cases_elem X _ _ f (fintype.fintype_list X)) in H0.
  simpl in H.
  rewrite (PLT.pair_hom_rel _ _ _ _ _ _ c c1 c2) in H. destruct H.
  apply PLT.compose_hom_rel in H1.
  simpl in *.
  destruct H1 as [q [??]].
  apply single_axiom in H2.
  exists c1. split; auto.
  destruct H2 as [[??][??]]. simpl in *.
  hnf in H3. subst c2. auto.
  apply fintype.fintype_complete.
  destruct a.
  apply PLT.compose_hom_rel in H.
  apply PLT.compose_hom_rel.
  destruct H as [q [??]].
  exists (q,x). split.
  apply PLT.pair_hom_rel. split; auto.
  apply PLT.compose_hom_rel.
  exists tt.
  split.
  destruct (PLT.hom_directed false _ _ g c nil); auto.
  hnf; auto. hnf; intros. apply nil_elem in H1. elim H1.
  destruct H1. apply erel_image_elem in H2. destruct x0. auto.
  simpl. apply single_axiom. auto.
  apply (mk_disc_cases_elem X _ _ f (fintype.fintype_list X)).
  apply fintype.fintype_complete.
  auto.   
Qed.


Lemma disc_cases_univ (X:fintype) (A B:PLT) (f:X -> A → B) q :
  (forall x, f x ≈ q ∘ 〈 id, disc_elem x ∘ PLT.terminate _ _〉) ->
  disc_cases f ≈ q.
Proof.
  intros. split; hnf; simpl; intros.
  destruct a. destruct p.
  apply (mk_disc_cases_elem X _ _ f (fintype.fintype_list X)) in H0.
  destruct (H c1).
  apply H1 in H0.
  apply PLT.compose_hom_rel in H0.
  destruct H0 as [z [??]].
  destruct z.
  apply (PLT.pair_hom_rel false A _ _ id(A) (disc_elem c1 ∘ PLT.terminate _ _))
     in H0.
  destruct H0.
  apply PLT.compose_hom_rel in H4.
  destruct H4 as [?[??]]. destruct x.
  revert H3. apply PLT.hom_order; auto.
  split; simpl.
  simpl in H0. apply ident_elem in H0. auto.
  simpl in H5. apply single_axiom in H5.
  destruct H5 as [[??][??]]; auto.
  apply fintype.fintype_complete.

  destruct a. destruct p.
  apply (mk_disc_cases_elem X _ _ f (fintype.fintype_list X)); auto.
  apply fintype.fintype_complete.
  assert ((c0,c) ∈ PLT.hom_rel (q ∘ 〈id, disc_elem c1 ∘ PLT.terminate false A〉)).
  apply PLT.compose_hom_rel.
  exists (c0,c1).
  split; auto.
  apply PLT.pair_hom_rel.
  split.
  simpl. apply ident_elem; auto.
  apply PLT.compose_hom_rel.
  exists tt. split; auto.
  simpl. apply eprod_elem.
  split. apply eff_complete.
  apply single_axiom; auto.
  simpl. apply single_axiom. auto.
  destruct (H c1).
  apply H3 in H1.
  auto.
Qed.

Lemma disc_cases_commute : forall (X : fintype) (A B C : PLT) 
       (f : X -> A → B) (g:C → A) (h:C → disc X),
       disc_cases f ∘ 〈 g, h 〉 ≈ disc_cases (fun x => f x ∘ g) ∘ 〈 id, h 〉.
Proof.
  intros. transitivity (disc_cases f ∘ PLT.pair_map g id ∘ 〈id,h〉).
  unfold PLT.pair_map.
  rewrite <- (cat_assoc PLT).
  rewrite (PLT.pair_compose_commute false).
  rewrite <- (cat_assoc PLT). rewrite PLT.pair_commute1.
  rewrite <- (cat_assoc PLT). rewrite PLT.pair_commute2.
  rewrite (cat_ident2 PLT). rewrite (cat_ident1 PLT). auto.
  apply cat_respects; auto.
  symmetry. apply disc_cases_univ.
  intros. 
  unfold PLT.pair_map.
  rewrite <- (cat_assoc PLT).
  rewrite (PLT.pair_compose_commute false).
  rewrite <- (cat_assoc PLT). rewrite PLT.pair_commute1.
  rewrite <- (cat_assoc PLT). rewrite PLT.pair_commute2.
  rewrite (cat_ident1 PLT). rewrite (cat_ident2 PLT).
  symmetry.
  apply disc_cases_elem'.
Qed.