Library CPS_subst2env
Equivalence between CPS semantics with environments and based on substitutions
Author : Zaynah Dargaye
Created : 29th April 2009
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import CPS_env.
Require Import CPS.
Require Import CPS_subst.
Require Import CPS_pre.
Require Import Cpsopt_pre1.
I. Correspondence between environments
Inductive match_val: cpsterm->CPSval->Prop:=
|mconstr: forall tl vl n,
match_vlist tl vl-> match_val (TConstr n tl) (CTc n vl)
|mclos: forall t ce l1 te l2 ari,
match_vlist l1 ce->match_vlist l2 te->
match_val (CTsubst_rec l1 l2 (TLamb ari t) O O)
(CTcl ari ce te t)
|mclosr: forall t ce l1 te l2 ari,
match_vlist l1 ce->match_vlist l2 te->
match_val (CTsubst_rec l1 l2 (TMu ari t) O O)
(CTclr ari ce te t)
with match_vlist: list cpsterm-> list CPSval->Prop:=
|mnil: match_vlist nil nil
|mcons: forall hd1 hd2 tl1 tl2,
match_val hd1 hd2->match_vlist tl1 tl2->
match_vlist (hd1::tl1) (hd2::tl2).
Scheme mv_ind6 := Minimality for match_val Sort Prop
with mvl_ind6 := Minimality for match_vlist Sort Prop.
Lemma match_length:
forall l1 l2, match_vlist l1 l2->length l2= length l1.
Lemma match_app:
forall l1 l2, match_vlist l1 l2->forall l3 l4, match_vlist l3 l4->
match_vlist (l1++l3) (l2++l4).
Lemma match_rev:
forall l1 l2, match_vlist l1 l2->match_vlist (rev l1) (rev l2).
Lemma match_nth:
forall l1 l2, match_vlist l1 l2->
forall n t, nth_error l1 n = Some t->
exists v, nth_error l2 n = Some v/\ match_val t v.
Fixpoint is_cval (t:cpsterm){struct t}:bool:=
match t with
| TLamb _ _ =>true
| TMu _ _ =>true
| TConstr _ l => let fix is_cval_list (l:list cpsterm) {struct l}:bool:=
match l with
| nil=>true
|a::m=>
if ( is_cval a) then is_cval_list m else false end
in is_cval_list l
| _ => false
end .
Fixpoint is_cval_list (l:list cpsterm) {struct l}:bool:=
match l with
| nil=>true
|a::m=>
if ( is_cval a) then is_cval_list m else false end .
Lemma is_cval_nth:
forall l n t,is_cval_list l = true->
nth_error l n = Some t->is_cval t = true.
Lemma match_cval :
forall t v, match_val t v-> is_cval t = true.
Lemma match_env_cval:
forall tl vl, match_vlist tl vl->is_cval_list tl = true.
Ltac DO_IT :=
match goal with
| [ |- context[lt_ge_dec ?a ?b] ] =>
case_eq (lt_ge_dec a b); intros; simpl; auto; DO_IT
| [ |- context[compare_dec ?a ?b] ] =>
case_eq(compare_dec a b); intros; simpl; auto; DO_IT
| [ |- context[match ?x with Some _ => _ | None => _ end] ] =>
case_eq x; intros; simpl; auto; DO_IT
| [ |-context[compare_bd_dec ?a ?b ?c] ] =>
case_eq (compare_bd_dec a b c);intros;simpl;auto;DO_IT
| _ =>
omega || (elimtype False; omega) || (progress f_equal; auto; DO_IT; fail) ||
intuition || auto
end.
II. Properties of the semantics based on substitution
Lemma ceval_det:
forall t v, ceval_term t v ->forall v' (A: ceval_term t v'),v=v'.
Lemma ceval_list_det:
forall t v , ceval_list t v ->forall v', ceval_list t v'->v=v'.
Lemma ceval_is_cval:
forall v, is_cval v =true-> ceval_term v v.
Lemma ceval_iscval_list:
forall v, is_cval_list v =true-> ceval_list v v.
Lemma ceval_match_spec:
forall l1 l2, match_vlist l1 l2 ->
forall l3, ceval_list l1 l3 -> l3 =l1.
Lemma CTeval_length:
forall l1 l2 a b , CPSeval_list a b l1 l2 -> length l1=length l2.
Properties of continuation variables lifting
Lemma Cllift_Clift_1:
forall t n , Clift_rec t n = Cllift_rec t n 1.
Lemma Cllift_Clift_1_list:
forall t n , Clift_list_rec t n = Cllift_list_rec t n 1.
Lemma Cllift_O :
forall t n , Cllift_rec t n O =t.
Lemma Cllift_list_O:
forall t n , Cllift_list_rec t n O =t.
Lemma Pat_nth:
forall l p l1 l2 nc nt n ca,
nth_error (CTsubst_patlist_rec l1 l2 l nc nt) p =
Some (TPatc n ca) ->
exists c , ca = CTsubst_rec (Tlift_list l1 n) (Tlift_list l2 n) c nc (nt+n) /\
nth_error l p = Some (TPatc n c).
III. Big-step based on substitution corresponds to big-step with environments
Definition e_prop (t:cpsterm) (v:cpsterm):Prop:=
forall m ce l1 te l2
(MEC: match_vlist l1 ce)
(MET: match_vlist l2 te)
(SB: t = (CTsubst_rec l1 l2 m O O)),
exists v', CPSeval ce te m v' /\ match_val v v'.
Definition el_prop (t:list cpsterm) (v:list cpsterm):Prop:=
forall m ce l1 te l2
(MEC: match_vlist l1 ce)
(MET: match_vlist l2 te)
(SB: t = (CTsubst_list_rec l1 l2 m O O)),
exists v', CPSeval_list ce te m v' /\ match_vlist v v'.
Lemma lamb_correct:
forall (ari : nat) (t : cpsterm), e_prop (TLamb ari t) (TLamb ari t).
Lemma mu_correct:
forall (ari : nat) (t : cpsterm), e_prop (TMu ari t) (TMu ari t).
Lemma app1_correct:
forall (t1 c : cpsterm) (t2 : list cpsterm) (cv : cpsterm)
(vb : list cpsterm) (t v : cpsterm) (ari : nat),
ceval_term t1 (TLamb ari t) ->
e_prop t1 (TLamb ari t) -> length t2 = ari ->ceval_term c cv ->
e_prop c cv -> ceval_list t2 vb -> el_prop t2 vb ->
ceval_term (CTsubst_rec (cv :: nil) (rev vb) t 0 0) v ->
e_prop (CTsubst_rec (cv :: nil) (rev vb) t 0 0) v ->
e_prop (TApp t1 (c :: t2)) v.
Lemma app2_correct:
forall (t1 c cv t v : cpsterm) (t2 vb : list cpsterm) (ari : nat),
ceval_term t1 (TMu ari t) ->e_prop t1 (TMu ari t) ->
length t2 = ari -> ceval_term c cv ->
e_prop c cv -> ceval_list t2 vb ->
el_prop t2 vb ->
ceval_term
(CTsubst_rec (cv :: nil) (rev vb ++ TMu ari t :: nil) t 0 0) v ->
e_prop (CTsubst_rec (cv :: nil) (rev vb ++ TMu ari t :: nil) t 0 0) v ->
e_prop (TApp t1 (c :: t2)) v.
Lemma let_correct:
forall t1 t2 v1 v2 : cpsterm,
ceval_term t1 v1 -> e_prop t1 v1 ->
ceval_term (CTsubst_rec nil (v1 :: nil) t2 0 0) v2 ->
e_prop (CTsubst_rec nil (v1 :: nil) t2 0 0) v2 ->
e_prop (TLet t1 t2) v2.
Lemma constr_correct:
forall (n : nat) (l vl : list cpsterm),
ceval_list l vl -> el_prop l vl -> e_prop (TConstr n l) (TConstr n vl).
Lemma match_correct:
forall (t : cpsterm) (n : nat) (lv : list cpsterm) (p : list cpat)
(ca v : cpsterm),
ceval_term t (TConstr n lv) ->
e_prop t (TConstr n lv) ->
nth_error p n = Some (TPatc (length lv) ca) ->
ceval_term (CTsubst_rec nil (rev lv) ca 0 0) v ->
e_prop (CTsubst_rec nil (rev lv) ca 0 0) v -> e_prop (TMatch t p) v.
Lemma nil_correct: el_prop nil nil .
Lemma cons_correct:
forall (a va : cpsterm) (m vm : list cpsterm),
ceval_term a va ->e_prop a va ->
ceval_list m vm -> el_prop m vm -> el_prop (a :: m) (va :: vm).
Theorem s2env_correct:
forall c c0 : cpsterm, ceval_term c c0 -> e_prop c c0.