Library f2dp
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Compare_dec.
Require Import EqNat.
Require Import Fml.
Require Import Dml.
Require Import f2d.
I Properties of translation environments
Definition ident_free_in_var_info (id: ident) (vi: var_info) : Prop :=
match vi with
| Var_var id' => id = id'
| Var_field id' pos => id = id'
end.
Definition ident_free_in_var_env (id: ident) (ce: var_env) : Prop :=
exists n, exists vi, In (n, vi) ce /\ ident_free_in_var_info id vi.
Definition not_idents_free_in_var_env (lid:list ident) (ce:var_env) :Prop:=
forall id, In id lid -> ~ident_free_in_var_env id ce .
Lemma name_O :
forall n cl id,
In id (names_params n cl) -> Plt cl id.
Lemma names_1:
forall n cl id,
In id (names_params n cl) -> id <> cl.
Lemma in_shift:
forall ce m n vi,
In (n, vi) (map (shift_var_info m) ce) ->
exists k, n = m+k /\ In (k,vi) ce.
Lemma shiftIn :
forall ce n vi m, In (n,vi) ce -> In (n+m, vi) (map (shift_var_info m) ce).
Lemma ident_var_shift:
forall ce id ,
~ident_free_in_var_env id ce ->
~ident_free_in_var_env id (map (shift_var_info 1) ce).
Lemma ident_vars_let:
forall ce id id2,id<>id2->
~ident_free_in_var_env id ce ->
~ident_free_in_var_env id (cenv_let ce id2 ).
Lemma ident_vars_case:
forall n i0 ce
(A:forall i, Ple (Psucc i0) i -> ~ident_free_in_var_env i ce),
forall i : positive,
Ple ( i0 + (P_of_succ_nat n)) i ->
~ident_free_in_var_env i (cenv_case n ce i0).
Lemma infree:
forall l j n m v,
In (n, v) (cenv_fv j m l) -> exists pos, v=Var_field j pos.
Lemma shift_o:
forall ce, map (shift_var_info O) ce =ce.
Lemma inparams:
forall m j l n v,
In (n,v) (cenv_params m j l) ->
(exists k , In (k,v) l/\ n=k+m) \/ (exists id, Plt id ( j +
P_of_succ_nat m)/\v = Var_var id).
Lemma in_cenv_recfun:
forall m l j n v,
In (n,v) (cenv_recfun m l j) ->
( exists pos, v=Var_field j pos) \/ (exists id, Plt id ( j +
P_of_succ_nat m)/\ v= Var_var id).
Lemma in_cenv_fun:
forall m l j n v,
In (n,v) (cenv_fun m l j) ->
( exists pos, v=Var_field j pos) \/ (exists id, Plt id ( j +
P_of_succ_nat m)/\ v= Var_var id).
Lemma ident_vars_recfun:
forall ari l j ,
forall i : positive, Ple ( j + P_of_succ_nat (S ari)) i->
~ident_free_in_var_env i (cenv_recfun (S ari) l j).
Lemma ident_vars_fun:
forall ari l j ,
forall i : positive, Ple ( j + P_of_succ_nat (S ari)) i->
~ident_free_in_var_env i (cenv_fun (S ari) l j).
Lemma norepetparams:
forall n j , list_norepet (names_params n j).
Lemma recup_none:
forall l x (A: list_norepet (map (@fst ident def) l)), recup_fun x l = None ->
~ In x (map (@fst ident def) l).
Lemma par_constr_not_xH:
forall ari i0 ,
Plt xH i0 ->
( forall x : ident,
In x (names_params ari i0) ->
x <> 1%positive).
Lemma param_not_xH:
forall ari i0 ,
Plt xH i0 ->
( forall x : ident,
In x (i0 :: names_params (S ari) i0) ->
x <> 1%positive).
Lemma names_param_length:
forall n id, length (names_params n id) = n.
Lemma fenv_let_S:
forall fe d1 n finfo, nth_error fe n = Some finfo->
nth_error (fenv_let fe d1) (S n) = Some finfo.
Lemma map_shift_eq:
forall ce n m info,
recup (m+ n) (map (shift_var_info m) ce) = Some info ->
recup n ce = Some info.
Lemma recup_in :
forall ce info n,
recup n ce = Some info-> In (n,info) ce.
Lemma set_local_length_some:
forall lx lv e1, length lv= length lx ->
exists e , set_local_par lx lv e1 = Some e.
Lemma eval_length:
forall e tl vl, eval_list e tl vl -> length vl = length tl.
Lemma fenv_para_app:
forall n fe, fenv_params n fe = (fenv_params n nil) ++ fe.
Lemma fenv_nil_length:
forall n , length (fenv_params n nil) = n .
Lemma fenv_comm:
forall n fe0, None ::fenv_params n fe0 = (fenv_params n (None::fe0)).
Lemma recup_app :
forall n l1 l2 i j, recup n (l1++(l2,i)::nil) = Some j->
recup n l1 = Some j \/ (l2=n /\ i=j).
Section Match_term.
Variable s : list (ident*def ).
Inductive match_term : var_env->fun_env->term->Dterm->Prop:=
|match_var : forall n d ce fe,
transf_var ce n = Some d ->
match_term ce fe (Var n) d
|match_mu : forall ce fe fid d ari body ce1 tl env,
(forall x, In x (funct_par d) -> x <> xH) ->
recup_fun fid s = Some d-> list_norepet (funct_par d)->
(funct_par d) = env::(names_params (S ari) env ) ->
not_idents_free_in_var_env (names_params (S ari) env)
((0,Var_var env):: map (shift_var_info 1)
(cenv_freevars env (var_free (S (S ari)) (@nil nat) body) )) ->
cenv_recfun (S ari) (var_free (S (S ari)) (@nil nat) body) env = ce1->
match_list ce fe (List.map (fun n=>Var n)
(var_free (S (S ari)) (@nil nat) body)) tl ->
match_term ce1 (fenv_recfun fid (S ari) fe) body (funct_body d) ->
match_term ce fe (Mu ari body) (Clos fid tl)
|match_lamb : forall ce fe fid d ari body ce1 tl env,
recup_fun fid s = Some d->
list_norepet (funct_par d)->
(forall x, In x (funct_par d) -> x <> xH) ->
(funct_par d) = env::(names_params (S ari) env ) ->
not_idents_free_in_var_env (names_params (S ari) env)
(cenv_freevars env (var_free (S ari) (@nil nat) body) ) ->
cenv_fun (S ari) (var_free (S ari) (@nil nat) body) env =ce1->
match_list ce fe (List.map (fun n=>Var n)
(var_free (S ari) (@nil nat)body)) tl ->
match_term ce1 (fenv_fun (S ari) fe) body (funct_body d) ->
match_term ce fe (Lamb ari body) (Clos fid tl)
|match_app: forall ce fe tf df targs dargs,
match_term ce fe tf df->
match_list ce fe targs dargs->
match_term ce fe (App tf targs) (Dapp (known_app fe tf) df dargs)
|match_let: forall ce fe id t1 t2 d1 d2,
match_term ce fe t1 d1 -> id<>xH ->
~ident_free_in_var_env id ce ->
match_term ((O,(Var_var id))::List.map (shift_var_info 1) ce)
(fenv_let fe d1) t2 d2 ->
match_term ce fe (tLet t1 t2) (Dlet id d1 d2)
|match_con: forall ce fe m tl dl,
match_list ce fe tl dl ->match_term ce fe (Con m tl) (Dcon m dl)
| match_m: forall ce fe ta da tpl dpl,
match_term ce fe ta da ->match_plist ce fe tpl dpl->
match_term ce fe (Match ta tpl) (Dmatch da dpl)
with match_list:var_env->fun_env->list term->list Dterm->Prop:=
|match_nil:forall ce fe, match_list ce fe nil nil
|match_cons: forall ce fe t d tl dl, match_term ce fe t d->
match_list ce fe tl dl->match_list ce fe (t::tl)(d::dl)
with match_plist: var_env->fun_env->list pat->list dpat->Prop:=
|match_pnil: forall ce fe , match_plist ce fe nil nil
|match_pcons: forall ce fe th dh tl dl,
match_pat ce fe th dh ->match_plist ce fe tl dl->
match_plist ce fe (th::tl) (dh::dl)
with match_pat: var_env->fun_env->pat->dpat->Prop:=
|match_p: forall ce ce1 fe n ta da e ,
list_norepet (names_params ( n) e)->
(forall x, In x (names_params ( n) e) -> x <> xH) ->
cenv_case ( n) ce e= ce1 ->
not_idents_free_in_var_env (names_params ( n) e) ce->
match_term ce1 (fenv_match ( n) fe) ta da->
match_pat ce fe (Patc n ta) (DPatc (names_params ( n) e) da)
.
a- Properties of the reloation of closure conversion
Lemma match_length:
forall ce fe tl dl, match_list ce fe tl dl ->
length dl = length tl.
Lemma match_append:
forall ce fe tl1 dl1, match_list ce fe tl1 dl1 ->
forall tl2 dl2 , match_list ce fe tl2 dl2 ->
match_list ce fe (tl1++tl2) (dl1++dl2).
Lemma match_rev:
forall ce fe tl dl, match_list ce fe tl dl ->
match_list ce fe (rev tl) (rev dl).
Lemma match_plist_nth:
forall ce fe tpl dpl, match_plist ce fe tpl dpl->
forall n tp, nth_error tpl n = Some tp ->
exists dp, nth_error dpl n = Some dp /\
match_pat ce fe tp dp.
Definition match_fin (finfo:fun_info) (v:dval):Prop:=
match finfo with |None =>True
|Some fid =>exists lv, v = (dclos fid lv)
end.
Fixpoint nth_list (A:Set) (e:list A) (l:list nat) {struct l}:option (list A):=
match l with
| nil => Some nil
| a::m => match nth_error e a with | None => None
| Some v => match nth_list e m with | None => None
| Some vl =>Some (v::vl) end
end
end.
Definition get_val_list (e:list val) (l:list nat) := nth_list e l.
Definition get_finfo_list (fe: fun_env) (l:list nat):=nth_list fe l.
Inductive match_fin_list: list fun_info->list dval->Prop:=
|fnil : match_fin_list nil nil
|fcons: forall finfo v fl vl, match_fin finfo v-> match_fin_list fl vl->
match_fin_list (finfo::fl) (v::vl).
III. Correspondence between environments
Inductive match_val: val->dval->Prop:=
| mcon: forall m tvl dvl,
match_vlist tvl dvl -> match_val (constr m tvl) (dconstr m dvl)
|mclos: forall t te fid lv d fe n ce1 cl mvl lfinfo,
recup_fun fid s =Some d->
list_norepet (funct_par d)->
length (funct_par d) = (S (S n)) ->
(forall x , In x (funct_par d) -> x<>xH) ->
get_val_list te (var_free (S n) nil t) = Some mvl->
get_finfo_list fe (var_free (S n) nil t) = Some lfinfo->
match_vlist mvl lv ->
match_fin_list lfinfo lv->
(funct_par d) = cl::(names_params (S n) cl) ->
not_idents_free_in_var_env (names_params (S n) cl)
(cenv_freevars cl (var_free (S n) (@nil nat) t) ) ->
cenv_fun (S n) (var_free (S n) (@nil nat) t) cl = ce1->
match_term ce1 (fenv_fun (S n) fe) t (funct_body d) ->
match_val ( clos n t te ) (dclos fid lv)
|mclosr: forall t te fid lv d fe n ce1 cl mvl lfinfo,
recup_fun fid s =Some d->list_norepet (funct_par d)->
length (funct_par d) = (S (S n)) ->
(forall x , In x (funct_par d) -> x<>xH) ->
get_val_list te (var_free (S (S n) )nil t) = Some mvl->
get_finfo_list fe (var_free (S (S n)) nil t) = Some lfinfo->
match_vlist mvl lv ->
match_fin_list lfinfo lv->
(funct_par d) = cl::(names_params (S n) cl) ->
not_idents_free_in_var_env (names_params (S n) cl)
((0,Var_var cl):: map (shift_var_info 1) (cenv_freevars cl (var_free (S(S n)) (@nil nat) t) ) )->
cenv_recfun (S n) (var_free (S (S n)) (@nil nat) t) cl = ce1->
match_term ce1 (fenv_recfun fid (S n) fe) t (funct_body d) ->
match_val ( closr n t te ) (dclos fid lv)
with match_vlist: list val->list dval->Prop:=
|mnil: match_vlist nil nil
|mc: forall h1 t1 h2 t2, match_val h1 h2->match_vlist t1 t2->
match_vlist (h1::t1) (h2::t2).
Lemma matchv_length:
forall tl dl, match_vlist tl dl ->
length dl = length tl.
Lemma matchv_append:
forall tl1 dl1, match_vlist tl1 dl1 ->
forall tl2 dl2 , match_vlist tl2 dl2 ->
match_vlist (tl1++tl2) (dl1++dl2).
Lemma matchv_rev:
forall tl dl, match_vlist tl dl ->
match_vlist (rev tl) (rev dl).
Definition match_env_intro (vinfo: var_info) (de:env) (v': dval) :Prop:=
match vinfo with
| Var_var id => id<> xH /\ PTree.get id de = Some v'
|Var_field id n => id<> xH /\exists fid, exists lv,
PTree.get id de = Some (dclos fid lv) /\
nth_error lv n = Some v'
end.
Definition match_env (te:list val) (ce:var_env) (fe:fun_env)(de: env) :Prop:=
forall n info,
recup n ce = Some info ->
exists v , nth_error te n = Some v /\
exists finfo, nth_error fe n = Some finfo/\
(exists v' , match_env_intro info de v' /\ match_val v v'/\ match_fin finfo v') .
Lemma fenv_correct:
forall e ce fe de tf fid td v,
match_env e ce fe de ->
known_app fe tf =Some fid ->
match_term ce fe tf td ->
deval_term s de td v -> exists l, v=(dclos fid l).
Lemma match_env_let:
forall id e ce fe de v1 vl d1,
deval_term s de d1 vl-> id<> xH ->
~ ident_free_in_var_env id ce->
match_env e ce fe de->
match_val v1 vl->
match_env (v1::e) ((0, Var_var id) :: map (shift_var_info 1) ce)
(fenv_let fe d1) (PTree.set id vl de).
Lemma match_env_let_spec:
forall id e ce fe de v1 vl (ID: id<>xH),
~ ident_free_in_var_env id ce->
match_env e ce fe de->
match_val v1 vl->
match_env (v1::e) ((0, Var_var id) :: map (shift_var_info 1) ce)
(None:: fe ) (PTree.set id vl de) .
Lemma match_env_match:
forall vl dvl, match_vlist vl dvl->
forall e ce fe de eb e0
(IDs: forall x, In x (names_params (length vl) e0) -> x<>xH) ,
not_idents_free_in_var_env ((names_params (length vl) e0)) ce->
match_env e ce fe de->
set_local_par (names_params (length vl) e0) dvl de = Some eb->
match_env (rev vl ++ e) (cenv_case (length vl) ce e0)
(fenv_params (length vl) fe) eb.
Lemma match_free_vars:
forall l e1 mvl fe0 cl lv lfinfo fid l2 l3 (A:length l2=length l3)
(B: cl <>xH) ,
nth_list e1 l = Some mvl->
nth_list fe0 l = Some lfinfo->
match_vlist mvl lv->
match_fin_list lfinfo lv->
(forall n info, recup n l2 = Some info ->
exists v, nth_error e1 n = Some v /\
(exists finfo : fun_info,
nth_error fe0 n = Some finfo /\
(exists v' : dval,
match_env_intro info
(PTree.set cl (dclos fid (l3 ++ lv)) (PTree.empty dval)) v' /\
match_val v v' /\ match_fin finfo v')))->
match_env e1 (l2++cenv_fv cl (length l2) l) fe0
(PTree.set cl (dclos fid (l3++lv)) (PTree.empty dval)).
Lemma match_freevars:
forall e1 l mvl fe0 lfinfo lv cl fid (ID: cl <> xH),
get_val_list e1 l = Some mvl->
get_finfo_list fe0 l = Some lfinfo->
match_vlist mvl lv->
match_fin_list lfinfo lv->
match_env e1 (cenv_freevars cl l) fe0
(PTree.set cl (dclos fid lv) (PTree.empty dval)).
Lemma match_env_params:
forall vl vargs ,
match_vlist vl vargs ->
forall cl e ce fe0 e1 eb
(IDs : forall x , In x (names_params (length vl) cl) -> x <> xH) ,
not_idents_free_in_var_env (names_params (length vl) cl) ce ->
set_local_par (names_params (length vl) cl) vargs e = Some eb->
match_env e1 ce fe0 e ->
match_env (rev vl++e1) (cenv_params (length vl) cl ce)
(fenv_params (length vl) fe0) eb.
IV. Simulation scheme
Definition match_correct_prop (e: list val) (t:term) (v:val):Prop:=
forall d ce fe de
(ME: match_env e ce fe de)
(M: match_term ce fe t d),
exists v', deval_term s de d v' /\ match_val v v'.
Definition matchl_correct_prop (e: list val) (t:list term) (v:list val):Prop:=
forall d ce fe de
(ME: match_env e ce fe de)
(M: match_list ce fe t d),
exists v', deval_list s de d v' /\ match_vlist v v'.
Lemma let_correct:
forall (e : list val) (a1 a2 : term) (v1 v : val),
eval_term e a1 v1 ->
match_correct_prop e a1 v1 ->
eval_term (v1 :: e) a2 v ->
match_correct_prop (v1 :: e) a2 v ->
match_correct_prop e (tLet a1 a2) v.
Lemma var_correct:
forall (n : nat) (e : list val) (v : val),
nth_error e n = Some v -> match_correct_prop e (Var n) v.
Lemma free_var_1:
forall l e ce fe de tl,
match_env e ce fe de->
match_list ce fe (map (fun n : nat => Var n) l) tl ->
exists lv, (exists mvl,exists lfinfo,
get_val_list e l = Some mvl /\
get_finfo_list fe l = Some lfinfo/\
match_vlist mvl lv /\
match_fin_list lfinfo lv ) /\
deval_list s de tl lv.
Lemma lamb_correct:
forall (n : nat) (e : list val) (t : term),
match_correct_prop e (Lamb n t) (clos n t e).
Lemma mu_correct:
forall (n : nat) (e : list val) (t : term),
match_correct_prop e (Mu n t) (closr n t e).
Lemma constr_correct:
forall (e : list val) (n : nat) (tl : list term) (vl : list val),
eval_list e tl vl ->
matchl_correct_prop e tl vl ->
match_correct_prop e (Con n tl) (constr n vl).
Lemma app_correct:
forall (e : list val) (tf : term) (tl : list term) (n : nat)
(v : val) (tb : term) (vl e1 : list val),
eval_term e tf (clos n tb e1) ->
match_correct_prop e tf (clos n tb e1) ->
eval_list e tl vl ->
matchl_correct_prop e tl vl ->
length tl = S n ->
eval_term (rev vl ++ e1) tb v ->
match_correct_prop (rev vl ++ e1) tb v ->
match_correct_prop e (App tf tl) v.
Lemma appr_correct:
forall (e : list val) (tf : term) (tl : list term) (n : nat)
(v : val) (tb : term) (vl e1 : list val),
eval_term e tf (closr n tb e1) ->
match_correct_prop e tf (closr n tb e1) ->
eval_list e tl vl ->
matchl_correct_prop e tl vl ->
length tl = S n ->
eval_term (rev vl ++ closr n tb e1 :: e1) tb v ->
match_correct_prop (rev vl ++ closr n tb e1 :: e1) tb v ->
match_correct_prop e (App tf tl) v.
Lemma match_correct:
forall (e : list val) (a : term) (n : nat) (vl : list val)
(pl : list pat) (p : term) (m : nat) (v : val),
eval_term e a (constr n vl) ->
match_correct_prop e a (constr n vl) ->
nth_error pl n = Some (Patc m p) ->
length vl = m ->
eval_term (rev vl ++ e) p v ->
match_correct_prop (rev vl ++ e) p v ->
match_correct_prop e (Match a pl) v.
Lemma nil_correct:
forall e : list val, matchl_correct_prop e nil nil.
Lemma cons_correct:
forall (e : list val) (hd : term) (vhd : val) (tl : list term)
(vtl : list val),
eval_term e hd vhd ->
match_correct_prop e hd vhd ->
eval_list e tl vtl ->
matchl_correct_prop e tl vtl ->
matchl_correct_prop e (hd :: tl) (vhd :: vtl).
Theorem match_term_correct:
forall (l : list val) (t : term) (v : val),
eval_term l t v -> match_correct_prop l t v.
End Match_term.
VI. State monotonicity property
Definition match_term_trans (n:term):Prop:=
forall ce fe si sf m , match_term si ce fe n m -> incl si sf ->
(forall i f, recup_fun i si= Some f ->
recup_fun i sf = Some f) ->
match_term sf ce fe n m.
Definition match_list_trans (nl:list term):Prop:=
forall ce fe si sf ml , match_list si ce fe nl ml -> incl si sf ->
(forall i f, recup_fun i si= Some f ->
recup_fun i sf = Some f) ->
match_list sf ce fe nl ml.
Definition match_pat_trans (np:pat):Prop:=
forall ce fe si sf mp, match_pat si ce fe np mp -> incl si sf ->
(forall i f, recup_fun i si= Some f ->
recup_fun i sf = Some f) ->
match_pat sf ce fe np mp.
Definition match_plist_trans (npl: list pat):Prop:=
forall ce fe si sf mpl, match_plist si ce fe npl mpl -> incl si sf->
(forall i f, recup_fun i si= Some f ->
recup_fun i sf = Some f) ->
match_plist sf ce fe npl mpl.
Lemma match_var_spec:
forall ce fe si sf n m, match_term si ce fe (Var n) m ->
incl si sf ->
(forall i f, recup_fun i si= Some f -> recup_fun i sf = Some f) ->
match_term sf ce fe (Var n) m .
Lemma match_freevars_spec:
forall l ce fe si sf m,
match_list si ce fe (map (fun n : nat => Var n) l) m ->
incl si sf ->
(forall i f, recup_fun i si= Some f -> recup_fun i sf = Some f) ->
match_list sf ce fe (map (fun n : nat => Var n) l) m .
Theorem match_trans:
forall n ce fe si sf m
(A :match_term si ce fe n m ), incl si sf ->
(forall i f, recup_fun i si= Some f ->
recup_fun i sf = Some f) ->
match_term sf ce fe n m.
Theorem match_trans':
forall n ce fe si sf m limit
(A :match_term si ce fe n m ), incl si sf ->
(forall i, Plt i limit -> recup_fun i sf = recup_fun i si) ->
(forall i, Ple limit i -> recup_fun i si = None) ->
match_term sf ce fe n m.
Lemma match_pat_trans' :
forall n ce fe si sf m limit
(A :match_pat si ce fe n m ), incl si sf ->
(forall i, Plt i limit -> recup_fun i sf = recup_fun i si) ->
(forall i, Ple limit i -> recup_fun i si = None) ->
match_pat sf ce fe n m.
Definition n2m_match (n:term) :Prop:=
forall si sf p ce fe i j i1 j1 (CM : Plt xH j)
(TR:transf ce fe n si i j= OK p sf i1 j1)
(S2: list_norepet (map (@fst ident def ) si))
( S3:forall x , Ple i x->recup_fun x si = None ),
(forall i, Ple j i ->~ ident_free_in_var_env i ce) ->
match_term sf ce fe n p /\ incl si sf/\ Ple i i1/\ Ple j j1/\
(forall x , Plt x i -> recup_fun x sf = recup_fun x si) /\
(forall x , Ple i1 x->recup_fun x sf = None )/\
( list_norepet (map (@fst ident def ) sf)).
Definition n2m_list_match (n:list term) :Prop:=
forall si sf p ce fe i j i1 j1(CM : Plt xH j)
(TR:transf_list ce fe n si i j = OK p sf i1 j1)
(S2: list_norepet (map (@fst ident def ) si))
( S3:forall x , Ple i x->recup_fun x si = None ) ,
(forall i, Ple j i ->~ ident_free_in_var_env i ce) ->
match_list sf ce fe n p /\ incl si sf/\ Ple i i1/\ Ple j j1/\
(forall x , Plt x i -> recup_fun x sf = recup_fun x si)/\
(forall x , Ple i1 x->recup_fun x sf = None )/\
( list_norepet (map (@fst ident def ) sf)).
Definition n2m_pat_match (np:pat): Prop:=
forall si sf mp ce fe i j i1 j1(CM : Plt xH j)
(TR : transf_pat ce fe np si i j= OK mp sf i1 j1)
(S2: list_norepet (map (@fst ident def ) si))
( S3:forall x , Ple i x->recup_fun x si = None ),
(forall i, Ple j i ->~ ident_free_in_var_env i ce) ->
match_pat sf ce fe np mp /\ incl si sf/\ Ple i i1/\ Ple j j1/\
(forall x , Plt x i -> recup_fun x sf = recup_fun x si)/\
(forall x , Ple i1 x->recup_fun x sf = None )/\
( list_norepet (map (@fst ident def ) sf)).
Definition n2m_pat_list_match (np:list pat): Prop:=
forall si sf mp ce fe i j i1 j1(CM : Plt xH j)
(TR : transf_plist ce fe np si i j= OK mp sf i1 j1)
(S2: list_norepet (map (@fst ident def ) si))
( S3:forall x , Ple i x->recup_fun x si = None ),
(forall i, Ple j i ->~ ident_free_in_var_env i ce) ->
match_plist sf ce fe np mp /\ incl si sf/\ Ple i i1/\ Ple j j1/\
(forall x , Plt x i -> recup_fun x sf = recup_fun x si) /\
(forall x , Ple i1 x->recup_fun x sf = None )/\
( list_norepet (map (@fst ident def ) sf)).
Ltac monadSimpl1 :=
match goal with
| [ |- (bind ?F ?G ?X ?Y ?Z = OK ?X' ?Y' ?Z' ?W) -> _ ] =>
unfold bind at 1;
generalize (refl_equal (F X Y Z));
pattern (F X Y Z) at -1 in |- *;
case (F X Y Z);
[ intro; intro; discriminate
| (let EQ := fresh "EQ" in (intro; intro; intro; intro; intro EQ; try monadSimpl1)) ]
| [ |- (Error = OK _ _ _ _ ) -> _ ] =>
intro; discriminate
| [ |- (OK _ _ _ _ = OK _ _ _ _ ) -> _ ] =>
let h := fresh "H" in
(intro h; injection h; intro; intro; intro; intro; clear h)
| [ |- (_ = OK _ _ _ _ ) -> _ ] =>
let EQ := fresh "EQ" in intro EQ
end.
Ltac monadSimpl :=
match goal with
| [ |- (bind ?F ?G ?X ?Y ?Z = OK ?X' ?Y' ?Z' ?W) -> _ ] => monadSimpl1
| [ |- (Error = OK _ _ _ _ ) -> _ ] => monadSimpl1
| [ |- (OK _ _ _ _ = OK _ _ _ _ ) -> _ ] => monadSimpl1
| [ |- (ret _ _ _ _ = OK _ _ _ _ ) -> _ ] => unfold ret; monadSimpl1
| [ |- (?F _ _ _ _ _ _ = OK _ _ _ _ ) -> _ ] => simpl F; monadSimpl1
| [ |- (?F _ _ _ _ _ = OK _ _ _ _ ) -> _ ] => simpl F; monadSimpl1
| [ |- (?F _ _ _ _ = OK _ _ _ _ ) -> _ ] => simpl F; monadSimpl1
| [ |- (?F _ _ _ = OK _ _ _ _ ) -> _ ] => simpl F; monadSimpl1
| [ |- (?F _ _ = OK _ _ _ _ ) -> _ ] => simpl F; monadSimpl1
| [ |- (?F _ = OK _ _ _ _ ) -> _ ] => simpl F; monadSimpl1
end.
Ltac monadInv H :=
generalize H; monadSimpl.
Ltac omegaContradiction :=
cut False; [contradiction|omega].
Lemma transf_var_match:
forall ce n p fe sf ,
transf_var ce n = Some p -> match_term sf ce fe (Var n) p .
Lemma transf_varl_match:
forall l ce p fe sf ,
transf_varl ce l = Some p ->
match_list sf ce fe (map (fun n => Var n) l) p .
Theorem transf_match:
forall n si sf p ce fe i j i1 j1
(CM: Plt xH j)
(TR:transf ce fe n si i j = OK p sf i1 j1)
(S2: list_norepet (map (@fst ident def ) si))
(S3 : forall x, Ple i x-> recup_fun x si =None),
(forall i, Ple j i ->~ ident_free_in_var_env i ce) ->
match_term sf ce fe n p /\ incl si sf/\ Ple i i1/\ Ple j j1/\
(forall i2 , Plt i2 i ->recup_fun i2 sf = recup_fun i2 si )/\
(forall x, Ple i1 x ->recup_fun x sf = None )/\
( list_norepet (map (@fst ident def ) sf)).
VIII. Semantics preservation of closure conversion
Theorem closure_conversion_correct:
forall t v p (A : transf_program t = Some p)
(B:eval_term nil t v),
exists v', eval_prog p v'/\ match_val (prog_def p) v v'.