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

root / lam_models.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
(* Copyright (c) 2014, Robert Dockins *)

Require Import List.

Require Import basics.
Require Import categories.
Require Import preord.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import plotkin.
Require Import profinite.
Require Import embed.
Require Import joinable.
Require Import directed.
Require Import cont_functors.
Require Import bilimit.
Require Import exp_functor.
Require Import profinite_adj.
Require Import cont_adj.

Notation Ue := liftEMBED.
Notation Le := forgetEMBED.

(**  * Models of untyped λ-calculi
  *)

Definition eagerLamF : functor (EMBED true) (EMBED true)
  := expF true ∘ pairF id id.

Definition cbvLamF : functor (EMBED true) (EMBED true)
  := Le ∘ Ue ∘ expF true ∘ pairF id id.

Definition cbnLamF : functor (EMBED true) (EMBED true)
  := Le ∘ expF false ∘ pairF id id ∘ Ue.

Lemma eagerLamF_continuous : continuous_functor eagerLamF.
Proof.
  unfold eagerLamF.
  apply composeF_continuous.
  apply expF_continuous.
  apply pairF_continuous.
  apply identF_continuous.
  apply identF_continuous.
Qed.

Lemma cbvLamF_continuous : continuous_functor cbvLamF.
Proof.
  unfold cbvLamF.
  apply composeF_continuous.
  apply composeF_continuous.
  apply composeF_continuous.
  apply forgetEMBED_continuous.
  apply liftEMBED_continuous.
  apply expF_continuous.
  apply pairF_continuous.
  apply identF_continuous.
  apply identF_continuous.
Qed.

Lemma cbnLamF_continuous : continuous_functor cbnLamF.
Proof.
  unfold cbnLamF.
  apply composeF_continuous.
  apply composeF_continuous.
  apply composeF_continuous.
  apply forgetEMBED_continuous.
  apply expF_continuous.
  apply pairF_continuous.
  apply identF_continuous.
  apply identF_continuous.
  apply liftEMBED_continuous.
Qed.

Definition lamModelEager : ∂PLT := fixpoint eagerLamF.

Definition lamModelCBV : ∂PLT := fixpoint cbvLamF.

Definition lamModelCBN : ∂PLT := fixpoint cbnLamF.

Lemma lamModelEager_iso :
  ((lamModelEager ⊸ lamModelEager) : ob (EMBED true)) ↔ lamModelEager.
Proof.
  apply (fixpoint_iso eagerLamF).
  apply eagerLamF_continuous.
Qed.

Lemma lamModelCBV_iso :
  (colift (lamModelCBV ⊸ lamModelCBV) : ob (EMBED true)) ↔ lamModelCBV.
Proof.
  apply (fixpoint_iso cbvLamF).
  apply cbvLamF_continuous.
Qed.

Lemma lamModelCBN_iso :
  (L (U lamModelCBN ⇒ U lamModelCBN) : ob (EMBED true))  ↔ lamModelCBN.
Proof.
  apply (fixpoint_iso cbnLamF).
  apply cbnLamF_continuous.
Qed.


(* We can also directly construct a model of lambdas in total PLT...
     but this seems to be the trivial one-point model.

Program Definition lamModelIn : PLT.unit false ⇀ lamF false (PLT.unit false) :=
  Embedding false (PLT.unit false) (lamF false (PLT.unit false)) 
    (fun x => exist _ ((tt,tt)::nil) _) _ _ _ _.
Next Obligation.
  repeat intro.
  hnf. split. hnf; auto.
  simpl. intros. exists tt.
  destruct x0. split; auto.
  apply cons_elem. auto.
  hnf; simpl; intros.
  hnf; auto.
Qed.
Next Obligation.
  hnf; simpl; intros.
  red. hnf. simpl. intros.
  exists tt. exists tt.
  split.
  apply cons_elem; auto.
  split; hnf; auto.
Qed.
Next Obligation.
  repeat intro; hnf; auto.
Qed.
Next Obligation.
  intros. exists tt.
  simpl. hnf; auto.
  simpl; intros.
  exists tt. exists tt.
  split.
  destruct y. simpl.
  destruct i.
  simpl in H1.
  destruct (H1 x) with tt; auto.
  hnf; auto.
  split.
  hnf. intros; hnf; auto.
  intros; hnf; auto.
  destruct H2. destruct x0; auto.
  split; hnf; auto.
Qed.
Next Obligation.
  hnf; simpl. intros.
  exists tt.
  split; hnf; auto.
  split; hnf; auto.
Qed.

Definition lamModelCBN : ob PLT
  := fixpoint_alt (lamF false) (PLT.unit false) lamModelIn.

Lemma lamModelCBN_iso : (PLT.exp lamModelCBN lamModelCBN : ob (EMBED false)) ↔ lamModelCBN.
Proof.
  apply (fixpoint_alt_iso (lamF false)).
  apply lamF_continuous.
Qed.
*)