Mercurial > cpdt > repo

comparison src/Firstorder.v @ 152:8157e8e28e2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proved concrete substitution
author Adam Chlipala <adamc@hcoop.net>
date Sun, 02 Nov 2008 12:16:55 -0500
parents
children 8c19768f1a1a
comparison
equal deleted inserted replaced
151:e71904f61e69 152:8157e8e28e2e
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import List String.
12
13 Require Import Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\section{Formalizing Programming Languages and Compilers}
20
21 \chapter{First-Order Variable Representations}% *)
22
23 (** TODO: Prose for this chapter *)
24
25
26 (** * Concrete Binding *)
27
28 Module Concrete.
29
30 Definition var := string.
31 Definition var_eq := string_dec.
32
33 Inductive exp : Set :=
34 | Const : bool -> exp
35 | Var : var -> exp
36 | App : exp -> exp -> exp
37 | Abs : var -> exp -> exp.
38
39 Inductive type : Set :=
40 | Bool : type
41 | Arrow : type -> type -> type.
42
43 Infix "-->" := Arrow (right associativity, at level 60).
44
45 Definition ctx := list (var * type).
46
47 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
48
49 Inductive lookup : ctx -> var -> type -> Prop :=
50 | First : forall x t G,
51 (x, t) :: G |-v x : t
52 | Next : forall x t x' t' G,
53 x <> x'
54 -> G |-v x : t
55 -> (x', t') :: G |-v x : t
56
57 where "G |-v x : t" := (lookup G x t).
58
59 Hint Constructors lookup.
60
61 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
62
63 Inductive hasType : ctx -> exp -> type -> Prop :=
64 | TConst : forall G b,
65 G |-e Const b : Bool
66 | TVar : forall G v t,
67 G |-v v : t
68 -> G |-e Var v : t
69 | TApp : forall G e1 e2 dom ran,
70 G |-e e1 : dom --> ran
71 -> G |-e e2 : dom
72 -> G |-e App e1 e2 : ran
73 | TAbs : forall G x e' dom ran,
74 (x, dom) :: G |-e e' : ran
75 -> G |-e Abs x e' : dom --> ran
76
77 where "G |-e e : t" := (hasType G e t).
78
79 Hint Constructors hasType.
80
81 Notation "x ## G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
82
83 Notation "G' # G" := (forall (x : var) (t : type), In (x, t) G -> x ## G') (no associativity, at level 90).
84
85 Lemma lookup_In : forall G x t,
86 G |-v x : t
87 -> In (x, t) G.
88 induction 1; crush.
89 Qed.
90
91 Hint Resolve lookup_In.
92
93 Lemma disjoint_invert1 : forall G x t G' x' t',
94 G |-v x : t
95 -> (x', t') :: G' # G
96 -> x <> x'.
97 crush; eauto.
98 Qed.
99
100 Lemma disjoint_invert2 : forall G' G p,
101 p :: G' # G
102 -> G' # G.
103 firstorder.
104 Qed.
105
106 Hint Resolve disjoint_invert1 disjoint_invert2.
107 Hint Extern 1 (_ <> _) => (intro; subst).
108
109 Lemma weaken_lookup' : forall G x t,
110 G |-v x : t
111 -> forall G', G' # G
112 -> G' ++ G |-v x : t.
113 induction G' as [ | [x' t'] tl ]; crush; eauto 9.
114 Qed.
115
116 Lemma weaken_lookup : forall G2 x t G',
117 G' # G2
118 -> forall G1, G1 ++ G2 |-v x : t
119 -> G1 ++ G' ++ G2 |-v x : t.
120 Hint Resolve weaken_lookup'.
121
122 induction G1 as [ | [x' t'] tl ]; crush;
123 match goal with
124 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
125 end.
126 Qed.
127
128 Hint Resolve weaken_lookup.
129
130 Lemma hasType_push : forall x t G1 G2 e t',
131 ((x, t) :: G1) ++ G2 |-e e : t'
132 -> (x, t) :: G1 ++ G2 |-e e : t'.
133 trivial.
134 Qed.
135
136 Hint Resolve hasType_push.
137
138 Theorem weaken_hasType' : forall G' G e t,
139 G |-e e : t
140 -> forall G1 G2, G = G1 ++ G2
141 -> G' # G2
142 -> G1 ++ G' ++ G2 |-e e : t.
143 induction 1; crush; eauto.
144 Qed.
145
146 Theorem weaken_hasType : forall G e t,
147 G |-e e : t
148 -> forall G', G' # G
149 -> G' ++ G |-e e : t.
150 intros; change (G' ++ G) with (nil ++ G' ++ G);
151 eapply weaken_hasType'; eauto.
152 Qed.
153
154 Theorem weaken_hasType_closed : forall e t,
155 nil |-e e : t
156 -> forall G, G |-e e : t.
157 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
158 Qed.
159
160 Theorem weaken_hasType1 : forall G e t,
161 G |-e e : t
162 -> forall x t', x ## G
163 -> (x, t') :: G |-e e : t.
164 intros; change ((x, t') :: G) with (((x, t') :: nil) ++ G);
165 apply weaken_hasType; crush;
166 match goal with
167 | [ H : (_, _) = (_, _) |- _ ] => injection H
168 end; crush; eauto.
169 Qed.
170
171 Hint Resolve weaken_hasType_closed weaken_hasType1.
172
173 Section subst.
174 Variable x : var.
175 Variable e1 : exp.
176
177 Fixpoint subst (e2 : exp) : exp :=
178 match e2 with
179 | Const b => Const b
180 | Var x' =>
181 if var_eq x' x
182 then e1
183 else Var x'
184 | App e1 e2 => App (subst e1) (subst e2)
185 | Abs x' e' =>
186 Abs x' (if var_eq x' x
187 then e'
188 else subst e')
189 end.
190
191 Variable xt : type.
192 Hypothesis Ht' : nil |-e e1 : xt.
193
194 Lemma subst_lookup' : forall G2 x' t,
195 x' ## G2
196 -> (x, xt) :: G2 |-v x' : t
197 -> t = xt.
198 inversion 2; crush; elimtype False; eauto.
199 Qed.
200
201 Lemma subst_lookup : forall x' t G2,
202 x <> x'
203 -> forall G1, G1 ++ (x, xt) :: G2 |-v x' : t
204 -> G1 ++ G2 |-v x' : t.
205 induction G1 as [ | [x'' t'] tl ]; crush;
206 match goal with
207 | [ H : _ |-v _ : _ |- _ ] => inversion H
208 end; crush.
209 Qed.
210
211 Hint Resolve subst_lookup.
212
213 Lemma subst_lookup'' : forall G2 x' t,
214 x' ## G2
215 -> forall G1, x' ## G1
216 -> G1 ++ (x, xt) :: G2 |-v x' : t
217 -> t = xt.
218 Hint Resolve subst_lookup'.
219
220 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
221 match goal with
222 | [ H : _ |-v _ : _ |- _ ] => inversion H
223 end; crush; elimtype False; eauto.
224 Qed.
225
226 Implicit Arguments subst_lookup'' [G2 x' t G1].
227
228 Lemma disjoint_cons : forall x x' t (G : ctx),
229 x ## G
230 -> x' <> x
231 -> x ## (x', t) :: G.
232 firstorder;
233 match goal with
234 | [ H : (_, _) = (_, _) |- _ ] => injection H
235 end; crush.
236 Qed.
237
238 Hint Resolve disjoint_cons.
239
240 Lemma shadow_lookup : forall G2 v t t' G1,
241 G1 |-v x : t'
242 -> G1 ++ (x, xt) :: G2 |-v v : t
243 -> G1 ++ G2 |-v v : t.
244 induction G1 as [ | [x'' t''] tl ]; crush;
245 match goal with
246 | [ H : nil |-v _ : _ |- _ ] => inversion H
247 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
248 inversion H1; crush; inversion H2; crush
249 end.
250 Qed.
251
252 Lemma shadow_hasType' : forall G2 G e t,
253 G |-e e : t
254 -> forall G1, G = G1 ++ (x, xt) :: G2
255 -> forall t'', G1 |-v x : t''
256 -> G1 ++ G2 |-e e : t.
257 Hint Resolve shadow_lookup.
258
259 induction 1; crush; eauto;
260 match goal with
261 | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
262 destruct (var_eq x0 x); subst; eauto
263 end.
264 Qed.
265
266 Lemma shadow_hasType : forall G1 G2 e t t'',
267 G1 ++ (x, xt) :: G2 |-e e : t
268 -> G1 |-v x : t''
269 -> G1 ++ G2 |-e e : t.
270 intros; eapply shadow_hasType'; eauto.
271 Qed.
272
273 Hint Resolve shadow_hasType.
274
275 Theorem subst_hasType : forall G e2 t,
276 G |-e e2 : t
277 -> forall G1 G2, G = G1 ++ (x, xt) :: G2
278 -> x ## G1
279 -> x ## G2
280 -> G1 ++ G2 |-e subst e2 : t.
281 induction 1; crush;
282 try match goal with
283 | [ |- context[if ?E then _ else _] ] => destruct E
284 end; crush; eauto 6;
285 match goal with
286 | [ H1 : x ## _, H2 : x ## _, H3 : _ |-v x : _ |- _ ] =>
287 rewrite (subst_lookup'' H2 H1 H3)
288 end; crush.
289 Qed.
290
291 Theorem subst_hasType_closed : forall e2 t,
292 (x, xt) :: nil |-e e2 : t
293 -> nil |-e subst e2 : t.
294 intros; change (nil ++ nil |-e subst e2 : t);
295 eapply subst_hasType; eauto.
296 Qed.
297 End subst.
298
299 End Concrete.