Mercurial > cpdt > repo

annotate src/OpSem.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 dce88a5c170c
children 2c88fc1dbe33
rev   line source
adamc@265 1 (* Copyright (c) 2009, 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
adamc@262 13 Require Import Tactics.
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
adamc@263 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
adamc@263 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.
adamc@263 86 Infix "~>" := extends (no associativity, at level 80).
adamc@262 87
adamc@263 88 (** We prove and add as hints a few basic theorems about [lookup] and [extends]. *)
adamc@262 89
adamc@262 90 Theorem lookup1 : forall x ls,
adamc@262 91 (x :: ls) ## (length ls) = Some x.
adamc@262 92 crush; match goal with
adamc@262 93 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262 94 end; crush.
adamc@262 95 Qed.
adamc@262 96
adamc@262 97 Theorem extends_refl : forall ls, ls ~> ls.
adamc@262 98 exists nil; reflexivity.
adamc@262 99 Qed.
adamc@262 100
adamc@262 101 Theorem extends1 : forall v ls, ls ~> v :: ls.
adamc@262 102 intros; exists (v :: nil); reflexivity.
adamc@262 103 Qed.
adamc@262 104
adamc@262 105 Theorem extends_trans : forall ls1 ls2 ls3,
adamc@262 106 ls1 ~> ls2
adamc@262 107 -> ls2 ~> ls3
adamc@262 108 -> ls1 ~> ls3.
adamc@262 109 intros ? ? ? [l1 ?] [l2 ?]; exists (l2 ++ l1); crush.
adamc@262 110 Qed.
adamc@262 111
adamc@262 112 Lemma lookup_contra : forall n v ls,
adamc@262 113 ls ## n = Some v
adamc@262 114 -> n >= length ls
adamc@262 115 -> False.
adamc@262 116 induction ls; crush;
adamc@262 117 match goal with
adamc@262 118 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@262 119 end; crush.
adamc@262 120 Qed.
adamc@262 121
adamc@262 122 Hint Resolve lookup_contra.
adamc@262 123
adamc@262 124 Theorem extends_lookup : forall ls1 ls2 n v,
adamc@262 125 ls1 ~> ls2
adamc@262 126 -> ls1 ## n = Some v
adamc@262 127 -> ls2 ## n = Some v.
adamc@262 128 intros ? ? ? ? [l ?]; crush; induction l; crush;
adamc@262 129 match goal with
adamc@262 130 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262 131 end; crush; elimtype False; eauto.
adamc@262 132 Qed.
adamc@262 133 End lookup.
adamc@262 134
adamc@262 135 Infix "##" := lookup (left associativity, at level 1).
adamc@262 136 Infix "~>" := extends (no associativity, at level 80).
adamc@262 137
adamc@262 138 Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup.
adamc@262 139
adamc@263 140 (** 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 141
adamc@262 142
adamc@262 143 (** * Languages and Translation *)
adamc@262 144
adamc@263 145 (** 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 146
adamc@262 147 Module Source.
adamc@263 148 (** We define the syntax of source expressions in our usual way. *)
adamc@263 149
adamc@262 150 Section exp.
adamc@262 151 Variable var : Type.
adamc@262 152
adamc@262 153 Inductive exp : Type :=
adamc@262 154 | Var : var -> exp
adamc@262 155 | App : exp -> exp -> exp
adamc@262 156 | Abs : (var -> exp) -> exp
adamc@262 157 | Bool : bool -> exp.
adamc@262 158 End exp.
adamc@262 159
adamc@262 160 Implicit Arguments Bool [var].
adamc@262 161
adamc@262 162 Definition Exp := forall var, exp var.
adamc@262 163
adamc@263 164 (** 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 165
adamc@262 166 Inductive val : Set :=
adamc@262 167 | VFun : nat -> val
adamc@262 168 | VBool : bool -> val.
adamc@262 169
adamc@263 170 (** A closure, then, follows the usual representation of function abstraction bodies, where we represent variables as values. *)
adamc@263 171
adamc@262 172 Definition closure := val -> exp val.
adamc@262 173 Definition closures := list closure.
adamc@262 174
adamc@263 175 (** 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 176
adamc@262 177 Inductive eval : closures -> exp val -> closures -> val -> Prop :=
adamc@262 178 | EvVar : forall cs v,
adamc@262 179 eval cs (Var v) cs v
adamc@262 180
adamc@262 181 | EvApp : forall cs1 e1 e2 cs2 v1 c cs3 v2 cs4 v3,
adamc@262 182 eval cs1 e1 cs2 (VFun v1)
adamc@262 183 -> eval cs2 e2 cs3 v2
adamc@262 184 -> cs2 ## v1 = Some c
adamc@262 185 -> eval cs3 (c v2) cs4 v3
adamc@262 186 -> eval cs1 (App e1 e2) cs4 v3
adamc@262 187
adamc@262 188 | EvAbs : forall cs c,
adamc@262 189 eval cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262 190
adamc@262 191 | EvBool : forall cs b,
adamc@262 192 eval cs (Bool b) cs (VBool b).
adamc@262 193
adamc@263 194 (** A simple wrapper produces an evaluation relation suitable for use on the main expression type [Exp]. *)
adamc@263 195
adamc@263 196 Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) :=
adamc@263 197 eval cs1 (E _) cs2 v.
adamc@263 198
adamc@263 199 (** To prove our translation's correctness, we will need the usual notions of expression equivalence and well-formedness. *)
adamc@262 200
adamc@262 201 Section exp_equiv.
adamc@262 202 Variables var1 var2 : Type.
adamc@262 203
adamc@262 204 Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop :=
adamc@262 205 | EqVar : forall G v1 v2,
adamc@262 206 In (v1, v2) G
adamc@262 207 -> exp_equiv G (Var v1) (Var v2)
adamc@262 208
adamc@262 209 | EqApp : forall G f1 x1 f2 x2,
adamc@262 210 exp_equiv G f1 f2
adamc@262 211 -> exp_equiv G x1 x2
adamc@262 212 -> exp_equiv G (App f1 x1) (App f2 x2)
adamc@262 213 | EqAbs : forall G f1 f2,
adamc@262 214 (forall v1 v2, exp_equiv ((v1, v2) :: G) (f1 v1) (f2 v2))
adamc@262 215 -> exp_equiv G (Abs f1) (Abs f2)
adamc@262 216
adamc@262 217 | EqBool : forall G b,
adamc@262 218 exp_equiv G (Bool b) (Bool b).
adamc@262 219 End exp_equiv.
adamc@262 220
adamc@262 221 Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2).
adamc@262 222 End Source.
adamc@262 223
adamc@263 224 (** Our target language can be defined without introducing any additional tricks. *)
adamc@263 225
adamc@262 226 Module CPS.
adamc@262 227 Section exp.
adamc@262 228 Variable var : Type.
adamc@262 229
adamc@262 230 Inductive prog : Type :=
adamc@262 231 | Halt : var -> prog
adamc@262 232 | App : var -> var -> prog
adamc@262 233 | Bind : primop -> (var -> prog) -> prog
adamc@262 234
adamc@262 235 with primop : Type :=
adamc@262 236 | Abs : (var -> prog) -> primop
adamc@262 237
adamc@262 238 | Bool : bool -> primop
adamc@262 239
adamc@262 240 | Pair : var -> var -> primop
adamc@262 241 | Fst : var -> primop
adamc@262 242 | Snd : var -> primop.
adamc@262 243 End exp.
adamc@262 244
adamc@262 245 Implicit Arguments Bool [var].
adamc@262 246
adamc@262 247 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@262 248 (right associativity, at level 76, p at next level).
adamc@262 249
adamc@262 250 Definition Prog := forall var, prog var.
adamc@262 251 Definition Primop := forall var, primop var.
adamc@262 252
adamc@262 253 Inductive val : Type :=
adamc@262 254 | VFun : nat -> val
adamc@262 255 | VBool : bool -> val
adamc@262 256 | VPair : val -> val -> val.
adamc@262 257 Definition closure := val -> prog val.
adamc@262 258 Definition closures := list closure.
adamc@262 259
adamc@262 260 Inductive eval : closures -> prog val -> val -> Prop :=
adamc@262 261 | EvHalt : forall cs v,
adamc@262 262 eval cs (Halt v) v
adamc@262 263
adamc@262 264 | EvApp : forall cs n v2 c v3,
adamc@262 265 cs ## n = Some c
adamc@262 266 -> eval cs (c v2) v3
adamc@262 267 -> eval cs (App (VFun n) v2) v3
adamc@262 268
adamc@262 269 | EvBind : forall cs1 p e cs2 v1 v2,
adamc@262 270 evalP cs1 p cs2 v1
adamc@262 271 -> eval cs2 (e v1) v2
adamc@262 272 -> eval cs1 (Bind p e) v2
adamc@262 273
adamc@262 274 with evalP : closures -> primop val -> closures -> val -> Prop :=
adamc@262 275 | EvAbs : forall cs c,
adamc@262 276 evalP cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262 277
adamc@262 278 | EvPair : forall cs v1 v2,
adamc@262 279 evalP cs (Pair v1 v2) cs (VPair v1 v2)
adamc@262 280 | EvFst : forall cs v1 v2,
adamc@262 281 evalP cs (Fst (VPair v1 v2)) cs v1
adamc@262 282 | EvSnd : forall cs v1 v2,
adamc@262 283 evalP cs (Snd (VPair v1 v2)) cs v2
adamc@262 284
adamc@262 285 | EvBool : forall cs b,
adamc@262 286 evalP cs (Bool b) cs (VBool b).
adamc@262 287
adamc@262 288 Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v.
adamc@262 289 End CPS.
adamc@262 290
adamc@262 291 Import Source CPS.
adamc@262 292
adamc@263 293 (** Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus. *)
adamc@263 294
adamc@262 295 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@262 296
adamc@262 297 Section cpsExp.
adamc@262 298 Variable var : Type.
adamc@262 299
adamc@262 300 Import Source.
adamc@262 301
adamc@262 302 Fixpoint cpsExp (e : exp var)
adamc@262 303 : (var -> prog var) -> prog var :=
adamc@262 304 match e with
adamc@262 305 | Var v => fun k => k v
adamc@262 306
adamc@262 307 | App e1 e2 => fun k =>
adamc@262 308 f <-- e1;
adamc@262 309 x <-- e2;
adamc@262 310 kf <- CPS.Abs k;
adamc@262 311 p <- Pair x kf;
adamc@262 312 CPS.App f p
adamc@262 313 | Abs e' => fun k =>
adamc@262 314 f <- CPS.Abs (var := var) (fun p =>
adamc@262 315 x <- Fst p;
adamc@262 316 kf <- Snd p;
adamc@262 317 r <-- e' x;
adamc@262 318 CPS.App kf r);
adamc@262 319 k f
adamc@262 320
adamc@262 321 | Bool b => fun k =>
adamc@262 322 x <- CPS.Bool b;
adamc@262 323 k x
adamc@262 324 end
adamc@262 325
adamc@262 326 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262 327 End cpsExp.
adamc@262 328
adamc@262 329 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262 330
adamc@262 331 Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)).
adamc@262 332
adamc@262 333
adamc@262 334 (** * Correctness Proof *)
adamc@262 335
adamc@263 336 (** 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 337
adamc@262 338 Definition cpsFunc var (e' : var -> Source.exp var) :=
adamc@262 339 fun p : var =>
adamc@262 340 x <- Fst p;
adamc@262 341 kf <- Snd p;
adamc@262 342 r <-- e' x;
adamc@262 343 CPS.App kf r.
adamc@262 344
adamc@263 345 (** Now we can define our correctness relation [cr], which is parameterized by source-level and CPS-level closure heaps. *)
adamc@263 346
adamc@262 347 Section cr.
adamc@262 348 Variable s1 : Source.closures.
adamc@262 349 Variable s2 : CPS.closures.
adamc@262 350
adamc@262 351 Import Source.
adamc@262 352
adamc@263 353 (** 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 354
adamc@262 355 Inductive cr : Source.val -> CPS.val -> Prop :=
adamc@263 356 | CrBool : forall b,
adamc@263 357 cr (Source.VBool b) (CPS.VBool b)
adamc@263 358
adamc@262 359 | CrFun : forall l1 l2 G f1 f2,
adamc@262 360 (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2))
adamc@262 361 -> (forall x1 x2, In (x1, x2) G -> cr x1 x2)
adamc@262 362 -> s1 ## l1 = Some f1
adamc@262 363 -> s2 ## l2 = Some (cpsFunc f2)
adamc@263 364 -> cr (Source.VFun l1) (CPS.VFun l2).
adamc@262 365 End cr.
adamc@262 366
adamc@262 367 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70).
adamc@262 368
adamc@262 369 Hint Constructors cr.
adamc@262 370
adamc@263 371 (** 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 372
adamc@262 373 Lemma eval_monotone : forall cs1 e cs2 v,
adamc@262 374 Source.eval cs1 e cs2 v
adamc@262 375 -> cs1 ~> cs2.
adamc@262 376 induction 1; crush; eauto.
adamc@262 377 Qed.
adamc@262 378
adamc@263 379 (** Further, [cr] continues to hold when its closure heap arguments are evolved in legal ways. *)
adamc@263 380
adamc@262 381 Lemma cr_monotone : forall cs1 cs2 cs1' cs2',
adamc@262 382 cs1 ~> cs1'
adamc@262 383 -> cs2 ~> cs2'
adamc@262 384 -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2
adamc@262 385 -> cs1' & cs2' |-- v1 ~~ v2.
adamc@262 386 induction 3; crush; eauto.
adamc@262 387 Qed.
adamc@262 388
adamc@262 389 Hint Resolve eval_monotone cr_monotone.
adamc@262 390
adamc@263 391 (** 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 392
adamc@262 393 Lemma push : forall G s1 s2 v1' v2',
adamc@262 394 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262 395 -> s1 & s2 |-- v1' ~~ v2'
adamc@262 396 -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2).
adamc@262 397 crush.
adamc@262 398 Qed.
adamc@262 399
adamc@262 400 Hint Resolve push.
adamc@262 401
adamc@263 402 (** 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 403
adamc@262 404 Ltac evalOne :=
adamc@262 405 match goal with
adamc@262 406 | [ |- CPS.eval ?cs ?e ?v ] =>
adamc@262 407 let e := eval hnf in e in
adamc@262 408 change (CPS.eval cs e v);
adamc@262 409 econstructor; [ solve [ eauto ] | ]
adamc@262 410 end.
adamc@262 411
adamc@263 412 (** 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 413
adamc@262 414 Hint Constructors evalP.
adamc@262 415 Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne.
adamc@262 416
adamc@263 417 (** 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 418
adamc@263 419 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 420
adamc@262 421 Lemma cpsExp_correct : forall s1 e1 s1' r1,
adamc@262 422 Source.eval s1 e1 s1' r1
adamc@262 423 -> forall G (e2 : exp CPS.val),
adamc@262 424 exp_equiv G e1 e2
adamc@262 425 -> forall s2,
adamc@262 426 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262 427 -> forall k, exists s2', exists r2,
adamc@262 428 (forall r, CPS.eval s2' (k r2) r
adamc@262 429 -> CPS.eval s2 (cpsExp e2 k) r)
adamc@262 430 /\ s1' & s2' |-- r1 ~~ r2
adamc@262 431 /\ s2 ~> s2'.
adamc@263 432
adamc@263 433 (** 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 434
adamc@263 435 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 436
adamc@263 437 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 438
adamc@262 439 induction 1; inversion 1; crush;
adamc@262 440 repeat (match goal with
adamc@262 441 | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H
adamc@262 442 | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1
adamc@262 443 | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] =>
adamc@262 444 match goal with
adamc@262 445 | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _,
adamc@262 446 _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1
adamc@262 447 | _ => match goal with
adamc@263 448 | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _,
adamc@263 449 _ : context[VFun] |- _ ] =>
adamc@262 450 guess (k :: cs) H
adamc@262 451 | _ => guess tt H
adamc@262 452 end
adamc@262 453 end
adamc@262 454 end; crush); eauto 13.
adamc@262 455 Qed.
adamc@262 456
adamc@263 457 (** The final theorem follows easily from this lemma. *)
adamc@263 458
adamc@263 459 Theorem CpsExp_correct : forall E cs b,
adamc@262 460 Source.Eval nil E cs (Source.VBool b)
adamc@262 461 -> Wf E
adamc@262 462 -> CPS.Eval nil (CpsExp E) (CPS.VBool b).
adamc@262 463 Hint Constructors CPS.eval.
adamc@262 464
adamc@262 465 unfold Source.Eval, CPS.Eval, CpsExp; intros ? ? ? H1 H2;
adamc@262 466 generalize (cpsExp_correct H1 (H2 _ _) (s2 := nil)
adamc@262 467 (fun _ _ pf => match pf with end) (Halt (var := _))); crush;
adamc@262 468 match goal with
adamc@262 469 | [ H : _ & _ |-- _ ~~ _ |- _ ] => inversion H
adamc@262 470 end; crush.
adamc@262 471 Qed.