Mercurial > cpdt > repo

annotate src/Extensional.v @ 305:690796f4690d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Further emphasize necessity and purpose of Set Implicit Arguments; tweak Makefile to support parallel builds
author Adam Chlipala <adam@chlipala.net>
date Wed, 03 Aug 2011 10:34:53 -0400
parents 7b38729be069
children d5787b70cf48
rev   line source
adam@297 1 (* Copyright (c) 2008-2011, 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
adam@297 13 Require Import 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.
adam@292 40 (** printing --> $\longrightarrow$ *)
adamc@256 41 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@175 42
adamc@256 43 Open Scope source_scope.
adamc@256 44 Bind Scope source_scope with type.
adamc@256 45 Delimit Scope source_scope with source.
adamc@175 46
adamc@256 47 (** 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 48
adamc@256 49 (* begin hide *)
adamc@256 50 Section vars.
adamc@256 51 Variable var : type -> Type.
adamc@175 52
adamc@256 53 Inductive exp : type -> Type :=
adamc@256 54 | Var : forall t,
adamc@256 55 var t
adamc@256 56 -> exp t
adamc@175 57
adamc@256 58 | Const : nat -> exp Nat
adamc@256 59 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@175 60
adamc@256 61 | App : forall t1 t2,
adamc@256 62 exp (t1 --> t2)
adamc@256 63 -> exp t1
adamc@256 64 -> exp t2
adamc@256 65 | Abs : forall t1 t2,
adamc@256 66 (var t1 -> exp t2)
adamc@256 67 -> exp (t1 --> t2).
adamc@256 68 End vars.
adamc@175 69
adamc@256 70 Definition Exp t := forall var, exp var t.
adamc@175 71
adamc@256 72 Implicit Arguments Var [var t].
adamc@256 73 Implicit Arguments Const [var].
adamc@256 74 Implicit Arguments Plus [var].
adamc@256 75 Implicit Arguments App [var t1 t2].
adamc@256 76 Implicit Arguments Abs [var t1 t2].
adamc@175 77
adamc@256 78 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@175 79
adamc@256 80 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@256 81 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@175 82
adamc@256 83 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@256 84 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@256 85 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@175 86
adamc@256 87 Bind Scope source_scope with exp.
adamc@256 88
adamc@257 89 Example zero : Exp Nat := fun _ => ^0.
adamc@257 90 Example one : Exp Nat := fun _ => ^1.
adamc@257 91 Example zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@257 92 Example ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@257 93 Example app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@257 94 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@256 95 \f, \x, #f @ #x.
adamc@257 96 Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@256 97
adamc@256 98 Fixpoint typeDenote (t : type) : Set :=
adamc@256 99 match t with
adamc@256 100 | Nat => nat
adamc@256 101 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@256 102 end.
adamc@256 103
adamc@256 104 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@256 105 match e with
adamc@256 106 | Var _ v => v
adamc@256 107
adamc@256 108 | Const n => n
adamc@256 109 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@256 110
adamc@256 111 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@256 112 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@256 113 end.
adamc@256 114
adamc@256 115 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@256 116 (* end hide *)
adamc@256 117
adamc@256 118 (** 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 119
adamc@180 120 (* begin thide *)
adamc@256 121 Section exp_equiv.
adamc@256 122 Variables var1 var2 : type -> Type.
adamc@176 123
adamc@256 124 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
adamc@256 125 -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@256 126 | EqVar : forall G t (v1 : var1 t) v2,
adamc@256 127 In (existT _ t (v1, v2)) G
adamc@256 128 -> exp_equiv G (#v1) (#v2)
adamc@176 129
adamc@256 130 | EqConst : forall G n,
adam@292 131 exp_equiv G (^ n) (^ n)
adamc@256 132 | EqPlus : forall G x1 y1 x2 y2,
adamc@256 133 exp_equiv G x1 x2
adamc@256 134 -> exp_equiv G y1 y2
adamc@256 135 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176 136
adamc@256 137 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@256 138 exp_equiv G f1 f2
adamc@256 139 -> exp_equiv G x1 x2
adamc@256 140 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@256 141 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@256 142 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@256 143 -> exp_equiv G (Abs f1) (Abs f2).
adamc@256 144 End exp_equiv.
adamc@176 145
adamc@256 146 (** 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 147
adamc@256 148 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@256 149 exp_equiv nil (E var1) (E var2).
adamc@180 150 (* end thide *)
adamc@256 151 End Source.
adamc@175 152
adamc@256 153 (** 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 154
adamc@256 155 Module CPS.
adamc@256 156 Inductive type : Type :=
adamc@256 157 | TNat : type
adamc@256 158 | Cont : type -> type
adamc@256 159 | Prod : type -> type -> type.
adamc@175 160
adamc@256 161 Notation "'Nat'" := TNat : cps_scope.
adam@292 162 (** printing ---> $\Longrightarrow$ *)
adamc@256 163 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@256 164 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 165
adamc@256 166 Bind Scope cps_scope with type.
adamc@256 167 Delimit Scope cps_scope with cps.
adamc@175 168
adamc@256 169 Section vars.
adamc@256 170 Variable var : type -> Type.
adamc@175 171
adamc@256 172 (** 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 173
adamc@256 174 Inductive prog : Type :=
adamc@256 175 | PHalt :
adamc@256 176 var Nat
adamc@256 177 -> prog
adamc@256 178 | App : forall t,
adamc@256 179 var (t --->)
adamc@256 180 -> var t
adamc@256 181 -> prog
adamc@256 182 | Bind : forall t,
adamc@256 183 primop t
adamc@256 184 -> (var t -> prog)
adamc@256 185 -> prog
adamc@175 186
adamc@256 187 with primop : type -> Type :=
adamc@256 188 | Const : nat -> primop Nat
adamc@256 189 | Plus : var Nat -> var Nat -> primop Nat
adamc@256 190
adamc@256 191 | Abs : forall t,
adamc@256 192 (var t -> prog)
adamc@256 193 -> primop (t --->)
adamc@175 194
adamc@256 195 | Pair : forall t1 t2,
adamc@256 196 var t1
adamc@256 197 -> var t2
adamc@256 198 -> primop (t1 ** t2)
adamc@256 199 | Fst : forall t1 t2,
adamc@256 200 var (t1 ** t2)
adamc@256 201 -> primop t1
adamc@256 202 | Snd : forall t1 t2,
adamc@256 203 var (t1 ** t2)
adamc@256 204 -> primop t2.
adamc@256 205 End vars.
adamc@175 206
adamc@256 207 Implicit Arguments PHalt [var].
adamc@256 208 Implicit Arguments App [var t].
adamc@175 209
adamc@256 210 Implicit Arguments Const [var].
adamc@256 211 Implicit Arguments Plus [var].
adamc@256 212 Implicit Arguments Abs [var t].
adamc@256 213 Implicit Arguments Pair [var t1 t2].
adamc@256 214 Implicit Arguments Fst [var t1 t2].
adamc@256 215 Implicit Arguments Snd [var t1 t2].
adamc@175 216
adamc@256 217 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@256 218 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@256 219 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@256 220 (right associativity, at level 76, p at next level) : cps_scope.
adamc@256 221 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@256 222 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 223
adamc@256 224 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@256 225 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 226
adamc@256 227 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@256 228 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 229
adamc@256 230 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
adamc@256 231 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@256 232 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 233
adamc@256 234 Bind Scope cps_scope with prog primop.
adamc@175 235
adamc@256 236 Open Scope cps_scope.
adamc@175 237
adamc@256 238 (** In interpreting types, we treat continuations as functions with codomain [nat], choosing [nat] as our arbitrary program result type. *)
adamc@175 239
adamc@256 240 Fixpoint typeDenote (t : type) : Set :=
adamc@256 241 match t with
adamc@256 242 | Nat => nat
adamc@256 243 | t' ---> => typeDenote t' -> nat
adamc@256 244 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@256 245 end.
adamc@175 246
adamc@256 247 (** A mutually-recursive definition establishes the meanings of programs and primops. *)
adamc@175 248
adamc@256 249 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@256 250 match e with
adamc@256 251 | PHalt n => n
adamc@256 252 | App _ f x => f x
adamc@256 253 | Bind _ p x => progDenote (x (primopDenote p))
adamc@256 254 end
adamc@175 255
adamc@256 256 with primopDenote t (p : primop typeDenote t) : typeDenote t :=
adamc@256 257 match p with
adamc@256 258 | Const n => n
adamc@256 259 | Plus n1 n2 => n1 + n2
adamc@175 260
adamc@256 261 | Abs _ e => fun x => progDenote (e x)
adamc@175 262
adamc@256 263 | Pair _ _ v1 v2 => (v1, v2)
adamc@256 264 | Fst _ _ v => fst v
adamc@256 265 | Snd _ _ v => snd v
adamc@256 266 end.
adamc@256 267
adamc@256 268 Definition Prog := forall var, prog var.
adamc@256 269 Definition Primop t := forall var, primop var t.
adamc@256 270 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@256 271 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@256 272 End CPS.
adamc@256 273
adamc@256 274 Import Source CPS.
adamc@256 275
adamc@256 276 (** 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 277
adamc@180 278 (* begin thide *)
adamc@256 279 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@256 280 match t with
adamc@256 281 | Nat => Nat%cps
adam@292 282 | t1 --> t2 => (cpsType t1 ** (cpsType t2 ---> ) ---> )%cps
adamc@256 283 end%source.
adamc@175 284
adamc@256 285 (** 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 286
adam@292 287 (** printing <-- $\longleftarrow$ *)
adamc@256 288 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 289
adamc@256 290 Section cpsExp.
adamc@256 291 Variable var : CPS.type -> Type.
adamc@175 292
adamc@256 293 Import Source.
adamc@256 294 Open Scope cps_scope.
adamc@175 295
adamc@256 296 (** 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 297
adamc@256 298 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t)
adamc@256 299 : (var (cpsType t) -> prog var) -> prog var :=
adamc@256 300 match e with
adamc@256 301 | Var _ v => fun k => k v
adamc@175 302
adamc@256 303 | Const n => fun k =>
adam@292 304 x <- ^ n;
adamc@256 305 k x
adamc@256 306 | Plus e1 e2 => fun k =>
adamc@256 307 x1 <-- e1;
adamc@256 308 x2 <-- e2;
adamc@256 309 x <- x1 +^ x2;
adamc@256 310 k x
adamc@175 311
adamc@256 312 | App _ _ e1 e2 => fun k =>
adamc@256 313 f <-- e1;
adamc@256 314 x <-- e2;
adam@292 315 kf <- \ r, k r;
adamc@256 316 p <- [x, kf];
adamc@256 317 f @@ p
adamc@256 318 | Abs _ _ e' => fun k =>
adamc@256 319 f <- CPS.Abs (var := var) (fun p =>
adamc@256 320 x <- #1 p;
adamc@256 321 kf <- #2 p;
adamc@256 322 r <-- e' x;
adamc@256 323 kf @@ r);
adamc@256 324 k f
adamc@256 325 end
adamc@175 326
adamc@256 327 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@256 328 End cpsExp.
adamc@256 329
adamc@256 330 (** Since notations do not survive the closing of sections, we redefine the notation associated with [cpsExp]. *)
adamc@256 331
adamc@256 332 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@256 333
adamc@256 334 Implicit Arguments cpsExp [var t].
adamc@256 335
adamc@256 336 (** We wrap [cpsExp] into the parametric version [CpsExp], passing an always-halt continuation at the root of the recursion. *)
adamc@256 337
adamc@256 338 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@256 339 fun _ => cpsExp (E _) (PHalt (var := _)).
adamc@180 340 (* end thide *)
adamc@175 341
adamc@256 342 Eval compute in CpsExp zero.
adamc@256 343 (** %\vspace{-.15in}% [[
adamc@256 344 = fun var : type -> Type => x <- ^0; Halt x
adamc@256 345 : Prog
adam@302 346 ]]
adam@302 347 *)
adamc@175 348
adamc@256 349 Eval compute in CpsExp one.
adamc@256 350 (** %\vspace{-.15in}% [[
adamc@256 351 = fun var : type -> Type => x <- ^1; Halt x
adamc@256 352 : Prog
adam@302 353 ]]
adam@302 354 *)
adamc@256 355
adamc@256 356 Eval compute in CpsExp zpo.
adamc@256 357 (** %\vspace{-.15in}% [[
adamc@256 358 = fun var : type -> Type => x <- ^0; x0 <- ^1; x1 <- (x +^ x0); Halt x1
adamc@256 359 : Prog
adam@302 360 ]]
adam@302 361 *)
adamc@256 362
adamc@256 363 Eval compute in CpsExp app_ident.
adamc@256 364 (** %\vspace{-.15in}% [[
adamc@256 365 = fun var : type -> Type =>
adamc@256 366 f <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x);
adamc@256 367 x <- ^0;
adamc@256 368 x0 <- ^1; x1 <- (x +^ x0); kf <- (\ r, Halt r); p <- [x1, kf]; f @@ p
adamc@256 369 : Prog
adam@302 370 ]]
adam@302 371 *)
adamc@256 372
adamc@256 373 Eval compute in CpsExp app_ident'.
adamc@256 374 (** %\vspace{-.15in}% [[
adamc@256 375 = fun var : type -> Type =>
adamc@256 376 f <-
adamc@256 377 (\ p,
adamc@256 378 x <- #1 p;
adamc@256 379 kf <- #2 p;
adamc@256 380 f <-
adamc@256 381 (\ p0,
adamc@256 382 x0 <- #1 p0;
adamc@256 383 kf0 <- #2 p0; kf1 <- (\ r, kf0 @@ r); p1 <- [x0, kf1]; x @@ p1);
adamc@256 384 kf @@ f);
adamc@256 385 f0 <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x);
adamc@256 386 kf <-
adamc@256 387 (\ r,
adamc@256 388 x <- ^0;
adamc@256 389 x0 <- ^1;
adamc@256 390 x1 <- (x +^ x0); kf <- (\ r0, Halt r0); p <- [x1, kf]; r @@ p);
adamc@256 391 p <- [f0, kf]; f @@ p
adamc@256 392 : Prog
adam@302 393 ]]
adam@302 394 *)
adamc@256 395
adamc@256 396 Eval compute in ProgDenote (CpsExp zero).
adamc@256 397 (** %\vspace{-.15in}% [[
adamc@256 398 = 0
adamc@256 399 : nat
adam@302 400 ]]
adam@302 401 *)
adamc@256 402
adamc@256 403 Eval compute in ProgDenote (CpsExp one).
adamc@256 404 (** %\vspace{-.15in}% [[
adamc@256 405 = 1
adamc@256 406 : nat
adam@302 407 ]]
adam@302 408 *)
adamc@256 409
adamc@256 410 Eval compute in ProgDenote (CpsExp zpo).
adamc@256 411 (** %\vspace{-.15in}% [[
adamc@256 412 = 1
adamc@256 413 : nat
adam@302 414 ]]
adam@302 415 *)
adamc@256 416
adamc@256 417 Eval compute in ProgDenote (CpsExp app_ident).
adamc@256 418 (** %\vspace{-.15in}% [[
adamc@256 419 = 1
adamc@256 420 : nat
adam@302 421 ]]
adam@302 422 *)
adamc@256 423
adamc@256 424 Eval compute in ProgDenote (CpsExp app_ident').
adamc@256 425 (** %\vspace{-.15in}% [[
adamc@256 426 = 1
adamc@256 427 : nat
adam@302 428 ]]
adam@302 429 *)
adamc@256 430
adamc@256 431
adamc@256 432 (** 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 433
adamc@180 434 (* begin thide *)
adamc@256 435 Fixpoint lr (t : Source.type)
adamc@256 436 : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@256 437 match t with
adamc@256 438 | Nat => fun n1 n2 => n1 = n2
adamc@256 439 | t1 --> t2 => fun f1 f2 =>
adamc@256 440 forall x1 x2, lr _ x1 x2
adamc@256 441 -> forall k, exists r,
adamc@256 442 f2 (x2, k) = k r
adamc@256 443 /\ lr _ (f1 x1) r
adamc@256 444 end%source.
adamc@176 445
adamc@256 446 (** 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 447
adamc@256 448 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 449
adamc@256 450 Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@256 451 exp_equiv G e1 e2
adamc@256 452 -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@256 453 -> forall k, exists r,
adamc@256 454 progDenote (cpsExp e2 k) = progDenote (k r)
adamc@256 455 /\ lr t (expDenote e1) r.
adamc@256 456 induction 1; crush;
adamc@256 457 repeat (match goal with
adamc@256 458 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176 459 |- context[cpsExp ?E ?K] ] =>
adamc@256 460 generalize (H K); clear H
adamc@256 461 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@256 462 exists R
adamc@256 463 | [ t1 : Source.type |- _ ] =>
adamc@256 464 match goal with
adamc@256 465 | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@256 466 generalize (IH X1 X2); clear IH; intro IH;
adamc@256 467 match type of IH with
adamc@256 468 | ?P -> _ => assert P
adamc@256 469 end
adamc@256 470 end
adamc@256 471 end; crush); eauto.
adamc@256 472 Qed.
adamc@176 473
adamc@256 474 (** A simple lemma establishes the degenerate case of [cpsExp_correct]'s hypothesis about [G]. *)
adamc@176 475
adamc@256 476 Lemma vars_easy : forall t v1 v2,
adamc@256 477 In (existT (fun t0 => (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@256 478 (v1, v2)) nil -> lr t v1 v2.
adamc@256 479 crush.
adamc@256 480 Qed.
adamc@256 481
adamc@256 482 (** A manual application of [cpsExp_correct] proves a version applicable to [CpsExp]. This is where we use the axiom [Exp_equiv]. *)
adamc@256 483
adamc@256 484 Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@256 485 ProgDenote (CpsExp E) = ExpDenote E.
adamc@256 486 unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@256 487 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@256 488 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@256 489 Qed.
adamc@180 490 (* end thide *)
adamc@176 491
adamc@177 492
adamc@181 493 (** * Exercises *)
adamc@181 494
adamc@181 495 (** %\begin{enumerate}%#<ol>#
adamc@181 496
adamc@181 497 %\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 498
adamc@181 499 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 500
adamc@200 501 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 502 #</li>#
adamc@181 503
adamc@181 504 #</ol>#%\end{enumerate}% *)