Library d2mp

Semantics preservation of the conversion to intermediate monadic form

Author: Zaynah Dargaye

Created: 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import AST.

Require Import Globalenvs.

Require Import Maps.

Require Import Dml.

Require Import Mml.

Require Import d2m.

I. Induction scheme of Fml terms


Section dterm_ind_sect.

Variable

(P: Dterm->Prop) 

 (Pl: list Dterm-> Prop) 

(Pp: dpat->Prop)

(Ppl:list dpat->Prop) .




Hypothesis 

(Hv: forall n, P(Dvar n) )

(Hfield: forall n t, P t -> P (Dfield n t))

(Hclos: forall id l , Pl l -> P (Clos id l))

(Happ : forall info d dl, P d ->Pl dl -> P (Dapp info d dl)) 

(Hcon: forall n dl, Pl dl -> P (Dcon n dl)) 

(Hlet: forall x d1 d2, P d1 -> P d2 -> P (Dlet x d1 d2)) 

(Hmtch: forall d pl,   P d -> Ppl pl -> P (Dmatch d pl)) 

(Hnil : Pl nil)

(Hcons: forall t tl, P t -> Pl tl -> Pl (t::tl)) 

(Hpat: forall n t, P t -> Pp (DPatc n t))

(Hpnil: Ppl nil)

(Hpcons: forall p pl, Pp p -> Ppl pl-> Ppl (p::pl)).




Fixpoint dterm_ind2 (t:Dterm) : P t := 

 match t as x return P x with 

 | Dvar n => Hv n

 | Dfield n t => Hfield n t (dterm_ind2 t) 

 | Clos id dl => Hclos id dl 

    ((fix l_ind (tl:list Dterm) : Pl tl := match tl as x return Pl x with 

     | nil => Hnil | a::m=> Hcons a m (dterm_ind2 a) (l_ind m)end) dl) 

 |Dapp info d1 dl => Happ info d1 dl (dterm_ind2 d1) 

    ((fix l_ind (tl:list Dterm) : Pl tl := match tl as x return Pl x with 

     | nil => Hnil | a::m=> Hcons a m (dterm_ind2 a) (l_ind m)end) dl) 

 | Dcon n dl => Hcon n dl 

     ((fix l_ind (tl:list Dterm) : Pl tl := match tl as x return Pl x with 

     | nil => Hnil | a::m=> Hcons a m (dterm_ind2 a) (l_ind m)end) dl) 

| Dlet x d1 d2 => Hlet x d1 d2 (dterm_ind2 d1) (dterm_ind2 d2) 

| Dmatch d1 pl => Hmtch d1 pl (dterm_ind2 d1) 

  ((fix l_ind (tl:list dpat) : Ppl tl := match tl as x return Ppl x with 

      | nil => Hpnil | a::m=> Hpcons a m (dpat_ind2 a) (l_ind m)end) pl) 

end

with dpat_ind2 (d:dpat):Pp d:= 

 match d as x return Pp x with | DPatc m t => Hpat m t (dterm_ind2 t) end.




End dterm_ind_sect.

II. Introduced names properties


Definition name_cor (fe:env) (lid:ident):Prop:= 

 forall x, Ple lid x -> PTree.get (xI x) fe = None.




Lemma name_cor_match: 

forall xl vl e lid  e1, 

 name_cor e lid->  

 (forall x : positive, In x xl -> exists j : positive, x = xO j) ->

 set_local_par xl vl e = Some e1-> 

 name_cor e1 lid.

III. Equivalence between environments


