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.