adamc@152
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@152
|
2 *
|
adamc@152
|
3 * This work is licensed under a
|
adamc@152
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@152
|
5 * Unported License.
|
adamc@152
|
6 * The license text is available at:
|
adamc@152
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@152
|
8 *)
|
adamc@152
|
9
|
adamc@152
|
10 (* begin hide *)
|
adamc@156
|
11 Require Import Arith String List.
|
adamc@152
|
12
|
adamc@152
|
13 Require Import Tactics.
|
adamc@152
|
14
|
adamc@152
|
15 Set Implicit Arguments.
|
adamc@152
|
16 (* end hide *)
|
adamc@152
|
17
|
adamc@152
|
18
|
adamc@153
|
19 (** %\part{Formalizing Programming Languages and Compilers}
|
adamc@152
|
20
|
adamc@153
|
21 \chapter{First-Order Abstract Syntax}% *)
|
adamc@152
|
22
|
adamc@152
|
23 (** TODO: Prose for this chapter *)
|
adamc@152
|
24
|
adamc@152
|
25
|
adamc@152
|
26 (** * Concrete Binding *)
|
adamc@152
|
27
|
adamc@152
|
28 Module Concrete.
|
adamc@152
|
29
|
adamc@152
|
30 Definition var := string.
|
adamc@152
|
31 Definition var_eq := string_dec.
|
adamc@152
|
32
|
adamc@152
|
33 Inductive exp : Set :=
|
adamc@152
|
34 | Const : bool -> exp
|
adamc@152
|
35 | Var : var -> exp
|
adamc@152
|
36 | App : exp -> exp -> exp
|
adamc@152
|
37 | Abs : var -> exp -> exp.
|
adamc@152
|
38
|
adamc@152
|
39 Inductive type : Set :=
|
adamc@152
|
40 | Bool : type
|
adamc@152
|
41 | Arrow : type -> type -> type.
|
adamc@152
|
42
|
adamc@152
|
43 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@152
|
44
|
adamc@152
|
45 Definition ctx := list (var * type).
|
adamc@152
|
46
|
adamc@152
|
47 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
|
adamc@152
|
48
|
adamc@152
|
49 Inductive lookup : ctx -> var -> type -> Prop :=
|
adamc@152
|
50 | First : forall x t G,
|
adamc@152
|
51 (x, t) :: G |-v x : t
|
adamc@152
|
52 | Next : forall x t x' t' G,
|
adamc@152
|
53 x <> x'
|
adamc@152
|
54 -> G |-v x : t
|
adamc@152
|
55 -> (x', t') :: G |-v x : t
|
adamc@152
|
56
|
adamc@152
|
57 where "G |-v x : t" := (lookup G x t).
|
adamc@152
|
58
|
adamc@152
|
59 Hint Constructors lookup.
|
adamc@152
|
60
|
adamc@152
|
61 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
|
adamc@152
|
62
|
adamc@152
|
63 Inductive hasType : ctx -> exp -> type -> Prop :=
|
adamc@152
|
64 | TConst : forall G b,
|
adamc@152
|
65 G |-e Const b : Bool
|
adamc@152
|
66 | TVar : forall G v t,
|
adamc@152
|
67 G |-v v : t
|
adamc@152
|
68 -> G |-e Var v : t
|
adamc@152
|
69 | TApp : forall G e1 e2 dom ran,
|
adamc@152
|
70 G |-e e1 : dom --> ran
|
adamc@152
|
71 -> G |-e e2 : dom
|
adamc@152
|
72 -> G |-e App e1 e2 : ran
|
adamc@152
|
73 | TAbs : forall G x e' dom ran,
|
adamc@152
|
74 (x, dom) :: G |-e e' : ran
|
adamc@152
|
75 -> G |-e Abs x e' : dom --> ran
|
adamc@152
|
76
|
adamc@152
|
77 where "G |-e e : t" := (hasType G e t).
|
adamc@152
|
78
|
adamc@152
|
79 Hint Constructors hasType.
|
adamc@152
|
80
|
adamc@155
|
81 Lemma weaken_lookup : forall x t G' G1,
|
adamc@155
|
82 G1 |-v x : t
|
adamc@155
|
83 -> G1 ++ G' |-v x : t.
|
adamc@152
|
84 induction G1 as [ | [x' t'] tl ]; crush;
|
adamc@152
|
85 match goal with
|
adamc@152
|
86 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
|
adamc@152
|
87 end.
|
adamc@152
|
88 Qed.
|
adamc@152
|
89
|
adamc@152
|
90 Hint Resolve weaken_lookup.
|
adamc@152
|
91
|
adamc@152
|
92 Theorem weaken_hasType' : forall G' G e t,
|
adamc@152
|
93 G |-e e : t
|
adamc@155
|
94 -> G ++ G' |-e e : t.
|
adamc@152
|
95 induction 1; crush; eauto.
|
adamc@152
|
96 Qed.
|
adamc@152
|
97
|
adamc@155
|
98 Theorem weaken_hasType : forall e t,
|
adamc@155
|
99 nil |-e e : t
|
adamc@155
|
100 -> forall G', G' |-e e : t.
|
adamc@155
|
101 intros; change G' with (nil ++ G');
|
adamc@152
|
102 eapply weaken_hasType'; eauto.
|
adamc@152
|
103 Qed.
|
adamc@152
|
104
|
adamc@152
|
105 Theorem weaken_hasType_closed : forall e t,
|
adamc@152
|
106 nil |-e e : t
|
adamc@152
|
107 -> forall G, G |-e e : t.
|
adamc@152
|
108 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
|
adamc@152
|
109 Qed.
|
adamc@152
|
110
|
adamc@157
|
111 Hint Resolve weaken_hasType_closed.
|
adamc@152
|
112
|
adamc@152
|
113 Section subst.
|
adamc@152
|
114 Variable x : var.
|
adamc@152
|
115 Variable e1 : exp.
|
adamc@152
|
116
|
adamc@152
|
117 Fixpoint subst (e2 : exp) : exp :=
|
adamc@152
|
118 match e2 with
|
adamc@152
|
119 | Const b => Const b
|
adamc@152
|
120 | Var x' =>
|
adamc@152
|
121 if var_eq x' x
|
adamc@152
|
122 then e1
|
adamc@152
|
123 else Var x'
|
adamc@152
|
124 | App e1 e2 => App (subst e1) (subst e2)
|
adamc@152
|
125 | Abs x' e' =>
|
adamc@152
|
126 Abs x' (if var_eq x' x
|
adamc@152
|
127 then e'
|
adamc@152
|
128 else subst e')
|
adamc@152
|
129 end.
|
adamc@152
|
130
|
adamc@152
|
131 Variable xt : type.
|
adamc@152
|
132 Hypothesis Ht' : nil |-e e1 : xt.
|
adamc@152
|
133
|
adamc@157
|
134 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
|
adamc@152
|
135
|
adamc@157
|
136 Lemma subst_lookup' : forall x' t,
|
adamc@152
|
137 x <> x'
|
adamc@155
|
138 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
|
adamc@155
|
139 -> G1 |-v x' : t.
|
adamc@152
|
140 induction G1 as [ | [x'' t'] tl ]; crush;
|
adamc@152
|
141 match goal with
|
adamc@152
|
142 | [ H : _ |-v _ : _ |- _ ] => inversion H
|
adamc@152
|
143 end; crush.
|
adamc@152
|
144 Qed.
|
adamc@152
|
145
|
adamc@157
|
146 Hint Resolve subst_lookup'.
|
adamc@152
|
147
|
adamc@157
|
148 Lemma subst_lookup : forall x' t G1,
|
adamc@157
|
149 x' # G1
|
adamc@155
|
150 -> G1 ++ (x, xt) :: nil |-v x' : t
|
adamc@155
|
151 -> t = xt.
|
adamc@152
|
152 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
|
adamc@152
|
153 match goal with
|
adamc@152
|
154 | [ H : _ |-v _ : _ |- _ ] => inversion H
|
adamc@155
|
155 end; crush; elimtype False; eauto;
|
adamc@155
|
156 match goal with
|
adamc@155
|
157 | [ H : nil |-v _ : _ |- _ ] => inversion H
|
adamc@155
|
158 end.
|
adamc@152
|
159 Qed.
|
adamc@152
|
160
|
adamc@157
|
161 Implicit Arguments subst_lookup [x' t G1].
|
adamc@152
|
162
|
adamc@155
|
163 Lemma shadow_lookup : forall v t t' G1,
|
adamc@152
|
164 G1 |-v x : t'
|
adamc@155
|
165 -> G1 ++ (x, xt) :: nil |-v v : t
|
adamc@155
|
166 -> G1 |-v v : t.
|
adamc@152
|
167 induction G1 as [ | [x'' t''] tl ]; crush;
|
adamc@152
|
168 match goal with
|
adamc@152
|
169 | [ H : nil |-v _ : _ |- _ ] => inversion H
|
adamc@152
|
170 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
|
adamc@152
|
171 inversion H1; crush; inversion H2; crush
|
adamc@152
|
172 end.
|
adamc@152
|
173 Qed.
|
adamc@152
|
174
|
adamc@155
|
175 Lemma shadow_hasType' : forall G e t,
|
adamc@152
|
176 G |-e e : t
|
adamc@155
|
177 -> forall G1, G = G1 ++ (x, xt) :: nil
|
adamc@152
|
178 -> forall t'', G1 |-v x : t''
|
adamc@155
|
179 -> G1 |-e e : t.
|
adamc@152
|
180 Hint Resolve shadow_lookup.
|
adamc@152
|
181
|
adamc@152
|
182 induction 1; crush; eauto;
|
adamc@152
|
183 match goal with
|
adamc@152
|
184 | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
|
adamc@152
|
185 destruct (var_eq x0 x); subst; eauto
|
adamc@152
|
186 end.
|
adamc@155
|
187 Qed.
|
adamc@152
|
188
|
adamc@155
|
189 Lemma shadow_hasType : forall G1 e t t'',
|
adamc@155
|
190 G1 ++ (x, xt) :: nil |-e e : t
|
adamc@152
|
191 -> G1 |-v x : t''
|
adamc@155
|
192 -> G1 |-e e : t.
|
adamc@152
|
193 intros; eapply shadow_hasType'; eauto.
|
adamc@152
|
194 Qed.
|
adamc@152
|
195
|
adamc@152
|
196 Hint Resolve shadow_hasType.
|
adamc@152
|
197
|
adamc@157
|
198 Lemma disjoint_cons : forall x x' t (G : ctx),
|
adamc@157
|
199 x # G
|
adamc@157
|
200 -> x' <> x
|
adamc@157
|
201 -> x # (x', t) :: G.
|
adamc@157
|
202 firstorder;
|
adamc@157
|
203 match goal with
|
adamc@157
|
204 | [ H : (_, _) = (_, _) |- _ ] => injection H
|
adamc@157
|
205 end; crush.
|
adamc@157
|
206 Qed.
|
adamc@157
|
207
|
adamc@157
|
208 Hint Resolve disjoint_cons.
|
adamc@157
|
209
|
adamc@152
|
210 Theorem subst_hasType : forall G e2 t,
|
adamc@152
|
211 G |-e e2 : t
|
adamc@155
|
212 -> forall G1, G = G1 ++ (x, xt) :: nil
|
adamc@157
|
213 -> x # G1
|
adamc@155
|
214 -> G1 |-e subst e2 : t.
|
adamc@152
|
215 induction 1; crush;
|
adamc@152
|
216 try match goal with
|
adamc@152
|
217 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@152
|
218 end; crush; eauto 6;
|
adamc@152
|
219 match goal with
|
adamc@157
|
220 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
|
adamc@157
|
221 rewrite (subst_lookup H1 H2)
|
adamc@152
|
222 end; crush.
|
adamc@152
|
223 Qed.
|
adamc@152
|
224
|
adamc@152
|
225 Theorem subst_hasType_closed : forall e2 t,
|
adamc@152
|
226 (x, xt) :: nil |-e e2 : t
|
adamc@152
|
227 -> nil |-e subst e2 : t.
|
adamc@155
|
228 intros; eapply subst_hasType; eauto.
|
adamc@152
|
229 Qed.
|
adamc@152
|
230 End subst.
|
adamc@152
|
231
|
adamc@154
|
232 Hint Resolve subst_hasType_closed.
|
adamc@154
|
233
|
adamc@154
|
234 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
|
adamc@154
|
235
|
adamc@154
|
236 Inductive val : exp -> Prop :=
|
adamc@154
|
237 | VConst : forall b, val (Const b)
|
adamc@154
|
238 | VAbs : forall x e, val (Abs x e).
|
adamc@154
|
239
|
adamc@154
|
240 Hint Constructors val.
|
adamc@154
|
241
|
adamc@154
|
242 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
|
adamc@154
|
243
|
adamc@154
|
244 Inductive step : exp -> exp -> Prop :=
|
adamc@154
|
245 | Beta : forall x e1 e2,
|
adamc@154
|
246 App (Abs x e1) e2 ==> [x ~> e2] e1
|
adamc@154
|
247 | Cong1 : forall e1 e2 e1',
|
adamc@154
|
248 e1 ==> e1'
|
adamc@154
|
249 -> App e1 e2 ==> App e1' e2
|
adamc@154
|
250 | Cong2 : forall e1 e2 e2',
|
adamc@154
|
251 val e1
|
adamc@154
|
252 -> e2 ==> e2'
|
adamc@154
|
253 -> App e1 e2 ==> App e1 e2'
|
adamc@154
|
254
|
adamc@154
|
255 where "e1 ==> e2" := (step e1 e2).
|
adamc@154
|
256
|
adamc@154
|
257 Hint Constructors step.
|
adamc@154
|
258
|
adamc@155
|
259 Lemma progress' : forall G e t, G |-e e : t
|
adamc@154
|
260 -> G = nil
|
adamc@154
|
261 -> val e \/ exists e', e ==> e'.
|
adamc@154
|
262 induction 1; crush; eauto;
|
adamc@154
|
263 try match goal with
|
adamc@154
|
264 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
|
adamc@154
|
265 end;
|
adamc@154
|
266 repeat match goal with
|
adamc@154
|
267 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
|
adamc@154
|
268 end.
|
adamc@154
|
269 Qed.
|
adamc@154
|
270
|
adamc@155
|
271 Theorem progress : forall e t, nil |-e e : t
|
adamc@155
|
272 -> val e \/ exists e', e ==> e'.
|
adamc@155
|
273 intros; eapply progress'; eauto.
|
adamc@155
|
274 Qed.
|
adamc@155
|
275
|
adamc@155
|
276 Lemma preservation' : forall G e t, G |-e e : t
|
adamc@154
|
277 -> G = nil
|
adamc@154
|
278 -> forall e', e ==> e'
|
adamc@155
|
279 -> nil |-e e' : t.
|
adamc@154
|
280 induction 1; inversion 2; crush; eauto;
|
adamc@154
|
281 match goal with
|
adamc@154
|
282 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
|
adamc@154
|
283 end; eauto.
|
adamc@154
|
284 Qed.
|
adamc@154
|
285
|
adamc@155
|
286 Theorem preservation : forall e t, nil |-e e : t
|
adamc@155
|
287 -> forall e', e ==> e'
|
adamc@155
|
288 -> nil |-e e' : t.
|
adamc@155
|
289 intros; eapply preservation'; eauto.
|
adamc@155
|
290 Qed.
|
adamc@155
|
291
|
adamc@152
|
292 End Concrete.
|
adamc@156
|
293
|
adamc@156
|
294
|
adamc@156
|
295 (** * De Bruijn Indices *)
|
adamc@156
|
296
|
adamc@156
|
297 Module DeBruijn.
|
adamc@156
|
298
|
adamc@156
|
299 Definition var := nat.
|
adamc@156
|
300 Definition var_eq := eq_nat_dec.
|
adamc@156
|
301
|
adamc@156
|
302 Inductive exp : Set :=
|
adamc@156
|
303 | Const : bool -> exp
|
adamc@156
|
304 | Var : var -> exp
|
adamc@156
|
305 | App : exp -> exp -> exp
|
adamc@156
|
306 | Abs : exp -> exp.
|
adamc@156
|
307
|
adamc@156
|
308 Inductive type : Set :=
|
adamc@156
|
309 | Bool : type
|
adamc@156
|
310 | Arrow : type -> type -> type.
|
adamc@156
|
311
|
adamc@156
|
312 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@156
|
313
|
adamc@156
|
314 Definition ctx := list type.
|
adamc@156
|
315
|
adamc@156
|
316 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
|
adamc@156
|
317
|
adamc@156
|
318 Inductive lookup : ctx -> var -> type -> Prop :=
|
adamc@156
|
319 | First : forall t G,
|
adamc@156
|
320 t :: G |-v O : t
|
adamc@156
|
321 | Next : forall x t t' G,
|
adamc@156
|
322 G |-v x : t
|
adamc@156
|
323 -> t' :: G |-v S x : t
|
adamc@156
|
324
|
adamc@156
|
325 where "G |-v x : t" := (lookup G x t).
|
adamc@156
|
326
|
adamc@156
|
327 Hint Constructors lookup.
|
adamc@156
|
328
|
adamc@156
|
329 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
|
adamc@156
|
330
|
adamc@156
|
331 Inductive hasType : ctx -> exp -> type -> Prop :=
|
adamc@156
|
332 | TConst : forall G b,
|
adamc@156
|
333 G |-e Const b : Bool
|
adamc@156
|
334 | TVar : forall G v t,
|
adamc@156
|
335 G |-v v : t
|
adamc@156
|
336 -> G |-e Var v : t
|
adamc@156
|
337 | TApp : forall G e1 e2 dom ran,
|
adamc@156
|
338 G |-e e1 : dom --> ran
|
adamc@156
|
339 -> G |-e e2 : dom
|
adamc@156
|
340 -> G |-e App e1 e2 : ran
|
adamc@156
|
341 | TAbs : forall G e' dom ran,
|
adamc@156
|
342 dom :: G |-e e' : ran
|
adamc@156
|
343 -> G |-e Abs e' : dom --> ran
|
adamc@156
|
344
|
adamc@156
|
345 where "G |-e e : t" := (hasType G e t).
|
adamc@156
|
346
|
adamc@156
|
347 Hint Constructors hasType.
|
adamc@156
|
348
|
adamc@156
|
349 Lemma weaken_lookup : forall G' v t G,
|
adamc@156
|
350 G |-v v : t
|
adamc@156
|
351 -> G ++ G' |-v v : t.
|
adamc@156
|
352 induction 1; crush.
|
adamc@156
|
353 Qed.
|
adamc@156
|
354
|
adamc@156
|
355 Hint Resolve weaken_lookup.
|
adamc@156
|
356
|
adamc@156
|
357 Theorem weaken_hasType' : forall G' G e t,
|
adamc@156
|
358 G |-e e : t
|
adamc@156
|
359 -> G ++ G' |-e e : t.
|
adamc@156
|
360 induction 1; crush; eauto.
|
adamc@156
|
361 Qed.
|
adamc@156
|
362
|
adamc@156
|
363 Theorem weaken_hasType : forall e t,
|
adamc@156
|
364 nil |-e e : t
|
adamc@156
|
365 -> forall G', G' |-e e : t.
|
adamc@156
|
366 intros; change G' with (nil ++ G');
|
adamc@156
|
367 eapply weaken_hasType'; eauto.
|
adamc@156
|
368 Qed.
|
adamc@156
|
369
|
adamc@156
|
370 Theorem weaken_hasType_closed : forall e t,
|
adamc@156
|
371 nil |-e e : t
|
adamc@156
|
372 -> forall G, G |-e e : t.
|
adamc@156
|
373 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
|
adamc@156
|
374 Qed.
|
adamc@156
|
375
|
adamc@157
|
376 Hint Resolve weaken_hasType_closed.
|
adamc@156
|
377
|
adamc@156
|
378 Section subst.
|
adamc@156
|
379 Variable e1 : exp.
|
adamc@156
|
380
|
adamc@156
|
381 Fixpoint subst (x : var) (e2 : exp) : exp :=
|
adamc@156
|
382 match e2 with
|
adamc@156
|
383 | Const b => Const b
|
adamc@156
|
384 | Var x' =>
|
adamc@156
|
385 if var_eq x' x
|
adamc@156
|
386 then e1
|
adamc@156
|
387 else Var x'
|
adamc@156
|
388 | App e1 e2 => App (subst x e1) (subst x e2)
|
adamc@156
|
389 | Abs e' => Abs (subst (S x) e')
|
adamc@156
|
390 end.
|
adamc@156
|
391
|
adamc@156
|
392 Variable xt : type.
|
adamc@156
|
393
|
adamc@156
|
394 Lemma subst_eq : forall t G1,
|
adamc@156
|
395 G1 ++ xt :: nil |-v length G1 : t
|
adamc@156
|
396 -> t = xt.
|
adamc@156
|
397 induction G1; inversion 1; crush.
|
adamc@156
|
398 Qed.
|
adamc@156
|
399
|
adamc@156
|
400 Implicit Arguments subst_eq [t G1].
|
adamc@156
|
401
|
adamc@156
|
402 Lemma subst_eq' : forall t G1 x,
|
adamc@156
|
403 G1 ++ xt :: nil |-v x : t
|
adamc@156
|
404 -> x <> length G1
|
adamc@156
|
405 -> G1 |-v x : t.
|
adamc@156
|
406 induction G1; inversion 1; crush;
|
adamc@156
|
407 match goal with
|
adamc@156
|
408 | [ H : nil |-v _ : _ |- _ ] => inversion H
|
adamc@156
|
409 end.
|
adamc@156
|
410 Qed.
|
adamc@156
|
411
|
adamc@156
|
412 Hint Resolve subst_eq'.
|
adamc@156
|
413
|
adamc@156
|
414 Lemma subst_neq : forall v t G1,
|
adamc@156
|
415 G1 ++ xt :: nil |-v v : t
|
adamc@156
|
416 -> v <> length G1
|
adamc@156
|
417 -> G1 |-e Var v : t.
|
adamc@156
|
418 induction G1; inversion 1; crush.
|
adamc@156
|
419 Qed.
|
adamc@156
|
420
|
adamc@156
|
421 Hint Resolve subst_neq.
|
adamc@156
|
422
|
adamc@156
|
423 Hypothesis Ht' : nil |-e e1 : xt.
|
adamc@156
|
424
|
adamc@156
|
425 Lemma hasType_push : forall dom G1 e' ran,
|
adamc@156
|
426 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
|
adamc@156
|
427 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
|
adamc@156
|
428 trivial.
|
adamc@156
|
429 Qed.
|
adamc@156
|
430
|
adamc@156
|
431 Hint Resolve hasType_push.
|
adamc@156
|
432
|
adamc@156
|
433 Theorem subst_hasType : forall G e2 t,
|
adamc@156
|
434 G |-e e2 : t
|
adamc@156
|
435 -> forall G1, G = G1 ++ xt :: nil
|
adamc@156
|
436 -> G1 |-e subst (length G1) e2 : t.
|
adamc@156
|
437 induction 1; crush;
|
adamc@156
|
438 try match goal with
|
adamc@156
|
439 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@156
|
440 end; crush; eauto 6;
|
adamc@156
|
441 try match goal with
|
adamc@156
|
442 | [ H : _ |-v _ : _ |- _ ] =>
|
adamc@156
|
443 rewrite (subst_eq H)
|
adamc@156
|
444 end; crush.
|
adamc@156
|
445 Qed.
|
adamc@156
|
446
|
adamc@156
|
447 Theorem subst_hasType_closed : forall e2 t,
|
adamc@156
|
448 xt :: nil |-e e2 : t
|
adamc@156
|
449 -> nil |-e subst O e2 : t.
|
adamc@156
|
450 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
|
adamc@156
|
451 Qed.
|
adamc@156
|
452 End subst.
|
adamc@156
|
453
|
adamc@156
|
454 Hint Resolve subst_hasType_closed.
|
adamc@156
|
455
|
adamc@156
|
456 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
|
adamc@156
|
457
|
adamc@156
|
458 Inductive val : exp -> Prop :=
|
adamc@156
|
459 | VConst : forall b, val (Const b)
|
adamc@156
|
460 | VAbs : forall e, val (Abs e).
|
adamc@156
|
461
|
adamc@156
|
462 Hint Constructors val.
|
adamc@156
|
463
|
adamc@156
|
464 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
|
adamc@156
|
465
|
adamc@156
|
466 Inductive step : exp -> exp -> Prop :=
|
adamc@156
|
467 | Beta : forall e1 e2,
|
adamc@156
|
468 App (Abs e1) e2 ==> [O ~> e2] e1
|
adamc@156
|
469 | Cong1 : forall e1 e2 e1',
|
adamc@156
|
470 e1 ==> e1'
|
adamc@156
|
471 -> App e1 e2 ==> App e1' e2
|
adamc@156
|
472 | Cong2 : forall e1 e2 e2',
|
adamc@156
|
473 val e1
|
adamc@156
|
474 -> e2 ==> e2'
|
adamc@156
|
475 -> App e1 e2 ==> App e1 e2'
|
adamc@156
|
476
|
adamc@156
|
477 where "e1 ==> e2" := (step e1 e2).
|
adamc@156
|
478
|
adamc@156
|
479 Hint Constructors step.
|
adamc@156
|
480
|
adamc@156
|
481 Lemma progress' : forall G e t, G |-e e : t
|
adamc@156
|
482 -> G = nil
|
adamc@156
|
483 -> val e \/ exists e', e ==> e'.
|
adamc@156
|
484 induction 1; crush; eauto;
|
adamc@156
|
485 try match goal with
|
adamc@156
|
486 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
|
adamc@156
|
487 end;
|
adamc@156
|
488 repeat match goal with
|
adamc@156
|
489 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
|
adamc@156
|
490 end.
|
adamc@156
|
491 Qed.
|
adamc@156
|
492
|
adamc@156
|
493 Theorem progress : forall e t, nil |-e e : t
|
adamc@156
|
494 -> val e \/ exists e', e ==> e'.
|
adamc@156
|
495 intros; eapply progress'; eauto.
|
adamc@156
|
496 Qed.
|
adamc@156
|
497
|
adamc@156
|
498 Lemma preservation' : forall G e t, G |-e e : t
|
adamc@156
|
499 -> G = nil
|
adamc@156
|
500 -> forall e', e ==> e'
|
adamc@156
|
501 -> nil |-e e' : t.
|
adamc@156
|
502 induction 1; inversion 2; crush; eauto;
|
adamc@156
|
503 match goal with
|
adamc@156
|
504 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
|
adamc@156
|
505 end; eauto.
|
adamc@156
|
506 Qed.
|
adamc@156
|
507
|
adamc@156
|
508 Theorem preservation : forall e t, nil |-e e : t
|
adamc@156
|
509 -> forall e', e ==> e'
|
adamc@156
|
510 -> nil |-e e' : t.
|
adamc@156
|
511 intros; eapply preservation'; eauto.
|
adamc@156
|
512 Qed.
|
adamc@156
|
513
|
adamc@156
|
514 End DeBruijn.
|