Library p2np

Semantics Preservation of the uncurrying

author : Zaynah Dargaye <dargaye@ensiie.fr>

created : 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import AST.

Require Import Pml.

Require Import Nml.

Require Import p2n.

I . Nterm induction scheme


Section correct_PMterm_ind.




Variables 

 (P : PMterm->Prop)

 (Pl : list PMterm -> Prop) 

 (Pp : pat -> Prop) 

 (Ppl : list pat -> Prop).




Hypothesis 

 (Hv : forall (n:nat), P (TVar n))

 ( Hlet : 

    forall (n1:PMterm), P n1 -> forall (n2:PMterm), P n2 -> P (TLet n1 n2))

 ( Hfun : forall (n:PMterm), P n -> P (TFun  n))

 ( Hletr : 

    forall   (n1:PMterm), P n1 -> forall (n2:PMterm), P n2 -> 

    P (TLetrec n1 n2))

 (Happ : 

    forall (n1:PMterm), P n1 -> forall (n2:PMterm), P n2 -> P (TApply n1 n2)) 

 ( Hcnstr : forall (m:nat) (nl: list PMterm) , Pl nl -> P (TConstr m nl))

 ( Hmtch : 

    forall (n1:PMterm), P n1 -> forall (npl: list pat), Ppl npl -> 

    P (TMatch n1 npl))

 

 ( Hnil : Pl nil) 

 ( Hcons : 

    forall (n: PMterm), P n -> forall (nl: list PMterm) , Pl nl ->Pl (n::nl)) 



 ( Hpnil : Ppl nil)

 ( Hpcons : 

     forall (np:pat) , Pp np -> forall (npl : list pat), Ppl npl -> Ppl (np::npl))

 (Hpat : forall (m:nat) (n:PMterm) , P n -> Pp (Patc m n)).




