Mercurial > cpdt > repo

comparison src/Firstorder.v @ 157:2022e3f2aa26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplify Concrete
author Adam Chlipala <adamc@hcoop.net>
date Sun, 02 Nov 2008 14:41:01 -0500
parents be15ed0a8bae
children 6087a32b1926
comparison
equal deleted inserted replaced
156:be15ed0a8bae 157:2022e3f2aa26
76 76
77 where "G |-e e : t" := (hasType G e t). 77 where "G |-e e : t" := (hasType G e t).
78 78
79 Hint Constructors hasType. 79 Hint Constructors hasType.
80 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 x t G' G1, 81 Lemma weaken_lookup : forall x t G' G1,
117 G1 |-v x : t 82 G1 |-v x : t
118 -> G1 ++ G' |-v x : t. 83 -> G1 ++ G' |-v x : t.
119 Hint Resolve weaken_lookup'.
120
121 induction G1 as [ | [x' t'] tl ]; crush; 84 induction G1 as [ | [x' t'] tl ]; crush;
122 match goal with 85 match goal with
123 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush 86 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
124 end. 87 end.
125 Qed. 88 Qed.
143 nil |-e e : t 106 nil |-e e : t
144 -> forall G, G |-e e : t. 107 -> forall G, G |-e e : t.
145 intros; rewrite (app_nil_end G); apply weaken_hasType; auto. 108 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
146 Qed. 109 Qed.
147 110
148 Theorem weaken_hasType1 : forall e t, 111 Hint Resolve weaken_hasType_closed.
149 nil |-e e : t
150 -> forall x t', (x, t') :: nil |-e e : t.
151 intros; change ((x, t') :: nil) with (((x, t') :: nil) ++ nil);
152 apply weaken_hasType; crush.
153 Qed.
154
155 Hint Resolve weaken_hasType_closed weaken_hasType1.
156 112
157 Section subst. 113 Section subst.
158 Variable x : var. 114 Variable x : var.
159 Variable e1 : exp. 115 Variable e1 : exp.
160 116
173 end. 129 end.
174 130
175 Variable xt : type. 131 Variable xt : type.
176 Hypothesis Ht' : nil |-e e1 : xt. 132 Hypothesis Ht' : nil |-e e1 : xt.
177 133
178 Lemma subst_lookup' : forall G2 x' t, 134 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
179 x' ## G2 135
180 -> (x, xt) :: G2 |-v x' : t 136 Lemma subst_lookup' : forall x' t,
181 -> t = xt.
182 inversion 2; crush; elimtype False; eauto.
183 Qed.
184
185 Lemma subst_lookup : forall x' t,
186 x <> x' 137 x <> x'
187 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t 138 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
188 -> G1 |-v x' : t. 139 -> G1 |-v x' : t.
189 induction G1 as [ | [x'' t'] tl ]; crush; 140 induction G1 as [ | [x'' t'] tl ]; crush;
190 match goal with 141 match goal with
191 | [ H : _ |-v _ : _ |- _ ] => inversion H 142 | [ H : _ |-v _ : _ |- _ ] => inversion H
192 end; crush. 143 end; crush.
193 Qed. 144 Qed.
194 145
195 Hint Resolve subst_lookup. 146 Hint Resolve subst_lookup'.
196 147
197 Lemma subst_lookup'' : forall x' t G1, 148 Lemma subst_lookup : forall x' t G1,
198 x' ## G1 149 x' # G1
199 -> G1 ++ (x, xt) :: nil |-v x' : t 150 -> G1 ++ (x, xt) :: nil |-v x' : t
200 -> t = xt. 151 -> t = xt.
201 Hint Resolve subst_lookup'.
202
203 induction G1 as [ | [x'' t'] tl ]; crush; eauto; 152 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
204 match goal with 153 match goal with
205 | [ H : _ |-v _ : _ |- _ ] => inversion H 154 | [ H : _ |-v _ : _ |- _ ] => inversion H
206 end; crush; elimtype False; eauto; 155 end; crush; elimtype False; eauto;
207 match goal with 156 match goal with
208 | [ H : nil |-v _ : _ |- _ ] => inversion H 157 | [ H : nil |-v _ : _ |- _ ] => inversion H
209 end. 158 end.
210 Qed. 159 Qed.
211 160
212 Implicit Arguments subst_lookup'' [x' t G1]. 161 Implicit Arguments subst_lookup [x' t G1].
213
214 Lemma disjoint_cons : forall x x' t (G : ctx),
215 x ## G
216 -> x' <> x
217 -> x ## (x', t) :: G.
218 firstorder;
219 match goal with
220 | [ H : (_, _) = (_, _) |- _ ] => injection H
221 end; crush.
222 Qed.
223
224 Hint Resolve disjoint_cons.
225 162
226 Lemma shadow_lookup : forall v t t' G1, 163 Lemma shadow_lookup : forall v t t' G1,
227 G1 |-v x : t' 164 G1 |-v x : t'
228 -> G1 ++ (x, xt) :: nil |-v v : t 165 -> G1 ++ (x, xt) :: nil |-v v : t
229 -> G1 |-v v : t. 166 -> G1 |-v v : t.
256 intros; eapply shadow_hasType'; eauto. 193 intros; eapply shadow_hasType'; eauto.
257 Qed. 194 Qed.
258 195
259 Hint Resolve shadow_hasType. 196 Hint Resolve shadow_hasType.
260 197
198 Lemma disjoint_cons : forall x x' t (G : ctx),
199 x # G
200 -> x' <> x
201 -> x # (x', t) :: G.
202 firstorder;
203 match goal with
204 | [ H : (_, _) = (_, _) |- _ ] => injection H
205 end; crush.
206 Qed.
207
208 Hint Resolve disjoint_cons.
209
261 Theorem subst_hasType : forall G e2 t, 210 Theorem subst_hasType : forall G e2 t,
262 G |-e e2 : t 211 G |-e e2 : t
263 -> forall G1, G = G1 ++ (x, xt) :: nil 212 -> forall G1, G = G1 ++ (x, xt) :: nil
264 -> x ## G1 213 -> x # G1
265 -> G1 |-e subst e2 : t. 214 -> G1 |-e subst e2 : t.
266 induction 1; crush; 215 induction 1; crush;
267 try match goal with 216 try match goal with
268 | [ |- context[if ?E then _ else _] ] => destruct E 217 | [ |- context[if ?E then _ else _] ] => destruct E
269 end; crush; eauto 6; 218 end; crush; eauto 6;
270 match goal with 219 match goal with
271 | [ H1 : x ## _, H2 : _ |-v x : _ |- _ ] => 220 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
272 rewrite (subst_lookup'' H1 H2) 221 rewrite (subst_lookup H1 H2)
273 end; crush. 222 end; crush.
274 Qed. 223 Qed.
275 224
276 Theorem subst_hasType_closed : forall e2 t, 225 Theorem subst_hasType_closed : forall e2 t,
277 (x, xt) :: nil |-e e2 : t 226 (x, xt) :: nil |-e e2 : t
422 nil |-e e : t 371 nil |-e e : t
423 -> forall G, G |-e e : t. 372 -> forall G, G |-e e : t.
424 intros; rewrite (app_nil_end G); apply weaken_hasType; auto. 373 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
425 Qed. 374 Qed.
426 375
427 Theorem weaken_hasType1 : forall e t, 376 Hint Resolve weaken_hasType_closed.
428 nil |-e e : t
429 -> forall t', t' :: nil |-e e : t.
430 intros; change (t' :: nil) with ((t' :: nil) ++ nil);
431 apply weaken_hasType; crush.
432 Qed.
433
434 Hint Resolve weaken_hasType_closed weaken_hasType1.
435 377
436 Section subst. 378 Section subst.
437 Variable e1 : exp. 379 Variable e1 : exp.
438 380
439 Fixpoint subst (x : var) (e2 : exp) : exp := 381 Fixpoint subst (x : var) (e2 : exp) : exp :=