``` ```

# 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. ```