Library cps2f_proof
Semantics preservation of the "come-back" translation from CPS to Nml for substitution
Author : Zaynah Dargaye
Created : 29th April 2009
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import Fml.
Require Import CPS.
Require Import CPS_env.
Require Import cps2f.
I. relation between environments
Inductive match_value : CPSval->val->Prop:=
| mctr: forall n lv1 lv2,
match_vlist lv1 lv2-> match_value (CTc n lv1) (constr n lv2)
|mcl: forall t t1 ce te cet tet e ari,
(forall n cv m, nth_error ce n = Some cv ->
nth_error cet n = Some m ->
exists v, nth_error e m = Some v/\
match_value cv v) ->
(forall n cv m, nth_error te n = Some cv ->
nth_error tet n = Some m ->
exists v, nth_error e m = Some v/\
match_value cv v) ->
flat t ( ari::liftup cet (S ari)) (mkari ari++liftup tet (S ari)) =Some t1->
match_value (CTcl ari ce te t) (clos ari t1 e)
|mcs: forall t t1 ce te cet tet e ari,
(forall n cv m, nth_error ce n = Some cv ->
nth_error cet n = Some m ->
exists v, nth_error e m = Some v/\
match_value cv v) ->
(forall n cv m, nth_error te n = Some cv ->
nth_error tet n = Some m ->
exists v, nth_error e m = Some v/\
match_value cv v) ->
flat t (ari::liftup cet (S(S ari))) (mkari ari++(S ari)::liftup tet (S(S ari)))= Some t1->
match_value (CTclr ari ce te t) (closr ari t1 e)
with match_vlist :list CPSval->list val->Prop:=
| mnil: match_vlist nil nil
|mcons: forall v1 v2 l1 l2, match_value v1 v2->match_vlist l1 l2->
match_vlist (v1::l1) (v2::l2).
Lemma match_v_length:
forall l1 l2, match_vlist l1 l2 ->length l2=length l1.
Definition match_env (ce:env) (cet:Cenv)
(te:env) (tet:Tenv) (e:list val):Prop:=
(forall n cv m, nth_error ce n = Some cv ->
nth_error cet n = Some m ->
exists v, nth_error e m = Some v/\
match_value cv v) /\
(forall n cv m, nth_error te n = Some cv ->
nth_error tet n = Some m ->
exists v, nth_error e m = Some v/\
match_value cv v) .
Open Scope nat_scope.
Lemma nth_liftup:
forall te n m r, nth_error (liftup te r) n = Some m ->
exists k, m=( k +r).
Lemma nth_liftup_incr:
forall te n m r, nth_error (liftup te r) n = Some (m+r) ->
nth_error te n = Some m.
Lemma liftup_plus:
forall te n m,
liftup te (n+m) = liftup (liftup te n) m.
Lemma liftup_O:
forall l, liftup l O = l.
Lemma match_env_tincr:
forall vb varg ceb cet0 teb tet0 e0,
match_env ceb cet0 teb tet0 e0 ->
match_value vb varg ->
match_env ceb (liftup cet0 1) (vb::teb) (0 :: liftup tet0 1) (varg::e0).
Lemma match_env_cincr:
forall ceb cet0 teb tet0 e0 vb varg,
match_env ceb cet0 teb tet0 e0 ->
match_value vb varg ->
match_env (vb::ceb) (O::liftup cet0 1) teb (liftup tet0 1) (varg::e0).
Ltac monadSimpl1 :=
match goal with
| [ |- (bind ?F ?G = Some ?X) -> _ ] =>
unfold bind at 1;
generalize (refl_equal F);
pattern F at -1 in |- *;
case F;
[ (let EQ := fresh "EQ" in
(intro; intro EQ; try monadSimpl1))
| intro; intro; discriminate ]
| [ |- (None = Some _) -> _ ] =>
intro; discriminate
| [ |- (Some _ = Some _) -> _ ] =>
let h := fresh "H" in
(intro h; injection h; intro; clear h)
| [ |- (_ = Some _) -> _ ] =>
let EQ := fresh "EQ" in intro EQ
end.
Ltac monadSimpl :=
match goal with
| [ |- (bind ?F ?G = Some ?X) -> _ ] => monadSimpl1
| [ |- (None = Some _) -> _ ] => monadSimpl1
| [ |- (Some _ = Some _) -> _ ] => monadSimpl1
| [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
| [ |- (?F _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
| [ |- (?F _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
| [ |- (?F _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
| [ |- (?F _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
| [ |- (?F _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1
end.
Ltac monadInv H :=
generalize H; monadSimpl.
Lemma match_args:
forall vl l2, match_vlist vl l2->
forall n ce1 cet0 te1 tet0 e0,
length vl = n ->
match_env ce1 cet0 te1 tet0 e0->
match_env (ce1) (liftup cet0 n)
(rev vl++te1) (mkari n++liftup tet0 n)
(rev l2++e0).
Lemma match_nth:
forall pl cet tet l m tn n,
flat_plist pl cet tet = Some l->
nth_error pl n = Some (TPatc m tn) ->
exists p, nth_error l n = Some p /\ flat_pat (TPatc m tn) cet tet = Some p.
Lemma CTeval_length:
forall l v ce te , CPSeval_list ce te l v -> length v=length l.
Lemma flat_length:
forall l1 c t l2, flat_list l1 c t = Some l2 -> length l2 = length l1.
II. Simulation scheme
Definition e_prop (ce:env) (te:env) (t:cpsterm) (v:CPSval):Prop:=
forall e cet tet t1
(ME:match_env ce cet te tet e)
(TR: flat t cet tet =Some t1),
exists v' , eval_term e t1 v'/\ match_value v v'.
Definition el_prop (ce:env) (te:env) (t:list cpsterm) (v:list CPSval):Prop:=
forall e cet tet t1
(ME:match_env ce cet te tet e)
(TR: flat_list t cet tet =Some t1),
exists v' , eval_list e t1 v'/\ match_vlist v v'.
Lemma tvar_correct:
forall (ce : env) (te : list CPSval) (n : nat) (v : CPSval),
nth_error te n = Some v -> e_prop ce te (TVar n) v.
Lemma cvar_correct:
forall (ce : list CPSval) (te : env) (n : nat) (v : CPSval),
nth_error ce n = Some v -> e_prop ce te (CVar n) v.
Lemma lamb_correct:
forall (ce te : env) (t : cpsterm) (ari : nat),
e_prop ce te (TLamb ari t) (CTcl ari ce te t).
Lemma mu_correct:
forall (ce te : env) (t : cpsterm) (ari : nat),
e_prop ce te (TMu ari t) (CTclr ari ce te t).
Lemma app_correct:
forall (ce te : env) (t1 : cpsterm) (tl : list cpsterm) (n : nat)
(vl : list CPSval) (cv res : CPSval) (t : cpsterm)
(ce1 te1 : list CPSval),
CPSeval ce te t1 (CTcl n ce1 te1 t) ->
e_prop ce te t1 (CTcl n ce1 te1 t) ->
CPSeval_list ce te tl (cv :: vl) ->
el_prop ce te tl (cv :: vl) ->
length tl = S n ->
CPSeval (cv :: ce1) (rev vl ++ te1) t res ->
e_prop (cv :: ce1) (rev vl ++ te1) t res ->
e_prop ce te (TApp t1 tl) res.
Lemma appr_correct:
forall (ce te : env) (t1 : cpsterm) (n : nat) (tl : list cpsterm)
(cv : CPSval) (vl : list CPSval) (res : CPSval) (t : cpsterm)
(ce1 te1 : list CPSval),
CPSeval ce te t1 (CTclr n ce1 te1 t) ->
e_prop ce te t1 (CTclr n ce1 te1 t) ->
CPSeval_list ce te tl (cv :: vl) ->
el_prop ce te tl (cv :: vl) ->
length tl =S n ->
CPSeval (cv :: ce1) (rev vl ++ CTclr n ce1 te1 t :: te1) t res ->
e_prop (cv :: ce1) (rev vl ++ CTclr n ce1 te1 t :: te1) t res ->
e_prop ce te (TApp t1 tl) res.
Lemma constr_correct:
forall (ce te : env) (tl : list cpsterm) (vl : list CPSval) (n : nat),
CPSeval_list ce te tl vl ->
el_prop ce te tl vl -> e_prop ce te (TConstr n tl) (CTc n vl).
Lemma match_correct:
forall (ce te : env) (t : cpsterm) (n : nat) (pl : list cpat)
(vl : list CPSval) (m : nat) (tn : cpsterm) (v : CPSval),
CPSeval ce te t (CTc n vl) ->
e_prop ce te t (CTc n vl) ->
nth_error pl n = Some (TPatc m tn) ->
length vl = m ->
CPSeval ce (rev vl ++ te) tn v ->
e_prop ce (rev vl ++ te) tn v -> e_prop ce te (TMatch t pl) v.
Lemma tlet_correct:
forall (ce te : env) (t1 t2 : cpsterm) (v1 v : CPSval),
CPSeval ce te t1 v1 ->
e_prop ce te t1 v1 ->
CPSeval ce (v1 :: te) t2 v ->
e_prop ce (v1 :: te) t2 v -> e_prop ce te (TLet t1 t2) v.
Lemma nil_correct:
forall ce te : env, el_prop ce te nil nil.
Lemma cons_correct:
forall (ce te : env) (t : cpsterm) (lt : list cpsterm) (v : CPSval) (lv : list CPSval),
CPSeval ce te t v ->
e_prop ce te t v ->
CPSeval_list ce te lt lv ->
el_prop ce te lt lv -> el_prop ce te (t :: lt) (v :: lv).
Theorem flat_correct:
forall (e e0 : env) (c : cpsterm) (c0 : CPSval),
CPSeval e e0 c c0 -> e_prop e e0 c c0.
Lemma match_init:
match_env nil nil nil nil nil.
Theorem ct2t_correct:
forall ct cv t, CPSeval nil nil ct cv->
ct2t ct = Some t ->
exists v, eval_term nil t v/\match_value cv v.