Mercurial > cpdt > repo

comparison src/Extensional.v @ 176:9b1f58dbc464

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CpsExp_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 11:36:00 -0500
parents 022feabdff50
children cee290647641
comparison
equal deleted inserted replaced
175:022feabdff50 176:9b1f58dbc464
100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) 100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
101 | Abs _ _ e' => fun x => expDenote (e' x) 101 | Abs _ _ e' => fun x => expDenote (e' x)
102 end. 102 end.
103 103
104 Definition ExpDenote t (e : Exp t) := expDenote (e _). 104 Definition ExpDenote t (e : Exp t) := expDenote (e _).
105
106 Section exp_equiv.
107 Variables var1 var2 : type -> Type.
108
109 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
110 | EqEVar : forall G t (v1 : var1 t) v2,
111 In (existT _ t (v1, v2)) G
112 -> exp_equiv G (#v1) (#v2)
113
114 | EqEConst : forall G n,
115 exp_equiv G (^n) (^n)
116 | EqEPlus : forall G x1 y1 x2 y2,
117 exp_equiv G x1 x2
118 -> exp_equiv G y1 y2
119 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
120
121 | EqEApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
122 exp_equiv G f1 f2
123 -> exp_equiv G x1 x2
124 -> exp_equiv G (f1 @ x1) (f2 @ x2)
125 | EqEAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
126 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
127 -> exp_equiv G (Abs f1) (Abs f2).
128 End exp_equiv.
129
130 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
131 exp_equiv nil (E var1) (E var2).
105 End Source. 132 End Source.
106 133
107 Module CPS. 134 Module CPS.
108 Inductive type : Type := 135 Inductive type : Type :=
109 | TNat : type 136 | TNat : type
294 Eval compute in ProgDenote (CpsExp one). 321 Eval compute in ProgDenote (CpsExp one).
295 Eval compute in ProgDenote (CpsExp zpo). 322 Eval compute in ProgDenote (CpsExp zpo).
296 Eval compute in ProgDenote (CpsExp app_ident). 323 Eval compute in ProgDenote (CpsExp app_ident).
297 Eval compute in ProgDenote (CpsExp app_ident'). 324 Eval compute in ProgDenote (CpsExp app_ident').
298 325
326 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
327 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
328 | Nat => fun n1 n2 => n1 = n2
329 | t1 --> t2 => fun f1 f2 =>
330 forall x1 x2, lr _ x1 x2
331 -> forall k, exists r,
332 f2 (x2, k) = k r
333 /\ lr _ (f1 x1) r
334 end%source.
335
336 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
337 exp_equiv G e1 e2
338 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
339 -> forall k, exists r,
340 progDenote (cpsExp e2 k) = progDenote (k r)
341 /\ lr t (expDenote e1) r.
342 induction 1; crush; fold typeDenote in *;
343 repeat (match goal with
344 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
345 |- context[cpsExp ?E ?K] ] =>
346 generalize (H K); clear H
347 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
348 exists R
349 | [ t1 : Source.type |- _ ] =>
350 match goal with
351 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
352 generalize (IH X1 X2); clear IH; intro IH;
353 match type of IH with
354 | ?P -> _ => assert P
355 end
356 end
357 end; crush); eauto.
358 Qed.
359
360 Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
361 (v2 : typeDenote (cpsType t)),
362 In
363 (existT
364 (fun t0 : Source.type =>
365 (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
366 (v1, v2)) nil -> lr t v1 v2.
367 crush.
368 Qed.
369
370 Theorem CpsExp_correct : forall (E : Exp Nat),
371 ProgDenote (CpsExp E) = ExpDenote E.
372 unfold ProgDenote, CpsExp, ExpDenote; intros;
373 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
374 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
375 Qed.
376
299 End STLC. 377 End STLC.