Mercurial > cpdt > repo

annotate src/Extensional.v @ 290:758778c0468c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC comments for FirstOrder
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 15:37:01 -0500
parents 108ec446fbaf
children 2c88fc1dbe33
rev   line source
adamc@216 1 (* Copyright (c) 2008-2009, Adam Chlipala
adamc@175 2 *
adamc@175 3 * This work is licensed under a
adamc@175 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@175 5 * Unported License.
adamc@175 6 * The license text is available at:
adamc@175 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@175 8 *)
adamc@175 9
adamc@175 10 (* begin hide *)
adamc@175 11 Require Import String List.
adamc@175 12
adamc@182 13 Require Import Axioms Tactics DepList.
adamc@175 14
adamc@175 15 Set Implicit Arguments.
adamc@175 16 (* end hide *)
adamc@175 17
adamc@175 18
adamc@181 19 (** %\chapter{Extensional Transformations}% *)
adamc@175 20
adamc@256 21 (** Last chapter's constant folding example was particularly easy to verify, because that transformation used the same source and target language. In this chapter, we verify a different translation, illustrating the added complexities in translating between languages.
adamc@175 22
adamc@256 23 Program transformations can be classified as %\textit{%#<i>#intensional#</i>#%}%, when they require some notion of inequality between variables; or %\textit{%#<i>#extensional#</i>#%}%, otherwise. This chapter's example is extensional, and the next chapter deals with the trickier intensional case. *)
adamc@175 24
adamc@175 25
adamc@256 26 (** * CPS Conversion for Simply-Typed Lambda Calculus *)
adamc@175 27
adamc@256 28 (** A convenient method for compiling functional programs begins with conversion to %\textit{%#<i>#continuation-passing style#</i>#%}%, or CPS. In this restricted form, function calls never return; instead, we pass explicit return pointers, much as in assembly language. Additionally, we make order of evaluation explicit, breaking complex expressions into sequences of primitive operations.
adamc@175 29
adamc@256 30 Our translation will operate over the same source language that we used in the first part of last chapter, so we omit most of the language definition. However, we do make one significant change: since we will be working with multiple languages that involve similar constructs, we use Coq's %\textit{%#<i>#notation scope#</i>#%}% mechanism to disambiguate. For instance, the span of code dealing with type notations looks like this: *)
adamc@175 31
adamc@256 32 (* begin hide *)
adamc@256 33 Module Source.
adamc@256 34 Inductive type : Type :=
adamc@256 35 | TNat : type
adamc@256 36 | Arrow : type -> type -> type.
adamc@256 37 (* end hide *)
adamc@175 38
adamc@256 39 Notation "'Nat'" := TNat : source_scope.
adamc@256 40 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@175 41
adamc@256 42 Open Scope source_scope.
adamc@256 43 Bind Scope source_scope with type.
adamc@256 44 Delimit Scope source_scope with source.
adamc@175 45
adamc@256 46 (** We explicitly place our notations inside a scope named [source_scope], and we associate a delimiting key [source] with [source_scope]. Without further commands, our notations would only be used in expressions like [(...)%source]. We also open our scope locally within this module, so that we avoid repeating [%source] in many places. Further, we %\textit{%#<i>#bind#</i>#%}% our scope to [type]. In some circumstances where Coq is able to infer that some subexpression has type [type], that subexpression will automatically be parsed in [source_scope]. *)
adamc@175 47
adamc@256 48 (* begin hide *)
adamc@256 49 Section vars.
adamc@256 50 Variable var : type -> Type.
adamc@175 51
adamc@256 52 Inductive exp : type -> Type :=
adamc@256 53 | Var : forall t,
adamc@256 54 var t
adamc@256 55 -> exp t
adamc@175 56
adamc@256 57 | Const : nat -> exp Nat
adamc@256 58 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@175 59
adamc@256 60 | App : forall t1 t2,
adamc@256 61 exp (t1 --> t2)
adamc@256 62 -> exp t1
adamc@256 63 -> exp t2
adamc@256 64 | Abs : forall t1 t2,
adamc@256 65 (var t1 -> exp t2)
adamc@256 66 -> exp (t1 --> t2).
adamc@256 67 End vars.
adamc@175 68
adamc@256 69 Definition Exp t := forall var, exp var t.
adamc@175 70
adamc@256 71 Implicit Arguments Var [var t].
adamc@256 72 Implicit Arguments Const [var].
adamc@256 73 Implicit Arguments Plus [var].
adamc@256 74 Implicit Arguments App [var t1 t2].
adamc@256 75 Implicit Arguments Abs [var t1 t2].
adamc@175 76
adamc@256 77 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@175 78
adamc@256 79 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@256 80 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@175 81
adamc@256 82 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@256 83 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@256 84 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@175 85
adamc@256 86 Bind Scope source_scope with exp.
adamc@256 87
adamc@257 88 Example zero : Exp Nat := fun _ => ^0.
adamc@257 89 Example one : Exp Nat := fun _ => ^1.
adamc@257 90 Example zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@257 91 Example ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@257 92 Example app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@257 93 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@256 94 \f, \x, #f @ #x.
adamc@257 95 Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@256 96
adamc@256 97 Fixpoint typeDenote (t : type) : Set :=
adamc@256 98 match t with
adamc@256 99 | Nat => nat
adamc@256 100 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@256 101 end.
adamc@256 102
adamc@256 103 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@256 104 match e with
adamc@256 105 | Var _ v => v
adamc@256 106
adamc@256 107 | Const n => n
adamc@256 108 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@256 109
adamc@256 110 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@256 111 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@256 112 end.
adamc@256 113
adamc@256 114 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@256 115 (* end hide *)
adamc@256 116
adamc@256 117 (** The other critical new ingredient is a generalization of the [Closed] relation from two chapters ago. The new relation [exp_equiv] characters when two expressions may be considered syntactically equal. We need to be able to handle cases where each expression uses a different [var] type. Intuitively, we will want to compare expressions that use their variables to store source-level and target-level values. We express pairs of equivalent variables using a list parameter to the relation; variable expressions will be considered equivalent if and only if their variables belong to this list. The rule for function abstraction extends the list in a higher-order way. The remaining rules just implement the obvious congruence over expressions. *)
adamc@176 118
adamc@180 119 (* begin thide *)
adamc@256 120 Section exp_equiv.
adamc@256 121 Variables var1 var2 : type -> Type.
adamc@176 122
adamc@256 123 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
adamc@256 124 -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@256 125 | EqVar : forall G t (v1 : var1 t) v2,
adamc@256 126 In (existT _ t (v1, v2)) G
adamc@256 127 -> exp_equiv G (#v1) (#v2)
adamc@176 128
adamc@256 129 | EqConst : forall G n,
adamc@256 130 exp_equiv G (^n) (^n)
adamc@256 131 | EqPlus : forall G x1 y1 x2 y2,
adamc@256 132 exp_equiv G x1 x2
adamc@256 133 -> exp_equiv G y1 y2
adamc@256 134 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176 135
adamc@256 136 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@256 137 exp_equiv G f1 f2
adamc@256 138 -> exp_equiv G x1 x2
adamc@256 139 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@256 140 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@256 141 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@256 142 -> exp_equiv G (Abs f1) (Abs f2).
adamc@256 143 End exp_equiv.
adamc@176 144
adamc@256 145 (** It turns out that, for any parametric expression [E], any two instantiations of [E] with particular [var] types must be equivalent, with respect to an empty variable list. The parametricity of Gallina guarantees this, in much the same way that it guaranteed the truth of the axiom about [Closed]. Thus, we assert an analogous axiom here. *)
adamc@256 146
adamc@256 147 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@256 148 exp_equiv nil (E var1) (E var2).
adamc@180 149 (* end thide *)
adamc@256 150 End Source.
adamc@175 151
adamc@256 152 (** Now we need to define the CPS language, where binary function types are replaced with unary continuation types, and we add product types because they will be useful in our translation. *)
adamc@175 153
adamc@256 154 Module CPS.
adamc@256 155 Inductive type : Type :=
adamc@256 156 | TNat : type
adamc@256 157 | Cont : type -> type
adamc@256 158 | Prod : type -> type -> type.
adamc@175 159
adamc@256 160 Notation "'Nat'" := TNat : cps_scope.
adamc@256 161 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@256 162 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 163
adamc@256 164 Bind Scope cps_scope with type.
adamc@256 165 Delimit Scope cps_scope with cps.
adamc@175 166
adamc@256 167 Section vars.
adamc@256 168 Variable var : type -> Type.
adamc@175 169
adamc@256 170 (** A CPS program is a series of bindings of primitive operations (primops), followed by either a halt with a final program result or by a call to a continuation. The arguments to these program-ending operations are enforced to be variables. To use the values of compound expressions instead, those expressions must be decomposed into bindings of primops. The primop language itself similarly forces variables for all arguments besides bodies of function abstractions. *)
adamc@175 171
adamc@256 172 Inductive prog : Type :=
adamc@256 173 | PHalt :
adamc@256 174 var Nat
adamc@256 175 -> prog
adamc@256 176 | App : forall t,
adamc@256 177 var (t --->)
adamc@256 178 -> var t
adamc@256 179 -> prog
adamc@256 180 | Bind : forall t,
adamc@256 181 primop t
adamc@256 182 -> (var t -> prog)
adamc@256 183 -> prog
adamc@175 184
adamc@256 185 with primop : type -> Type :=
adamc@256 186 | Const : nat -> primop Nat
adamc@256 187 | Plus : var Nat -> var Nat -> primop Nat
adamc@256 188
adamc@256 189 | Abs : forall t,
adamc@256 190 (var t -> prog)
adamc@256 191 -> primop (t --->)
adamc@175 192
adamc@256 193 | Pair : forall t1 t2,
adamc@256 194 var t1
adamc@256 195 -> var t2
adamc@256 196 -> primop (t1 ** t2)
adamc@256 197 | Fst : forall t1 t2,
adamc@256 198 var (t1 ** t2)
adamc@256 199 -> primop t1
adamc@256 200 | Snd : forall t1 t2,
adamc@256 201 var (t1 ** t2)
adamc@256 202 -> primop t2.
adamc@256 203 End vars.
adamc@175 204
adamc@256 205 Implicit Arguments PHalt [var].
adamc@256 206 Implicit Arguments App [var t].
adamc@175 207
adamc@256 208 Implicit Arguments Const [var].
adamc@256 209 Implicit Arguments Plus [var].
adamc@256 210 Implicit Arguments Abs [var t].
adamc@256 211 Implicit Arguments Pair [var t1 t2].
adamc@256 212 Implicit Arguments Fst [var t1 t2].
adamc@256 213 Implicit Arguments Snd [var t1 t2].
adamc@175 214
adamc@256 215 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@256 216 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@256 217 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@256 218 (right associativity, at level 76, p at next level) : cps_scope.
adamc@256 219 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@256 220 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 221
adamc@256 222 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@256 223 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 224
adamc@256 225 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@256 226 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 227
adamc@256 228 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
adamc@256 229 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@256 230 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 231
adamc@256 232 Bind Scope cps_scope with prog primop.
adamc@175 233
adamc@256 234 Open Scope cps_scope.
adamc@175 235
adamc@256 236 (** In interpreting types, we treat continuations as functions with codomain [nat], choosing [nat] as our arbitrary program result type. *)
adamc@175 237
adamc@256 238 Fixpoint typeDenote (t : type) : Set :=
adamc@256 239 match t with
adamc@256 240 | Nat => nat
adamc@256 241 | t' ---> => typeDenote t' -> nat
adamc@256 242 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@256 243 end.
adamc@175 244
adamc@256 245 (** A mutually-recursive definition establishes the meanings of programs and primops. *)
adamc@175 246
adamc@256 247 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@256 248 match e with
adamc@256 249 | PHalt n => n
adamc@256 250 | App _ f x => f x
adamc@256 251 | Bind _ p x => progDenote (x (primopDenote p))
adamc@256 252 end
adamc@175 253
adamc@256 254 with primopDenote t (p : primop typeDenote t) : typeDenote t :=
adamc@256 255 match p with
adamc@256 256 | Const n => n
adamc@256 257 | Plus n1 n2 => n1 + n2
adamc@175 258
adamc@256 259 | Abs _ e => fun x => progDenote (e x)
adamc@175 260
adamc@256 261 | Pair _ _ v1 v2 => (v1, v2)
adamc@256 262 | Fst _ _ v => fst v
adamc@256 263 | Snd _ _ v => snd v
adamc@256 264 end.
adamc@256 265
adamc@256 266 Definition Prog := forall var, prog var.
adamc@256 267 Definition Primop t := forall var, primop var t.
adamc@256 268 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@256 269 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@256 270 End CPS.
adamc@256 271
adamc@256 272 Import Source CPS.
adamc@256 273
adamc@256 274 (** The translation itself begins with a type-level compilation function. We change every function into a continuation whose argument is a pair, consisting of the translation of the original argument and of an explicit return pointer. *)
adamc@175 275
adamc@180 276 (* begin thide *)
adamc@256 277 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@256 278 match t with
adamc@256 279 | Nat => Nat%cps
adamc@256 280 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@256 281 end%source.
adamc@175 282
adamc@256 283 (** Now we can define the expression translation. The notation [x <-- e1; e2] stands for translating source-level expression [e1], binding [x] to the CPS-level result of running the translated program, and then evaluating CPS-level expression [e2] in that context. *)
adamc@175 284
adamc@256 285 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 286
adamc@256 287 Section cpsExp.
adamc@256 288 Variable var : CPS.type -> Type.
adamc@175 289
adamc@256 290 Import Source.
adamc@256 291 Open Scope cps_scope.
adamc@175 292
adamc@256 293 (** We implement a well-known variety of higher-order, one-pass CPS translation. The translation [cpsExp] is parameterized not only by the expression [e] to translate, but also by a meta-level continuation. The idea is that [cpsExp] evaluates the translation of [e] and calls the continuation on the result. With this convention, [cpsExp] itself is a natural match for the notation we just reserved. *)
adamc@175 294
adamc@256 295 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t)
adamc@256 296 : (var (cpsType t) -> prog var) -> prog var :=
adamc@256 297 match e with
adamc@256 298 | Var _ v => fun k => k v
adamc@175 299
adamc@256 300 | Const n => fun k =>
adamc@256 301 x <- ^n;
adamc@256 302 k x
adamc@256 303 | Plus e1 e2 => fun k =>
adamc@256 304 x1 <-- e1;
adamc@256 305 x2 <-- e2;
adamc@256 306 x <- x1 +^ x2;
adamc@256 307 k x
adamc@175 308
adamc@256 309 | App _ _ e1 e2 => fun k =>
adamc@256 310 f <-- e1;
adamc@256 311 x <-- e2;
adamc@256 312 kf <- \r, k r;
adamc@256 313 p <- [x, kf];
adamc@256 314 f @@ p
adamc@256 315 | Abs _ _ e' => fun k =>
adamc@256 316 f <- CPS.Abs (var := var) (fun p =>
adamc@256 317 x <- #1 p;
adamc@256 318 kf <- #2 p;
adamc@256 319 r <-- e' x;
adamc@256 320 kf @@ r);
adamc@256 321 k f
adamc@256 322 end
adamc@175 323
adamc@256 324 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@256 325 End cpsExp.
adamc@256 326
adamc@256 327 (** Since notations do not survive the closing of sections, we redefine the notation associated with [cpsExp]. *)
adamc@256 328
adamc@256 329 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@256 330
adamc@256 331 Implicit Arguments cpsExp [var t].
adamc@256 332
adamc@256 333 (** We wrap [cpsExp] into the parametric version [CpsExp], passing an always-halt continuation at the root of the recursion. *)
adamc@256 334
adamc@256 335 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@256 336 fun _ => cpsExp (E _) (PHalt (var := _)).
adamc@180 337 (* end thide *)
adamc@175 338
adamc@256 339 Eval compute in CpsExp zero.
adamc@256 340 (** %\vspace{-.15in}% [[
adamc@256 341 = fun var : type -> Type => x <- ^0; Halt x
adamc@256 342 : Prog
adamc@256 343 ]] *)
adamc@175 344
adamc@256 345 Eval compute in CpsExp one.
adamc@256 346 (** %\vspace{-.15in}% [[
adamc@256 347 = fun var : type -> Type => x <- ^1; Halt x
adamc@256 348 : Prog
adamc@256 349 ]] *)
adamc@256 350
adamc@256 351 Eval compute in CpsExp zpo.
adamc@256 352 (** %\vspace{-.15in}% [[
adamc@256 353 = fun var : type -> Type => x <- ^0; x0 <- ^1; x1 <- (x +^ x0); Halt x1
adamc@256 354 : Prog
adamc@256 355 ]] *)
adamc@256 356
adamc@256 357 Eval compute in CpsExp app_ident.
adamc@256 358 (** %\vspace{-.15in}% [[
adamc@256 359 = fun var : type -> Type =>
adamc@256 360 f <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x);
adamc@256 361 x <- ^0;
adamc@256 362 x0 <- ^1; x1 <- (x +^ x0); kf <- (\ r, Halt r); p <- [x1, kf]; f @@ p
adamc@256 363 : Prog
adamc@256 364 ]] *)
adamc@256 365
adamc@256 366 Eval compute in CpsExp app_ident'.
adamc@256 367 (** %\vspace{-.15in}% [[
adamc@256 368 = fun var : type -> Type =>
adamc@256 369 f <-
adamc@256 370 (\ p,
adamc@256 371 x <- #1 p;
adamc@256 372 kf <- #2 p;
adamc@256 373 f <-
adamc@256 374 (\ p0,
adamc@256 375 x0 <- #1 p0;
adamc@256 376 kf0 <- #2 p0; kf1 <- (\ r, kf0 @@ r); p1 <- [x0, kf1]; x @@ p1);
adamc@256 377 kf @@ f);
adamc@256 378 f0 <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x);
adamc@256 379 kf <-
adamc@256 380 (\ r,
adamc@256 381 x <- ^0;
adamc@256 382 x0 <- ^1;
adamc@256 383 x1 <- (x +^ x0); kf <- (\ r0, Halt r0); p <- [x1, kf]; r @@ p);
adamc@256 384 p <- [f0, kf]; f @@ p
adamc@256 385 : Prog
adamc@256 386 ]] *)
adamc@256 387
adamc@256 388 Eval compute in ProgDenote (CpsExp zero).
adamc@256 389 (** %\vspace{-.15in}% [[
adamc@256 390 = 0
adamc@256 391 : nat
adamc@256 392 ]] *)
adamc@256 393
adamc@256 394 Eval compute in ProgDenote (CpsExp one).
adamc@256 395 (** %\vspace{-.15in}% [[
adamc@256 396 = 1
adamc@256 397 : nat
adamc@256 398 ]] *)
adamc@256 399
adamc@256 400 Eval compute in ProgDenote (CpsExp zpo).
adamc@256 401 (** %\vspace{-.15in}% [[
adamc@256 402 = 1
adamc@256 403 : nat
adamc@256 404 ]] *)
adamc@256 405
adamc@256 406 Eval compute in ProgDenote (CpsExp app_ident).
adamc@256 407 (** %\vspace{-.15in}% [[
adamc@256 408 = 1
adamc@256 409 : nat
adamc@256 410 ]] *)
adamc@256 411
adamc@256 412 Eval compute in ProgDenote (CpsExp app_ident').
adamc@256 413 (** %\vspace{-.15in}% [[
adamc@256 414 = 1
adamc@256 415 : nat
adamc@256 416 ]] *)
adamc@256 417
adamc@256 418
adamc@256 419 (** Our main inductive lemma about [cpsExp] needs a notion of compatibility between source-level and CPS-level values. We express compatibility with a %\textit{%#<i>#logical relation#</i>#%}%; that is, we define a binary relation by recursion on type structure, and the function case of the relation considers functions related if they map related arguments to related results. In detail, the function case is slightly more complicated, since it must deal with our continuation-based calling convention. *)
adamc@175 420
adamc@180 421 (* begin thide *)
adamc@256 422 Fixpoint lr (t : Source.type)
adamc@256 423 : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@256 424 match t with
adamc@256 425 | Nat => fun n1 n2 => n1 = n2
adamc@256 426 | t1 --> t2 => fun f1 f2 =>
adamc@256 427 forall x1 x2, lr _ x1 x2
adamc@256 428 -> forall k, exists r,
adamc@256 429 f2 (x2, k) = k r
adamc@256 430 /\ lr _ (f1 x1) r
adamc@256 431 end%source.
adamc@176 432
adamc@256 433 (** The main lemma is now easily stated and proved. The most surprising aspect of the statement is the presence of %\textit{%#<i>#two#</i>#%}% versions of the expression to be compiled. The first, [e1], uses a [var] choice that makes it a suitable argument to [expDenote]. The second expression, [e2], uses a [var] choice that makes its compilation, [cpsExp e2 k], a suitable argument to [progDenote]. We use [exp_equiv] to assert that [e1] and [e2] have the same underlying structure, up to a variable correspondence list [G]. A hypothesis about [G] ensures that all of its pairs of variables belong to the logical relation [lr]. We also use [lr], in concert with some quantification over continuations and program results, in the conclusion of the lemma.
adamc@256 434
adamc@256 435 The lemma's proof should be unsurprising by now. It uses our standard bag of Ltac tricks to help out with quantifier instantiation; [crush] and [eauto] can handle the rest. *)
adamc@256 436
adamc@256 437 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@256 438 exp_equiv G e1 e2
adamc@256 439 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@256 440 -> forall k, exists r,
adamc@256 441 progDenote (cpsExp e2 k) = progDenote (k r)
adamc@256 442 /\ lr t (expDenote e1) r.
adamc@256 443 induction 1; crush;
adamc@256 444 repeat (match goal with
adamc@256 445 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176 446 |- context[cpsExp ?E ?K] ] =>
adamc@256 447 generalize (H K); clear H
adamc@256 448 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@256 449 exists R
adamc@256 450 | [ t1 : Source.type |- _ ] =>
adamc@256 451 match goal with
adamc@256 452 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@256 453 generalize (IH X1 X2); clear IH; intro IH;
adamc@256 454 match type of IH with
adamc@256 455 | ?P -> _ => assert P
adamc@256 456 end
adamc@256 457 end
adamc@256 458 end; crush); eauto.
adamc@256 459 Qed.
adamc@176 460
adamc@256 461 (** A simple lemma establishes the degenerate case of [cpsExp_correct]'s hypothesis about [G]. *)
adamc@176 462
adamc@256 463 Lemma vars_easy : forall t v1 v2,
adamc@256 464 In (existT (fun t0 => (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@256 465 (v1, v2)) nil -> lr t v1 v2.
adamc@256 466 crush.
adamc@256 467 Qed.
adamc@256 468
adamc@256 469 (** A manual application of [cpsExp_correct] proves a version applicable to [CpsExp]. This is where we use the axiom [Exp_equiv]. *)
adamc@256 470
adamc@256 471 Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@256 472 ProgDenote (CpsExp E) = ExpDenote E.
adamc@256 473 unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@256 474 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@256 475 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@256 476 Qed.
adamc@180 477 (* end thide *)
adamc@176 478
adamc@177 479
adamc@181 480 (** * Exercises *)
adamc@181 481
adamc@181 482 (** %\begin{enumerate}%#<ol>#
adamc@181 483
adamc@181 484 %\item%#<li># When in the last chapter we implemented constant folding for simply-typed lambda calculus, it may have seemed natural to try applying beta reductions. This would have been a lot more trouble than is apparent at first, because we would have needed to convince Coq that our normalizing function always terminated.
adamc@181 485
adamc@181 486 It might also seem that beta reduction is a lost cause because we have no effective way of substituting in the [exp] type; we only managed to write a substitution function for the parametric [Exp] type. This is not as big of a problem as it seems. For instance, for the language we built by extending simply-typed lambda calculus with products and sums, it also appears that we need substitution for simplifying [case] expressions whose discriminees are known to be [inl] or [inr], but the function is still implementable.
adamc@181 487
adamc@200 488 For this exercise, extend the products and sums constant folder from the last chapter so that it simplifies [case] expressions as well, by checking if the discriminee is a known [inl] or known [inr]. Also extend the correctness theorem to apply to your new definition. You will probably want to assert an axiom relating to an expression equivalence relation like the one defined in this chapter. Any such axiom should only mention syntax; it should not mention any compilation or denotation functions. Following the format of the axiom from the last chapter is the safest bet to avoid proving a worthless theorem.
adamc@181 489 #</li>#
adamc@181 490
adamc@181 491 #</ol>#%\end{enumerate}% *)