adamc@222
|
1 (* Copyright (c) 2008-2009, 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@245
|
23 (** Many people interested in interactive theorem-proving want to prove theorems about programming languages. That domain also provides a good setting for demonstrating how to apply the ideas from the earlier parts of this book. This part introduces some techniques for encoding the syntax and semantics of programming languages, along with some example proofs designed to be as practical as possible, rather than to illustrate basic Coq technique.
|
adamc@245
|
24
|
adamc@245
|
25 To prove anything about a language, we must first formalize the language's syntax. We have a broad design space to choose from, and it makes sense to start with the simplest options, so-called %\textit{%#<i>#first-order#</i>#%}% syntax encodings that do not use dependent types. These encodings are first-order because they do not use Coq function types in a critical way. In this chapter, we consider the most popular first-order encodings, using each to prove a basic type soundness theorem. *)
|
adamc@152
|
26
|
adamc@152
|
27
|
adamc@152
|
28 (** * Concrete Binding *)
|
adamc@152
|
29
|
adamc@245
|
30 (** The most obvious encoding of the syntax of programming languages follows usual context-free grammars literally. We represent variables as strings and include a variable in our AST definition wherever a variable appears in the informal grammar. Concrete binding turns out to involve a surprisingly large amount of menial bookkeeping, especially when we encode higher-order languages with nested binder scopes. This section's example should give a flavor of what is required. *)
|
adamc@245
|
31
|
adamc@152
|
32 Module Concrete.
|
adamc@152
|
33
|
adamc@245
|
34 (** We need our variable type and its decidable equality operation. *)
|
adamc@245
|
35
|
adamc@152
|
36 Definition var := string.
|
adamc@152
|
37 Definition var_eq := string_dec.
|
adamc@152
|
38
|
adamc@245
|
39 (** We will formalize basic simply-typed lambda calculus. The syntax of expressions and types follows what we would write in a context-free grammar. *)
|
adamc@245
|
40
|
adamc@152
|
41 Inductive exp : Set :=
|
adamc@152
|
42 | Const : bool -> exp
|
adamc@152
|
43 | Var : var -> exp
|
adamc@152
|
44 | App : exp -> exp -> exp
|
adamc@152
|
45 | Abs : var -> exp -> exp.
|
adamc@152
|
46
|
adamc@152
|
47 Inductive type : Set :=
|
adamc@152
|
48 | Bool : type
|
adamc@152
|
49 | Arrow : type -> type -> type.
|
adamc@152
|
50
|
adamc@245
|
51 (** It is useful to define a syntax extension that lets us write function types in more standard notation. *)
|
adamc@245
|
52
|
adamc@152
|
53 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@152
|
54
|
adamc@245
|
55 (** Now we turn to a typing judgment. We will need to define it in terms of typing contexts, which we represent as lists of pairs of variables and types. *)
|
adamc@245
|
56
|
adamc@152
|
57 Definition ctx := list (var * type).
|
adamc@152
|
58
|
adamc@245
|
59 (** The definitions of our judgments will be prettier if we write them using mixfix syntax. To define a judgment for looking up the type of a variable in a context, we first %\textit{%#</i>#reserve#</i>#%}% a notation for the judgment. Reserved notations enable mutually-recursive definition of a judgment and its notation; in this sense, the reservation is like a forward declaration in C. *)
|
adamc@245
|
60
|
adamc@152
|
61 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
|
adamc@152
|
62
|
adamc@245
|
63 (** Now we define the judgment itself, using a [where] clause to associate a notation definition. *)
|
adamc@245
|
64
|
adamc@152
|
65 Inductive lookup : ctx -> var -> type -> Prop :=
|
adamc@152
|
66 | First : forall x t G,
|
adamc@152
|
67 (x, t) :: G |-v x : t
|
adamc@152
|
68 | Next : forall x t x' t' G,
|
adamc@152
|
69 x <> x'
|
adamc@152
|
70 -> G |-v x : t
|
adamc@152
|
71 -> (x', t') :: G |-v x : t
|
adamc@152
|
72
|
adamc@152
|
73 where "G |-v x : t" := (lookup G x t).
|
adamc@152
|
74
|
adamc@152
|
75 Hint Constructors lookup.
|
adamc@152
|
76
|
adamc@245
|
77 (** The same technique applies to defining the main typing judgment. We use an [at next level] clause to cause the argument [e] of the notation to be parsed at a low enough precedence level. *)
|
adamc@245
|
78
|
adamc@152
|
79 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
|
adamc@152
|
80
|
adamc@152
|
81 Inductive hasType : ctx -> exp -> type -> Prop :=
|
adamc@152
|
82 | TConst : forall G b,
|
adamc@152
|
83 G |-e Const b : Bool
|
adamc@152
|
84 | TVar : forall G v t,
|
adamc@152
|
85 G |-v v : t
|
adamc@152
|
86 -> G |-e Var v : t
|
adamc@152
|
87 | TApp : forall G e1 e2 dom ran,
|
adamc@152
|
88 G |-e e1 : dom --> ran
|
adamc@152
|
89 -> G |-e e2 : dom
|
adamc@152
|
90 -> G |-e App e1 e2 : ran
|
adamc@152
|
91 | TAbs : forall G x e' dom ran,
|
adamc@152
|
92 (x, dom) :: G |-e e' : ran
|
adamc@152
|
93 -> G |-e Abs x e' : dom --> ran
|
adamc@152
|
94
|
adamc@152
|
95 where "G |-e e : t" := (hasType G e t).
|
adamc@152
|
96
|
adamc@152
|
97 Hint Constructors hasType.
|
adamc@152
|
98
|
adamc@245
|
99 (** It is useful to know that variable lookup results are unchanged by adding extra bindings to the end of a context. *)
|
adamc@245
|
100
|
adamc@155
|
101 Lemma weaken_lookup : forall x t G' G1,
|
adamc@155
|
102 G1 |-v x : t
|
adamc@155
|
103 -> G1 ++ G' |-v x : t.
|
adamc@245
|
104 induction G1 as [ | [? ?] ? ]; crush;
|
adamc@152
|
105 match goal with
|
adamc@152
|
106 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
|
adamc@152
|
107 end.
|
adamc@152
|
108 Qed.
|
adamc@152
|
109
|
adamc@152
|
110 Hint Resolve weaken_lookup.
|
adamc@152
|
111
|
adamc@245
|
112 (** The same property extends to the full typing judgment. *)
|
adamc@245
|
113
|
adamc@152
|
114 Theorem weaken_hasType' : forall G' G e t,
|
adamc@152
|
115 G |-e e : t
|
adamc@155
|
116 -> G ++ G' |-e e : t.
|
adamc@152
|
117 induction 1; crush; eauto.
|
adamc@152
|
118 Qed.
|
adamc@152
|
119
|
adamc@155
|
120 Theorem weaken_hasType : forall e t,
|
adamc@155
|
121 nil |-e e : t
|
adamc@155
|
122 -> forall G', G' |-e e : t.
|
adamc@155
|
123 intros; change G' with (nil ++ G');
|
adamc@152
|
124 eapply weaken_hasType'; eauto.
|
adamc@152
|
125 Qed.
|
adamc@152
|
126
|
adamc@161
|
127 Hint Resolve weaken_hasType.
|
adamc@152
|
128
|
adamc@245
|
129 (** Much of the inconvenience of first-order encodings comes from the need to treat capture-avoiding substitution explicitly. We must start by defining a substitution function. *)
|
adamc@245
|
130
|
adamc@152
|
131 Section subst.
|
adamc@152
|
132 Variable x : var.
|
adamc@152
|
133 Variable e1 : exp.
|
adamc@152
|
134
|
adamc@245
|
135 (** We are substituting expression [e1] for every free occurrence of [x]. Note that this definition is specialized to the case where [e1] is closed; substitution is substantially more complicated otherwise, potentially involving explicit alpha-variation. Luckily, our example of type safety for a call-by-value semantics only requires this restricted variety of substitution. *)
|
adamc@245
|
136
|
adamc@152
|
137 Fixpoint subst (e2 : exp) : exp :=
|
adamc@152
|
138 match e2 with
|
adamc@246
|
139 | Const _ => e2
|
adamc@246
|
140 | Var x' => if var_eq x' x then e1 else e2
|
adamc@152
|
141 | App e1 e2 => App (subst e1) (subst e2)
|
adamc@246
|
142 | Abs x' e' => Abs x' (if var_eq x' x then e' else subst e')
|
adamc@152
|
143 end.
|
adamc@152
|
144
|
adamc@245
|
145 (** We can prove a few theorems about substitution in well-typed terms, where we assume that [e1] is closed and has type [xt]. *)
|
adamc@245
|
146
|
adamc@152
|
147 Variable xt : type.
|
adamc@152
|
148 Hypothesis Ht' : nil |-e e1 : xt.
|
adamc@152
|
149
|
adamc@245
|
150 (** It is helpful to establish a notation asserting the freshness of a particular variable in a context. *)
|
adamc@245
|
151
|
adamc@157
|
152 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
|
adamc@152
|
153
|
adamc@245
|
154 (** To prove type preservation, we will need lemmas proving consequences of variable lookup proofs. *)
|
adamc@245
|
155
|
adamc@157
|
156 Lemma subst_lookup' : forall x' t,
|
adamc@152
|
157 x <> x'
|
adamc@155
|
158 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
|
adamc@155
|
159 -> G1 |-v x' : t.
|
adamc@245
|
160 induction G1 as [ | [? ?] ? ]; crush;
|
adamc@152
|
161 match goal with
|
adamc@152
|
162 | [ H : _ |-v _ : _ |- _ ] => inversion H
|
adamc@152
|
163 end; crush.
|
adamc@152
|
164 Qed.
|
adamc@152
|
165
|
adamc@157
|
166 Hint Resolve subst_lookup'.
|
adamc@152
|
167
|
adamc@157
|
168 Lemma subst_lookup : forall x' t G1,
|
adamc@157
|
169 x' # G1
|
adamc@155
|
170 -> G1 ++ (x, xt) :: nil |-v x' : t
|
adamc@155
|
171 -> t = xt.
|
adamc@245
|
172 induction G1 as [ | [? ?] ? ]; crush; eauto;
|
adamc@152
|
173 match goal with
|
adamc@152
|
174 | [ H : _ |-v _ : _ |- _ ] => inversion H
|
adamc@183
|
175 end; crush; (elimtype False; eauto;
|
adamc@183
|
176 match goal with
|
adamc@183
|
177 | [ H : nil |-v _ : _ |- _ ] => inversion H
|
adamc@183
|
178 end)
|
adamc@183
|
179 || match goal with
|
adamc@183
|
180 | [ H : _ |- _ ] => apply H; crush; eauto
|
adamc@183
|
181 end.
|
adamc@152
|
182 Qed.
|
adamc@152
|
183
|
adamc@157
|
184 Implicit Arguments subst_lookup [x' t G1].
|
adamc@152
|
185
|
adamc@245
|
186 (** Another set of lemmas allows us to remove provably unused variables from the ends of typing contexts. *)
|
adamc@245
|
187
|
adamc@155
|
188 Lemma shadow_lookup : forall v t t' G1,
|
adamc@152
|
189 G1 |-v x : t'
|
adamc@155
|
190 -> G1 ++ (x, xt) :: nil |-v v : t
|
adamc@155
|
191 -> G1 |-v v : t.
|
adamc@245
|
192 induction G1 as [ | [? ?] ? ]; crush;
|
adamc@152
|
193 match goal with
|
adamc@152
|
194 | [ H : nil |-v _ : _ |- _ ] => inversion H
|
adamc@152
|
195 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
|
adamc@152
|
196 inversion H1; crush; inversion H2; crush
|
adamc@152
|
197 end.
|
adamc@152
|
198 Qed.
|
adamc@152
|
199
|
adamc@155
|
200 Lemma shadow_hasType' : forall G e t,
|
adamc@152
|
201 G |-e e : t
|
adamc@155
|
202 -> forall G1, G = G1 ++ (x, xt) :: nil
|
adamc@152
|
203 -> forall t'', G1 |-v x : t''
|
adamc@155
|
204 -> G1 |-e e : t.
|
adamc@152
|
205 Hint Resolve shadow_lookup.
|
adamc@152
|
206
|
adamc@152
|
207 induction 1; crush; eauto;
|
adamc@152
|
208 match goal with
|
adamc@245
|
209 | [ H : (?x0, _) :: _ ++ (?x, _) :: _ |-e _ : _ |- _ ] =>
|
adamc@152
|
210 destruct (var_eq x0 x); subst; eauto
|
adamc@152
|
211 end.
|
adamc@155
|
212 Qed.
|
adamc@152
|
213
|
adamc@155
|
214 Lemma shadow_hasType : forall G1 e t t'',
|
adamc@155
|
215 G1 ++ (x, xt) :: nil |-e e : t
|
adamc@152
|
216 -> G1 |-v x : t''
|
adamc@155
|
217 -> G1 |-e e : t.
|
adamc@152
|
218 intros; eapply shadow_hasType'; eauto.
|
adamc@152
|
219 Qed.
|
adamc@152
|
220
|
adamc@152
|
221 Hint Resolve shadow_hasType.
|
adamc@152
|
222
|
adamc@245
|
223 (** Disjointness facts may be extended to larger contexts when the appropriate obligations are met. *)
|
adamc@245
|
224
|
adamc@157
|
225 Lemma disjoint_cons : forall x x' t (G : ctx),
|
adamc@157
|
226 x # G
|
adamc@157
|
227 -> x' <> x
|
adamc@157
|
228 -> x # (x', t) :: G.
|
adamc@157
|
229 firstorder;
|
adamc@157
|
230 match goal with
|
adamc@157
|
231 | [ H : (_, _) = (_, _) |- _ ] => injection H
|
adamc@157
|
232 end; crush.
|
adamc@157
|
233 Qed.
|
adamc@157
|
234
|
adamc@157
|
235 Hint Resolve disjoint_cons.
|
adamc@157
|
236
|
adamc@245
|
237 (** Finally, we arrive at the main theorem about substitution: it preserves typing. *)
|
adamc@245
|
238
|
adamc@152
|
239 Theorem subst_hasType : forall G e2 t,
|
adamc@152
|
240 G |-e e2 : t
|
adamc@155
|
241 -> forall G1, G = G1 ++ (x, xt) :: nil
|
adamc@157
|
242 -> x # G1
|
adamc@155
|
243 -> G1 |-e subst e2 : t.
|
adamc@152
|
244 induction 1; crush;
|
adamc@152
|
245 try match goal with
|
adamc@152
|
246 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@152
|
247 end; crush; eauto 6;
|
adamc@152
|
248 match goal with
|
adamc@157
|
249 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
|
adamc@157
|
250 rewrite (subst_lookup H1 H2)
|
adamc@152
|
251 end; crush.
|
adamc@152
|
252 Qed.
|
adamc@152
|
253
|
adamc@245
|
254 (** We wrap the last theorem into an easier-to-apply form specialized to closed expressions. *)
|
adamc@245
|
255
|
adamc@152
|
256 Theorem subst_hasType_closed : forall e2 t,
|
adamc@152
|
257 (x, xt) :: nil |-e e2 : t
|
adamc@152
|
258 -> nil |-e subst e2 : t.
|
adamc@155
|
259 intros; eapply subst_hasType; eauto.
|
adamc@152
|
260 Qed.
|
adamc@152
|
261 End subst.
|
adamc@152
|
262
|
adamc@154
|
263 Hint Resolve subst_hasType_closed.
|
adamc@154
|
264
|
adamc@245
|
265 (** A notation for substitution will make the operational semantics easier to read. *)
|
adamc@245
|
266
|
adamc@154
|
267 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
|
adamc@154
|
268
|
adamc@245
|
269 (** To define a call-by-value small-step semantics, we rely on a standard judgment characterizing which expressions are values. *)
|
adamc@245
|
270
|
adamc@154
|
271 Inductive val : exp -> Prop :=
|
adamc@154
|
272 | VConst : forall b, val (Const b)
|
adamc@154
|
273 | VAbs : forall x e, val (Abs x e).
|
adamc@154
|
274
|
adamc@154
|
275 Hint Constructors val.
|
adamc@154
|
276
|
adamc@245
|
277 (** Now the step relation is easy to define. *)
|
adamc@245
|
278
|
adamc@154
|
279 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
|
adamc@154
|
280
|
adamc@154
|
281 Inductive step : exp -> exp -> Prop :=
|
adamc@154
|
282 | Beta : forall x e1 e2,
|
adamc@161
|
283 val e2
|
adamc@161
|
284 -> App (Abs x e1) e2 ==> [x ~> e2] e1
|
adamc@154
|
285 | Cong1 : forall e1 e2 e1',
|
adamc@154
|
286 e1 ==> e1'
|
adamc@154
|
287 -> App e1 e2 ==> App e1' e2
|
adamc@154
|
288 | Cong2 : forall e1 e2 e2',
|
adamc@154
|
289 val e1
|
adamc@154
|
290 -> e2 ==> e2'
|
adamc@154
|
291 -> App e1 e2 ==> App e1 e2'
|
adamc@154
|
292
|
adamc@154
|
293 where "e1 ==> e2" := (step e1 e2).
|
adamc@154
|
294
|
adamc@154
|
295 Hint Constructors step.
|
adamc@154
|
296
|
adamc@245
|
297 (** The progress theorem says that any well-typed expression can take a step. To deal with limitations of the [induction] tactic, we put most of the proof in a lemma whose statement uses the usual trick of introducing extra equality hypotheses. *)
|
adamc@245
|
298
|
adamc@155
|
299 Lemma progress' : forall G e t, G |-e e : t
|
adamc@154
|
300 -> G = nil
|
adamc@154
|
301 -> val e \/ exists e', e ==> e'.
|
adamc@154
|
302 induction 1; crush; eauto;
|
adamc@154
|
303 try match goal with
|
adamc@154
|
304 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
|
adamc@154
|
305 end;
|
adamc@245
|
306 match goal with
|
adamc@245
|
307 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
|
adamc@245
|
308 end.
|
adamc@154
|
309 Qed.
|
adamc@154
|
310
|
adamc@155
|
311 Theorem progress : forall e t, nil |-e e : t
|
adamc@155
|
312 -> val e \/ exists e', e ==> e'.
|
adamc@155
|
313 intros; eapply progress'; eauto.
|
adamc@155
|
314 Qed.
|
adamc@155
|
315
|
adamc@245
|
316 (** A similar pattern works for the preservation theorem, which says that any step of execution preserves an expression's type. *)
|
adamc@245
|
317
|
adamc@155
|
318 Lemma preservation' : forall G e t, G |-e e : t
|
adamc@154
|
319 -> G = nil
|
adamc@154
|
320 -> forall e', e ==> e'
|
adamc@155
|
321 -> nil |-e e' : t.
|
adamc@154
|
322 induction 1; inversion 2; crush; eauto;
|
adamc@154
|
323 match goal with
|
adamc@154
|
324 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
|
adamc@154
|
325 end; eauto.
|
adamc@154
|
326 Qed.
|
adamc@154
|
327
|
adamc@155
|
328 Theorem preservation : forall e t, nil |-e e : t
|
adamc@155
|
329 -> forall e', e ==> e'
|
adamc@155
|
330 -> nil |-e e' : t.
|
adamc@155
|
331 intros; eapply preservation'; eauto.
|
adamc@155
|
332 Qed.
|
adamc@155
|
333
|
adamc@152
|
334 End Concrete.
|
adamc@156
|
335
|
adamc@245
|
336 (** This was a relatively simple example, giving only a taste of the proof burden associated with concrete syntax. We were helped by the fact that, with call-by-value semantics, we only need to reason about substitution in closed expressions. There was also no need to alpha-vary an expression. *)
|
adamc@245
|
337
|
adamc@156
|
338
|
adamc@156
|
339 (** * De Bruijn Indices *)
|
adamc@156
|
340
|
adamc@245
|
341 (** De Bruijn indices are much more popular than concrete syntax. This technique provides a %\textit{%#<i>#canonical#</i>#%}% representation of syntax, where any two alpha-equivalent expressions have syntactically equal encodings, removing the need for explicit reasoning about alpha conversion. Variables are represented as natural numbers, where variable [n] denotes a reference to the [n]th closest enclosing binder. Because variable references in effect point to binders, there is no need to label binders, such as function abstraction, with variables. *)
|
adamc@245
|
342
|
adamc@156
|
343 Module DeBruijn.
|
adamc@156
|
344
|
adamc@156
|
345 Definition var := nat.
|
adamc@156
|
346 Definition var_eq := eq_nat_dec.
|
adamc@156
|
347
|
adamc@156
|
348 Inductive exp : Set :=
|
adamc@156
|
349 | Const : bool -> exp
|
adamc@156
|
350 | Var : var -> exp
|
adamc@156
|
351 | App : exp -> exp -> exp
|
adamc@156
|
352 | Abs : exp -> exp.
|
adamc@156
|
353
|
adamc@156
|
354 Inductive type : Set :=
|
adamc@156
|
355 | Bool : type
|
adamc@156
|
356 | Arrow : type -> type -> type.
|
adamc@156
|
357
|
adamc@156
|
358 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@156
|
359
|
adamc@245
|
360 (** The definition of typing proceeds much the same as in the last section. Since variables are numbers, contexts can be simple lists of types. This makes it possible to write the lookup judgment without mentioning inequality of variables. *)
|
adamc@245
|
361
|
adamc@156
|
362 Definition ctx := list type.
|
adamc@156
|
363
|
adamc@156
|
364 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
|
adamc@156
|
365
|
adamc@156
|
366 Inductive lookup : ctx -> var -> type -> Prop :=
|
adamc@156
|
367 | First : forall t G,
|
adamc@156
|
368 t :: G |-v O : t
|
adamc@156
|
369 | Next : forall x t t' G,
|
adamc@156
|
370 G |-v x : t
|
adamc@156
|
371 -> t' :: G |-v S x : t
|
adamc@156
|
372
|
adamc@156
|
373 where "G |-v x : t" := (lookup G x t).
|
adamc@156
|
374
|
adamc@156
|
375 Hint Constructors lookup.
|
adamc@156
|
376
|
adamc@156
|
377 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
|
adamc@156
|
378
|
adamc@156
|
379 Inductive hasType : ctx -> exp -> type -> Prop :=
|
adamc@156
|
380 | TConst : forall G b,
|
adamc@156
|
381 G |-e Const b : Bool
|
adamc@156
|
382 | TVar : forall G v t,
|
adamc@156
|
383 G |-v v : t
|
adamc@156
|
384 -> G |-e Var v : t
|
adamc@156
|
385 | TApp : forall G e1 e2 dom ran,
|
adamc@156
|
386 G |-e e1 : dom --> ran
|
adamc@156
|
387 -> G |-e e2 : dom
|
adamc@156
|
388 -> G |-e App e1 e2 : ran
|
adamc@156
|
389 | TAbs : forall G e' dom ran,
|
adamc@156
|
390 dom :: G |-e e' : ran
|
adamc@156
|
391 -> G |-e Abs e' : dom --> ran
|
adamc@156
|
392
|
adamc@156
|
393 where "G |-e e : t" := (hasType G e t).
|
adamc@156
|
394
|
adamc@245
|
395 (** In the [hasType] case for function abstraction, there is no need to choose a variable name. We simply push the function domain type onto the context [G]. *)
|
adamc@245
|
396
|
adamc@156
|
397 Hint Constructors hasType.
|
adamc@156
|
398
|
adamc@245
|
399 (** We prove roughly the same weakening theorems as before. *)
|
adamc@245
|
400
|
adamc@156
|
401 Lemma weaken_lookup : forall G' v t G,
|
adamc@156
|
402 G |-v v : t
|
adamc@156
|
403 -> G ++ G' |-v v : t.
|
adamc@156
|
404 induction 1; crush.
|
adamc@156
|
405 Qed.
|
adamc@156
|
406
|
adamc@156
|
407 Hint Resolve weaken_lookup.
|
adamc@156
|
408
|
adamc@156
|
409 Theorem weaken_hasType' : forall G' G e t,
|
adamc@156
|
410 G |-e e : t
|
adamc@156
|
411 -> G ++ G' |-e e : t.
|
adamc@156
|
412 induction 1; crush; eauto.
|
adamc@156
|
413 Qed.
|
adamc@156
|
414
|
adamc@156
|
415 Theorem weaken_hasType : forall e t,
|
adamc@156
|
416 nil |-e e : t
|
adamc@156
|
417 -> forall G', G' |-e e : t.
|
adamc@156
|
418 intros; change G' with (nil ++ G');
|
adamc@156
|
419 eapply weaken_hasType'; eauto.
|
adamc@156
|
420 Qed.
|
adamc@156
|
421
|
adamc@161
|
422 Hint Resolve weaken_hasType.
|
adamc@156
|
423
|
adamc@156
|
424 Section subst.
|
adamc@156
|
425 Variable e1 : exp.
|
adamc@156
|
426
|
adamc@245
|
427 (** Substitution is easier to define than with concrete syntax. While our old definition needed to use two comparisons for equality of variables, the de Bruijn substitution only needs one comparison. *)
|
adamc@245
|
428
|
adamc@156
|
429 Fixpoint subst (x : var) (e2 : exp) : exp :=
|
adamc@156
|
430 match e2 with
|
adamc@246
|
431 | Const _ => e2
|
adamc@246
|
432 | Var x' => if var_eq x' x then e1 else e2
|
adamc@156
|
433 | App e1 e2 => App (subst x e1) (subst x e2)
|
adamc@156
|
434 | Abs e' => Abs (subst (S x) e')
|
adamc@156
|
435 end.
|
adamc@156
|
436
|
adamc@156
|
437 Variable xt : type.
|
adamc@156
|
438
|
adamc@245
|
439 (** We prove similar theorems about inversion of variable lookup. *)
|
adamc@245
|
440
|
adamc@156
|
441 Lemma subst_eq : forall t G1,
|
adamc@156
|
442 G1 ++ xt :: nil |-v length G1 : t
|
adamc@156
|
443 -> t = xt.
|
adamc@156
|
444 induction G1; inversion 1; crush.
|
adamc@156
|
445 Qed.
|
adamc@156
|
446
|
adamc@156
|
447 Implicit Arguments subst_eq [t G1].
|
adamc@156
|
448
|
adamc@156
|
449 Lemma subst_eq' : forall t G1 x,
|
adamc@156
|
450 G1 ++ xt :: nil |-v x : t
|
adamc@156
|
451 -> x <> length G1
|
adamc@156
|
452 -> G1 |-v x : t.
|
adamc@156
|
453 induction G1; inversion 1; crush;
|
adamc@156
|
454 match goal with
|
adamc@156
|
455 | [ H : nil |-v _ : _ |- _ ] => inversion H
|
adamc@156
|
456 end.
|
adamc@156
|
457 Qed.
|
adamc@156
|
458
|
adamc@156
|
459 Hint Resolve subst_eq'.
|
adamc@156
|
460
|
adamc@156
|
461 Lemma subst_neq : forall v t G1,
|
adamc@156
|
462 G1 ++ xt :: nil |-v v : t
|
adamc@156
|
463 -> v <> length G1
|
adamc@156
|
464 -> G1 |-e Var v : t.
|
adamc@156
|
465 induction G1; inversion 1; crush.
|
adamc@156
|
466 Qed.
|
adamc@156
|
467
|
adamc@156
|
468 Hint Resolve subst_neq.
|
adamc@156
|
469
|
adamc@156
|
470 Hypothesis Ht' : nil |-e e1 : xt.
|
adamc@156
|
471
|
adamc@245
|
472 (** The next lemma is included solely to guide [eauto], which will not apply computational equivalences automatically. *)
|
adamc@245
|
473
|
adamc@156
|
474 Lemma hasType_push : forall dom G1 e' ran,
|
adamc@156
|
475 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
|
adamc@156
|
476 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
|
adamc@156
|
477 trivial.
|
adamc@156
|
478 Qed.
|
adamc@156
|
479
|
adamc@156
|
480 Hint Resolve hasType_push.
|
adamc@156
|
481
|
adamc@245
|
482 (** Finally, we are ready for the main theorem about substitution and typing. *)
|
adamc@245
|
483
|
adamc@156
|
484 Theorem subst_hasType : forall G e2 t,
|
adamc@156
|
485 G |-e e2 : t
|
adamc@156
|
486 -> forall G1, G = G1 ++ xt :: nil
|
adamc@156
|
487 -> G1 |-e subst (length G1) e2 : t.
|
adamc@156
|
488 induction 1; crush;
|
adamc@156
|
489 try match goal with
|
adamc@156
|
490 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@156
|
491 end; crush; eauto 6;
|
adamc@156
|
492 try match goal with
|
adamc@156
|
493 | [ H : _ |-v _ : _ |- _ ] =>
|
adamc@156
|
494 rewrite (subst_eq H)
|
adamc@156
|
495 end; crush.
|
adamc@156
|
496 Qed.
|
adamc@156
|
497
|
adamc@156
|
498 Theorem subst_hasType_closed : forall e2 t,
|
adamc@156
|
499 xt :: nil |-e e2 : t
|
adamc@156
|
500 -> nil |-e subst O e2 : t.
|
adamc@156
|
501 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
|
adamc@156
|
502 Qed.
|
adamc@156
|
503 End subst.
|
adamc@156
|
504
|
adamc@156
|
505 Hint Resolve subst_hasType_closed.
|
adamc@156
|
506
|
adamc@245
|
507 (** We define the operational semantics much as before. *)
|
adamc@245
|
508
|
adamc@156
|
509 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
|
adamc@156
|
510
|
adamc@156
|
511 Inductive val : exp -> Prop :=
|
adamc@156
|
512 | VConst : forall b, val (Const b)
|
adamc@156
|
513 | VAbs : forall e, val (Abs e).
|
adamc@156
|
514
|
adamc@156
|
515 Hint Constructors val.
|
adamc@156
|
516
|
adamc@156
|
517 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
|
adamc@156
|
518
|
adamc@156
|
519 Inductive step : exp -> exp -> Prop :=
|
adamc@156
|
520 | Beta : forall e1 e2,
|
adamc@161
|
521 val e2
|
adamc@161
|
522 -> App (Abs e1) e2 ==> [O ~> e2] e1
|
adamc@156
|
523 | Cong1 : forall e1 e2 e1',
|
adamc@156
|
524 e1 ==> e1'
|
adamc@156
|
525 -> App e1 e2 ==> App e1' e2
|
adamc@156
|
526 | Cong2 : forall e1 e2 e2',
|
adamc@156
|
527 val e1
|
adamc@156
|
528 -> e2 ==> e2'
|
adamc@156
|
529 -> App e1 e2 ==> App e1 e2'
|
adamc@156
|
530
|
adamc@156
|
531 where "e1 ==> e2" := (step e1 e2).
|
adamc@156
|
532
|
adamc@156
|
533 Hint Constructors step.
|
adamc@156
|
534
|
adamc@245
|
535 (** Since we have added the right hints, the progress and preservation theorem statements and proofs are exactly the same as in the concrete encoding example. *)
|
adamc@245
|
536
|
adamc@156
|
537 Lemma progress' : forall G e t, G |-e e : t
|
adamc@156
|
538 -> G = nil
|
adamc@156
|
539 -> val e \/ exists e', e ==> e'.
|
adamc@156
|
540 induction 1; crush; eauto;
|
adamc@156
|
541 try match goal with
|
adamc@156
|
542 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
|
adamc@156
|
543 end;
|
adamc@156
|
544 repeat match goal with
|
adamc@156
|
545 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
|
adamc@156
|
546 end.
|
adamc@156
|
547 Qed.
|
adamc@156
|
548
|
adamc@156
|
549 Theorem progress : forall e t, nil |-e e : t
|
adamc@156
|
550 -> val e \/ exists e', e ==> e'.
|
adamc@156
|
551 intros; eapply progress'; eauto.
|
adamc@156
|
552 Qed.
|
adamc@156
|
553
|
adamc@156
|
554 Lemma preservation' : forall G e t, G |-e e : t
|
adamc@156
|
555 -> G = nil
|
adamc@156
|
556 -> forall e', e ==> e'
|
adamc@156
|
557 -> nil |-e e' : t.
|
adamc@156
|
558 induction 1; inversion 2; crush; eauto;
|
adamc@156
|
559 match goal with
|
adamc@156
|
560 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
|
adamc@156
|
561 end; eauto.
|
adamc@156
|
562 Qed.
|
adamc@156
|
563
|
adamc@156
|
564 Theorem preservation : forall e t, nil |-e e : t
|
adamc@156
|
565 -> forall e', e ==> e'
|
adamc@156
|
566 -> nil |-e e' : t.
|
adamc@156
|
567 intros; eapply preservation'; eauto.
|
adamc@156
|
568 Qed.
|
adamc@156
|
569
|
adamc@156
|
570 End DeBruijn.
|
adamc@246
|
571
|
adamc@246
|
572
|
adamc@246
|
573 (** * Locally Nameless Syntax *)
|
adamc@246
|
574
|
adamc@246
|
575 Module LocallyNameless.
|
adamc@246
|
576
|
adamc@246
|
577 Definition free_var := string.
|
adamc@246
|
578 Definition bound_var := nat.
|
adamc@246
|
579
|
adamc@246
|
580 Inductive exp : Set :=
|
adamc@246
|
581 | Const : bool -> exp
|
adamc@246
|
582 | FreeVar : free_var -> exp
|
adamc@246
|
583 | BoundVar : bound_var -> exp
|
adamc@246
|
584 | App : exp -> exp -> exp
|
adamc@246
|
585 | Abs : exp -> exp.
|
adamc@246
|
586
|
adamc@246
|
587 Inductive type : Set :=
|
adamc@246
|
588 | Bool : type
|
adamc@246
|
589 | Arrow : type -> type -> type.
|
adamc@246
|
590
|
adamc@246
|
591 Infix "-->" := Arrow (right associativity, at level 60).
|
adamc@246
|
592
|
adamc@246
|
593 Definition ctx := list (free_var * type).
|
adamc@246
|
594
|
adamc@246
|
595 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
|
adamc@246
|
596
|
adamc@246
|
597 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
|
adamc@246
|
598
|
adamc@246
|
599 Inductive lookup : ctx -> free_var -> type -> Prop :=
|
adamc@246
|
600 | First : forall x t G,
|
adamc@246
|
601 (x, t) :: G |-v x : t
|
adamc@246
|
602 | Next : forall x t x' t' G,
|
adamc@246
|
603 x <> x'
|
adamc@246
|
604 -> G |-v x : t
|
adamc@246
|
605 -> (x', t') :: G |-v x : t
|
adamc@246
|
606
|
adamc@246
|
607 where "G |-v x : t" := (lookup G x t).
|
adamc@246
|
608
|
adamc@246
|
609 Hint Constructors lookup.
|
adamc@246
|
610
|
adamc@246
|
611 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
|
adamc@246
|
612
|
adamc@246
|
613 Section open.
|
adamc@246
|
614 Variable x : free_var.
|
adamc@246
|
615
|
adamc@246
|
616 Fixpoint open (n : bound_var) (e : exp) : exp :=
|
adamc@246
|
617 match e with
|
adamc@246
|
618 | Const _ => e
|
adamc@246
|
619 | FreeVar _ => e
|
adamc@246
|
620 | BoundVar n' =>
|
adamc@246
|
621 if eq_nat_dec n' n
|
adamc@246
|
622 then FreeVar x
|
adamc@246
|
623 else if le_lt_dec n' n
|
adamc@246
|
624 then e
|
adamc@246
|
625 else BoundVar (pred n')
|
adamc@246
|
626 | App e1 e2 => App (open n e1) (open n e2)
|
adamc@246
|
627 | Abs e1 => Abs (open (S n) e1)
|
adamc@246
|
628 end.
|
adamc@246
|
629 End open.
|
adamc@246
|
630
|
adamc@247
|
631 Fixpoint freeVars (e : exp) : list free_var :=
|
adamc@247
|
632 match e with
|
adamc@247
|
633 | Const _ => nil
|
adamc@247
|
634 | FreeVar x => x :: nil
|
adamc@247
|
635 | BoundVar _ => nil
|
adamc@247
|
636 | App e1 e2 => freeVars e1 ++ freeVars e2
|
adamc@247
|
637 | Abs e1 => freeVars e1
|
adamc@247
|
638 end.
|
adamc@246
|
639
|
adamc@246
|
640 Inductive hasType : ctx -> exp -> type -> Prop :=
|
adamc@246
|
641 | TConst : forall G b,
|
adamc@246
|
642 G |-e Const b : Bool
|
adamc@246
|
643 | TFreeVar : forall G v t,
|
adamc@246
|
644 G |-v v : t
|
adamc@246
|
645 -> G |-e FreeVar v : t
|
adamc@246
|
646 | TApp : forall G e1 e2 dom ran,
|
adamc@246
|
647 G |-e e1 : dom --> ran
|
adamc@246
|
648 -> G |-e e2 : dom
|
adamc@246
|
649 -> G |-e App e1 e2 : ran
|
adamc@247
|
650 | TAbs : forall G e' dom ran L,
|
adamc@247
|
651 (forall x, ~In x L -> (x, dom) :: G |-e open x O e' : ran)
|
adamc@246
|
652 -> G |-e Abs e' : dom --> ran
|
adamc@246
|
653
|
adamc@246
|
654 where "G |-e e : t" := (hasType G e t).
|
adamc@246
|
655
|
adamc@246
|
656 Hint Constructors hasType.
|
adamc@246
|
657
|
adamc@247
|
658 Lemma lookup_push : forall G G' x t x' t',
|
adamc@247
|
659 (forall x t, G |-v x : t -> G' |-v x : t)
|
adamc@247
|
660 -> (x, t) :: G |-v x' : t'
|
adamc@247
|
661 -> (x, t) :: G' |-v x' : t'.
|
adamc@247
|
662 inversion 2; crush.
|
adamc@247
|
663 Qed.
|
adamc@246
|
664
|
adamc@247
|
665 Hint Resolve lookup_push.
|
adamc@247
|
666
|
adamc@247
|
667 Theorem weaken_hasType : forall G e t,
|
adamc@247
|
668 G |-e e : t
|
adamc@247
|
669 -> forall G', (forall x t, G |-v x : t -> G' |-v x : t)
|
adamc@247
|
670 -> G' |-e e : t.
|
adamc@247
|
671 induction 1; crush; eauto.
|
adamc@247
|
672 Qed.
|
adamc@247
|
673
|
adamc@247
|
674 Hint Resolve weaken_hasType.
|
adamc@247
|
675
|
adamc@247
|
676 Inductive lclosed : nat -> exp -> Prop :=
|
adamc@247
|
677 | CConst : forall n b, lclosed n (Const b)
|
adamc@247
|
678 | CFreeVar : forall n v, lclosed n (FreeVar v)
|
adamc@247
|
679 | CBoundVar : forall n v, v < n -> lclosed n (BoundVar v)
|
adamc@247
|
680 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2)
|
adamc@247
|
681 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1).
|
adamc@247
|
682
|
adamc@247
|
683 Hint Constructors lclosed.
|
adamc@247
|
684
|
adamc@248
|
685 Ltac ln := crush;
|
adamc@248
|
686 repeat (match goal with
|
adamc@248
|
687 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@248
|
688 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
|
adamc@248
|
689 end; crush); eauto.
|
adamc@248
|
690
|
adamc@247
|
691 Lemma lclosed_S : forall x e n,
|
adamc@247
|
692 lclosed n (open x n e)
|
adamc@247
|
693 -> lclosed (S n) e.
|
adamc@248
|
694 induction e; inversion 1; ln.
|
adamc@247
|
695 Qed.
|
adamc@247
|
696
|
adamc@247
|
697 Hint Resolve lclosed_S.
|
adamc@247
|
698
|
adamc@247
|
699 Lemma lclosed_weaken : forall n e,
|
adamc@247
|
700 lclosed n e
|
adamc@247
|
701 -> forall n', n' >= n
|
adamc@247
|
702 -> lclosed n' e.
|
adamc@246
|
703 induction 1; crush.
|
adamc@246
|
704 Qed.
|
adamc@246
|
705
|
adamc@247
|
706 Hint Resolve lclosed_weaken.
|
adamc@247
|
707 Hint Extern 1 (_ >= _) => omega.
|
adamc@246
|
708
|
adamc@247
|
709 Open Scope string_scope.
|
adamc@247
|
710
|
adamc@247
|
711 Fixpoint primes (n : nat) : string :=
|
adamc@247
|
712 match n with
|
adamc@247
|
713 | O => "x"
|
adamc@247
|
714 | S n' => primes n' ++ "'"
|
adamc@247
|
715 end.
|
adamc@247
|
716
|
adamc@247
|
717 Fixpoint sumLengths (L : list free_var) : nat :=
|
adamc@247
|
718 match L with
|
adamc@247
|
719 | nil => O
|
adamc@247
|
720 | x :: L' => String.length x + sumLengths L'
|
adamc@247
|
721 end.
|
adamc@248
|
722
|
adamc@247
|
723 Definition fresh (L : list free_var) := primes (sumLengths L).
|
adamc@247
|
724
|
adamc@247
|
725 Theorem freshOk' : forall x L, String.length x > sumLengths L
|
adamc@247
|
726 -> ~In x L.
|
adamc@247
|
727 induction L; crush.
|
adamc@246
|
728 Qed.
|
adamc@246
|
729
|
adamc@247
|
730 Lemma length_app : forall s2 s1, String.length (s1 ++ s2) = String.length s1 + String.length s2.
|
adamc@247
|
731 induction s1; crush.
|
adamc@246
|
732 Qed.
|
adamc@246
|
733
|
adamc@247
|
734 Hint Rewrite length_app : cpdt.
|
adamc@247
|
735
|
adamc@247
|
736 Lemma length_primes : forall n, String.length (primes n) = S n.
|
adamc@247
|
737 induction n; crush.
|
adamc@247
|
738 Qed.
|
adamc@247
|
739
|
adamc@247
|
740 Hint Rewrite length_primes : cpdt.
|
adamc@247
|
741
|
adamc@247
|
742 Theorem freshOk : forall L, ~In (fresh L) L.
|
adamc@247
|
743 intros; apply freshOk'; unfold fresh; crush.
|
adamc@247
|
744 Qed.
|
adamc@247
|
745
|
adamc@247
|
746 Hint Resolve freshOk.
|
adamc@247
|
747
|
adamc@247
|
748 Lemma hasType_lclosed : forall G e t,
|
adamc@247
|
749 G |-e e : t
|
adamc@247
|
750 -> lclosed O e.
|
adamc@247
|
751 induction 1; eauto.
|
adamc@247
|
752 Qed.
|
adamc@247
|
753
|
adamc@247
|
754 Lemma lclosed_open : forall n e, lclosed n e
|
adamc@247
|
755 -> forall x, open x n e = e.
|
adamc@248
|
756 induction 1; ln.
|
adamc@247
|
757 Qed.
|
adamc@247
|
758
|
adamc@247
|
759 Hint Resolve lclosed_open hasType_lclosed.
|
adamc@247
|
760
|
adamc@247
|
761 Open Scope list_scope.
|
adamc@247
|
762
|
adamc@248
|
763 Lemma In_cons1 : forall T (x x' : T) ls,
|
adamc@248
|
764 x = x'
|
adamc@248
|
765 -> In x (x' :: ls).
|
adamc@248
|
766 crush.
|
adamc@248
|
767 Qed.
|
adamc@248
|
768
|
adamc@248
|
769 Lemma In_cons2 : forall T (x x' : T) ls,
|
adamc@248
|
770 In x ls
|
adamc@248
|
771 -> In x (x' :: ls).
|
adamc@248
|
772 crush.
|
adamc@248
|
773 Qed.
|
adamc@248
|
774
|
adamc@247
|
775 Lemma In_app1 : forall T (x : T) ls2 ls1,
|
adamc@247
|
776 In x ls1
|
adamc@247
|
777 -> In x (ls1 ++ ls2).
|
adamc@247
|
778 induction ls1; crush.
|
adamc@247
|
779 Qed.
|
adamc@247
|
780
|
adamc@247
|
781 Lemma In_app2 : forall T (x : T) ls2 ls1,
|
adamc@247
|
782 In x ls2
|
adamc@247
|
783 -> In x (ls1 ++ ls2).
|
adamc@247
|
784 induction ls1; crush.
|
adamc@247
|
785 Qed.
|
adamc@247
|
786
|
adamc@248
|
787 Lemma freshOk_app1 : forall L1 L2,
|
adamc@248
|
788 ~ In (fresh (L1 ++ L2)) L1.
|
adamc@248
|
789 intros; generalize (freshOk (L1 ++ L2)); crush.
|
adamc@248
|
790 Qed.
|
adamc@248
|
791
|
adamc@248
|
792 Lemma freshOk_app2 : forall L1 L2,
|
adamc@248
|
793 ~ In (fresh (L1 ++ L2)) L2.
|
adamc@248
|
794 intros; generalize (freshOk (L1 ++ L2)); crush.
|
adamc@248
|
795 Qed.
|
adamc@248
|
796
|
adamc@248
|
797 Hint Resolve In_cons1 In_cons2 In_app1 In_app2.
|
adamc@246
|
798
|
adamc@246
|
799 Section subst.
|
adamc@248
|
800 Hint Resolve freshOk_app1 freshOk_app2.
|
adamc@248
|
801
|
adamc@246
|
802 Variable x : free_var.
|
adamc@246
|
803 Variable e1 : exp.
|
adamc@246
|
804
|
adamc@246
|
805 Fixpoint subst (e2 : exp) : exp :=
|
adamc@246
|
806 match e2 with
|
adamc@246
|
807 | Const _ => e2
|
adamc@246
|
808 | FreeVar x' => if string_dec x' x then e1 else e2
|
adamc@246
|
809 | BoundVar _ => e2
|
adamc@246
|
810 | App e1 e2 => App (subst e1) (subst e2)
|
adamc@246
|
811 | Abs e' => Abs (subst e')
|
adamc@246
|
812 end.
|
adamc@247
|
813
|
adamc@247
|
814 Variable xt : type.
|
adamc@247
|
815
|
adamc@247
|
816 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
|
adamc@247
|
817 Infix "#" := disj (no associativity, at level 90).
|
adamc@247
|
818
|
adamc@248
|
819 Ltac disj := crush;
|
adamc@248
|
820 match goal with
|
adamc@248
|
821 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
|
adamc@248
|
822 end; crush; eauto.
|
adamc@248
|
823
|
adamc@247
|
824 Lemma lookup_disj' : forall t G1,
|
adamc@247
|
825 G1 |-v x : t
|
adamc@247
|
826 -> forall G, x # G
|
adamc@247
|
827 -> G1 = G ++ (x, xt) :: nil
|
adamc@247
|
828 -> t = xt.
|
adamc@248
|
829 unfold disj; induction 1; disj.
|
adamc@247
|
830 Qed.
|
adamc@247
|
831
|
adamc@247
|
832 Lemma lookup_disj : forall t G,
|
adamc@247
|
833 x # G
|
adamc@247
|
834 -> G ++ (x, xt) :: nil |-v x : t
|
adamc@247
|
835 -> t = xt.
|
adamc@247
|
836 intros; eapply lookup_disj'; eauto.
|
adamc@247
|
837 Qed.
|
adamc@247
|
838
|
adamc@247
|
839 Lemma lookup_ne' : forall G1 v t,
|
adamc@247
|
840 G1 |-v v : t
|
adamc@247
|
841 -> forall G, G1 = G ++ (x, xt) :: nil
|
adamc@247
|
842 -> v <> x
|
adamc@247
|
843 -> G |-v v : t.
|
adamc@248
|
844 induction 1; disj.
|
adamc@247
|
845 Qed.
|
adamc@247
|
846
|
adamc@247
|
847 Lemma lookup_ne : forall G v t,
|
adamc@247
|
848 G ++ (x, xt) :: nil |-v v : t
|
adamc@247
|
849 -> v <> x
|
adamc@247
|
850 -> G |-v v : t.
|
adamc@247
|
851 intros; eapply lookup_ne'; eauto.
|
adamc@247
|
852 Qed.
|
adamc@247
|
853
|
adamc@247
|
854 Hint Extern 1 (_ |-e _ : _) =>
|
adamc@247
|
855 match goal with
|
adamc@247
|
856 | [ H1 : _, H2 : _ |- _ ] => rewrite (lookup_disj H1 H2)
|
adamc@247
|
857 end.
|
adamc@247
|
858 Hint Resolve lookup_ne.
|
adamc@247
|
859
|
adamc@247
|
860 Hint Extern 1 (@eq exp _ _) => f_equal.
|
adamc@247
|
861
|
adamc@247
|
862 Lemma open_subst : forall x0 e' n,
|
adamc@247
|
863 lclosed n e1
|
adamc@247
|
864 -> x <> x0
|
adamc@247
|
865 -> open x0 n (subst e') = subst (open x0 n e').
|
adamc@248
|
866 induction e'; ln.
|
adamc@247
|
867 Qed.
|
adamc@247
|
868
|
adamc@248
|
869 Lemma hasType_open_subst : forall G x0 e t,
|
adamc@248
|
870 G |-e subst (open x0 0 e) : t
|
adamc@248
|
871 -> x <> x0
|
adamc@248
|
872 -> lclosed 0 e1
|
adamc@248
|
873 -> G |-e open x0 0 (subst e) : t.
|
adamc@248
|
874 intros; rewrite open_subst; eauto.
|
adamc@248
|
875 Qed.
|
adamc@248
|
876
|
adamc@248
|
877 Hint Resolve hasType_open_subst.
|
adamc@247
|
878
|
adamc@247
|
879 Lemma disj_push : forall x0 (t : type) G,
|
adamc@247
|
880 x # G
|
adamc@247
|
881 -> x <> x0
|
adamc@247
|
882 -> x # (x0, t) :: G.
|
adamc@247
|
883 unfold disj; crush.
|
adamc@247
|
884 Qed.
|
adamc@247
|
885
|
adamc@248
|
886 Hint Resolve disj_push.
|
adamc@247
|
887
|
adamc@247
|
888 Lemma lookup_cons : forall x0 dom G x1 t,
|
adamc@247
|
889 G |-v x1 : t
|
adamc@248
|
890 -> ~In x0 (map (@fst _ _) G)
|
adamc@247
|
891 -> (x0, dom) :: G |-v x1 : t.
|
adamc@248
|
892 induction 1; crush;
|
adamc@247
|
893 match goal with
|
adamc@247
|
894 | [ H : _ |-v _ : _ |- _ ] => inversion H
|
adamc@247
|
895 end; crush.
|
adamc@247
|
896 Qed.
|
adamc@247
|
897
|
adamc@247
|
898 Hint Resolve lookup_cons.
|
adamc@247
|
899 Hint Unfold disj.
|
adamc@247
|
900
|
adamc@248
|
901 Lemma TAbs_specialized : forall G e' dom ran L x1,
|
adamc@248
|
902 (forall x, ~In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran)
|
adamc@248
|
903 -> G |-e Abs e' : dom --> ran.
|
adamc@248
|
904 eauto.
|
adamc@248
|
905 Qed.
|
adamc@248
|
906
|
adamc@247
|
907 Lemma hasType_subst' : forall G1 e t,
|
adamc@247
|
908 G1 |-e e : t
|
adamc@247
|
909 -> forall G, G1 = G ++ (x, xt) :: nil
|
adamc@247
|
910 -> x # G
|
adamc@247
|
911 -> G |-e e1 : xt
|
adamc@247
|
912 -> G |-e subst e : t.
|
adamc@248
|
913 induction 1; ln;
|
adamc@248
|
914 match goal with
|
adamc@248
|
915 | [ L : list free_var, _ : ?x # _ |- _ ] =>
|
adamc@248
|
916 apply TAbs_specialized with L x; eauto 20
|
adamc@248
|
917 end.
|
adamc@247
|
918 Qed.
|
adamc@247
|
919
|
adamc@247
|
920 Theorem hasType_subst : forall e t,
|
adamc@247
|
921 (x, xt) :: nil |-e e : t
|
adamc@247
|
922 -> nil |-e e1 : xt
|
adamc@247
|
923 -> nil |-e subst e : t.
|
adamc@247
|
924 intros; eapply hasType_subst'; eauto.
|
adamc@247
|
925 Qed.
|
adamc@246
|
926 End subst.
|
adamc@246
|
927
|
adamc@247
|
928 Hint Resolve hasType_subst.
|
adamc@246
|
929
|
adamc@247
|
930 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
|
adamc@246
|
931
|
adamc@248
|
932 Lemma alpha_open : forall x1 x2 e1 e2 n,
|
adamc@248
|
933 ~In x1 (freeVars e2)
|
adamc@248
|
934 -> ~In x2 (freeVars e2)
|
adamc@248
|
935 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
|
adamc@248
|
936 induction e2; crush;
|
adamc@248
|
937 repeat (match goal with
|
adamc@248
|
938 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@248
|
939 end; crush).
|
adamc@248
|
940 Qed.
|
adamc@248
|
941
|
adamc@246
|
942 Inductive val : exp -> Prop :=
|
adamc@246
|
943 | VConst : forall b, val (Const b)
|
adamc@246
|
944 | VAbs : forall e, val (Abs e).
|
adamc@246
|
945
|
adamc@246
|
946 Hint Constructors val.
|
adamc@246
|
947
|
adamc@246
|
948 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
|
adamc@246
|
949
|
adamc@246
|
950 Inductive step : exp -> exp -> Prop :=
|
adamc@247
|
951 | Beta : forall e1 e2 x,
|
adamc@246
|
952 val e2
|
adamc@247
|
953 -> ~In x (freeVars e1)
|
adamc@246
|
954 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
|
adamc@246
|
955 | Cong1 : forall e1 e2 e1',
|
adamc@246
|
956 e1 ==> e1'
|
adamc@246
|
957 -> App e1 e2 ==> App e1' e2
|
adamc@246
|
958 | Cong2 : forall e1 e2 e2',
|
adamc@246
|
959 val e1
|
adamc@246
|
960 -> e2 ==> e2'
|
adamc@246
|
961 -> App e1 e2 ==> App e1 e2'
|
adamc@246
|
962
|
adamc@246
|
963 where "e1 ==> e2" := (step e1 e2).
|
adamc@246
|
964
|
adamc@246
|
965 Hint Constructors step.
|
adamc@246
|
966
|
adamc@246
|
967 Lemma progress' : forall G e t, G |-e e : t
|
adamc@246
|
968 -> G = nil
|
adamc@246
|
969 -> val e \/ exists e', e ==> e'.
|
adamc@246
|
970 induction 1; crush; eauto;
|
adamc@246
|
971 try match goal with
|
adamc@246
|
972 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
|
adamc@246
|
973 end;
|
adamc@246
|
974 repeat match goal with
|
adamc@246
|
975 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
|
adamc@246
|
976 end.
|
adamc@246
|
977 Qed.
|
adamc@246
|
978
|
adamc@246
|
979 Theorem progress : forall e t, nil |-e e : t
|
adamc@246
|
980 -> val e \/ exists e', e ==> e'.
|
adamc@246
|
981 intros; eapply progress'; eauto.
|
adamc@246
|
982 Qed.
|
adamc@246
|
983
|
adamc@248
|
984 Hint Resolve freshOk_app1 freshOk_app2.
|
adamc@248
|
985
|
adamc@248
|
986 Lemma hasType_alpha_open : forall G L e0 e2 x t,
|
adamc@248
|
987 ~ In x (freeVars e0)
|
adamc@248
|
988 -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t
|
adamc@248
|
989 -> G |-e [x ~> e2](open x 0 e0) : t.
|
adamc@248
|
990 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto.
|
adamc@247
|
991 Qed.
|
adamc@247
|
992
|
adamc@248
|
993 Hint Resolve hasType_alpha_open.
|
adamc@247
|
994
|
adamc@247
|
995 Lemma preservation' : forall G e t, G |-e e : t
|
adamc@246
|
996 -> G = nil
|
adamc@246
|
997 -> forall e', e ==> e'
|
adamc@246
|
998 -> nil |-e e' : t.
|
adamc@246
|
999 induction 1; inversion 2; crush; eauto;
|
adamc@246
|
1000 match goal with
|
adamc@246
|
1001 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
|
adamc@246
|
1002 end; eauto.
|
adamc@246
|
1003 Qed.
|
adamc@246
|
1004
|
adamc@246
|
1005 Theorem preservation : forall e t, nil |-e e : t
|
adamc@246
|
1006 -> forall e', e ==> e'
|
adamc@246
|
1007 -> nil |-e e' : t.
|
adamc@246
|
1008 intros; eapply preservation'; eauto.
|
adamc@247
|
1009 Qed.
|
adamc@246
|
1010
|
adamc@246
|
1011 End LocallyNameless.
|