adamc@170
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@170
|
2 *
|
adamc@170
|
3 * This work is licensed under a
|
adamc@170
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@170
|
5 * Unported License.
|
adamc@170
|
6 * The license text is available at:
|
adamc@170
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@170
|
8 *)
|
adamc@170
|
9
|
adamc@170
|
10 (* begin hide *)
|
adamc@170
|
11 Require Import String List.
|
adamc@170
|
12
|
adamc@173
|
13 Require Import AxiomsImpred Tactics.
|
adamc@170
|
14
|
adamc@170
|
15 Set Implicit Arguments.
|
adamc@170
|
16 (* end hide *)
|
adamc@170
|
17
|
adamc@170
|
18
|
adamc@170
|
19 (** %\chapter{Type-Theoretic Interpreters}% *)
|
adamc@170
|
20
|
adamc@170
|
21 (** TODO: Prose for this chapter *)
|
adamc@170
|
22
|
adamc@170
|
23
|
adamc@170
|
24 (** * Simply-Typed Lambda Calculus *)
|
adamc@170
|
25
|
adamc@170
|
26 Module STLC.
|
adamc@170
|
27 Inductive type : Type :=
|
adamc@170
|
28 | Nat : type
|
adamc@170
|
29 | Arrow : type -> type -> type.
|
adamc@170
|
30
|
adamc@170
|
31 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@170
|
32
|
adamc@170
|
33 Section vars.
|
adamc@170
|
34 Variable var : type -> Type.
|
adamc@170
|
35
|
adamc@170
|
36 Inductive exp : type -> Type :=
|
adamc@170
|
37 | Var : forall t,
|
adamc@170
|
38 var t
|
adamc@170
|
39 -> exp t
|
adamc@170
|
40
|
adamc@170
|
41 | Const : nat -> exp Nat
|
adamc@170
|
42 | Plus : exp Nat -> exp Nat -> exp Nat
|
adamc@170
|
43
|
adamc@170
|
44 | App : forall t1 t2,
|
adamc@170
|
45 exp (t1 --> t2)
|
adamc@170
|
46 -> exp t1
|
adamc@170
|
47 -> exp t2
|
adamc@170
|
48 | Abs : forall t1 t2,
|
adamc@170
|
49 (var t1 -> exp t2)
|
adamc@170
|
50 -> exp (t1 --> t2).
|
adamc@170
|
51 End vars.
|
adamc@170
|
52
|
adamc@170
|
53 Definition Exp t := forall var, exp var t.
|
adamc@170
|
54
|
adamc@170
|
55 Implicit Arguments Var [var t].
|
adamc@170
|
56 Implicit Arguments Const [var].
|
adamc@170
|
57 Implicit Arguments Plus [var].
|
adamc@170
|
58 Implicit Arguments App [var t1 t2].
|
adamc@170
|
59 Implicit Arguments Abs [var t1 t2].
|
adamc@170
|
60
|
adamc@170
|
61 Notation "# v" := (Var v) (at level 70).
|
adamc@170
|
62
|
adamc@170
|
63 Notation "^ n" := (Const n) (at level 70).
|
adamc@171
|
64 Infix "+^" := Plus (left associativity, at level 79).
|
adamc@170
|
65
|
adamc@170
|
66 Infix "@" := App (left associativity, at level 77).
|
adamc@170
|
67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
|
adamc@170
|
68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
|
adamc@170
|
69
|
adamc@172
|
70 Definition zero : Exp Nat := fun _ => ^0.
|
adamc@172
|
71 Definition one : Exp Nat := fun _ => ^1.
|
adamc@172
|
72 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
|
adamc@172
|
73 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
|
adamc@172
|
74 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
|
adamc@172
|
75 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
|
adamc@172
|
76 \f, \x, #f @ #x.
|
adamc@172
|
77 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
|
adamc@172
|
78
|
adamc@170
|
79 Fixpoint typeDenote (t : type) : Set :=
|
adamc@170
|
80 match t with
|
adamc@170
|
81 | Nat => nat
|
adamc@170
|
82 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@170
|
83 end.
|
adamc@170
|
84
|
adamc@170
|
85 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@170
|
86 match e in (exp _ t) return (typeDenote t) with
|
adamc@170
|
87 | Var _ v => v
|
adamc@170
|
88
|
adamc@170
|
89 | Const n => n
|
adamc@170
|
90 | Plus e1 e2 => expDenote e1 + expDenote e2
|
adamc@170
|
91
|
adamc@170
|
92 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@170
|
93 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@170
|
94 end.
|
adamc@170
|
95
|
adamc@170
|
96 Definition ExpDenote t (e : Exp t) := expDenote (e _).
|
adamc@170
|
97
|
adamc@172
|
98 Eval compute in ExpDenote zero.
|
adamc@172
|
99 Eval compute in ExpDenote one.
|
adamc@172
|
100 Eval compute in ExpDenote zpo.
|
adamc@172
|
101 Eval compute in ExpDenote ident.
|
adamc@172
|
102 Eval compute in ExpDenote app_ident.
|
adamc@172
|
103 Eval compute in ExpDenote app.
|
adamc@172
|
104 Eval compute in ExpDenote app_ident'.
|
adamc@172
|
105
|
adamc@170
|
106 Section cfold.
|
adamc@170
|
107 Variable var : type -> Type.
|
adamc@170
|
108
|
adamc@170
|
109 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
|
adamc@170
|
110 match e in exp _ t return exp _ t with
|
adamc@170
|
111 | Var _ v => #v
|
adamc@170
|
112
|
adamc@170
|
113 | Const n => ^n
|
adamc@170
|
114 | Plus e1 e2 =>
|
adamc@170
|
115 let e1' := cfold e1 in
|
adamc@170
|
116 let e2' := cfold e2 in
|
adamc@170
|
117 match e1', e2' with
|
adamc@170
|
118 | Const n1, Const n2 => ^(n1 + n2)
|
adamc@171
|
119 | _, _ => e1' +^ e2'
|
adamc@170
|
120 end
|
adamc@170
|
121
|
adamc@170
|
122 | App _ _ e1 e2 => cfold e1 @ cfold e2
|
adamc@170
|
123 | Abs _ _ e' => Abs (fun x => cfold (e' x))
|
adamc@170
|
124 end.
|
adamc@170
|
125 End cfold.
|
adamc@170
|
126
|
adamc@170
|
127 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
|
adamc@170
|
128
|
adamc@170
|
129 Lemma cfold_correct : forall t (e : exp _ t),
|
adamc@170
|
130 expDenote (cfold e) = expDenote e.
|
adamc@170
|
131 induction e; crush; try (ext_eq; crush);
|
adamc@170
|
132 repeat (match goal with
|
adamc@170
|
133 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
|
adamc@170
|
134 end; crush).
|
adamc@170
|
135 Qed.
|
adamc@170
|
136
|
adamc@170
|
137 Theorem Cfold_correct : forall t (E : Exp t),
|
adamc@170
|
138 ExpDenote (Cfold E) = ExpDenote E.
|
adamc@170
|
139 unfold ExpDenote, Cfold; intros; apply cfold_correct.
|
adamc@170
|
140 Qed.
|
adamc@170
|
141 End STLC.
|
adamc@171
|
142
|
adamc@171
|
143
|
adamc@171
|
144 (** * Adding Products and Sums *)
|
adamc@171
|
145
|
adamc@171
|
146 Module PSLC.
|
adamc@171
|
147 Inductive type : Type :=
|
adamc@171
|
148 | Nat : type
|
adamc@171
|
149 | Arrow : type -> type -> type
|
adamc@171
|
150 | Prod : type -> type -> type
|
adamc@171
|
151 | Sum : type -> type -> type.
|
adamc@171
|
152
|
adamc@171
|
153 Infix "-->" := Arrow (right associativity, at level 62).
|
adamc@171
|
154 Infix "**" := Prod (right associativity, at level 61).
|
adamc@171
|
155 Infix "++" := Sum (right associativity, at level 60).
|
adamc@171
|
156
|
adamc@171
|
157 Section vars.
|
adamc@171
|
158 Variable var : type -> Type.
|
adamc@171
|
159
|
adamc@171
|
160 Inductive exp : type -> Type :=
|
adamc@171
|
161 | Var : forall t,
|
adamc@171
|
162 var t
|
adamc@171
|
163 -> exp t
|
adamc@171
|
164
|
adamc@171
|
165 | Const : nat -> exp Nat
|
adamc@171
|
166 | Plus : exp Nat -> exp Nat -> exp Nat
|
adamc@171
|
167
|
adamc@171
|
168 | App : forall t1 t2,
|
adamc@171
|
169 exp (t1 --> t2)
|
adamc@171
|
170 -> exp t1
|
adamc@171
|
171 -> exp t2
|
adamc@171
|
172 | Abs : forall t1 t2,
|
adamc@171
|
173 (var t1 -> exp t2)
|
adamc@171
|
174 -> exp (t1 --> t2)
|
adamc@171
|
175
|
adamc@171
|
176 | Pair : forall t1 t2,
|
adamc@171
|
177 exp t1
|
adamc@171
|
178 -> exp t2
|
adamc@171
|
179 -> exp (t1 ** t2)
|
adamc@171
|
180 | Fst : forall t1 t2,
|
adamc@171
|
181 exp (t1 ** t2)
|
adamc@171
|
182 -> exp t1
|
adamc@171
|
183 | Snd : forall t1 t2,
|
adamc@171
|
184 exp (t1 ** t2)
|
adamc@171
|
185 -> exp t2
|
adamc@171
|
186
|
adamc@171
|
187 | Inl : forall t1 t2,
|
adamc@171
|
188 exp t1
|
adamc@171
|
189 -> exp (t1 ++ t2)
|
adamc@171
|
190 | Inr : forall t1 t2,
|
adamc@171
|
191 exp t2
|
adamc@171
|
192 -> exp (t1 ++ t2)
|
adamc@171
|
193 | SumCase : forall t1 t2 t,
|
adamc@171
|
194 exp (t1 ++ t2)
|
adamc@171
|
195 -> (var t1 -> exp t)
|
adamc@171
|
196 -> (var t2 -> exp t)
|
adamc@171
|
197 -> exp t.
|
adamc@171
|
198 End vars.
|
adamc@171
|
199
|
adamc@171
|
200 Definition Exp t := forall var, exp var t.
|
adamc@171
|
201
|
adamc@171
|
202 Implicit Arguments Var [var t].
|
adamc@171
|
203 Implicit Arguments Const [var].
|
adamc@171
|
204 Implicit Arguments Abs [var t1 t2].
|
adamc@171
|
205 Implicit Arguments Inl [var t1 t2].
|
adamc@171
|
206 Implicit Arguments Inr [var t1 t2].
|
adamc@171
|
207
|
adamc@171
|
208 Notation "# v" := (Var v) (at level 70).
|
adamc@171
|
209
|
adamc@171
|
210 Notation "^ n" := (Const n) (at level 70).
|
adamc@172
|
211 Infix "+^" := Plus (left associativity, at level 78).
|
adamc@171
|
212
|
adamc@171
|
213 Infix "@" := App (left associativity, at level 77).
|
adamc@171
|
214 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
|
adamc@171
|
215 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
|
adamc@171
|
216
|
adamc@171
|
217 Notation "[ e1 , e2 ]" := (Pair e1 e2).
|
adamc@171
|
218 Notation "#1 e" := (Fst e) (at level 75).
|
adamc@171
|
219 Notation "#2 e" := (Snd e) (at level 75).
|
adamc@171
|
220
|
adamc@171
|
221 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
|
adamc@171
|
222 (at level 79).
|
adamc@171
|
223
|
adamc@172
|
224 Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ =>
|
adamc@172
|
225 \p, [#2 #p, #1 #p].
|
adamc@172
|
226 Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
|
adamc@172
|
227 Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
|
adamc@172
|
228
|
adamc@172
|
229 Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
|
adamc@172
|
230 \s, case #s of x => #x | y => #y +^ #y.
|
adamc@172
|
231 Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
|
adamc@172
|
232 Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
|
adamc@172
|
233 Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
|
adamc@172
|
234 Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
|
adamc@172
|
235
|
adamc@171
|
236 Fixpoint typeDenote (t : type) : Set :=
|
adamc@171
|
237 match t with
|
adamc@171
|
238 | Nat => nat
|
adamc@171
|
239 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@171
|
240 | t1 ** t2 => typeDenote t1 * typeDenote t2
|
adamc@171
|
241 | t1 ++ t2 => typeDenote t1 + typeDenote t2
|
adamc@171
|
242 end%type.
|
adamc@171
|
243
|
adamc@171
|
244 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@171
|
245 match e in (exp _ t) return (typeDenote t) with
|
adamc@171
|
246 | Var _ v => v
|
adamc@171
|
247
|
adamc@171
|
248 | Const n => n
|
adamc@171
|
249 | Plus e1 e2 => expDenote e1 + expDenote e2
|
adamc@171
|
250
|
adamc@171
|
251 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@171
|
252 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@171
|
253
|
adamc@171
|
254 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
adamc@171
|
255 | Fst _ _ e' => fst (expDenote e')
|
adamc@171
|
256 | Snd _ _ e' => snd (expDenote e')
|
adamc@171
|
257
|
adamc@171
|
258 | Inl _ _ e' => inl _ (expDenote e')
|
adamc@171
|
259 | Inr _ _ e' => inr _ (expDenote e')
|
adamc@171
|
260 | SumCase _ _ _ e' e1 e2 =>
|
adamc@171
|
261 match expDenote e' with
|
adamc@171
|
262 | inl v => expDenote (e1 v)
|
adamc@171
|
263 | inr v => expDenote (e2 v)
|
adamc@171
|
264 end
|
adamc@171
|
265 end.
|
adamc@171
|
266
|
adamc@171
|
267 Definition ExpDenote t (e : Exp t) := expDenote (e _).
|
adamc@171
|
268
|
adamc@172
|
269 Eval compute in ExpDenote swap.
|
adamc@172
|
270 Eval compute in ExpDenote zo.
|
adamc@172
|
271 Eval compute in ExpDenote swap_zo.
|
adamc@172
|
272
|
adamc@172
|
273 Eval compute in ExpDenote natOut.
|
adamc@172
|
274 Eval compute in ExpDenote ns1.
|
adamc@172
|
275 Eval compute in ExpDenote ns2.
|
adamc@172
|
276 Eval compute in ExpDenote natOut_ns1.
|
adamc@172
|
277 Eval compute in ExpDenote natOut_ns2.
|
adamc@172
|
278
|
adamc@171
|
279 Section cfold.
|
adamc@171
|
280 Variable var : type -> Type.
|
adamc@171
|
281
|
adamc@172
|
282 Definition pairOutType t :=
|
adamc@172
|
283 match t with
|
adamc@172
|
284 | t1 ** t2 => option (exp var t1 * exp var t2)
|
adamc@172
|
285 | _ => unit
|
adamc@172
|
286 end.
|
adamc@172
|
287
|
adamc@172
|
288 Definition pairOutDefault (t : type) : pairOutType t :=
|
adamc@172
|
289 match t return pairOutType t with
|
adamc@172
|
290 | _ ** _ => None
|
adamc@172
|
291 | _ => tt
|
adamc@172
|
292 end.
|
adamc@172
|
293
|
adamc@172
|
294 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) :=
|
adamc@172
|
295 match e in exp _ t return pairOutType t with
|
adamc@172
|
296 | Pair _ _ e1 e2 => Some (e1, e2)
|
adamc@172
|
297 | _ => pairOutDefault _
|
adamc@172
|
298 end.
|
adamc@172
|
299
|
adamc@171
|
300 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
|
adamc@171
|
301 match e in exp _ t return exp _ t with
|
adamc@171
|
302 | Var _ v => #v
|
adamc@171
|
303
|
adamc@171
|
304 | Const n => ^n
|
adamc@171
|
305 | Plus e1 e2 =>
|
adamc@171
|
306 let e1' := cfold e1 in
|
adamc@171
|
307 let e2' := cfold e2 in
|
adamc@171
|
308 match e1', e2' with
|
adamc@171
|
309 | Const n1, Const n2 => ^(n1 + n2)
|
adamc@171
|
310 | _, _ => e1' +^ e2'
|
adamc@171
|
311 end
|
adamc@171
|
312
|
adamc@171
|
313 | App _ _ e1 e2 => cfold e1 @ cfold e2
|
adamc@171
|
314 | Abs _ _ e' => Abs (fun x => cfold (e' x))
|
adamc@171
|
315
|
adamc@171
|
316 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
|
adamc@172
|
317 | Fst t1 _ e' =>
|
adamc@172
|
318 let e'' := cfold e' in
|
adamc@172
|
319 match pairOut e'' with
|
adamc@172
|
320 | None => #1 e''
|
adamc@172
|
321 | Some (e1, _) => e1
|
adamc@172
|
322 end
|
adamc@172
|
323 | Snd _ _ e' =>
|
adamc@172
|
324 let e'' := cfold e' in
|
adamc@172
|
325 match pairOut e'' with
|
adamc@172
|
326 | None => #2 e''
|
adamc@172
|
327 | Some (_, e2) => e2
|
adamc@172
|
328 end
|
adamc@171
|
329
|
adamc@171
|
330 | Inl _ _ e' => Inl (cfold e')
|
adamc@171
|
331 | Inr _ _ e' => Inr (cfold e')
|
adamc@171
|
332 | SumCase _ _ _ e' e1 e2 =>
|
adamc@171
|
333 case cfold e' of
|
adamc@171
|
334 x => cfold (e1 x)
|
adamc@171
|
335 | y => cfold (e2 y)
|
adamc@171
|
336 end.
|
adamc@171
|
337 End cfold.
|
adamc@171
|
338
|
adamc@171
|
339 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
|
adamc@171
|
340
|
adamc@172
|
341 Section pairs.
|
adamc@172
|
342 Variables A B : Type.
|
adamc@172
|
343
|
adamc@172
|
344 Variable v1 : A.
|
adamc@172
|
345 Variable v2 : B.
|
adamc@172
|
346 Variable v : A * B.
|
adamc@172
|
347
|
adamc@172
|
348 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
|
adamc@172
|
349 destruct v; crush.
|
adamc@172
|
350 Qed.
|
adamc@172
|
351
|
adamc@172
|
352 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
|
adamc@172
|
353 destruct v; crush.
|
adamc@172
|
354 Qed.
|
adamc@172
|
355 End pairs.
|
adamc@172
|
356
|
adamc@172
|
357 Hint Resolve pair_eta1 pair_eta2.
|
adamc@172
|
358
|
adamc@171
|
359 Lemma cfold_correct : forall t (e : exp _ t),
|
adamc@171
|
360 expDenote (cfold e) = expDenote e.
|
adamc@171
|
361 induction e; crush; try (ext_eq; crush);
|
adamc@171
|
362 repeat (match goal with
|
adamc@171
|
363 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
|
adamc@171
|
364 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
|
adamc@172
|
365 end; crush); eauto.
|
adamc@171
|
366 Qed.
|
adamc@171
|
367
|
adamc@171
|
368 Theorem Cfold_correct : forall t (E : Exp t),
|
adamc@171
|
369 ExpDenote (Cfold E) = ExpDenote E.
|
adamc@171
|
370 unfold ExpDenote, Cfold; intros; apply cfold_correct.
|
adamc@171
|
371 Qed.
|
adamc@171
|
372 End PSLC.
|
adamc@173
|
373
|
adamc@173
|
374
|
adamc@173
|
375 (** * Type Variables *)
|
adamc@173
|
376
|
adamc@173
|
377 Module SysF.
|
adamc@173
|
378 Section vars.
|
adamc@173
|
379 Variable tvar : Type.
|
adamc@173
|
380
|
adamc@173
|
381 Inductive type : Type :=
|
adamc@173
|
382 | Nat : type
|
adamc@173
|
383 | Arrow : type -> type -> type
|
adamc@173
|
384 | TVar : tvar -> type
|
adamc@173
|
385 | All : (tvar -> type) -> type.
|
adamc@173
|
386
|
adamc@173
|
387 Notation "## v" := (TVar v) (at level 40).
|
adamc@173
|
388 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@173
|
389
|
adamc@173
|
390 Section Subst.
|
adamc@173
|
391 Variable t : type.
|
adamc@173
|
392
|
adamc@173
|
393 Inductive Subst : (tvar -> type) -> type -> Prop :=
|
adamc@173
|
394 | SNat : Subst (fun _ => Nat) Nat
|
adamc@173
|
395 | SArrow : forall dom ran dom' ran',
|
adamc@173
|
396 Subst dom dom'
|
adamc@173
|
397 -> Subst ran ran'
|
adamc@173
|
398 -> Subst (fun v => dom v --> ran v) (dom' --> ran')
|
adamc@173
|
399 | SVarEq : Subst TVar t
|
adamc@173
|
400 | SVarNe : forall v, Subst (fun _ => ##v) (##v)
|
adamc@173
|
401 | SAll : forall ran ran',
|
adamc@173
|
402 (forall v', Subst (fun v => ran v v') (ran' v'))
|
adamc@173
|
403 -> Subst (fun v => All (ran v)) (All ran').
|
adamc@173
|
404 End Subst.
|
adamc@173
|
405
|
adamc@173
|
406 Variable var : type -> Type.
|
adamc@173
|
407
|
adamc@173
|
408 Inductive exp : type -> Type :=
|
adamc@173
|
409 | Var : forall t,
|
adamc@173
|
410 var t
|
adamc@173
|
411 -> exp t
|
adamc@173
|
412
|
adamc@173
|
413 | Const : nat -> exp Nat
|
adamc@173
|
414 | Plus : exp Nat -> exp Nat -> exp Nat
|
adamc@173
|
415
|
adamc@173
|
416 | App : forall t1 t2,
|
adamc@173
|
417 exp (t1 --> t2)
|
adamc@173
|
418 -> exp t1
|
adamc@173
|
419 -> exp t2
|
adamc@173
|
420 | Abs : forall t1 t2,
|
adamc@173
|
421 (var t1 -> exp t2)
|
adamc@173
|
422 -> exp (t1 --> t2)
|
adamc@173
|
423
|
adamc@173
|
424 | TApp : forall tf,
|
adamc@173
|
425 exp (All tf)
|
adamc@173
|
426 -> forall t tf', Subst t tf tf'
|
adamc@173
|
427 -> exp tf'
|
adamc@173
|
428 | TAbs : forall tf,
|
adamc@173
|
429 (forall v, exp (tf v))
|
adamc@173
|
430 -> exp (All tf).
|
adamc@173
|
431 End vars.
|
adamc@173
|
432
|
adamc@173
|
433 Definition Typ := forall tvar, type tvar.
|
adamc@173
|
434 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
|
adamc@173
|
435
|
adamc@173
|
436 Implicit Arguments Nat [tvar].
|
adamc@173
|
437
|
adamc@173
|
438 Notation "## v" := (TVar v) (at level 40).
|
adamc@173
|
439 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@173
|
440 Notation "\\\ x , t" := (All (fun x => t)) (at level 65).
|
adamc@173
|
441
|
adamc@173
|
442 Implicit Arguments Var [tvar var t].
|
adamc@173
|
443 Implicit Arguments Const [tvar var].
|
adamc@173
|
444 Implicit Arguments Plus [tvar var].
|
adamc@173
|
445 Implicit Arguments App [tvar var t1 t2].
|
adamc@173
|
446 Implicit Arguments Abs [tvar var t1 t2].
|
adamc@173
|
447
|
adamc@173
|
448 Implicit Arguments TAbs [tvar var tf].
|
adamc@173
|
449
|
adamc@173
|
450 Notation "# v" := (Var v) (at level 70).
|
adamc@173
|
451
|
adamc@173
|
452 Notation "^ n" := (Const n) (at level 70).
|
adamc@173
|
453 Infix "+^" := Plus (left associativity, at level 79).
|
adamc@173
|
454
|
adamc@173
|
455 Infix "@" := App (left associativity, at level 77).
|
adamc@173
|
456 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
|
adamc@173
|
457 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
|
adamc@173
|
458
|
adamc@173
|
459 Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77).
|
adamc@173
|
460 Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78).
|
adamc@173
|
461 Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78).
|
adamc@173
|
462
|
adamc@173
|
463 Definition zero : Exp (fun _ => Nat) := fun _ _ =>
|
adamc@173
|
464 ^0.
|
adamc@173
|
465 Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ =>
|
adamc@173
|
466 \\T, \x, #x.
|
adamc@173
|
467 Definition ident_zero : Exp (fun _ => Nat).
|
adamc@173
|
468 do 2 intro; refine (ident _ @@ _ @ zero _);
|
adamc@173
|
469 repeat constructor.
|
adamc@173
|
470 Defined.
|
adamc@173
|
471 Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T).
|
adamc@173
|
472 do 2 intro; refine (ident _ @@ _ @ ident _);
|
adamc@173
|
473 repeat constructor.
|
adamc@173
|
474 Defined.
|
adamc@173
|
475 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
|
adamc@173
|
476 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
|
adamc@173
|
477 repeat constructor.
|
adamc@173
|
478 Defined.
|
adamc@173
|
479
|
adamc@173
|
480 Fixpoint typeDenote (t : type Set) : Set :=
|
adamc@173
|
481 match t with
|
adamc@173
|
482 | Nat => nat
|
adamc@173
|
483 | t1 --> t2 => typeDenote t1 -> typeDenote t2
|
adamc@173
|
484 | ##v => v
|
adamc@173
|
485 | All tf => forall T, typeDenote (tf T)
|
adamc@173
|
486 end.
|
adamc@173
|
487
|
adamc@173
|
488 Lemma Subst_typeDenote : forall t tf tf',
|
adamc@173
|
489 Subst t tf tf'
|
adamc@173
|
490 -> typeDenote (tf (typeDenote t)) = typeDenote tf'.
|
adamc@173
|
491 induction 1; crush; ext_eq; crush.
|
adamc@173
|
492 Defined.
|
adamc@173
|
493
|
adamc@173
|
494 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
|
adamc@173
|
495 match e in (exp _ t) return (typeDenote t) with
|
adamc@173
|
496 | Var _ v => v
|
adamc@173
|
497
|
adamc@173
|
498 | Const n => n
|
adamc@173
|
499 | Plus e1 e2 => expDenote e1 + expDenote e2
|
adamc@173
|
500
|
adamc@173
|
501 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
|
adamc@173
|
502 | Abs _ _ e' => fun x => expDenote (e' x)
|
adamc@173
|
503
|
adamc@173
|
504 | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with
|
adamc@173
|
505 | refl_equal => (expDenote e') (typeDenote t')
|
adamc@173
|
506 end
|
adamc@173
|
507 | TAbs _ e' => fun T => expDenote (e' T)
|
adamc@173
|
508 end.
|
adamc@173
|
509
|
adamc@173
|
510 Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
|
adamc@173
|
511
|
adamc@173
|
512 Eval compute in ExpDenote zero.
|
adamc@173
|
513 Eval compute in ExpDenote ident.
|
adamc@173
|
514 Eval compute in ExpDenote ident_zero.
|
adamc@173
|
515 Eval compute in ExpDenote ident_ident.
|
adamc@173
|
516 Eval compute in ExpDenote ident5.
|
adamc@173
|
517
|
adamc@173
|
518 Section cfold.
|
adamc@173
|
519 Variable tvar : Type.
|
adamc@173
|
520 Variable var : type tvar -> Type.
|
adamc@173
|
521
|
adamc@173
|
522 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
|
adamc@173
|
523 match e in exp _ t return exp _ t with
|
adamc@173
|
524 | Var _ v => #v
|
adamc@173
|
525
|
adamc@173
|
526 | Const n => ^n
|
adamc@173
|
527 | Plus e1 e2 =>
|
adamc@173
|
528 let e1' := cfold e1 in
|
adamc@173
|
529 let e2' := cfold e2 in
|
adamc@173
|
530 match e1', e2' with
|
adamc@173
|
531 | Const n1, Const n2 => ^(n1 + n2)
|
adamc@173
|
532 | _, _ => e1' +^ e2'
|
adamc@173
|
533 end
|
adamc@173
|
534
|
adamc@173
|
535 | App _ _ e1 e2 => cfold e1 @ cfold e2
|
adamc@173
|
536 | Abs _ _ e' => Abs (fun x => cfold (e' x))
|
adamc@173
|
537
|
adamc@173
|
538 | TApp _ e' _ _ pf => TApp (cfold e') pf
|
adamc@173
|
539 | TAbs _ e' => \\T, cfold (e' T)
|
adamc@173
|
540 end.
|
adamc@173
|
541 End cfold.
|
adamc@173
|
542
|
adamc@173
|
543 Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _).
|
adamc@173
|
544
|
adamc@173
|
545 Lemma cfold_correct : forall t (e : exp _ t),
|
adamc@173
|
546 expDenote (cfold e) = expDenote e.
|
adamc@173
|
547 induction e; crush; try (ext_eq; crush);
|
adamc@173
|
548 repeat (match goal with
|
adamc@173
|
549 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
|
adamc@173
|
550 end; crush).
|
adamc@173
|
551 Qed.
|
adamc@173
|
552
|
adamc@173
|
553 Theorem Cfold_correct : forall t (E : Exp t),
|
adamc@173
|
554 ExpDenote (Cfold E) = ExpDenote E.
|
adamc@173
|
555 unfold ExpDenote, Cfold; intros; apply cfold_correct.
|
adamc@173
|
556 Qed.
|
adamc@173
|
557 End SysF.
|