Mercurial > cpdt > repo

annotate src/OpSem.v @ 324:06d11a6363cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New LogicProg chapter
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Sep 2011 14:07:21 -0400
parents d5787b70cf48
children
rev   line source
adam@292 1 (* Copyright (c) 2009-2010, Adam Chlipala
adamc@190 2 *
adamc@190 3 * This work is licensed under a
adamc@190 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@190 5 * Unported License.
adamc@190 6 * The license text is available at:
adamc@190 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@190 8 *)
adamc@190 9
adamc@262 10 (* begin hide *)
adamc@262 11 Require Import Arith List.
adamc@190 12
adam@314 13 Require Import CpdtTactics.
adamc@190 14
adamc@262 15 Set Implicit Arguments.
adamc@262 16 (* end hide *)
adamc@190 17
adamc@262 18
adamc@262 19 (** %\chapter{Higher-Order Operational Semantics}% *)
adamc@262 20
adamc@263 21 (** The last few chapters have shown how PHOAS can make it relatively painless to reason about program transformations. Each of our example languages so far has had a semantics that is easy to implement with an interpreter in Gallina. Since Gallina is designed to rule out non-termination, we cannot hope to give interpreter-based semantics to Turing-complete programming languages. Falling back on standard operational semantics leaves us with the old bureaucratic concerns about capture-avoiding substitution. Can we encode Turing-complete, higher-order languages in Coq without sacrificing the advantages of higher-order encoding?
adamc@263 22
adam@292 23 Any approach that applies to basic untyped lambda calculus is likely to extend to most object languages of interest. We can attempt the %``%#"#obvious#"#%''% way of equipping a PHOAS definition for use in an operational semantics, without mentioning substitution explicitly. Specifically, we try to work with expressions with [var] instantiated with a type of values. *)
adamc@263 24
adamc@263 25 Section exp.
adamc@263 26 Variable var : Type.
adamc@263 27
adamc@263 28 Inductive exp : Type :=
adamc@263 29 | Var : var -> exp
adamc@263 30 | App : exp -> exp -> exp
adamc@263 31 | Abs : (var -> exp) -> exp.
adamc@263 32 End exp.
adamc@263 33
adamc@263 34 (** [[
adamc@263 35 Inductive val : Type :=
adamc@263 36 | VAbs : (val -> exp val) -> val.
adamc@263 37
adamc@263 38 Error: Non strictly positive occurrence of "val" in
adamc@263 39 "(val -> exp val) -> val".
adamc@263 40
adamc@263 41 ]]
adamc@263 42
adamc@263 43 We would like to represent values (which are all function abstractions) as functions from variables to expressions, where we represent variables as the same value type that we are defining. That way, a value can be substituted in a function body simply by applying the body to the value. Unfortunately, the positivity restriction rejects this definition, for much the same reason that we could not use the classical HOAS encoding.
adamc@263 44
adamc@263 45 We can try an alternate approach based on defining [val] like a usual class of syntax. *)
adamc@263 46
adamc@263 47 Section val.
adamc@263 48 Variable var : Type.
adamc@263 49
adamc@263 50 Inductive val : Type :=
adamc@263 51 | VAbs : (var -> exp var) -> val.
adamc@263 52 End val.
adamc@263 53
adamc@263 54 (** Now the puzzle is how to write the type of an expression whose variables are represented as values. We would like to be able to write a recursive definition like this one:
adamc@263 55
adamc@263 56 [[
adamc@263 57 Fixpoint expV := exp (val expV).
adamc@263 58
adamc@263 59 ]]
adamc@263 60
adam@292 61 Of course, this kind of definition is not structurally recursive, so Coq will not allow it. Getting %``%#"#substitution for free#"#%''% seems to require some similar kind of self-reference.
adamc@263 62
adamc@263 63 In this chapter, we will consider an alternate take on the problem. We add a level of indirection, introducing more explicit syntax to break the cycle in type definitions. Specifically, we represent function values as numbers that index into a %\emph{%#<i>#closure heap#</i>#%}% that our operational semantics maintains alongside the expression being evaluated. *)
adamc@263 64
adamc@263 65
adamc@262 66 (** * Closure Heaps *)
adamc@262 67
adamc@263 68 (** The essence of the technique is to store function bodies in lists that are extended monotonically as function abstractions are evaluated. We can define a set of functions and theorems that implement the core functionality generically. *)
adamc@263 69
adamc@262 70 Section lookup.
adamc@262 71 Variable A : Type.
adamc@262 72
adamc@263 73 (** We start with a [lookup] function that generalizes last chapter's function of the same name. It selects the element at a particular position in a list, where we number the elements starting from the end of the list, so that prepending new elements does not change the indices of old elements. *)
adamc@263 74
adamc@262 75 Fixpoint lookup (ls : list A) (n : nat) : option A :=
adamc@262 76 match ls with
adamc@262 77 | nil => None
adamc@262 78 | v :: ls' => if eq_nat_dec n (length ls') then Some v else lookup ls' n
adamc@262 79 end.
adamc@262 80
adamc@263 81 Infix "##" := lookup (left associativity, at level 1).
adamc@263 82
adamc@263 83 (** The second of our two definitions expresses when one list extends another. We will write [ls1 ~> ls2] to indicate that [ls1] could evolve into [ls2]; that is, [ls1] is a suffix of [ls2]. *)
adamc@263 84
adamc@262 85 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1.
adam@292 86 (** printing ~> $\leadsto$ *)
adamc@263 87 Infix "~>" := extends (no associativity, at level 80).
adamc@262 88
adamc@263 89 (** We prove and add as hints a few basic theorems about [lookup] and [extends]. *)
adamc@262 90
adamc@262 91 Theorem lookup1 : forall x ls,
adamc@262 92 (x :: ls) ## (length ls) = Some x.
adamc@262 93 crush; match goal with
adamc@262 94 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262 95 end; crush.
adamc@262 96 Qed.
adamc@262 97
adamc@262 98 Theorem extends_refl : forall ls, ls ~> ls.
adamc@262 99 exists nil; reflexivity.
adamc@262 100 Qed.
adamc@262 101
adamc@262 102 Theorem extends1 : forall v ls, ls ~> v :: ls.
adamc@262 103 intros; exists (v :: nil); reflexivity.
adamc@262 104 Qed.
adamc@262 105
adamc@262 106 Theorem extends_trans : forall ls1 ls2 ls3,
adamc@262 107 ls1 ~> ls2
adamc@262 108 -> ls2 ~> ls3
adamc@262 109 -> ls1 ~> ls3.
adamc@262 110 intros ? ? ? [l1 ?] [l2 ?]; exists (l2 ++ l1); crush.
adamc@262 111 Qed.
adamc@262 112
adamc@262 113 Lemma lookup_contra : forall n v ls,
adamc@262 114 ls ## n = Some v
adamc@262 115 -> n >= length ls
adamc@262 116 -> False.
adamc@262 117 induction ls; crush;
adamc@262 118 match goal with
adamc@262 119 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@262 120 end; crush.
adamc@262 121 Qed.
adamc@262 122
adamc@262 123 Hint Resolve lookup_contra.
adamc@262 124
adamc@262 125 Theorem extends_lookup : forall ls1 ls2 n v,
adamc@262 126 ls1 ~> ls2
adamc@262 127 -> ls1 ## n = Some v
adamc@262 128 -> ls2 ## n = Some v.
adamc@262 129 intros ? ? ? ? [l ?]; crush; induction l; crush;
adamc@262 130 match goal with
adamc@262 131 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262 132 end; crush; elimtype False; eauto.
adamc@262 133 Qed.
adamc@262 134 End lookup.
adamc@262 135
adamc@262 136 Infix "##" := lookup (left associativity, at level 1).
adamc@262 137 Infix "~>" := extends (no associativity, at level 80).
adamc@262 138
adamc@262 139 Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup.
adamc@262 140
adamc@263 141 (** We are dealing explicitly with the nitty-gritty of closure heaps. Why is this better than dealing with the nitty-gritty of variables? The inconvenience of modeling lambda calculus-style binders comes from the presence of nested scopes. Program evaluation will only involve one %\emph{%#<i>#global#</i>#%}% closure heap. Also, the short development that we just finished can be reused for many different object languages. None of these definitions or theorems needs to be redone to handle specific object language features. By adding the theorems as hints, no per-object-language effort is required to apply the critical facts as needed. *)
adamc@263 142
adamc@262 143
adamc@262 144 (** * Languages and Translation *)
adamc@262 145
adamc@263 146 (** For the rest of this chapter, we will consider the example of CPS translation for untyped lambda calculus with boolean constants. It is convenient to include these constants, because their presence makes it easy to state a final translation correctness theorem. *)
adamc@263 147
adamc@262 148 Module Source.
adamc@263 149 (** We define the syntax of source expressions in our usual way. *)
adamc@263 150
adamc@262 151 Section exp.
adamc@262 152 Variable var : Type.
adamc@262 153
adamc@262 154 Inductive exp : Type :=
adamc@262 155 | Var : var -> exp
adamc@262 156 | App : exp -> exp -> exp
adamc@262 157 | Abs : (var -> exp) -> exp
adamc@262 158 | Bool : bool -> exp.
adamc@262 159 End exp.
adamc@262 160
adamc@262 161 Implicit Arguments Bool [var].
adamc@262 162
adamc@262 163 Definition Exp := forall var, exp var.
adamc@262 164
adamc@263 165 (** We will implement a big-step operational semantics, where expressions are mapped to values. A value is either a function or a boolean. We represent a function as a number that will be interpreted as an index into the global closure heap. *)
adamc@263 166
adamc@262 167 Inductive val : Set :=
adamc@262 168 | VFun : nat -> val
adamc@262 169 | VBool : bool -> val.
adamc@262 170
adamc@263 171 (** A closure, then, follows the usual representation of function abstraction bodies, where we represent variables as values. *)
adamc@263 172
adamc@262 173 Definition closure := val -> exp val.
adamc@262 174 Definition closures := list closure.
adamc@262 175
adamc@263 176 (** Our evaluation relation has four places. We map an initial closure heap and an expression into a final closure heap and a value. The interesting cases are for [Abs], where we push the body onto the closure heap; and for [App], where we perform a lookup in a closure heap, to find the proper function body to execute next. *)
adamc@263 177
adamc@262 178 Inductive eval : closures -> exp val -> closures -> val -> Prop :=
adamc@262 179 | EvVar : forall cs v,
adamc@262 180 eval cs (Var v) cs v
adamc@262 181
adamc@262 182 | EvApp : forall cs1 e1 e2 cs2 v1 c cs3 v2 cs4 v3,
adamc@262 183 eval cs1 e1 cs2 (VFun v1)
adamc@262 184 -> eval cs2 e2 cs3 v2
adamc@262 185 -> cs2 ## v1 = Some c
adamc@262 186 -> eval cs3 (c v2) cs4 v3
adamc@262 187 -> eval cs1 (App e1 e2) cs4 v3
adamc@262 188
adamc@262 189 | EvAbs : forall cs c,
adamc@262 190 eval cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262 191
adamc@262 192 | EvBool : forall cs b,
adamc@262 193 eval cs (Bool b) cs (VBool b).
adamc@262 194
adamc@263 195 (** A simple wrapper produces an evaluation relation suitable for use on the main expression type [Exp]. *)
adamc@263 196
adamc@263 197 Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) :=
adamc@263 198 eval cs1 (E _) cs2 v.
adamc@263 199
adamc@263 200 (** To prove our translation's correctness, we will need the usual notions of expression equivalence and well-formedness. *)
adamc@262 201
adamc@262 202 Section exp_equiv.
adamc@262 203 Variables var1 var2 : Type.
adamc@262 204
adamc@262 205 Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop :=
adamc@262 206 | EqVar : forall G v1 v2,
adamc@262 207 In (v1, v2) G
adamc@262 208 -> exp_equiv G (Var v1) (Var v2)
adamc@262 209
adamc@262 210 | EqApp : forall G f1 x1 f2 x2,
adamc@262 211 exp_equiv G f1 f2
adamc@262 212 -> exp_equiv G x1 x2
adamc@262 213 -> exp_equiv G (App f1 x1) (App f2 x2)
adamc@262 214 | EqAbs : forall G f1 f2,
adamc@262 215 (forall v1 v2, exp_equiv ((v1, v2) :: G) (f1 v1) (f2 v2))
adamc@262 216 -> exp_equiv G (Abs f1) (Abs f2)
adamc@262 217
adamc@262 218 | EqBool : forall G b,
adamc@262 219 exp_equiv G (Bool b) (Bool b).
adamc@262 220 End exp_equiv.
adamc@262 221
adamc@262 222 Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2).
adamc@262 223 End Source.
adamc@262 224
adamc@263 225 (** Our target language can be defined without introducing any additional tricks. *)
adamc@263 226
adamc@262 227 Module CPS.
adamc@262 228 Section exp.
adamc@262 229 Variable var : Type.
adamc@262 230
adamc@262 231 Inductive prog : Type :=
adamc@262 232 | Halt : var -> prog
adamc@262 233 | App : var -> var -> prog
adamc@262 234 | Bind : primop -> (var -> prog) -> prog
adamc@262 235
adamc@262 236 with primop : Type :=
adamc@262 237 | Abs : (var -> prog) -> primop
adamc@262 238
adamc@262 239 | Bool : bool -> primop
adamc@262 240
adamc@262 241 | Pair : var -> var -> primop
adamc@262 242 | Fst : var -> primop
adamc@262 243 | Snd : var -> primop.
adamc@262 244 End exp.
adamc@262 245
adamc@262 246 Implicit Arguments Bool [var].
adamc@262 247
adamc@262 248 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@262 249 (right associativity, at level 76, p at next level).
adamc@262 250
adamc@262 251 Definition Prog := forall var, prog var.
adamc@262 252 Definition Primop := forall var, primop var.
adamc@262 253
adamc@262 254 Inductive val : Type :=
adamc@262 255 | VFun : nat -> val
adamc@262 256 | VBool : bool -> val
adamc@262 257 | VPair : val -> val -> val.
adamc@262 258 Definition closure := val -> prog val.
adamc@262 259 Definition closures := list closure.
adamc@262 260
adamc@262 261 Inductive eval : closures -> prog val -> val -> Prop :=
adamc@262 262 | EvHalt : forall cs v,
adamc@262 263 eval cs (Halt v) v
adamc@262 264
adamc@262 265 | EvApp : forall cs n v2 c v3,
adamc@262 266 cs ## n = Some c
adamc@262 267 -> eval cs (c v2) v3
adamc@262 268 -> eval cs (App (VFun n) v2) v3
adamc@262 269
adamc@262 270 | EvBind : forall cs1 p e cs2 v1 v2,
adamc@262 271 evalP cs1 p cs2 v1
adamc@262 272 -> eval cs2 (e v1) v2
adamc@262 273 -> eval cs1 (Bind p e) v2
adamc@262 274
adamc@262 275 with evalP : closures -> primop val -> closures -> val -> Prop :=
adamc@262 276 | EvAbs : forall cs c,
adamc@262 277 evalP cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262 278
adamc@262 279 | EvPair : forall cs v1 v2,
adamc@262 280 evalP cs (Pair v1 v2) cs (VPair v1 v2)
adamc@262 281 | EvFst : forall cs v1 v2,
adamc@262 282 evalP cs (Fst (VPair v1 v2)) cs v1
adamc@262 283 | EvSnd : forall cs v1 v2,
adamc@262 284 evalP cs (Snd (VPair v1 v2)) cs v2
adamc@262 285
adamc@262 286 | EvBool : forall cs b,
adamc@262 287 evalP cs (Bool b) cs (VBool b).
adamc@262 288
adamc@262 289 Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v.
adamc@262 290 End CPS.
adamc@262 291
adamc@262 292 Import Source CPS.
adamc@262 293
adamc@263 294 (** Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus. *)
adamc@263 295
adam@292 296 (** printing <-- $\longleftarrow$ *)
adamc@262 297 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@262 298
adamc@262 299 Section cpsExp.
adamc@262 300 Variable var : Type.
adamc@262 301
adamc@262 302 Import Source.
adamc@262 303
adamc@262 304 Fixpoint cpsExp (e : exp var)
adamc@262 305 : (var -> prog var) -> prog var :=
adamc@262 306 match e with
adamc@262 307 | Var v => fun k => k v
adamc@262 308
adamc@262 309 | App e1 e2 => fun k =>
adamc@262 310 f <-- e1;
adamc@262 311 x <-- e2;
adamc@262 312 kf <- CPS.Abs k;
adamc@262 313 p <- Pair x kf;
adamc@262 314 CPS.App f p
adamc@262 315 | Abs e' => fun k =>
adamc@262 316 f <- CPS.Abs (var := var) (fun p =>
adamc@262 317 x <- Fst p;
adamc@262 318 kf <- Snd p;
adamc@262 319 r <-- e' x;
adamc@262 320 CPS.App kf r);
adamc@262 321 k f
adamc@262 322
adamc@262 323 | Bool b => fun k =>
adamc@262 324 x <- CPS.Bool b;
adamc@262 325 k x
adamc@262 326 end
adamc@262 327
adamc@262 328 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262 329 End cpsExp.
adamc@262 330
adamc@262 331 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262 332
adamc@262 333 Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)).
adamc@262 334
adamc@262 335
adamc@262 336 (** * Correctness Proof *)
adamc@262 337
adamc@263 338 (** Our proof for simply-typed lambda calculus relied on a logical relation to state the key induction hypothesis. Since logical relations proceed by recursion on type structure, we cannot apply them directly in an untyped setting. Instead, we will use an inductive judgment to relate source-level and CPS-level values. First, it is helpful to define an abbreviation for the compiled version of a function body. *)
adamc@263 339
adamc@262 340 Definition cpsFunc var (e' : var -> Source.exp var) :=
adamc@262 341 fun p : var =>
adamc@262 342 x <- Fst p;
adamc@262 343 kf <- Snd p;
adamc@262 344 r <-- e' x;
adamc@262 345 CPS.App kf r.
adamc@262 346
adamc@263 347 (** Now we can define our correctness relation [cr], which is parameterized by source-level and CPS-level closure heaps. *)
adamc@263 348
adamc@262 349 Section cr.
adamc@262 350 Variable s1 : Source.closures.
adamc@262 351 Variable s2 : CPS.closures.
adamc@262 352
adamc@262 353 Import Source.
adamc@262 354
adamc@263 355 (** Only equal booleans are related. For two function addresses [l1] and [l2] to be related, they must point to valid functions in their respective closure heaps. The address [l1] must point to a function [f1], and [l2] must point to the result of compiling function [f2]. Further, [f1] and [f2] must be equivalent syntactically in some variable environment [G], and every variable pair in [G] must itself belong to the relation we are defining. *)
adamc@263 356
adamc@262 357 Inductive cr : Source.val -> CPS.val -> Prop :=
adamc@263 358 | CrBool : forall b,
adamc@263 359 cr (Source.VBool b) (CPS.VBool b)
adamc@263 360
adamc@262 361 | CrFun : forall l1 l2 G f1 f2,
adamc@262 362 (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2))
adamc@262 363 -> (forall x1 x2, In (x1, x2) G -> cr x1 x2)
adamc@262 364 -> s1 ## l1 = Some f1
adamc@262 365 -> s2 ## l2 = Some (cpsFunc f2)
adamc@263 366 -> cr (Source.VFun l1) (CPS.VFun l2).
adamc@262 367 End cr.
adamc@262 368
adam@292 369 (** printing |-- $\vdash$ *)
adam@292 370 (** printing ~~ $\sim$ *)
adamc@262 371 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70).
adamc@262 372
adamc@262 373 Hint Constructors cr.
adamc@262 374
adamc@263 375 (** To prove our main lemma, it will be useful to know that source-level evaluation never removes old closures from a closure heap. *)
adamc@263 376
adamc@262 377 Lemma eval_monotone : forall cs1 e cs2 v,
adamc@262 378 Source.eval cs1 e cs2 v
adamc@262 379 -> cs1 ~> cs2.
adamc@262 380 induction 1; crush; eauto.
adamc@262 381 Qed.
adamc@262 382
adamc@263 383 (** Further, [cr] continues to hold when its closure heap arguments are evolved in legal ways. *)
adamc@263 384
adamc@262 385 Lemma cr_monotone : forall cs1 cs2 cs1' cs2',
adamc@262 386 cs1 ~> cs1'
adamc@262 387 -> cs2 ~> cs2'
adamc@262 388 -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2
adamc@262 389 -> cs1' & cs2' |-- v1 ~~ v2.
adamc@262 390 induction 3; crush; eauto.
adamc@262 391 Qed.
adamc@262 392
adamc@262 393 Hint Resolve eval_monotone cr_monotone.
adamc@262 394
adamc@263 395 (** We state a trivial fact about the validity of variable environments, so that we may add this fact as a hint that [eauto] will apply. *)
adamc@263 396
adamc@262 397 Lemma push : forall G s1 s2 v1' v2',
adamc@262 398 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262 399 -> s1 & s2 |-- v1' ~~ v2'
adamc@262 400 -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2).
adamc@262 401 crush.
adamc@262 402 Qed.
adamc@262 403
adamc@262 404 Hint Resolve push.
adamc@262 405
adamc@263 406 (** Our final preparation for the main lemma involves adding effective hints about the CPS language's operational semantics. The following tactic performs one step of evaluation. It uses the Ltac code [eval hnf in e] to compute the %\emph{%#<i>#head normal form#</i>#%}% of [e], where the head normal form of an expression in an inductive type is an application of one of that inductive type's constructors. The final line below uses [solve] to ensure that we only take a [Bind] step if a full evaluation derivation for the associated primop may be found before proceeding. *)
adamc@263 407
adamc@262 408 Ltac evalOne :=
adamc@262 409 match goal with
adamc@262 410 | [ |- CPS.eval ?cs ?e ?v ] =>
adamc@262 411 let e := eval hnf in e in
adamc@262 412 change (CPS.eval cs e v);
adamc@262 413 econstructor; [ solve [ eauto ] | ]
adamc@262 414 end.
adamc@262 415
adamc@263 416 (** For primops, we rely on [eauto]'s usual approach. For goals that evaluate programs, we instead ask to treat one or more applications of [evalOne] as a single step, which helps us avoid passing [eauto] an excessively large bound on proof tree depth. *)
adamc@263 417
adamc@262 418 Hint Constructors evalP.
adamc@262 419 Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne.
adamc@262 420
adamc@263 421 (** The final lemma proceeds by induction on an evaluation derivation for an expression [e1] that is equivalent to some [e2] in some environment [G]. An initial closure heap for each language is quantified over, such that all variable pairs in [G] are compatible. The lemma's conclusion applies to an arbitrary continuation [k], asserting that a final CPS-level closure heap [s2] and a CPS-level program result value [r2] exist.
adamc@263 422
adamc@263 423 Three conditions establish that [s2] and [r2] are chosen properly: Evaluation of [e2]'s compilation with continuation [k] must be equivalent to evaluation of [k r2]. The original program result [r1] must be compatible with [r2] in the final closure heaps. Finally, [s2'] must be a proper evolution of the original CPS-level heap [s2]. *)
adamc@263 424
adamc@262 425 Lemma cpsExp_correct : forall s1 e1 s1' r1,
adamc@262 426 Source.eval s1 e1 s1' r1
adamc@262 427 -> forall G (e2 : exp CPS.val),
adamc@262 428 exp_equiv G e1 e2
adamc@262 429 -> forall s2,
adamc@262 430 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262 431 -> forall k, exists s2', exists r2,
adamc@262 432 (forall r, CPS.eval s2' (k r2) r
adamc@262 433 -> CPS.eval s2 (cpsExp e2 k) r)
adamc@262 434 /\ s1' & s2' |-- r1 ~~ r2
adamc@262 435 /\ s2 ~> s2'.
adamc@263 436
adamc@263 437 (** The proof script follows our standard approach. Its main loop applies three hints. First, we perform inversion on any derivation of equivalence between a source-level function value and some other value. Second, we eliminate redundant equality hypotheses. Finally, we look for opportunities to instantiate inductive hypotheses.
adamc@263 438
adamc@263 439 We identify an IH by its syntactic form, noting the expression [E] that it applies to. It is important to instantiate IHes in the right order, since existentially-quantified variables in the conclusion of one IH may need to be used in instantiating the universal quantifiers of a different IH. Thus, we perform a quick check to [fail 1] if the IH we found applies to an expression that was evaluated after another expression [E'] whose IH we did not yet instantiate. The flow of closure heaps through source-level evaluation is used to implement the check.
adamc@263 440
adamc@263 441 If the hypothesis [H] is indeed the right IH to handle next, we use the [guess] tactic to guess values for its universal quantifiers and prove its hypotheses with [eauto]. This tactic is very similar to [inster] from Chapter 12. It takes two arguments: the first is a value to use for any properly-typed universal quantifier, and the second is the hypothesis to instantiate. The final inner [match] deduces if we are at the point of executing the body of a called function. If so, we help [guess] by saying that the initial closure heap will be the current closure heap [cs] extended with the current continuation [k]. In all other cases, [guess] is smart enough to operate alone. *)
adamc@263 442
adamc@262 443 induction 1; inversion 1; crush;
adamc@262 444 repeat (match goal with
adamc@262 445 | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H
adamc@262 446 | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1
adamc@262 447 | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] =>
adamc@262 448 match goal with
adamc@262 449 | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _,
adamc@262 450 _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1
adamc@262 451 | _ => match goal with
adamc@263 452 | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _,
adamc@263 453 _ : context[VFun] |- _ ] =>
adamc@262 454 guess (k :: cs) H
adamc@262 455 | _ => guess tt H
adamc@262 456 end
adamc@262 457 end
adamc@262 458 end; crush); eauto 13.
adamc@262 459 Qed.
adamc@262 460
adamc@263 461 (** The final theorem follows easily from this lemma. *)
adamc@263 462
adamc@263 463 Theorem CpsExp_correct : forall E cs b,
adamc@262 464 Source.Eval nil E cs (Source.VBool b)
adamc@262 465 -> Wf E
adamc@262 466 -> CPS.Eval nil (CpsExp E) (CPS.VBool b).
adamc@262 467 Hint Constructors CPS.eval.
adamc@262 468
adamc@262 469 unfold Source.Eval, CPS.Eval, CpsExp; intros ? ? ? H1 H2;
adamc@262 470 generalize (cpsExp_correct H1 (H2 _ _) (s2 := nil)
adamc@262 471 (fun _ _ pf => match pf with end) (Halt (var := _))); crush;
adamc@262 472 match goal with
adamc@262 473 | [ H : _ & _ |-- _ ~~ _ |- _ ] => inversion H
adamc@262 474 end; crush.
adamc@262 475 Qed.