Fixpoint PMterm_ind2 (n:PMterm) : P n := 

 match n as x return P x with 

 | TVar m=> Hv m

 | TLet n1 n2 =>

      Hlet  n1 (PMterm_ind2 n1) n2 (PMterm_ind2 n2) 

  | TFun n1 => Hfun n1 (PMterm_ind2 n1)

  | TLetrec  n1 n2 => 

      Hletr n1 (PMterm_ind2 n1) n2 (PMterm_ind2 n2) 

  | TApply n1 l => 

      Happ  n1 (PMterm_ind2 n1) l (PMterm_ind2 l) 

  | TConstr m l => 

      Hcnstr m l 

          ((( fix l_ind (l': list PMterm) : Pl l' := 

            match l' as x return Pl x with 

            | nil => Hnil 

            | cons n1 nt => Hcons n1 (PMterm_ind2 n1) nt (l_ind nt)

           end)) l )

  | TMatch n1 npl => 

      Hmtch   n1 (PMterm_ind2 n1) npl 

           ((( fix lp_ind (pl: list pat) : Ppl pl := 

            match pl as x return Ppl x with 

            | nil => Hpnil 

            | cons n1 nt => Hpcons n1 (pat_ind n1) nt (lp_ind nt)

           end)) npl )      

  end 

with pat_ind (pn : pat) : Pp pn := 

 match pn as x return Pp x with 

 | Patc m n1 => Hpat m n1 (PMterm_ind2 n1) 

end .




End correct_PMterm_ind.

II Recursive functions


Fixpoint trad_list  (tl:list PMterm) (ce:cenv) {struct tl}:list Nterm:= 

match tl with 

  | nil => nil 

  | t::l => (trad t ce)::(trad_list l ce)

end.




Definition trad_pat (p : pat) (ce : cenv) := 

match p with 

| Patc n t => NPatc n (trad t (Unknown_n n ce)) 

end.




Fixpoint trad_pat_list (pl : list pat) (ce:cenv) {struct pl}:list npat:= 

match pl with 

| nil => nil 

| p::l => (trad_pat p ce)::(trad_pat_list l ce)

end.




Fixpoint uncurry (tf : PMterm) (ce:cenv) (n:nat) {struct tf}:nat*Nterm:= 

match tf with 

 | TFun t1 => uncurry t1 ce (S n) 

 | _ => (n, NFun n  (trad tf (Unknown_n (S n) ce)) )

end.




Fixpoint uncurry_rec (tf : PMterm) (ce:cenv) (n:nat) {struct tf}:nat*Nterm := 

match tf with 

 | TFun t1 => uncurry_rec t1 ce (S n) 

 | _ => (S n, (trad tf (Unknown_n (S (S n)) (Known (S n)::ce))))

end.




Fixpoint PMFun (n:nat) (t:PMterm) {struct n}:PMterm:=

 match n with 

 | O => t

 | S k => (PMFun k (TFun t))

 end.

Properties of intermediate functions


Lemma uncurry_nb: 

 forall n1 ce k j n0 , 

    uncurry n1 ce k = (j,n0) -> 

    le k j.




Lemma uncurry_rec_nb: 

 forall n1 ce k j n0 , 

    uncurry_rec n1 ce k = (j,n0) -> 

    lt k j.




Lemma MF_TF : 

 forall n t  , 

  TFun (PMFun n t) = PMFun n (TFun t).




Lemma Unknown_comm: 

 forall n ce, (Unknown_n n (Unknown::ce)) = Unknown::(Unknown_n n ce).




Lemma uncurry_inv : 

 forall n1 ce k j n0, 

  uncurry n1 ce k= (plus k j, n0) ->

  exists n, n1 = PMFun j n /\ (forall t, n<>TFun t) /\

                n0 = (NFun (k+j) (trad n (Unknown_n (S(k+j)) ce))).




Lemma uncurry_rec_inv : 

 forall n1 ce k j n0, 

  uncurry_rec n1 ce k= (S(plus k j), n0) ->

  exists n, n1 = PMFun j n /\ (forall t, n<>TFun t) /\

                n0 = (trad n (Unknown_n (S(S(k+j))) (Known (S(k+j))::ce))).




Lemma Runcurry_rec_simpl:

forall n nb k,

  (forall t : PMterm, nb <> TFun t )->

  Runcurry_rec (PMFun n nb) k =  ((plus n k), nb).




Lemma Runcurry_simpl:

 forall n nb,(forall t : PMterm, nb <> TFun t) ->

  Runcurry (TFun (PMFun n nb)) = Some (n, nb).







Lemma Runcurry_inv: 

 forall t1 k n t, 

 Runcurry_rec t1 k = (n,t) ->

 (forall t2, t<>TFun t2) /\

 le k n.




Lemma PMF_cor : 

forall t1 ar t k, 

(Runcurry_rec t1 k) = (ar , t) -> 

  t1 = (PMFun (minus ar k) t).




Lemma transl_uncurry:

forall n nb ce,

   transl ce (TFun (PMFun n nb)) (trad (TFun (PMFun n nb)) ce)->

   transl (Unknown_n (S n) ce) nb (trad nb (Unknown_n (S n) ce)).

Properties of the relation and the translation on lists of terms


Lemma transl_length: 

 forall l1 l2 ce, 

  transl_list ce l1 l2 -> length l1 = length l2.




Lemma transl_append : 

 forall l1 l2 l3 l4 ce, 

  transl_list ce l1 l2-> transl_list ce l3 l4 -> transl_list ce (l1++l3) (l2++l4).




Lemma transl_list_rev : 

 forall l1 l2 ce, 

    transl_list ce l1 l2 -> transl_list ce (rev l1) (rev l2).




Lemma trad_list_length: 

 forall l ce, length l = length (trad_list l ce).




Lemma trad_list_append: 

 forall l1 l2 ce, trad_list l1 ce ++trad_list l2 ce = trad_list (l1++l2) ce.




Lemma trad_list_rev: 

 forall l1 ce, trad_list (rev l1) ce = rev (trad_list l1 ce).

Properties of the uncurrying of application


Fixpoint app_curried

(ce: cenv) (a: PMterm) (args: list Nterm) {struct a}: cur_app :=

match a with

| TVar n =>

  if var_has_arity ce n (List.length args) 

   then (nary n args) else  unary

| TApply a1 a2 =>

  app_curried ce a1 ((trad a2 ce) :: args)

| _ =>  unary

end.




Lemma app_curried_Rapp_curried:

forall n1 ce l ,

 app_curried ce n1 (trad_list l ce ) = unary ->

  Rapp_curried ce n1 l = Runary.




Fixpoint Seq_app (a:PMterm) (l:list PMterm) {struct l} :PMterm:= 

 match l with  

 | nil => a 

 | b::k => Seq_app (TApply a b) k

 end .




Fixpoint Seq_app_rev (a:PMterm) (l:list PMterm) {struct l} :PMterm:= 

 match l with  

 | nil => a 

 | b::k => (TApply (Seq_app_rev a  k) b)

 end .




Lemma Seq_app_rev_cons : 

 forall l a0 a, 

    Seq_app_rev (TApply a0 a) l = Seq_app_rev a0 (l ++ a :: nil).




Lemma Seq_app_Seq_app_rev: 

 forall  l a, 

  Seq_app a l = Seq_app_rev a  (rev l).




Lemma Seq_app_comm : 

 forall l a  b, 

 TApply (Seq_app a l) b = Seq_app a (l++b::nil).




Lemma Seq_app_eq : 

 forall a b n n0, 

 Seq_app_rev (TVar n) a = Seq_app_rev (TVar n0) b -> 

 a = b/\n=n0.




Lemma Seq_app_app: 

 forall l a b  , 

 exists u , exists v, Seq_app (TApply a b) l = TApply u v.




Fixpoint Seq_napp (a:Nterm) (l:list Nterm) {struct l} :Nterm:= 

 match l with  

 | nil => a 

 | b::k => Seq_napp (NApply a (b::nil)) k

 end .




Fixpoint Seq_napp_rev (a:Nterm) (l:list Nterm) {struct l} :Nterm:= 

 match l with  

 | nil => a 

 | b::k => (NApply (Seq_napp_rev a  k) (b::nil))

 end .




Lemma Seq_napp_rev_cons : 

 forall l a0 a, 

    Seq_napp_rev (NApply a0 (a::nil)) l = 

    Seq_napp_rev a0 (l ++ a :: nil).




Lemma Seq_napp_Seq_napp_rev: 

 forall  l a, 

  Seq_napp a l = Seq_napp_rev a  (rev l).




Lemma app_curried_append: 

 forall n1 ce l1 n l2, 

   app_curried ce n1 l1 = nary n l2 -> 

   exists l3, l2 = l3++l1.




Lemma app_curried_inv : 

 forall n1 ce l1 n l ,

   app_curried ce n1 l1 = nary n (rev l++l1) -> 

  exists pl,n1 = (Seq_app (TVar n) pl) /\ 

                         rev l = trad_list pl ce/\

                         var_has_arity ce n (length (rev l++l1)) =true.




Lemma Rapp_curried_ok:

forall pl n ce l,

   var_has_arity ce n ((length pl)+length l) = true ->  

   Rapp_curried ce (Seq_app_rev (TVar n) pl) l = 

   Rnary n ((rev pl)++l).




Lemma Rapp_app_curriedn : 

forall t1 l ce args n, 

 Rapp_curried ce t1 l = Rnary n args ->

 app_curried ce t1 (trad_list l ce) = nary n (trad_list args ce).




Lemma var_has_arity_one: 

 forall n0 m k ce, 

 k<>  m ->

  var_has_arity ce n0 m = true->

  var_has_arity ce n0 k = false.




Lemma transl_Seq_correct: 

forall pl ce n m,

  var_has_arity ce n m  = true -> 

  le (length pl ) m ->

  transl ce (Seq_app_rev (TVar n) pl)

                (trad (Seq_app_rev (TVar n) pl) ce) ->

             transl_list ce pl (trad_list pl ce).

I. Correctness of the uncurrying relation





Definition transl_correct (t:PMterm):= 

 forall ce,transl ce t  (trad t ce).




Definition transl_pat_correct (p:pat) :=

 forall ce,transl_pat ce p (trad_pat p ce).




Definition transl_pat_list_correct (pl:list pat):=

 forall ce,transl_pat_list ce pl (trad_pat_list pl ce).




Definition transl_list_correct (tl: list PMterm) :=

 forall ce,transl_list ce tl (trad_list tl ce).




Lemma transl_var_correct:

 forall n : nat, transl_correct (TVar n).




Lemma transl_let_correct:

 forall n1 : PMterm,transl_correct n1 ->

 forall n2 : PMterm, transl_correct n2 -> transl_correct (TLet n1 n2).




Lemma transl_fun_correct :

 forall n : PMterm, transl_correct n -> transl_correct (TFun n).




Lemma transl_letrec_correct:

 forall n1 : PMterm,transl_correct n1 ->

 forall n2 : PMterm,transl_correct n2 -> 

 transl_correct (TLetrec n1 n2).




Lemma transl_apply_correct:

 forall n1 : PMterm,transl_correct n1 ->

 forall n2 : PMterm,transl_correct n2 -> 

 transl_correct (TApply n1 n2).




Lemma transl_constr_correct:

 forall (m : nat) (nl : list PMterm),

 transl_list_correct nl -> transl_correct (TConstr m nl).




Lemma transl_match_correct:

 forall n1 : PMterm,transl_correct n1 ->

 forall npl : list pat,transl_pat_list_correct npl -> 

 transl_correct (TMatch n1 npl).




Lemma transl_nil_correct:transl_list_correct nil.




Lemma transl_cons_correct:

 forall n : PMterm,transl_correct n ->

 forall nl : list PMterm,transl_list_correct nl -> 

 transl_list_correct (n :: nl).




Lemma trans_pnil_correct: transl_pat_list_correct nil.




Lemma transl_pcons_correct:

 forall np : pat,transl_pat_correct np ->

 forall npl : list pat,transl_pat_list_correct npl -> 

 transl_pat_list_correct (np :: npl).




Lemma transl_pat_cor:

forall (m : nat) (n : PMterm),

 transl_correct n -> transl_pat_correct (Patc m n).




Theorem trans_correct_prop:

   forall n : PMterm, transl_correct n.

Intermediate properties for the semantics preservation of the relation of uncurrying





Definition is_fun (t:PMterm) (n:nat):= 

 TFun (PMFun n t).




Lemma Runcurry_Some: 

 forall t1 ar t, Runcurry t1 = Some (ar,t) -> t1 = is_fun t ar.




Lemma Rapp_app_curried:

forall t1 l ce,

  Rapp_curried ce t1 l = Runary -> 

  app_curried ce t1 (trad_list l ce) = unary.




Lemma Rapp_curried_incr: 

 forall t1 l1 l2 n ce, 

 Rapp_curried ce t1 l1 = Rnary n l2 ->

 exists l3, l2 = l3++l1.




Lemma Rapp_curried_inv : 

forall t1 ce  n0  args  l,

 Rapp_curried ce t1 l = Rnary n0 (args++l) ->

 t1 = Seq_app (TVar n0) args /\

 var_has_arity ce n0  (length (args++l)) = true.




Lemma inf_arity_uncur:

forall l ce n0 n,

 nth_error ce n0 = Some (Known n) ->

(length l <  n)%nat -> Rapp_curried ce (TVar n0) l = Runary.

II. Correspondence relation between environments





Fixpoint PLam_n (n : nat) (a : PMterm) {struct n} : PMterm :=

match n with

  | O => a

  | S m => TFun (PLam_n m a)

  end.




Definition ncurry_clos (n: nat) (clos: Nval) (args e0: list Nval): Nval :=

  NClos 0 (args ++ clos :: e0) (NLam_n (n - length args) (ncurry_body n)) .




Definition pcurry_clos (n:nat) (a:PMterm) (args e:list PMval) :=

 PMClos  (args++e) (PMFun (n- (length args))a ) .




Definition pcurry_clos_rec (n:nat) (a:PMterm) (args e:list PMval) :=

 PMClos (args++(PMClos_rec e (PMFun n a) )::e) 

          (PMFun (minus n (length args)) a ).




Inductive match_val: PMval -> Nval -> Prop :=

 | match_val_constr : forall n vl nvl, 

          match_env (Unknown_n (length vl) nil) vl nvl ->

          match_val (PMConstr n vl) (Nconstr n nvl) 

  | match_val_clos: forall u e m e' ce,

      transl (Unknown :: ce) u m ->

      match_env ce e e' ->

      match_val (PMClos e u) (NClos 0 e' m)

  | match_val_clos_rec: forall u e m e' ce,

      transl (Unknown::Unknown:: ce) u m ->

      match_env ce e e' ->

      match_val (PMClos_rec e u ) (NClos_rec 0 e' m)

  | match_val_curry: forall ar u ue m me ce args args' e'' ,

      transl (Unknown_n (S ar) ce) u m ->

      match_env ce ue me ->

        le (List.length args)  ar ->

      match_env (Unknown_n (length args) nil) args args' ->

      match_val 

       (pcurry_clos ar u args ue) (ncurry_clos ar (NClos ar me m ) args' e'') 

   | match_val_curry_rec: forall ar u ue m me ce args args' e'' ,

      args <> nil -> 

      transl (Unknown_n  (S ar) (Known ar::ce)) u m ->

      match_env ce ue me ->

        le (List.length args)  ar ->

      match_env (Unknown_n (length args) nil) args args' ->

      match_val 

       (pcurry_clos_rec ar u args ue) (ncurry_clos ar (NClos_rec ar me m ) args' e'') 

   | match_val_curry_rec_init: forall ar ce u m ue me e'',

      transl (Unknown_n  (S (S ar)) ((Known (S ar))::ce)) u m ->

      match_env ce ue me ->

       match_val 

           (PMClos_rec ue (is_fun  u  ar) )

           (ncurry_clos  (S ar) (NClos_rec (S ar) me m ) nil e'')

with match_env: cenv -> (list PMval) -> (list Nval) -> Prop :=

  | match_env_nil:

      match_env nil nil nil

  | match_env_cons: forall ar ce uv ue mv me,

      match_val_arity ar uv mv -> match_env ce ue me ->

      match_env (ar :: ce) (uv :: ue) (mv :: me)

with match_val_arity: arity -> PMval -> Nval -> Prop :=

  | match_val_unknown: forall uv mv,

      match_val uv mv ->

      match_val_arity Unknown uv mv

 | match_val_known: forall ar u ue m me ce  ,

      transl (Unknown_n    (S ar) ce) u m ->

      match_env ce ue me ->

       match_val_arity (Known ar) 

       (pcurry_clos ar u nil ue) (NClos ar me m ) 

  | match_val_known_Or : forall u m e e' ce ,

       transl (Unknown::Unknown:: ce) u m ->

      match_env ce e e' ->

      match_val_arity (Known O)  (PMClos_rec e u) (NClos_rec 0 e' m)

  | match_val_known_rec: forall ar u ue m me ce  ,

      transl (Unknown_n (S (S ar)) ((Known (S ar))::ce)) u m ->

      match_env ce ue me -> 

       match_val_arity (Known (S ar)) 

       (PMClos_rec ue (is_fun u ar)  ) (NClos_rec (S ar) me m) .




Lemma Unknown_n_length: 

 forall n , 

 length (Unknown_n n nil) = n.




Lemma Unknown_inf: 

 forall m n, 

 lt n m ->  nth_error (Unknown_n m nil) n = Some Unknown.




Lemma Unknown_n_nth: 

forall A n (l:list A) (v:A) info ,

 nth_error (Unknown_n (length l) nil) n = Some info -> 

 nth_error l n = Some v-> 

 info = Unknown.




Lemma match_env_inv:

forall e ce ne n v,

  match_env ce e ne -> 

  nth_error e n = Some v -> 

  exists info, exists nv, 

         nth_error ce n = Some info /\ 

         nth_error ne n = Some nv /\

         match_val_arity info v nv.




Lemma match_env_form_ce: 

forall ce n0 n1 e ne ,

 nth_error ce n0 = Some (Known n1) -> 

 match_env ce e ne -> 

 (exists a, exists e',

 Peval e (TVar n0) (pcurry_clos n1 a nil e' )) \/

 (exists a, exists e',

 Peval e (TVar n0) (PMClos_rec a  e' )).




Lemma match_env_append : 

 forall ce1 ce2 pe1 pe2 ne1 ne2, 

 match_env ce1 pe1 ne1 -> match_env ce2 pe2 ne2 ->

 match_env (ce1++ce2) (pe1++pe2) (ne1++ne2).




Lemma match_env_Unknown_n: 

 forall n ce, 

 Unknown_n n ce = (Unknown_n n nil)++ce.




Lemma match_env_length : 

 forall ce pe ne , 

 match_env ce pe ne -> 

   length ce = length pe /\ length ce = length ne /\ length pe = length ne.




Lemma match_env_rev : 

 forall vl nvl , 

 match_env (Unknown_n (length vl) nil) vl nvl -> 

 match_env (Unknown_n (length vl) nil) (rev vl) (rev nvl).

III. Properties on evaluation


Lemma Peval_length : 

 forall pl vl pe, 

 Peval_list pe pl vl -> length pl = length vl.




Lemma Neval_length : 

 forall pl vl pe, 

 Neval_list pe pl vl -> length pl = length vl.




Lemma Neval_append : 

 forall nl1 nl2 vl1 vl2 ne, 

 Neval_list ne nl1 vl1 -> Neval_list ne nl2 vl2 -> 

 Neval_list ne (nl1++nl2) (vl1++vl2).




Lemma Neval_ncurry_args : 

 forall l e , 

 Neval_list ((rev l)++e) ( ncurry_args (length l))  l.




Lemma Neval_ncurry_term: 

 forall n e , 

 Neval e (ncurry_term n ) 

              (NClos 0 e (NLam_n (S n) (ncurry_body n)) ).




Lemma Neval_ncurry_term_inv: 

forall n ne n0 nv1 m me,

Neval ne (NApply (ncurry_term (S n)) (NVar n0 :: nil)) nv1 -> 

  nth_error ne n0 = Some (NClos (S n) me m) -> 

  nv1 = ncurry_clos (S n) (NClos (S n) me m) nil ne.




Lemma Neval_Seq_napp_list : 

 forall l a ne v , 

 Neval ne (Seq_napp a l) v -> 

 exists va, exists vl,

   Neval ne a va /\ Neval_list ne l vl.




Lemma Neval_Seq_napp_inv: 

forall nargs l n a ne   nv1 v,

 le   (plus (length nargs) (length l)) n-> 

 Neval ne a (ncurry_clos n v l ne) ->

 Neval ne (Seq_napp a nargs) nv1 -> 

 exists nvargs, 

  Neval_list ne nargs nvargs /\ 

  nv1 = ncurry_clos n v ((rev nvargs)++l) ne .




Lemma Neval_app_opt:

forall l n me m ne vres,

 length l = S(S n) ->

 Neval ((rev l) ++ NClos (S n) me m :: ne)(ncurry_body (S n)) vres ->

 Neval ((rev l) ++ me) m vres.




Lemma Neval_appr_opt: 

forall l n me m ne vres,

 length l = (S(S n)) -> 

 Neval ((rev l) ++ NClos_rec (S n) me m :: ne)

         (ncurry_body (S n)) vres -> 

 Neval ((rev l) ++ NClos_rec (S n) me m :: me) m vres.







Lemma Peval_list_from_Seq: 

forall args a v e,

  Peval e (Seq_app a args) v -> 

  exists vargs,exists va ,Peval_list e args vargs/\ 

  Peval e a va.




Lemma Peval_app_curried_partiel: 

forall args l n e a t e1 vargs,

  le (plus (length args) (length l)) n -> 

 Peval e a (pcurry_clos n t l e1) ->

 Peval_list e args vargs ->

    Peval e (Seq_app a args)  (pcurry_clos n t ((rev vargs)++l) e1) .




Lemma Peval_appr_curried_partiel_rec: 

forall args ar n0 ue u vargs l e, 

S ar = plus (length args) (length l) -> 

 Peval e n0 (pcurry_clos_rec (S ar) u l ue ) -> 

 Peval_list e args vargs ->

 Peval e (Seq_app n0 args) (pcurry_clos_rec (S ar) u ((rev vargs)++l) ue ).




Lemma Peval_appr_curried_partiel: 

forall args ar n0 ue u vargs e, 

S ar = length args -> 

 Peval e (TVar n0) (PMClos_rec ue (is_fun u ar)) -> 

 Peval_list e args vargs ->

 Peval e (Seq_app (TVar n0) args) (pcurry_clos_rec (S ar) u (rev vargs) ue ).




Lemma ncurry_args_length : 

 forall n , length (ncurry_args n) = n .




Lemma ncurry_body_final : 

forall args' ar va me  m vres e'',

   length args' = ar ->

   Neval (va :: args' ++ me) m vres ->

    Neval (va :: args' ++ NClos ar me m :: e'') (ncurry_body ar) vres.




Lemma ncurry_body_final_rec: 

forall args' ar va me  m vres e'', 

  length args' = S ar ->

  Neval (va :: args' ++ NClos_rec (S ar) me m :: me) m vres ->

  Neval (va :: args' ++ NClos_rec (S ar) me m :: e'') (ncurry_body (S ar)) vres .




Lemma PMFun_fonc: 

 forall n a b , 

 PMFun n a = PMFun n b -> a=b.




Lemma transl_Seq_app_napp:

forall args  ce a na nargs,

 (forall l , (lt (length l)   (length args) ) ->Rapp_curried ce  a l = Runary) -> 

 transl_list ce args nargs ->

 transl ce a na ->

 transl ce (Seq_app a args) (Seq_napp na nargs).

Properties on the relation for specific constructions


Lemma transl_NLam_n: 

forall ar ce t n0,

  transl (Unknown_n (S ar) ce) t n0 -> 

  transl ce (is_fun t ar ) (NLam_n (S ar) n0).




Lemma n_lam_transl:

forall n ce1 u m, 

  transl (Unknown_n (S (S n)) ce1) u m -> 

  transl (Unknown::ce1) (is_fun u n) (NLam_n  (S n) m).




Lemma transl_pat_list_nth : 

forall pl ce npl n m tn ,

 transl_pat_list ce pl npl -> 

 nth_error pl n = Some (Patc m tn) -> 

 exists t, transl (Unknown_n m ce) tn t /\

               nth_error npl n =Some (NPatc m t).




Lemma NLam_n_body_congruence: 

forall n1 n2 n3,

  NLam_n n1 (ncurry_body n2) = 

 NLam_n O (ncurry_body n3) -> 

 n1 = O /\ n2 =n3.

IV. Simulation scheme





Definition p2n_correct (pe: list PMval) (p:PMterm) (pv:PMval) := 

 forall ce n ne                                       

  (TRANSL: transl ce p n) 

  (ME: match_env ce pe ne), 

  exists nv, Neval ne n nv /\ match_val pv nv.




Definition p2nl_correct (pe: list PMval) (pl:list PMterm) (pv:list PMval) := 

 forall ce nl ne 

  (TRANSL: transl_list ce pl nl) 

  (ME: match_env ce pe ne), 

  exists nv, Neval_list ne nl nv /\ match_env (Unknown_n (length pv) nil) pv nv.




Lemma p2n_var_correct:

forall (n : nat) (e : list PMval) (v : PMval),

        nth_error e n = Some v -> p2n_correct e (TVar n) v.































Lemma p2n_fun_correct:

forall (e : list PMval) (t : PMterm),

 p2n_correct e (TFun t) (PMClos e t).




Lemma p2n_let_correct:

forall (e : list PMval) (t1 t2 : PMterm) (v1 v : PMval),

 Peval e t1 v1 ->

 p2n_correct e t1 v1 ->

 Peval (v1 :: e) t2 v ->

 p2n_correct (v1 :: e) t2 v -> 

 p2n_correct e (TLet t1 t2) v.













Lemma  p2n_letrec_correct:

forall (e : list PMval) (t1 t2 : PMterm) (v : PMval),

 Peval (PMClos_rec e t1 :: e) t2 v ->

 p2n_correct (PMClos_rec e t1 :: e) t2 v ->

 p2n_correct e (TLetrec t1 t2) v.













Lemma p2n_app_correct:

forall (e e' : list PMval) (t t1 t2 : PMterm) (v v2 : PMval),

 Peval e t1 (PMClos e' t) ->

 p2n_correct e t1 (PMClos e' t) ->

 Peval e t2 v2 ->

 p2n_correct e t2 v2 ->

 Peval (v2 :: e') t v ->

 p2n_correct (v2 :: e') t v -> 

 p2n_correct e (TApply t1 t2) v.




























































































































Lemma p2n_app_rec_correct:

forall (e e' : list PMval) (t t1 t2 : PMterm) (v v2 : PMval),

 Peval e t1 (PMClos_rec e' t) ->

 p2n_correct e t1 (PMClos_rec e' t) ->

 Peval e t2 v2 ->

 p2n_correct e t2 v2 ->

 Peval (v2 :: PMClos_rec e' t :: e') t v ->

 p2n_correct (v2 :: PMClos_rec e' t :: e') t v ->

 p2n_correct e (TApply t1 t2) v.








































Lemma p2n_nil_correct:

forall e : list PMval, p2nl_correct e nil nil.




Lemma p2n_cons_correct:

forall (e : list PMval) (t : PMterm) (lt : list PMterm) (v : PMval) (lv : list PMval),

  Peval e t v ->

  p2n_correct e t v ->

  Peval_list e lt lv ->

  p2nl_correct e lt lv -> 

  p2nl_correct e (t :: lt) (v :: lv).




Lemma p2n_constr_correct: 

forall (e : list PMval) (tl : list PMterm) (vl : list PMval) (n : nat),

  Peval_list e tl vl ->

  p2nl_correct e tl vl -> p2n_correct e (TConstr n tl) (PMConstr n vl).




Lemma p2n_match_correct: 

forall (e : list PMval) (t : PMterm) (n : nat) (pl : list pat)

    (vl : list PMval) (m : nat) (tn : PMterm) (v : PMval),

  Peval e t (PMConstr n vl) ->

  p2n_correct e t (PMConstr n vl) ->

  nth_error pl n = Some (Patc m tn) ->

  length vl = m ->

  Peval (rev vl ++ e) tn v ->

  p2n_correct (rev vl ++ e) tn v -> p2n_correct e (TMatch t pl) v.




Theorem p2n_eval_correct:

forall (l : list PMval) (p : PMterm) (p0 : PMval),

Peval l p p0 -> p2n_correct l p p0.

V. Semantics preservation of the uncurrying (functional version)


Theorem p2n_trad_correct: 

 forall p  v, 

   Peval nil p v ->

   exists v', Neval nil (trad p nil) v'/\ match_val v v'.