adamc@223: (* Copyright (c) 2008-2009, Adam Chlipala
adamc@190:  * 
adamc@190:  * This work is licensed under a
adamc@190:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@190:  * Unported License.
adamc@190:  * The license text is available at:
adamc@190:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@190:  *)
adamc@190: 
adamc@262: (* begin hide *)
adamc@262: Require Import Arith List.
adamc@190: 
adamc@262: Require Import Tactics.
adamc@190: 
adamc@262: Set Implicit Arguments.
adamc@262: (* end hide *)
adamc@190: 
adamc@262: 
adamc@262: (** %\chapter{Higher-Order Operational Semantics}% *)
adamc@262: 
adamc@262: (** * Closure Heaps *)
adamc@262: 
adamc@262: Section lookup.
adamc@262:   Variable A : Type.
adamc@262: 
adamc@262:   Fixpoint lookup (ls : list A) (n : nat) : option A :=
adamc@262:     match ls with
adamc@262:       | nil => None
adamc@262:       | v :: ls' => if eq_nat_dec n (length ls') then Some v else lookup ls' n
adamc@262:     end.
adamc@262: 
adamc@262:   Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1.
adamc@262: 
adamc@262:   Infix "##" := lookup (left associativity, at level 1).
adamc@262:   Infix "~>" := extends (no associativity, at level 80).
adamc@262: 
adamc@262:   Theorem lookup1 : forall x ls,
adamc@262:     (x :: ls) ## (length ls) = Some x.
adamc@262:     crush; match goal with
adamc@262:              | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262:            end; crush.
adamc@262:   Qed.
adamc@262: 
adamc@262:   Theorem extends_refl : forall ls, ls ~> ls.
adamc@262:     exists nil; reflexivity.
adamc@262:   Qed.
adamc@262: 
adamc@262:   Theorem extends1 : forall v ls, ls ~> v :: ls.
adamc@262:     intros; exists (v :: nil); reflexivity.
adamc@262:   Qed.
adamc@262: 
adamc@262:   Theorem extends_trans : forall ls1 ls2 ls3,
adamc@262:     ls1 ~> ls2
adamc@262:     -> ls2 ~> ls3
adamc@262:     -> ls1 ~> ls3.
adamc@262:     intros ? ? ? [l1 ?] [l2 ?]; exists (l2 ++ l1); crush.
adamc@262:   Qed.
adamc@262: 
adamc@262:   Lemma lookup_contra : forall n v ls,
adamc@262:     ls ## n = Some v
adamc@262:     -> n >= length ls
adamc@262:     -> False.
adamc@262:     induction ls; crush;
adamc@262:       match goal with
adamc@262:         | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@262:       end; crush.
adamc@262:   Qed.
adamc@262: 
adamc@262:   Hint Resolve lookup_contra.
adamc@262: 
adamc@262:   Theorem extends_lookup : forall ls1 ls2 n v,
adamc@262:     ls1 ~> ls2
adamc@262:     -> ls1 ## n = Some v
adamc@262:     -> ls2 ## n = Some v.
adamc@262:     intros ? ? ? ? [l ?]; crush; induction l; crush;
adamc@262:       match goal with
adamc@262:         | [ |- context[if ?E then _ else _] ] => destruct E
adamc@262:       end; crush; elimtype False; eauto.
adamc@262:   Qed.
adamc@262: End lookup.
adamc@262: 
adamc@262: Infix "##" := lookup (left associativity, at level 1).
adamc@262: Infix "~>" := extends (no associativity, at level 80).
adamc@262: 
adamc@262: Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup.
adamc@262: 
adamc@262: 
adamc@262: (** * Languages and Translation *)
adamc@262: 
adamc@262: Module Source.
adamc@262:   Section exp.
adamc@262:     Variable var : Type.
adamc@262: 
adamc@262:     Inductive exp : Type :=
adamc@262:     | Var : var -> exp
adamc@262:     | App : exp -> exp -> exp
adamc@262:     | Abs : (var -> exp) -> exp
adamc@262:     | Bool : bool -> exp.
adamc@262:   End exp.
adamc@262: 
adamc@262:   Implicit Arguments Bool [var].
adamc@262: 
adamc@262:   Definition Exp := forall var, exp var.
adamc@262: 
adamc@262:   Inductive val : Set :=
adamc@262:   | VFun : nat -> val
adamc@262:   | VBool : bool -> val.
adamc@262: 
adamc@262:   Definition closure := val -> exp val.
adamc@262:   Definition closures := list closure.
adamc@262: 
adamc@262:   Inductive eval : closures -> exp val -> closures -> val -> Prop :=
adamc@262:   | EvVar : forall cs v,
adamc@262:     eval cs (Var v) cs v
adamc@262: 
adamc@262:   | EvApp : forall cs1 e1 e2 cs2 v1 c cs3 v2 cs4 v3,
adamc@262:     eval cs1 e1 cs2 (VFun v1)
adamc@262:     -> eval cs2 e2 cs3 v2
adamc@262:     -> cs2 ## v1 = Some c
adamc@262:     -> eval cs3 (c v2) cs4 v3
adamc@262:     -> eval cs1 (App e1 e2) cs4 v3
adamc@262: 
adamc@262:   | EvAbs : forall cs c,
adamc@262:     eval cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262: 
adamc@262:   | EvBool : forall cs b,
adamc@262:     eval cs (Bool b) cs (VBool b).
adamc@262: 
adamc@262:   Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) := eval cs1 (E _) cs2 v.
adamc@262: 
adamc@262:   Section exp_equiv.
adamc@262:     Variables var1 var2 : Type.
adamc@262: 
adamc@262:     Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop :=
adamc@262:     | EqVar : forall G v1 v2,
adamc@262:       In (v1, v2) G
adamc@262:       -> exp_equiv G (Var v1) (Var v2)
adamc@262: 
adamc@262:     | EqApp : forall G f1 x1 f2 x2,
adamc@262:       exp_equiv G f1 f2
adamc@262:       -> exp_equiv G x1 x2
adamc@262:       -> exp_equiv G (App f1 x1) (App f2 x2)
adamc@262:     | EqAbs : forall G f1 f2,
adamc@262:       (forall v1 v2, exp_equiv ((v1, v2) :: G) (f1 v1) (f2 v2))
adamc@262:       -> exp_equiv G (Abs f1) (Abs f2)
adamc@262: 
adamc@262:     | EqBool : forall G b,
adamc@262:       exp_equiv G (Bool b) (Bool b).
adamc@262:   End exp_equiv.
adamc@262: 
adamc@262:   Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2).
adamc@262: End Source.
adamc@262: 
adamc@262: Module CPS.
adamc@262:   Section exp.
adamc@262:     Variable var : Type.
adamc@262: 
adamc@262:     Inductive prog : Type :=
adamc@262:     | Halt : var -> prog
adamc@262:     | App : var -> var -> prog
adamc@262:     | Bind : primop -> (var -> prog) -> prog
adamc@262: 
adamc@262:     with primop : Type :=
adamc@262:     | Abs : (var -> prog) -> primop
adamc@262: 
adamc@262:     | Bool : bool -> primop
adamc@262: 
adamc@262:     | Pair : var -> var -> primop
adamc@262:     | Fst : var -> primop
adamc@262:     | Snd : var -> primop.
adamc@262:   End exp.
adamc@262: 
adamc@262:   Implicit Arguments Bool [var].
adamc@262: 
adamc@262:   Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@262:     (right associativity, at level 76, p at next level).
adamc@262: 
adamc@262:   Definition Prog := forall var, prog var.
adamc@262:   Definition Primop := forall var, primop var.
adamc@262: 
adamc@262:   Inductive val : Type :=
adamc@262:   | VFun : nat -> val
adamc@262:   | VBool : bool -> val
adamc@262:   | VPair : val -> val -> val.
adamc@262:   Definition closure := val -> prog val.
adamc@262:   Definition closures := list closure.
adamc@262: 
adamc@262:   Inductive eval : closures -> prog val -> val -> Prop :=
adamc@262:   | EvHalt : forall cs v,
adamc@262:     eval cs (Halt v) v
adamc@262: 
adamc@262:   | EvApp : forall cs n v2 c v3,
adamc@262:     cs ## n = Some c
adamc@262:     -> eval cs (c v2) v3
adamc@262:     -> eval cs (App (VFun n) v2) v3
adamc@262: 
adamc@262:   | EvBind : forall cs1 p e cs2 v1 v2,
adamc@262:     evalP cs1 p cs2 v1
adamc@262:     -> eval cs2 (e v1) v2
adamc@262:     -> eval cs1 (Bind p e) v2
adamc@262: 
adamc@262:   with evalP : closures -> primop val -> closures -> val -> Prop :=
adamc@262:   | EvAbs : forall cs c,
adamc@262:     evalP cs (Abs c) (c :: cs) (VFun (length cs))
adamc@262: 
adamc@262:   | EvPair : forall cs v1 v2,
adamc@262:     evalP cs (Pair v1 v2) cs (VPair v1 v2)
adamc@262:   | EvFst : forall cs v1 v2,
adamc@262:     evalP cs (Fst (VPair v1 v2)) cs v1
adamc@262:   | EvSnd : forall cs v1 v2,
adamc@262:     evalP cs (Snd (VPair v1 v2)) cs v2
adamc@262: 
adamc@262:   | EvBool : forall cs b,
adamc@262:     evalP cs (Bool b) cs (VBool b).
adamc@262: 
adamc@262:   Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v.
adamc@262: End CPS.
adamc@262: 
adamc@262: Import Source CPS.
adamc@262: 
adamc@262: Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@262: 
adamc@262: Section cpsExp.
adamc@262:   Variable var : Type.
adamc@262: 
adamc@262:   Import Source.
adamc@262: 
adamc@262:   Fixpoint cpsExp (e : exp var)
adamc@262:     : (var -> prog var) -> prog var :=
adamc@262:     match e with
adamc@262:       | Var v => fun k => k v
adamc@262: 
adamc@262:       | App e1 e2 => fun k =>
adamc@262:         f <-- e1;
adamc@262:         x <-- e2;
adamc@262:         kf <- CPS.Abs k;
adamc@262:         p <- Pair x kf;
adamc@262:         CPS.App f p
adamc@262:       | Abs e' => fun k =>
adamc@262:         f <- CPS.Abs (var := var) (fun p =>
adamc@262:           x <- Fst p;
adamc@262:           kf <- Snd p;
adamc@262:           r <-- e' x;
adamc@262:           CPS.App kf r);
adamc@262:         k f
adamc@262: 
adamc@262:       | Bool b => fun k =>
adamc@262:         x <- CPS.Bool b;
adamc@262:         k x
adamc@262:     end
adamc@262: 
adamc@262:     where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262: End cpsExp.
adamc@262: 
adamc@262: Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@262: 
adamc@262: Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)).
adamc@262: 
adamc@262: 
adamc@262: (** * Correctness Proof *)
adamc@262: 
adamc@262: Definition cpsFunc var (e' : var -> Source.exp var) :=
adamc@262:   fun p : var =>
adamc@262:     x <- Fst p;
adamc@262:     kf <- Snd p;
adamc@262:     r <-- e' x;
adamc@262:     CPS.App kf r.
adamc@262: 
adamc@262: Section cr.
adamc@262:   Variable s1 : Source.closures.
adamc@262:   Variable s2 : CPS.closures.
adamc@262: 
adamc@262:   Import Source.
adamc@262: 
adamc@262:   Inductive cr : Source.val -> CPS.val -> Prop :=
adamc@262:   | CrFun : forall l1 l2 G f1 f2,
adamc@262:     (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2))
adamc@262:     -> (forall x1 x2, In (x1, x2) G -> cr x1 x2)
adamc@262:     -> s1 ## l1 = Some f1
adamc@262:     -> s2 ## l2 = Some (cpsFunc f2)
adamc@262:     -> cr (Source.VFun l1) (CPS.VFun l2)
adamc@262: 
adamc@262:   | CrBool : forall b,
adamc@262:     cr (Source.VBool b) (CPS.VBool b).
adamc@262: End cr.
adamc@262: 
adamc@262: Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70).
adamc@262: 
adamc@262: Hint Constructors cr.
adamc@262: 
adamc@262: Lemma eval_monotone : forall cs1 e cs2 v,
adamc@262:   Source.eval cs1 e cs2 v
adamc@262:   -> cs1 ~> cs2.
adamc@262:   induction 1; crush; eauto.
adamc@262: Qed.
adamc@262: 
adamc@262: Lemma cr_monotone : forall cs1 cs2 cs1' cs2',
adamc@262:   cs1 ~> cs1'
adamc@262:   -> cs2 ~> cs2'
adamc@262:   -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2
adamc@262:     -> cs1' & cs2' |-- v1 ~~ v2.
adamc@262:   induction 3; crush; eauto.
adamc@262: Qed.
adamc@262: 
adamc@262: Hint Resolve eval_monotone cr_monotone.
adamc@262: 
adamc@262: Lemma push : forall G s1 s2 v1' v2',
adamc@262:   (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262:   -> s1 & s2 |-- v1' ~~ v2'
adamc@262:   -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2).
adamc@262:   crush.
adamc@262: Qed.
adamc@262: 
adamc@262: Hint Resolve push.
adamc@262: 
adamc@262: Ltac evalOne :=
adamc@262:   match goal with
adamc@262:     | [ |- CPS.eval ?cs ?e ?v ] =>
adamc@262:       let e := eval hnf in e in
adamc@262:         change (CPS.eval cs e v);
adamc@262:           econstructor; [ solve [ eauto ] | ]
adamc@262:   end.
adamc@262: 
adamc@262: Hint Constructors evalP.
adamc@262: Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne.
adamc@262: 
adamc@262: Lemma cpsExp_correct : forall s1 e1 s1' r1,
adamc@262:   Source.eval s1 e1 s1' r1
adamc@262:   -> forall G (e2 : exp CPS.val),
adamc@262:     exp_equiv G e1 e2
adamc@262:     -> forall s2,
adamc@262:       (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2)
adamc@262:       -> forall k, exists s2', exists r2,
adamc@262:         (forall r, CPS.eval s2' (k r2) r
adamc@262:           -> CPS.eval s2 (cpsExp e2 k) r)
adamc@262:         /\ s1' & s2' |-- r1 ~~ r2
adamc@262:         /\ s2 ~> s2'.
adamc@262:   induction 1; inversion 1; crush;
adamc@262:     repeat (match goal with
adamc@262:               | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H
adamc@262:               | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1
adamc@262:               | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] =>
adamc@262:                 match goal with
adamc@262:                   | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _,
adamc@262:                       _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1
adamc@262:                   | _ => match goal with
adamc@262:                            | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _, _ : context[VFun] |- _ ] =>
adamc@262:                              guess (k :: cs) H
adamc@262:                            | _ => guess tt H
adamc@262:                          end
adamc@262:                 end
adamc@262:             end; crush); eauto 13.
adamc@262: Qed.
adamc@262: 
adamc@262: Lemma CpsExp_correct : forall E cs b,
adamc@262:   Source.Eval nil E cs (Source.VBool b)
adamc@262:   -> Wf E
adamc@262:   -> CPS.Eval nil (CpsExp E) (CPS.VBool b).
adamc@262:   Hint Constructors CPS.eval.
adamc@262: 
adamc@262:   unfold Source.Eval, CPS.Eval, CpsExp; intros ? ? ? H1 H2;
adamc@262:     generalize (cpsExp_correct H1 (H2 _ _) (s2 := nil)
adamc@262:       (fun _ _ pf => match pf with end) (Halt (var := _))); crush;
adamc@262:     match goal with
adamc@262:       | [ H : _ & _ |-- _ ~~ _ |- _ ] => inversion H
adamc@262:     end; crush.
adamc@262: Qed.