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'.