Mercurial > cpdt > repo

comparison src/Hoas.v @ 162:df02642f93b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Evaluation contexts ahoy
author Adam Chlipala <adamc@hcoop.net>
date Tue, 04 Nov 2008 12:39:28 -0500
parents 56e205f966cc
children ba306bf9ec80
comparison
equal deleted inserted replaced
161:6087a32b1926 162:df02642f93b8
82 | VConst : forall n, Val (Const n) 82 | VConst : forall n, Val (Const n)
83 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B). 83 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
84 84
85 Hint Constructors Val. 85 Hint Constructors Val.
86 86
87 Inductive Ctx : type -> type -> Type :=
88 | AppCong1 : forall (dom ran : type),
89 Exp dom -> Ctx (dom --> ran) ran
90 | AppCong2 : forall (dom ran : type),
91 Exp (dom --> ran) -> Ctx dom ran
92 | PlusCong1 : Exp Nat -> Ctx Nat Nat
93 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
94
95 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
96 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
97 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
98 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
99 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
100
101 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
102 match C in Ctx t1 t2 return Exp t1 -> Exp t2 with
103 | AppCong1 _ _ X => fun F => App F X
104 | AppCong2 _ _ F => fun X => App F X
105 | PlusCong1 E2 => fun E1 => Plus E1 E2
106 | PlusCong2 E1 => fun E2 => Plus E1 E2
107 end.
108
109 Infix "@" := plug (no associativity, at level 60).
110
87 Inductive Step : forall t, Exp t -> Exp t -> Prop := 111 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
88 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), 112 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
89 Val X 113 Val X
90 -> App (Abs B) X ==> Subst X B 114 -> App (Abs B) X ==> Subst X B
91 | AppCong1 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) F',
92 F ==> F'
93 -> App F X ==> App F' X
94 | AppCong2 : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom) X',
95 Val F
96 -> X ==> X'
97 -> App F X ==> App F X'
98
99 | Sum : forall n1 n2, 115 | Sum : forall n1 n2,
100 Plus (Const n1) (Const n2) ==> Const (n1 + n2) 116 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
101 | PlusCong1 : forall E1 E2 E1', 117 | Cong : forall t t' (C : Ctx t t') E E' E1,
102 E1 ==> E1' 118 isCtx C
103 -> Plus E1 E2 ==> Plus E1' E2 119 -> E1 = C @ E
104 | PlusCong2 : forall E1 E2 E2', 120 -> E ==> E'
105 Val E1 121 -> E1 ==> C @ E'
106 -> E2 ==> E2'
107 -> Plus E1 E2 ==> Plus E1 E2'
108 122
109 where "E1 ==> E2" := (Step E1 E2). 123 where "E1 ==> E2" := (Step E1 E2).
110 124
111 Hint Constructors Step. 125 Hint Constructors isCtx Step.
112 126
113 Inductive Closed : forall t, Exp t -> Prop := 127 Inductive Closed : forall t, Exp t -> Prop :=
114 | CConst : forall b, 128 | CConst : forall b,
115 Closed (Const b) 129 Closed (Const b)
116 | CPlus : forall E1 E2, 130 | CPlus : forall E1 E2,
135 Ltac my_crush := 149 Ltac my_crush :=
136 my_crush'; 150 my_crush';
137 try (match goal with 151 try (match goal with
138 | [ H : ?F = ?G |- _ ] => 152 | [ H : ?F = ?G |- _ ] =>
139 match goal with 153 match goal with
140 | [ _ : F (fun _ => unit) = G (fun _ => unit) |- _ ] => fail 1 154 (*| [ _ : F (fun _ => unit) = G (fun _ => unit) |- _ ] => fail 1*)
141 | _ => 155 | _ =>
142 let H' := fresh "H'" in 156 let H' := fresh "H'" in
143 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence 157 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
144 | discriminate || injection H' ]; 158 | discriminate || injection H' ];
145 clear H' 159 clear H'
161 end; injection H'; clear H'; my_crush' ] 175 end; injection H'; clear H'; my_crush' ]
162 | my_crush'; clear H2 ] 176 | my_crush'; clear H2 ]
163 end 177 end
164 end. 178 end.
165 179
180 Hint Extern 1 (_ = _ @ _) => simpl.
181
166 Lemma progress' : forall t (E : Exp t), 182 Lemma progress' : forall t (E : Exp t),
167 Closed E 183 Closed E
168 -> Val E \/ exists E', E ==> E'. 184 -> Val E \/ exists E', E ==> E'.
169 induction 1; crush; 185 induction 1; crush;
170 repeat match goal with 186 repeat match goal with
171 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush 187 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
172 end; eauto. 188 end; eauto 6.
173 Qed. 189 Qed.
174 190
175 Theorem progress : forall t (E : Exp t), 191 Theorem progress : forall t (E : Exp t),
176 Val E \/ exists E', E ==> E'. 192 Val E \/ exists E', E ==> E'.
177 intros; apply progress'; apply closed. 193 intros; apply progress'; apply closed.
220 -> E2 ==>* E3 236 -> E2 ==>* E3
221 -> E1 ==>* E3. 237 -> E1 ==>* E3.
222 induction 1; eauto. 238 induction 1; eauto.
223 Qed. 239 Qed.
224 240
225 Hint Resolve MultiStep_trans.
226
227 Theorem Big_Val : forall t (E V : Exp t), 241 Theorem Big_Val : forall t (E V : Exp t),
228 E ===> V 242 E ===> V
229 -> Val V. 243 -> Val V.
230 induction 1; crush. 244 induction 1; crush.
231 Qed. 245 Qed.
236 destruct 1; crush. 250 destruct 1; crush.
237 Qed. 251 Qed.
238 252
239 Hint Resolve Big_Val Val_Big. 253 Hint Resolve Big_Val Val_Big.
240 254
241 Ltac uiper := 255 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
242 repeat match goal with 256 isCtx C
243 | [ pf : _ = _ |- _ ] => 257 -> forall E E', E ==>* E'
244 generalize pf; subst; intro; 258 -> C @ E ==>* C @ E'.
245 rewrite (UIP_refl _ _ pf); simpl;
246 repeat match goal with
247 | [ H : forall pf : ?X = ?X, _ |- _ ] =>
248 generalize (H (refl_equal _)); clear H; intro H
249 end
250 end.
251
252 Lemma Multi_PlusCong1' : forall E2 t (pf : t = Nat) (E1 E1' : Exp t),
253 E1 ==>* E1'
254 -> Plus (match pf with refl_equal => E1 end) E2
255 ==>* Plus (match pf with refl_equal => E1' end) E2.
256 induction 1; crush; uiper; eauto.
257 Qed.
258
259 Lemma Multi_PlusCong1 : forall E1 E2 E1',
260 E1 ==>* E1'
261 -> Plus E1 E2 ==>* Plus E1' E2.
262 intros; generalize (Multi_PlusCong1' E2 (refl_equal _)); auto.
263 Qed.
264
265 Lemma Multi_PlusCong2' : forall E1 (_ : Val E1) t (pf : t = Nat) (E2 E2' : Exp t),
266 E2 ==>* E2'
267 -> Plus E1 (match pf with refl_equal => E2 end)
268 ==>* Plus E1 (match pf with refl_equal => E2' end).
269 induction 2; crush; uiper; eauto.
270 Qed.
271
272 Lemma Multi_PlusCong2 : forall E1 E2 E2',
273 Val E1
274 -> E2 ==>* E2'
275 -> Plus E1 E2 ==>* Plus E1 E2'.
276 intros E1 E2 E2' H; generalize (Multi_PlusCong2' H (refl_equal _)); auto.
277 Qed.
278
279 Lemma Multi_AppCong1' : forall dom ran E2 t (pf : t = dom --> ran) (E1 E1' : Exp t),
280 E1 ==>* E1'
281 -> App (match pf in _ = t' return Exp t' with refl_equal => E1 end) E2
282 ==>* App (match pf in _ = t' return Exp t' with refl_equal => E1' end) E2.
283 induction 1; crush; uiper; eauto.
284 Qed.
285
286 Lemma Multi_AppCong1 : forall dom ran (E1 : Exp (dom --> ran)) E2 E1',
287 E1 ==>* E1'
288 -> App E1 E2 ==>* App E1' E2.
289 intros; generalize (Multi_AppCong1' (ran := ran) E2 (refl_equal _)); auto.
290 Qed.
291
292 Lemma Multi_AppCong2 : forall dom ran (E1 : Exp (dom --> ran)) E2 E2',
293 Val E1
294 -> E2 ==>* E2'
295 -> App E1 E2 ==>* App E1 E2'.
296 induction 2; crush; eauto. 259 induction 2; crush; eauto.
297 Qed. 260 Qed.
298 261
299 Hint Resolve Multi_PlusCong1 Multi_PlusCong2 Multi_AppCong1 Multi_AppCong2. 262 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
263 isCtx C
264 -> E1 = C @ E
265 -> E2 = C @ E'
266 -> E ==>* E'
267 -> E1 ==>* E2.
268 crush; apply Multi_Cong; auto.
269 Qed.
270
271 Hint Resolve Multi_Cong'.
272
273 Ltac mtrans E :=
274 match goal with
275 | [ |- E ==>* _ ] => fail 1
276 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
277 end.
300 278
301 Theorem Big_Multi : forall t (E V : Exp t), 279 Theorem Big_Multi : forall t (E V : Exp t),
302 E ===> V 280 E ===> V
303 -> E ==>* V. 281 -> E ==>* V.
304 induction 1; crush; eauto 8. 282 induction 1; crush; eauto;
283 repeat match goal with
284 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
285 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
286 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
287 end.
305 Qed. 288 Qed.
306 289
307 Lemma Big_Val' : forall t (V1 V2 : Exp t), 290 Lemma Big_Val' : forall t (V1 V2 : Exp t),
308 Val V2 291 Val V2
309 -> V1 = V2 292 -> V1 = V2
318 -> forall E'', E' ===> E'' 301 -> forall E'', E' ===> E''
319 -> E ===> E''. 302 -> E ===> E''.
320 induction 1; crush; eauto; 303 induction 1; crush; eauto;
321 match goal with 304 match goal with
322 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto 305 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
306 end;
307 match goal with
308 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
323 end. 309 end.
324 Qed. 310 Qed.
325 311
326 Hint Resolve Multi_Big'. 312 Hint Resolve Multi_Big'.
327 313