Mercurial > cpdt > repo

annotate src/OpSem.v @ 262:de53c8bcfa8d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OpSem code
author Adam Chlipala <adamc@hcoop.net>
date Mon, 28 Dec 2009 12:35:44 -0500
parents src/Impure.v@2a34c4dc6a10
children af6f6d8dcfe7
rev   line source
adamc@223 1 (* Copyright (c) 2008-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@262 21 (** * Closure Heaps *)
adamc@262 22
adamc@262 23 Section lookup.
adamc@262 24 Variable A : Type.
adamc@262 25
adamc@262 26 Fixpoint lookup (ls : list A) (n : nat) : option A :=
adamc@262 27 match ls with
adamc@262 28 | nil => None
adamc@262 29 | v :: ls' => if eq_nat_dec n (length ls') then Some v else lookup ls' n
adamc@262 30 end.
adamc@262 31
adamc@262 32 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1.
adamc@262 33
adamc@262 34 Infix "##" := lookup (left associativity, at level 1).
adamc@262 35 Infix "~>" := extends (no associativity, at level 80).
adamc@262 36
adamc@262 37 Theorem lookup1 : forall x ls,
adamc@262 38 (x :: ls) ## (length ls) = Some x.
adamc@262 39 crush; match goal with
adamc@262 40 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262 41 end; crush.
adamc@262 42 Qed.
adamc@262 43
adamc@262 44 Theorem extends_refl : forall ls, ls ~> ls.
adamc@262 45 exists nil; reflexivity.
adamc@262 46 Qed.
adamc@262 47
adamc@262 48 Theorem extends1 : forall v ls, ls ~> v :: ls.
adamc@262 49 intros; exists (v :: nil); reflexivity.
adamc@262 50 Qed.
adamc@262 51
adamc@262 52 Theorem extends_trans : forall ls1 ls2 ls3,
adamc@262 53 ls1 ~> ls2
adamc@262 54 -> ls2 ~> ls3
adamc@262 55 -> ls1 ~> ls3.
adamc@262 56 intros ? ? ? [l1 ?] [l2 ?]; exists (l2 ++ l1); crush.
adamc@262 57 Qed.
adamc@262 58
adamc@262 59 Lemma lookup_contra : forall n v ls,
adamc@262 60 ls ## n = Some v
adamc@262 61 -> n >= length ls
adamc@262 62 -> False.
adamc@262 63 induction ls; crush;
adamc@262 64 match goal with
adamc@262 65 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@262 66 end; crush.
adamc@262 67 Qed.
adamc@262 68
adamc@262 69 Hint Resolve lookup_contra.
adamc@262 70
adamc@262 71 Theorem extends_lookup : forall ls1 ls2 n v,
adamc@262 72 ls1 ~> ls2
adamc@262 73 -> ls1 ## n = Some v
adamc@262 74 -> ls2 ## n = Some v.
adamc@262 75 intros ? ? ? ? [l ?]; crush; induction l; crush;
adamc@262 76 match goal with
adamc@262 77 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262 78 end; crush; elimtype False; eauto.
adamc@262 79 Qed.
adamc@262 80 End lookup.
adamc@262 81
adamc@262 82 Infix "##" := lookup (left associativity, at level 1).
adamc@262 83 Infix "~>" := extends (no associativity, at level 80).
adamc@262 84
adamc@262 85 Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup.
adamc@262 86
adamc@262 87
adamc@262 88 (** * Languages and Translation *)
adamc@262 89
adamc@262 90 Module Source.
adamc@262 91 Section exp.
adamc@262 92 Variable var : Type.
adamc@262 93
adamc@262 94 Inductive exp : Type :=
adamc@262 95 | Var : var -> exp
adamc@262 96 | App : exp -> exp -> exp
adamc@262 97 | Abs : (var -> exp) -> exp
adamc@262 98 | Bool : bool -> exp.
adamc@262 99 End exp.
adamc@262 100
adamc@262 101 Implicit Arguments Bool [var].
adamc@262 102
adamc@262 103 Definition Exp := forall var, exp var.
adamc@262 104
adamc@262 105 Inductive val : Set :=
adamc@262 106 | VFun : nat -> val
adamc@262 107 | VBool : bool -> val.
adamc@262 108
adamc@262 109 Definition closure := val -> exp val.
adamc@262 110 Definition closures := list closure.
adamc@262 111
adamc@262 112 Inductive eval : closures -> exp val -> closures -> val -> Prop :=
adamc@262 113 | EvVar : forall cs v,
adamc@262 114 eval cs (Var v) cs v
adamc@262 115
adamc@262 116 | EvApp : forall cs1 e1 e2 cs2 v1 c cs3 v2 cs4 v3,
adamc@262 117 eval cs1 e1 cs2 (VFun v1)
adamc@262 118 -> eval cs2 e2 cs3 v2
adamc@262 119 -> cs2 ## v1 = Some c
adamc@262 120 -> eval cs3 (c v2) cs4 v3
adamc@262 121 -> eval cs1 (App e1 e2) cs4 v3
adamc@262 122
adamc@262 123 | EvAbs : forall cs c,
adamc@262 124 eval cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262 125
adamc@262 126 | EvBool : forall cs b,
adamc@262 127 eval cs (Bool b) cs (VBool b).
adamc@262 128
adamc@262 129 Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) := eval cs1 (E _) cs2 v.
adamc@262 130
adamc@262 131 Section exp_equiv.
adamc@262 132 Variables var1 var2 : Type.
adamc@262 133
adamc@262 134 Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop :=
adamc@262 135 | EqVar : forall G v1 v2,
adamc@262 136 In (v1, v2) G
adamc@262 137 -> exp_equiv G (Var v1) (Var v2)
adamc@262 138
adamc@262 139 | EqApp : forall G f1 x1 f2 x2,
adamc@262 140 exp_equiv G f1 f2
adamc@262 141 -> exp_equiv G x1 x2
adamc@262 142 -> exp_equiv G (App f1 x1) (App f2 x2)
adamc@262 143 | EqAbs : forall G f1 f2,
adamc@262 144 (forall v1 v2, exp_equiv ((v1, v2) :: G) (f1 v1) (f2 v2))
adamc@262 145 -> exp_equiv G (Abs f1) (Abs f2)
adamc@262 146
adamc@262 147 | EqBool : forall G b,
adamc@262 148 exp_equiv G (Bool b) (Bool b).
adamc@262 149 End exp_equiv.
adamc@262 150
adamc@262 151 Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2).
adamc@262 152 End Source.
adamc@262 153
adamc@262 154 Module CPS.
adamc@262 155 Section exp.
adamc@262 156 Variable var : Type.
adamc@262 157
adamc@262 158 Inductive prog : Type :=
adamc@262 159 | Halt : var -> prog
adamc@262 160 | App : var -> var -> prog
adamc@262 161 | Bind : primop -> (var -> prog) -> prog
adamc@262 162
adamc@262 163 with primop : Type :=
adamc@262 164 | Abs : (var -> prog) -> primop
adamc@262 165
adamc@262 166 | Bool : bool -> primop
adamc@262 167
adamc@262 168 | Pair : var -> var -> primop
adamc@262 169 | Fst : var -> primop
adamc@262 170 | Snd : var -> primop.
adamc@262 171 End exp.
adamc@262 172
adamc@262 173 Implicit Arguments Bool [var].
adamc@262 174
adamc@262 175 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@262 176 (right associativity, at level 76, p at next level).
adamc@262 177
adamc@262 178 Definition Prog := forall var, prog var.
adamc@262 179 Definition Primop := forall var, primop var.
adamc@262 180
adamc@262 181 Inductive val : Type :=
adamc@262 182 | VFun : nat -> val
adamc@262 183 | VBool : bool -> val
adamc@262 184 | VPair : val -> val -> val.
adamc@262 185 Definition closure := val -> prog val.
adamc@262 186 Definition closures := list closure.
adamc@262 187
adamc@262 188 Inductive eval : closures -> prog val -> val -> Prop :=
adamc@262 189 | EvHalt : forall cs v,
adamc@262 190 eval cs (Halt v) v
adamc@262 191
adamc@262 192 | EvApp : forall cs n v2 c v3,
adamc@262 193 cs ## n = Some c
adamc@262 194 -> eval cs (c v2) v3
adamc@262 195 -> eval cs (App (VFun n) v2) v3
adamc@262 196
adamc@262 197 | EvBind : forall cs1 p e cs2 v1 v2,
adamc@262 198 evalP cs1 p cs2 v1
adamc@262 199 -> eval cs2 (e v1) v2
adamc@262 200 -> eval cs1 (Bind p e) v2
adamc@262 201
adamc@262 202 with evalP : closures -> primop val -> closures -> val -> Prop :=
adamc@262 203 | EvAbs : forall cs c,
adamc@262 204 evalP cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262 205
adamc@262 206 | EvPair : forall cs v1 v2,
adamc@262 207 evalP cs (Pair v1 v2) cs (VPair v1 v2)
adamc@262 208 | EvFst : forall cs v1 v2,
adamc@262 209 evalP cs (Fst (VPair v1 v2)) cs v1
adamc@262 210 | EvSnd : forall cs v1 v2,
adamc@262 211 evalP cs (Snd (VPair v1 v2)) cs v2
adamc@262 212
adamc@262 213 | EvBool : forall cs b,
adamc@262 214 evalP cs (Bool b) cs (VBool b).
adamc@262 215
adamc@262 216 Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v.
adamc@262 217 End CPS.
adamc@262 218
adamc@262 219 Import Source CPS.
adamc@262 220
adamc@262 221 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@262 222
adamc@262 223 Section cpsExp.
adamc@262 224 Variable var : Type.
adamc@262 225
adamc@262 226 Import Source.
adamc@262 227
adamc@262 228 Fixpoint cpsExp (e : exp var)
adamc@262 229 : (var -> prog var) -> prog var :=
adamc@262 230 match e with
adamc@262 231 | Var v => fun k => k v
adamc@262 232
adamc@262 233 | App e1 e2 => fun k =>
adamc@262 234 f <-- e1;
adamc@262 235 x <-- e2;
adamc@262 236 kf <- CPS.Abs k;
adamc@262 237 p <- Pair x kf;
adamc@262 238 CPS.App f p
adamc@262 239 | Abs e' => fun k =>
adamc@262 240 f <- CPS.Abs (var := var) (fun p =>
adamc@262 241 x <- Fst p;
adamc@262 242 kf <- Snd p;
adamc@262 243 r <-- e' x;
adamc@262 244 CPS.App kf r);
adamc@262 245 k f
adamc@262 246
adamc@262 247 | Bool b => fun k =>
adamc@262 248 x <- CPS.Bool b;
adamc@262 249 k x
adamc@262 250 end
adamc@262 251
adamc@262 252 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262 253 End cpsExp.
adamc@262 254
adamc@262 255 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262 256
adamc@262 257 Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)).
adamc@262 258
adamc@262 259
adamc@262 260 (** * Correctness Proof *)
adamc@262 261
adamc@262 262 Definition cpsFunc var (e' : var -> Source.exp var) :=
adamc@262 263 fun p : var =>
adamc@262 264 x <- Fst p;
adamc@262 265 kf <- Snd p;
adamc@262 266 r <-- e' x;
adamc@262 267 CPS.App kf r.
adamc@262 268
adamc@262 269 Section cr.
adamc@262 270 Variable s1 : Source.closures.
adamc@262 271 Variable s2 : CPS.closures.
adamc@262 272
adamc@262 273 Import Source.
adamc@262 274
adamc@262 275 Inductive cr : Source.val -> CPS.val -> Prop :=
adamc@262 276 | CrFun : forall l1 l2 G f1 f2,
adamc@262 277 (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2))
adamc@262 278 -> (forall x1 x2, In (x1, x2) G -> cr x1 x2)
adamc@262 279 -> s1 ## l1 = Some f1
adamc@262 280 -> s2 ## l2 = Some (cpsFunc f2)
adamc@262 281 -> cr (Source.VFun l1) (CPS.VFun l2)
adamc@262 282
adamc@262 283 | CrBool : forall b,
adamc@262 284 cr (Source.VBool b) (CPS.VBool b).
adamc@262 285 End cr.
adamc@262 286
adamc@262 287 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70).
adamc@262 288
adamc@262 289 Hint Constructors cr.
adamc@262 290
adamc@262 291 Lemma eval_monotone : forall cs1 e cs2 v,
adamc@262 292 Source.eval cs1 e cs2 v
adamc@262 293 -> cs1 ~> cs2.
adamc@262 294 induction 1; crush; eauto.
adamc@262 295 Qed.
adamc@262 296
adamc@262 297 Lemma cr_monotone : forall cs1 cs2 cs1' cs2',
adamc@262 298 cs1 ~> cs1'
adamc@262 299 -> cs2 ~> cs2'
adamc@262 300 -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2
adamc@262 301 -> cs1' & cs2' |-- v1 ~~ v2.
adamc@262 302 induction 3; crush; eauto.
adamc@262 303 Qed.
adamc@262 304
adamc@262 305 Hint Resolve eval_monotone cr_monotone.
adamc@262 306
adamc@262 307 Lemma push : forall G s1 s2 v1' v2',
adamc@262 308 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262 309 -> s1 & s2 |-- v1' ~~ v2'
adamc@262 310 -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2).
adamc@262 311 crush.
adamc@262 312 Qed.
adamc@262 313
adamc@262 314 Hint Resolve push.
adamc@262 315
adamc@262 316 Ltac evalOne :=
adamc@262 317 match goal with
adamc@262 318 | [ |- CPS.eval ?cs ?e ?v ] =>
adamc@262 319 let e := eval hnf in e in
adamc@262 320 change (CPS.eval cs e v);
adamc@262 321 econstructor; [ solve [ eauto ] | ]
adamc@262 322 end.
adamc@262 323
adamc@262 324 Hint Constructors evalP.
adamc@262 325 Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne.
adamc@262 326
adamc@262 327 Lemma cpsExp_correct : forall s1 e1 s1' r1,
adamc@262 328 Source.eval s1 e1 s1' r1
adamc@262 329 -> forall G (e2 : exp CPS.val),
adamc@262 330 exp_equiv G e1 e2
adamc@262 331 -> forall s2,
adamc@262 332 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262 333 -> forall k, exists s2', exists r2,
adamc@262 334 (forall r, CPS.eval s2' (k r2) r
adamc@262 335 -> CPS.eval s2 (cpsExp e2 k) r)
adamc@262 336 /\ s1' & s2' |-- r1 ~~ r2
adamc@262 337 /\ s2 ~> s2'.
adamc@262 338 induction 1; inversion 1; crush;
adamc@262 339 repeat (match goal with
adamc@262 340 | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H
adamc@262 341 | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1
adamc@262 342 | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] =>
adamc@262 343 match goal with
adamc@262 344 | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _,
adamc@262 345 _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1
adamc@262 346 | _ => match goal with
adamc@262 347 | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _, _ : context[VFun] |- _ ] =>
adamc@262 348 guess (k :: cs) H
adamc@262 349 | _ => guess tt H
adamc@262 350 end
adamc@262 351 end
adamc@262 352 end; crush); eauto 13.
adamc@262 353 Qed.
adamc@262 354
adamc@262 355 Lemma CpsExp_correct : forall E cs b,
adamc@262 356 Source.Eval nil E cs (Source.VBool b)
adamc@262 357 -> Wf E
adamc@262 358 -> CPS.Eval nil (CpsExp E) (CPS.VBool b).
adamc@262 359 Hint Constructors CPS.eval.
adamc@262 360
adamc@262 361 unfold Source.Eval, CPS.Eval, CpsExp; intros ? ? ? H1 H2;
adamc@262 362 generalize (cpsExp_correct H1 (H2 _ _) (s2 := nil)
adamc@262 363 (fun _ _ pf => match pf with end) (Halt (var := _))); crush;
adamc@262 364 match goal with
adamc@262 365 | [ H : _ & _ |-- _ ~~ _ |- _ ] => inversion H
adamc@262 366 end; crush.
adamc@262 367 Qed.