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

root / preord.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
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
(* Copyright (c) 2014, Robert Dockins *)

Require Import Setoid.
Require Import Coq.Program.Basics.

Require Import basics.
Require Import categories.

Delimit Scope preord_scope with preord.
Open Scope preord_scope.

(**  * Preordered types and monotone functions.

     A preorder is a type equipped with a transitive,
     reflexive relation.  Unlike standard domain theory,
     we will be concentrating on preorders rather than
     partial orders as the basis of order theory.

     As compared to partial orders, preorders lack the
     axiom of antisymmetry.  Instead, we work (almost) always
     up to the equivalence relation induced by the preorder.
     On a preorder, we automatically define a setoid
     by setting [x ≈ y] iff [x ≤ y /\ y ≤ x].  Thus, we
     "recover" antisymmetry by convention.
  *)
Module Preord.
  Record mixin_of (T:Type) :=
    Mixin
    { ord : T -> T -> Prop
    ; refl : forall x, ord x x
    ; trans : forall {x y z},
             ord x y -> ord y z -> ord x z
    }.
  Structure type : Type :=
    Pack { carrier :> Type ; mixin : mixin_of carrier }.

  Definition ord_op T := ord _ (mixin T).

  Record hom (X Y:type) := Hom
    { map :> carrier X -> carrier Y
    ; axiom : forall (a b:carrier X), ord_op X a b -> ord_op Y (map a) (map b)
    }.

  Program Definition ident (X:type) : hom X X := Hom X X (fun x => x) _.
  Program Definition compose (X Y Z:type) (g:hom Y Z) (f:hom X Y)
    := Hom X Z (fun x => g (f x)) _.
  Next Obligation.
    apply axiom. apply axiom. auto.
  Qed.

  Definition comp_mixin := Comp.Mixin type hom ident compose.

  Definition eq (X:type) (a b:X) := ord_op X a b /\ ord_op X b a.

  Definition hom_ord (X Y:type) (f g:hom X Y) := forall x, ord_op Y (f x) (g x).
  Definition hom_eq (X Y:type) (f g:hom X Y) := forall x, eq Y (f x) (g x).

  Program Definition ord_mixin X Y := Mixin (hom X Y) (hom_ord X Y) _ _.
  Next Obligation.
    red; intro. apply refl.
  Qed.
  Next Obligation.
    red; intro. eapply trans; eauto.
    apply (H x0). apply (H0 x0).
  Qed.

  Program Definition eq_mixin X Y := Eq.Mixin (hom X Y) (hom_eq X Y) _ _ _.
  Next Obligation.
    red; intros. red. split; apply refl.
  Qed.
  Next Obligation.
    red; intros. red. split.
    destruct (H x0); auto.
    destruct (H x0); auto.
  Qed.
  Next Obligation.
    intro.
    destruct (H x0). destruct (H0 x0).
    split; eapply trans; eauto.
  Qed.

  Lemma cat_axioms : Category.axioms type hom eq_mixin comp_mixin.
    constructor.
    
    repeat intro. split. simpl. red. apply refl.
    repeat intro. simpl. red. apply refl.

    repeat intro. split. simpl. red. apply refl.
    simpl. red. apply refl.
    
    repeat intro. split; simpl; red; apply refl.
    repeat intro. split; simpl; red.
    apply trans with (f (g' x)).
    apply axiom.
    destruct (H0 x); auto.
    destruct (H (g' x)); auto.
    apply trans with (f (g' x)).
    destruct (H (g' x)); auto.
    apply axiom.
    destruct (H0 x); auto.
  Qed.

  Program Definition ord_eq (T:type) : Eq.mixin_of T :=
    Eq.Mixin T (eq T) _ _ _.
  Next Obligation.
    split; apply refl.
  Qed.
  Next Obligation.
    destruct H; split; auto.
  Qed.
  Next Obligation.
    destruct H; destruct H0.
    split; eapply trans; eauto.
  Qed.
End Preord.
Notation preord := Preord.type.

Notation "x ≤ y" := (@Preord.ord_op _ x y) : preord_scope.
Notation "y ≥ x" := (@Preord.ord_op _ x y) (only parsing) : preord_scope.
Notation "x ≰ y" := (~ (@Preord.ord_op _ x y)) : preord_scope.
Notation "y ≱ x" := (~ (@Preord.ord_op _ x y)) (only parsing) : preord_scope.

(**  Here we set up the category PREORD of preorders with montone functions
     and the canonical structure magic that makes notation work.
  *) 
Coercion Preord.carrier : Preord.type >-> Sortclass.
Coercion Preord.map : Preord.hom >-> Funclass.

Canonical Structure hom_order X Y := Preord.Pack (Preord.hom X Y) (Preord.ord_mixin X Y).
Canonical Structure Preord_Eq (X:preord) : Eq.type :=
  Eq.Pack (Preord.carrier X) (Preord.ord_eq X).

Canonical Structure PREORD :=
  Category preord Preord.hom _ _ Preord.cat_axioms.

Canonical Structure preord_hom_eq (A B:preord):=
  Eq.Pack (Preord.hom A B) (Preord.eq_mixin A B).
Canonical Structure preord_comp :=
  Comp.Pack preord Preord.hom Preord.comp_mixin.

(**  The preorder axioms and their relation to equality.
  *)
Lemma ord_refl : forall (T:preord) (x:T), x ≤ x.
Proof.
  intros. destruct T. destruct mixin. apply refl.
Qed.

Lemma ord_trans : forall (T:preord) (x y z:T), x ≤ y -> y ≤ z -> x ≤ z.
Proof.
  intros. destruct T. destruct mixin. eapply trans; eauto.
Qed.

Lemma ord_antisym : forall (T:preord) (x y:T), x ≤ y -> y ≤ x -> x ≈ y.
Proof.
  intros. split; auto.
Qed.

Lemma eq_ord : forall (T:preord) (x y:T), x ≈ y -> x ≤ y.
Proof.
  intros; destruct H; auto.
Qed.

Lemma eq_ord' : forall (T:preord) (x y:T), x ≈ y -> y ≤ x.
Proof.
  intros; destruct H; auto.
Qed.


(**  Set up setoid rewriting
  *)
Add Parametric Relation (A:preord) : (Preord.carrier A) (@Preord.ord_op A)
  reflexivity proved by (ord_refl A)
  transitivity proved by (ord_trans A)
    as ord_rel.

Add Parametric Morphism (A:preord) :
  (@Preord.ord_op A)
    with signature (Preord.ord_op A) -->
                   (Preord.ord_op A) ++>
                   impl
     as ord_morphism.
Proof.
  repeat intro.
  transitivity x; auto.
  transitivity x0; auto.
Qed.

Add Parametric Morphism (A:preord) :
  (@Preord.ord_op A)
    with signature (eq_op (Preord_Eq A)) ==>
                   (eq_op (Preord_Eq A)) ==>
                   iff
     as ord_eq_morphism.
Proof.
  intros. 
  destruct H; destruct H0.
  split; intros.
  transitivity x; auto.
  transitivity x0; auto.
  transitivity y; auto.
  transitivity y0; auto.
Qed.

Add Parametric Morphism (A B:preord) :
  (@Preord.map A B)
   with signature (Preord.ord_op (hom_order A B)) ++>
                  (Preord.ord_op A) ++>
                  (Preord.ord_op B)
    as preord_map_morphism.
Proof.
  intros.
  transitivity (x y0).
  apply Preord.axiom. auto.
  apply H.
Qed.
  
Add Parametric Morphism (A B:preord) :
  (@Preord.map A B)
   with signature (eq_op (Preord_Eq (hom_order A B))) ==>
                  (eq_op (Preord_Eq A)) ==>
                  (eq_op (Preord_Eq B))
    as preord_map_eq_morphism.
Proof.
  intros.
  transitivity (x y0).
  destruct H0; split; apply Preord.axiom; auto.
  destruct H; split; auto.
Qed.

(**  This lemma is handy for using an equality in the context to prove a goal
     by transitivity on both sides.
  *)
Lemma use_ord (A:preord) (a b c d:A) :
  b ≤ c -> a ≤ b -> c ≤ d -> a ≤ d.
Proof.
  intros.
  transitivity b; auto.
  transitivity c; auto.
Qed.
Arguments use_ord [A] [a] [b] [c] [d] _ _ _.


(**  PREORD is a concrete category.
  *)
Program Definition PREORD_concrete : concrete PREORD :=
  Concrete PREORD
  Preord.carrier
  (fun X => Eq.mixin (Preord_Eq X))
  Preord.map _ _.
Next Obligation.
  split. 
  apply ord_trans with (Preord.map A B f y).
  apply Preord.axiom. destruct H0; auto. 
  destruct (H y); auto.
  apply ord_trans with (Preord.map A B f y).
  destruct (H y); auto.
  apply Preord.axiom. destruct H0; auto. 
Qed.
Next Obligation.
  split; apply Preord.refl.
Qed.

Canonical Structure PREORD_concrete.


(**  Monotone functions respect equality and order.
  *)
Lemma preord_eq : forall (X Y:preord) (f:X → Y) (x y:X), x ≈ y -> f x ≈ f y.
Proof.
  intros. rewrite H. auto.
Qed.

Lemma preord_ord : forall (X Y:preord) (f:X → Y) (x y:X), x ≤ y -> f x ≤ f y.
Proof.
  intros. apply Preord.axiom. auto.
Qed.  

Hint Resolve ord_refl ord_trans ord_antisym preord_ord preord_eq eq_ord eq_ord'.

Add Parametric Morphism (X Y:preord) :
  (@hommap PREORD PREORD_concrete X Y)
  with signature (eq_op (CAT_EQ PREORD X Y)) ==> 
                 (eq_op (Preord_Eq X)) ==>
                 (eq_op (Preord_Eq Y))
  as preord_apply_eq_morphism.
Proof.
  intros.
  transitivity (x#y0).
  apply preord_eq; auto.
  apply H.
Qed.

Add Parametric Morphism (X Y:preord) :
  (@hommap PREORD PREORD_concrete X Y)
  with signature (eq_op (CAT_EQ PREORD X Y)) ++> 
                 (eq_op (Preord_Eq X)) ++>
                 (Preord.ord_op Y)
  as preord_apply_eqord_morphism.
Proof.
  intros.
  transitivity (x#y0).
  apply preord_eq; auto.
  apply H.
Qed.

Add Parametric Morphism (X Y:preord) :
  (@hommap PREORD PREORD_concrete X Y)
  with signature (fun (x y:hom PREORD X Y) => Preord.ord_op (hom_order X Y) x y) ==> 
                 (Preord.ord_op X) ==>
                 (Preord.ord_op Y)
  as preord_apply_ord_morphism.
Proof.
  intros. 
  transitivity (x#y0).
  apply preord_ord. auto.
  apply H.
Qed.

(** PREORD is termianted. *)

Program Definition unitpo := Preord.Pack unit (Preord.Mixin _ (fun _ _ => True) _ _).
Canonical Structure unitpo.

Program Definition preord_terminate (A:preord) : A → unitpo :=
  Preord.Hom A unitpo (fun x => tt) _.

Program Definition preord_terminated_mixin :=
  Terminated.Mixin 
     preord Preord.hom 
     Preord.eq_mixin
     unitpo preord_terminate
     _.
Next Obligation.
  split; simpl; hnf; auto.
Qed.
     
Canonical Structure preord_terminated :=
  Terminated 
     preord Preord.hom 
     Preord.eq_mixin
     Preord.comp_mixin
     Preord.cat_axioms
     preord_terminated_mixin.

(** PREORD is initialized. *)
Program Definition emptypo :=
  Preord.Pack False (Preord.Mixin _ (fun _ _ => False) _ _).
Canonical Structure emptypo.

Program Definition preord_initiate (A:preord) : emptypo → A :=
  Preord.Hom emptypo A (fun x => False_rect _ x) _.
Next Obligation. elim a. Qed.

Program Definition preord_initialized_mixin :=
  Initialized.Mixin
     preord Preord.hom 
     Preord.eq_mixin
     emptypo preord_initiate
     _.
Next Obligation.
  split; simpl; elim x.
Qed.

Canonical Structure preord_initialized :=
  Initialized
     preord Preord.hom 
     Preord.eq_mixin
     Preord.comp_mixin
     Preord.cat_axioms
     preord_initialized_mixin.

(**  The preorder on products, defined pointwise. *)
Definition prod_ord (A B:preord) (x y:A*B):=
  (fst x) ≤ (fst y) /\ (snd x) ≤ (snd y).

Program Definition prod_preord (A B:preord) : preord :=
  Preord.Pack (A*B) (Preord.Mixin _ (prod_ord A B) _ _).
Next Obligation.
  hnf. simpl; auto.
Qed.
Next Obligation.
  destruct H; destruct H0; split; simpl in *.
  eapply ord_trans; eauto.
  eapply ord_trans; eauto.
Qed.

Canonical Structure prod_preord.


(** PREORD is a cartesian category. *)
Program Definition pi1 {A B:preord} : prod_preord A B → A :=
  Preord.Hom (prod_preord A B) A (fun x => fst x) _.
Next Obligation.
  destruct H; simpl; auto.
Qed.

Program Definition pi2 {A B:preord} : prod_preord A B → B :=
  Preord.Hom (prod_preord A B) B (fun x => snd x) _.
Next Obligation.
  destruct H; simpl; auto.
Qed.

Program Definition mk_pair {C A B:preord} (f:C → A) (g:C → B) : C → prod_preord A B :=
  Preord.Hom C (prod_preord A B) (fun c => (f c, g c)) _.
Next Obligation.
  intros. split; simpl; apply Preord.axiom; auto.
Qed.  

Program Definition preord_cartesian_mixin
  := Cartesian.Mixin
      Preord.type Preord.hom
      Preord.eq_mixin
      Preord.comp_mixin
      prod_preord (@pi1) (@pi2) (@mk_pair) _.
Next Obligation.      
  constructor.

  intros. split; simpl; auto.
  intros. split; simpl; auto.

  intros. intro. split. simpl.
  split; simpl.
  destruct (H x); auto.
  destruct (H0 x); auto.
  split; simpl.
  destruct (H x); auto.
  destruct (H0 x); auto.
Qed.
    
Canonical Structure preord_cartesian : cartesian :=
  Cartesian Preord.type Preord.hom
      Preord.eq_mixin
      Preord.comp_mixin
      Preord.cat_axioms
      preord_terminated_mixin
      preord_cartesian_mixin.

(** Further, PREORD is a cartesian closed category. *)
Program Definition preord_curry (C A B:preord) (f:C×A → B) : C → hom_order A B :=
  Preord.Hom C (hom_order A B) (fun c => Preord.Hom A B (fun a => f (c,a)) _) _.
Next Obligation.
  apply preord_ord. split; auto.
Qed.
Next Obligation.
  intro x. simpl.
  apply preord_ord. split; auto.
Qed.

Program Definition preord_apply (A B:preord) : (hom_order A B × A) → B :=
  Preord.Hom (hom_order A B × A) B (fun fx => fst fx (snd fx)) _.
Next Obligation.
  simpl. destruct H; simpl in *.
  apply preord_map_morphism; auto.
Qed.

Program Definition preord_ccc_mixin 
   := CartesianClosed.Mixin
       Preord.type Preord.hom
       Preord.eq_mixin
       Preord.comp_mixin
       Preord.cat_axioms
       preord_terminated_mixin
       preord_cartesian_mixin
       hom_order preord_curry preord_apply
       _.
Next Obligation.
  constructor.

  simpl. intros.
  split; simpl; destruct x; simpl; auto.
  
  simpl. intros.
  split; intro z; simpl.
  rewrite <- H. simpl; auto.
  rewrite <- H. simpl; auto.
Qed.

Canonical Structure preord_ccc : cartesian_closed :=
  CartesianClosed 
       Preord.type Preord.hom
       Preord.eq_mixin
       Preord.comp_mixin
       Preord.cat_axioms
       preord_cartesian_mixin
       preord_terminated_mixin
       preord_ccc_mixin.


(** The preorder on sums, defined in the standard way.
  *)
Definition sum_ord (A B:preord) (x y:A+B):=
  match x, y with
  | inl x', inl y' => x' ≤ y'
  | inr x', inr y' => x' ≤ y'
  | _, _ => False
  end.

Program Definition sum_preord (A B:preord) : preord :=
  Preord.Pack (A+B) (Preord.Mixin _ (sum_ord A B) _ _).
Next Obligation.
  hnf. destruct x; auto.
Qed.
Next Obligation.
  hnf. destruct x; destruct y; destruct z; simpl in *; intuition.
  eapply ord_trans; eauto.
  eapply ord_trans; eauto.
Qed.

Canonical Structure sum_preord.

(**  Preorders with an [ord_dec] structure have a decidable order relation.
  *)
Record ord_dec (A:preord) :=
  OrdDec
  { orddec :> forall x y:A, {x ≤ y}+{x ≰ y} }.

Arguments orddec [A] [o] x y.

(**  Preorders with decidable ordering also have decidable equality.
  *)
Canonical Structure PREORD_EQ_DEC (A:preord) (OD:ord_dec A) :=
  EqDec (Preord_Eq A) (fun (x y:A) =>
      match @orddec A OD x y with
      | left H1 => 
          match @orddec A OD y x with
          | left H2 => left _ (conj H1 H2)
          | right H => right _ (fun HEQ => H (proj2 HEQ))
          end
      | right H => right (fun HEQ => H (proj1 HEQ))
      end).

(** The "lift" preorder, which adjoins a new bottom element.
    The lift construction gives rise to an endofunctor on PREORD.
  *)
Definition lift_ord (A:preord) (x:option A) (y:option A) : Prop :=
   match x with None => True | Some x' =>
     match y with None => False | Some y' => x' ≤ y' end end.

Program Definition lift_mixin (A:preord) : Preord.mixin_of (option A) :=
  Preord.Mixin (option A) (lift_ord A) _ _.
Next Obligation.
  destruct x; simpl; auto.
Qed.
Next Obligation.
  destruct x; destruct y; destruct z; simpl in *; intuition. eauto.
Qed.

Canonical Structure lift (A:preord) : preord :=
  Preord.Pack (option A) (lift_mixin A).

Program Definition liftup (A:preord) : A → lift A :=
  Preord.Hom A (lift A) (@Some A) _.

Program Definition lift_map {A B:preord} (f:A → B) : lift A → lift B :=
  Preord.Hom (lift A) (lift B) (option_map (Preord.map A B f)) _.
Next Obligation.
  red; intros. destruct a; destruct b; simpl in *; auto.
Qed.

Lemma lift_map_id (A:preord) : lift_map id(A) ≈ id(lift A).
Proof.
  split; hnf; destruct x; simpl; auto.
Qed.

Lemma lift_map_compose (A B C:preord) (g:B → C) (f:A → B) :
  lift_map (g ∘ f) ≈ lift_map g ∘ lift_map f.
Proof.
  split; hnf; destruct x; simpl; auto.
Qed.

Lemma lift_map_eq (A B:preord) (f f':A → B) : f ≈ f' -> lift_map f ≈ lift_map f'.
Proof.
  intros.
  split; hnf; destruct x; simpl; auto.
  apply H. apply H.
Qed.

Program Definition liftF : functor PREORD PREORD :=
  (Functor PREORD PREORD lift (@lift_map) _ _ _).
Next Obligation.
  transitivity (lift_map id(A)).
  apply lift_map_eq; auto.
  apply lift_map_id.
Qed.
Next Obligation.
  transitivity (lift_map (f ∘ g)).
  apply lift_map_eq; auto.
  apply lift_map_compose.
Qed.
Next Obligation.
  apply lift_map_eq. auto.
Qed.