Definition equi_env (e e':env):Prop:= 

 forall x v, PTree.get x e =Some v-> PTree.get x e'=Some v.




Lemma equi_env_let: 

 forall e ee id v, equi_env e ee->

                           equi_env (PTree.set id v e) (PTree.set id v ee).




Lemma equi_env_set_local_par: 

 forall xl e ee vl e1, 

   equi_env e ee->

   set_local_par xl vl e= Some e1->

   exists ee1, set_local_par xl vl ee=Some ee1/\ equi_env e1 ee1.







Lemma env_equi_refl: 

 forall e, equi_env e e.




Lemma env_equi_trans: 

 forall e1 e2 e3, equi_env e1 e2->equi_env e2 e3->

                           equi_env e1 e3.




Lemma env_equi_comm: 

 forall e p1 p2 v1 v2, 

 p1<>p2 ->

 equi_env (PTree.set p1 v1 (PTree.set p2 v2 e)) 

                (PTree.set p2 v2 (PTree.set p1 v1 e)).







Lemma set_par_length: 

 forall xl vl e e1, set_local_par xl vl e = Some e1 -> length xl = length vl.




Lemma set_par_ok : 

 forall xl vl e , length xl = length vl ->

  exists e1, set_local_par xl vl e = Some e1.




Lemma match_equi_spec: 

forall xl vl e lid x e1 ee1 v', 

 name_cor e lid-> Ple lid x-> 

 (forall x : positive, In x xl -> exists j : positive, x = xO j) ->

 set_local_par xl vl e = Some e1-> 

 set_local_par xl vl (PTree.set (xI x) v' e) = Some ee1->

 equi_env (PTree.set (xI x) v' e1) ee1.













Section EQUI_ENV.

Variable sf: list (ident*funct).




Lemma feval_atom_equiv: 

 forall fe a v, feval_atom fe a v -> 

   forall fe2 (EE:equi_env fe fe2) , 

    feval_atom fe2 a v.




Lemma feval_atomlist_equiv: 

   forall fe a v, feval_atlist fe a v -> 

   forall fe2 (EE:equi_env fe fe2) , 

    feval_atlist fe2 a v.




Theorem eval_equi_env: 

 forall sf e t v, feval_term sf e t v->

 forall e1 (EE: equi_env e e1 ), 

 feval_term sf e1 t v.




Theorem eval_list_equi_env: 

 forall sf e t v, feval_list sf e t v->

 forall e1 (EE: equi_env e e1 ), 

 feval_list sf e1 t v.




End EQUI_ENV.

IV. Variables properties


Lemma x0_22: 

forall l, 

 forall x : positive,

 In x (map (fun n : positive => xO n) l) ->

 exists j : positive, x = xO j.




Lemma var_test_not_xH: 

 forall id, id <>xH -> var_test_prop (xO id).




Lemma varl_test_not_xH : 

forall l (LN: list_norepet l), 

  (forall x, In x l -> x<>xH) -> 

  varl_test_prop (List.map (fun x => xO x) l).




Lemma var_test_not_xH_new_var: 

 forall id, id<>xH-> var_test_prop (xI id).




Lemma var_test_succ: 

 forall m , var_test_prop m -> var_test_prop (Psucc m).




Lemma var_test_xI: 

 forall m , var_test_prop m -> var_test_prop (xI m).




Lemma var_test_xO: 

 forall m , var_test_prop m -> var_test_prop (xO m).




Lemma name_cor_sup: 

 forall m fe z, name_cor fe m -> Ple m z ->name_cor fe z.




Lemma name_cor_succ: 

 forall m fe , name_cor fe m ->name_cor fe (Psucc m).




Lemma name_cor_add: 

 forall m fe v, name_cor fe m ->name_cor 

 (PTree.set (xI m) v fe ) (Psucc m).




 Lemma name_cor_adds: 

 forall m fe v r, name_cor fe m -> Plt m r->name_cor 

 (PTree.set (xI m) v fe ) r.




Lemma name_cor_add_x0: 

 forall m fe z v, 

 name_cor fe m ->name_cor 

 (PTree.set (xO z) v fe )  m.




Lemma equi_env_name_cor: 

 forall m fe' v,  name_cor fe' m->

 equi_env fe' (PTree.set (xI m) v fe').

V. Properties of evaluation of list of terms


Lemma feval_at_app: 

 forall  fe al1 vl1, feval_atlist  fe al1 vl1 -> 

 forall al2 vl2, feval_atlist  fe al2 vl2 -> 

 feval_atlist  fe (al1++al2) (vl1++vl2).




Lemma feval_at_rev: 

 forall  fe al vl, feval_atlist  fe al vl -> 

 feval_atlist  fe (rev al) (rev vl).




Lemma Fset_par_length: 

 forall xl vl e e1, Dml.set_local_par xl vl e = Some e1 -> length xl = length vl.




Lemma Fset_par_ok : 

 forall xl vl e , length xl = length vl ->

  exists e1, Dml.set_local_par xl vl e = Some e1.

VI. Evaluation of atomisation contexts


Lemma feval_mk_Field: 

forall sf d fe fid fvl n fv lid (ID:  lid <> xH),

 name_cor fe lid-> 

  feval_term sf fe d (fclos fid fvl) -> 

 nth_error fvl n = Some fv-> 

 feval_term sf fe (mk_Field (S n) d lid) fv.




Lemma feval_mk_Clos_rec:

forall  sf dl fvl fe,  feval_list sf fe dl fvl -> 

forall  fid m d dl1 fvl1 fe' (ID: m <> xH), equi_env fe fe' ->

name_cor fe m-> 

feval_atlist  fe' dl1 fvl1 -> 

recup_funct fid sf = Some d->

name_cor fe' m ->

feval_term sf fe'

  (atom_list dl  dl1  (fun args' => Fclos fid args')

     m) (fclos fid (rev fvl1++fvl)).













Lemma feval_mk_Clos: 

 forall sf fe m fid d dl fvl (ID: m <> xH), 

 feval_list sf fe dl fvl -> name_cor fe m->

 recup_funct fid sf = Some d->

 feval_term sf fe (mk_Clos fid dl m )

  (fclos fid fvl).




Lemma feval_mk_Con_rec:

forall   sf dl fvl fe,  feval_list sf fe dl fvl -> 

forall fid m  dl1 fvl1 fe' (ID: m<>xH), equi_env fe fe' ->

name_cor fe m-> 

feval_atlist  fe' dl1 fvl1 -> 

name_cor fe' m ->

feval_term sf fe'

  (atom_list dl  dl1  (fun args' => Fcon fid args')

     m) (fconstr fid (rev fvl1++fvl)).













Lemma feval_mk_Con: 

 forall sf fe m n dl fvl (ID: m<>xH), 

 feval_list sf fe dl fvl -> name_cor fe m->

 feval_term sf fe (mk_Con n dl m )

  (fconstr n fvl).




Lemma feval_mk_App_rec1: 

forall targs sf fe fvl, feval_list sf fe targs fvl-> 

  forall lid dvl1 fvl1 fe' fres d0 fid fvl0 fe3 a info (ID:lid<>xH)

  (PID:varl_test_prop (fun_par d0) ),  

  name_cor fe lid-> equi_env fe fe' ->name_cor fe' lid->

  list_norepet (fun_par d0) -> 

 feval_atlist fe' dvl1 fvl1-> 

 recup_funct fid sf = Some d0-> 

 ( info = None \/ info = Some fid)-> 

 set_local_par (fun_par d0) (fclos fid fvl0 :: rev fvl1 ++ fvl)

       (PTree.empty fval) = Some fe3-> 

 feval_term sf fe3 (fun_body d0) fres-> 

 feval_atom  fe a (fclos fid fvl0)-> 

 feval_term sf fe'

  (atom_list targs dvl1 (fun al : list atom => Fapp info a al) lid)

  fres.










Lemma feval_mk_App:

forall sf fe lid t1 targs fid fvl d0 fres info fe3 fvl0 

 (LN: list_norepet (fun_par d0)) 

 (ID: lid<>xH) 

 (PID: varl_test_prop (fun_par d0)), 

   name_cor fe lid -> 

   (forall x, In x (fun_par d0) ->exists j, x = xO j) ->

   feval_term sf fe t1  (fclos fid fvl0)->

   feval_list sf fe targs  fvl->

   recup_funct fid sf = Some d0-> 

   (info = None \/ info = Some fid) -> 

   set_local_par (fun_par d0)

        (fclos fid fvl0 :: fvl) (PTree.empty fval) = Some fe3-> 

   feval_term sf fe3 (fun_body d0) fres->

   feval_term sf fe (mk_App info t1 targs lid) fres.







Lemma feval_mk_match: 

forall fe  sf a n fvl xl p vres pl lid fe1

 (LN: list_norepet xl) 

 (ID: lid<>xH) 

 (PID: varl_test_prop xl), 

 name_cor fe lid-> 

 feval_term sf fe a (fconstr n fvl)-> 

 (forall x, In x xl ->exists j , x =xO j) -> 

  nth_error pl n =Some (FPatc xl p)-> 

  set_local_par xl fvl fe = Some fe1->

  name_cor fe1 lid->

  feval_term sf fe1 p vres->

  feval_term sf fe (mk_Match a pl lid) vres.

VII. Name generation coherence


Lemma transl_gen_name: 

 forall f lid d zid, transl f lid = (d,zid) -> 

   Ple lid zid.































Lemma transl_list_gen_name: 

 forall f lid d zid, transl_list f lid = (d,zid) -> 

   Ple lid zid.




Lemma transl_pat_gen_name: 

 forall f lid d zid, transl_pat f lid = (d,zid) -> 

   Ple lid zid.




 Lemma transl_plist_gen_name: 

 forall f lid d zid, transl_plist f lid = (d,zid) -> 

   Ple lid zid.




Lemma transl_plist_nth: 

 forall pl n p , nth_error pl n = Some p -> 

    forall al lid zid,

       transl_plist pl lid = (al,zid) -> 

      exists a,exists z, exists z0, 

      transl_pat p z0 = (a,z)/\

      nth_error al n = Some a/\

      Ple lid z0 /\Ple z zid.







Section Cor.

Variable sd: list (ident*def).




Hypothesis recup_correct: 

 forall f d, 

  recup_fun f sd = Some d -> 

           recup_funct f (List.map transl_def  sd) = 

           Some (snd (transl_def (f,d))).

VII. Correspondence between environments


Inductive match_val : dval->fval->Prop:= 

 | mcl: forall f d dvl fvl, match_vallist dvl fvl -> 

           recup_fun f sd = Some d -> 

           recup_funct f (List.map transl_def  sd) = 

           Some (snd (transl_def (f,d)))->

           match_val (dclos f dvl) (fclos f fvl) 

 | mctr: forall dvl fvl n, match_vallist dvl fvl -> 

           match_val (dconstr n dvl) (fconstr n fvl) 

with match_vallist:list dval->list fval->Prop:=  

| mnil: match_vallist nil nil 

|mcons: forall dhd fhd dtl ftl, match_val dhd fhd -> 

 match_vallist dtl ftl-> match_vallist (dhd::dtl) (fhd::ftl).




Lemma match_val_nth: 

 forall dl fl, match_vallist dl fl -> 

 forall n dv, nth_error  dl n= Some dv -> 

 exists fv, nth_error fl n= Some fv /\ match_val dv fv.




Lemma match_val_app: 

 forall dl1 fl1, match_vallist dl1 fl1 -> 

 forall dl2 fl2, match_vallist dl2 fl2 -> 

 match_vallist (dl1++dl2) (fl1++fl2).




Lemma match_val_rev: 

 forall dl fl, match_vallist dl fl-> 

 match_vallist (rev dl) (rev fl).




Definition match_env (se:Dml.env) (fe: env):Prop:= 

 forall id v , PTree.get id se = Some v-> 

 exists v' , PTree.get (xO id) fe=Some v' /\ match_val v v'.




Lemma match_env_let: 

 forall e fe x dv fv, match_val dv fv-> 

  match_env e fe-> 

  match_env (PTree.set x dv e) (PTree.set (xO x) fv fe).




Lemma match_empty: 

 match_env (PTree.empty dval) (PTree.empty fval).




Lemma name_cor_empty: 

 name_cor (PTree.empty fval) (Psucc xH).




Lemma set_local_par_match: 

forall vargs fvl,    match_vallist  vargs fvl->

    forall e f l e1,  match_env e f ->

    Dml.set_local_par l  vargs e = Some e1 -> 

    exists f1,

    set_local_par (map (fun n : positive => xO n) l) 

    fvl f = Some f1/\ match_env e1 f1.

VIII. Simulation scheme





Definition transl_prop (se:Dml.env) (d:Dterm) (dv:dval):Prop:= 

 forall fe lid a z (ME: match_env se fe ) (VT: lid <> xH)  

   (NC: name_cor fe lid) (Eq: transl d lid = (a,z)), 

     exists fv, feval_term (List.map transl_def  sd) fe a fv 

                    /\ match_val dv fv.




Definition transl_list_prop (se:Dml.env) (dl :list Dterm) (dvl:list dval):Prop:= 

 forall fe lid al z (ME: match_env se fe )   (VT: lid <> xH) 

         (NC: name_cor fe lid) (Eq: transl_list dl lid = (al,z)), 

     exists fvl, feval_list (List.map transl_def  sd) fe al fvl /\ 

      match_vallist dvl fvl.




Scheme deval_term_ind6 := Minimality for deval_term Sort Prop

 with deval_terml_ind6 := Minimality for deval_list Sort Prop.




Lemma var_correct: 

forall (e : PTree.t dval) (id : positive) (v : dval),

        id<>xH -> e ! id = Some v -> transl_prop e (Dvar id) v.




Lemma field_correct:

 forall (e : Dml.env) (n : nat) (fid : ident) (t : Dterm)

 (vl : list dval) (v : dval),

 deval_term sd e t (dclos fid vl) ->

 transl_prop e t (dclos fid vl) ->

 nth_error vl n = Some v -> transl_prop e (Dfield (S n) t) v.




Lemma clos_correct:

forall (e : Dml.env) (fid : ident) (tl : list Dterm) (vl : list dval)

(d : def),

  recup_fun fid sd = Some d ->deval_list sd e tl vl ->

  transl_list_prop e tl vl ->

  transl_prop e (Clos fid tl) (dclos fid vl).




Lemma con_correct:

 forall (e : Dml.env) (n : nat) (tl : list Dterm) (vl : list dval),

 deval_list sd e tl vl ->

 transl_list_prop e tl vl -> transl_prop e (Dcon n tl) (dconstr n vl).




Lemma Ple_pos : 

 forall n, Ple xH n .




Lemma Zl34: 

 forall x y, Ple x y -> x <> xH -> y<>xH.




Lemma let_correct:  

forall (e : Dml.env) (id : positive) (t1 : Dterm) (v1 : dval)

(t2 : Dterm) (v2 : dval),

deval_term sd e t1 v1 ->

transl_prop e t1 v1 -> id <> xH -> 

deval_term sd (PTree.set id v1 e) t2 v2 ->

transl_prop (PTree.set id v1 e) t2 v2 ->

transl_prop e (Dlet id t1 t2) v2.










Lemma app_correct:

forall (e : Dml.env) (t1 : Dterm) (fid : ident) (vl : list dval)

(targs : list Dterm) (vargs : list dval) (d : def) (e1 : Dml.env)

(v : dval) (info : option ident),

deval_term sd e t1 (dclos fid vl) ->

transl_prop e t1 (dclos fid vl) ->

recup_fun fid sd = Some d ->

deval_list sd e targs vargs ->

transl_list_prop e targs vargs ->  

list_norepet (funct_par d) -> (forall x, In x (funct_par d) -> x<>xH) ->  

Dml.set_local_par (funct_par d) (dclos fid vl :: vargs)

(PTree.empty dval) = Some e1 ->

deval_term sd e1 (funct_body d) v ->

transl_prop e1 (funct_body d) v ->

info = None \/ info = Some fid ->

transl_prop e (Dapp info t1 targs) v.













Lemma match_correct: 

 forall (e : Dml.env) (a : Dterm) (pl : list dpat) (n : nat)

 (vl : list dval) (xl : list ident) (p : Dterm) (e1 : Dml.env)

 (v : dval),

 deval_term sd e a (dconstr n vl) ->

 transl_prop e a (dconstr n vl) ->

 nth_error pl n = Some (DPatc xl p) ->(forall x, In x xl-> x<>xH) ->

 list_norepet xl -> 

 Dml.set_local_par xl vl e = Some e1 ->

 deval_term sd e1 p v ->

 transl_prop e1 p v -> transl_prop e (Dmatch a pl) v.




Lemma nil_correct:

   forall e : Dml.env, transl_list_prop e nil nil.




Lemma cons_correct:

 forall (e : Dml.env) (hd : Dterm) (vhd : dval) (tl : list Dterm)

 (vtl : list dval),

 deval_term sd e hd vhd ->

 transl_prop e hd vhd ->

 deval_list sd e tl vtl ->

 transl_list_prop e tl vtl ->

 transl_list_prop e (hd :: tl) (vhd :: vtl).




Lemma transl_cor:

forall (e : Dml.env) (d : Dterm) (d0 : dval),

deval_term sd e d d0 -> transl_prop e d d0.




Theorem transl_correct: 

 forall se d dv, deval_term sd  se d dv->

 forall fe lid a z (ME: match_env se fe ) 

         (VT:lid<>xH)

         (NC: name_cor fe lid)

         (Eq : transl d lid = (a,z)), 

     exists fv, feval_term (List.map transl_def  sd) fe a fv /\ match_val dv fv.




End Cor.




Lemma recup_correct: 

 forall sf ,

  list_norepet (map (@fst ident def) sf) -> 

  forall f d,recup_fun f sf = Some d -> 

           recup_funct f  (List.map transl_def  sf)= Some (snd (transl_def (f,d))).




Lemma transl_def_ident: 

 forall sf, 

   (map (@fst ident def) sf) =(map (@fst ident funct)  (map transl_def sf)).

IX. Semantics preservation


Theorem transl_prog_correct: 

 forall p v, 

 Dml.eval_prog p v ->  

 exists fv , eval_prog (transl_prog p) fv /\ match_val (prog_def p) v fv.