Mercurial > cpdt > repo
comparison src/Firstorder.v @ 157:2022e3f2aa26
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 := |