Library n2fp

From Nml to Nml for substitution : semantics preservation

Author : Zaynah Dargaye

Created : 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import AST.

Require Import Nml.

Require Import Fml.

Require Import n2f.




Fixpoint  trans_list (ln:list Nterm):list term:= 

       match ln with 

       | nil => nil 

       |a::m => trans a::trans_list m 

      end .




Fixpoint  trans_pat_list (pl:list npat):list pat:= 

      match pl with 

     | nil => nil 

     | a::m => trans_pat a :: trans_pat_list m 

     end.

I. Correspondence between environments


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

|mclos : forall n env tenv tbody, 

                   match_val_list env tenv -> 

                   match_val (NClos n env tbody)

                                     (clos n (trans tbody) tenv)      

|mclosr : forall n env tenv tbody, 

                       match_val_list env tenv ->

                       match_val (NClos_rec n env tbody)

                                         (closr n (trans tbody) tenv) 

|mconst: forall n l tl,  

      match_val_list l tl -> match_val (Nconstr n l) (constr n tl)

with match_val_list : list Nval->list val->Prop:= 

 |mnil: match_val_list nil nil 

 |mcons: forall n t nl tl, match_val n t -> match_val_list nl tl -> 

        match_val_list (n::nl) (t::tl).




Scheme mv_ind6 := Minimality for match_val Sort Prop

 with mvl_ind6 := Minimality for match_val_list Sort Prop.




Lemma match_val_nth_none : 

 forall l1 l2 , match_val_list l1 l2 -> 

 forall i, nth_error l1 i = None -> nth_error l2 i = None.




Lemma match_val_nth_sm : 

  forall l1 l2 , match_val_list l1 l2 -> 

 forall i v, nth_error l1 i = Some v -> 

 exists tv , nth_error l2 i = Some tv /\ match_val v tv.




Lemma match_val_length: 

  forall l1 l2 , match_val_list l1 l2 -> length l2 = length l1.




Lemma match_val_app: 

 forall l1 l2, match_val_list l1 l2-> 

 forall l3 l4, match_val_list l3 l4 -> 

 match_val_list (l1++l3) (l2++l4).




Lemma match_val_list_rev: 

 forall l1 l2, match_val_list l1 l2 -> 

 match_val_list (rev l1) (rev l2).

Intermediate properties


Lemma trans_length: 

 forall l, length (trans_list l ) = length l.




Lemma eval_length: 

 forall e l v, eval_list e l v -> length v = length l.




Lemma neval_length: 

 forall l v e , Neval_list e l v -> length v = length l.




Lemma trans_pat_nth_sm : 

 forall pl n m tn, 

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

  nth_error (trans_pat_list pl) n = Some (Patc m (trans tn)).

II. Simulation scheme


Definition trans_correct_prop (nenv: list Nval) (n:Nterm) (nv:Nval):Prop:= 

  forall fe, match_val_list nenv fe -> 

  exists v, eval_term fe (trans n)  v /\ match_val nv v.




Definition trans_list_correct_prop 

  (nenv: list Nval) (n:list Nterm) (nv:list Nval):Prop:= 

   forall fe, match_val_list nenv fe -> 

  exists v, eval_list  fe (trans_list n)  v

      /\ match_val_list nv v.




Lemma var_correct:

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

        nth_error e n = Some v -> trans_correct_prop e (NVar n) v.







Lemma fun_correct:

   forall (e : list Nval) (n : nat) (t : Nterm),

   trans_correct_prop e (NFun n t) (NClos n e t).




Lemma let_correct:

 forall (e : list Nval) (t1 t2 : Nterm) (v1 v : Nval),

 Neval e t1 v1 ->

 trans_correct_prop e t1 v1 ->

 Neval (v1 :: e) t2 v ->

 trans_correct_prop (v1 :: e) t2 v ->

 trans_correct_prop e (NLet t1 t2) v.




Lemma letrec_correct:

 forall (e : list Nval) (n : nat) (t1 t2 : Nterm) (v : Nval),

 Neval (NClos_rec n e t1 :: e) t2 v ->

 trans_correct_prop (NClos_rec n e t1 :: e) t2 v ->

 trans_correct_prop e (NLetrec n t1 t2) v.




Lemma app_correct: 

 forall (e : list Nval) (n : nat) (e' : list Nval) (t t1 : Nterm)

 (tl : list Nterm) (v : Nval) (vl : list Nval),

 Neval e t1 (NClos n e' t) ->

 trans_correct_prop e t1 (NClos n e' t) ->

 Neval_list e tl vl ->

 trans_list_correct_prop e tl vl ->

 length tl = S n ->

 Neval (rev vl ++ e') t v ->

 trans_correct_prop (rev vl ++ e') t v ->

 trans_correct_prop e (NApply t1 tl) v.




Lemma appr_correct: 

  forall (e : list Nval) (n : nat) (e' : list Nval) (t t1 : Nterm)

  (tl : list Nterm) (v : Nval) (vl : list Nval),

  Neval e t1 (NClos_rec n e' t) ->

  trans_correct_prop e t1 (NClos_rec n e' t) ->

  Neval_list e tl vl ->

  trans_list_correct_prop e tl vl ->

  length tl = S n ->

  Neval (rev vl ++ NClos_rec n e' t :: e') t v ->

  trans_correct_prop (rev vl ++ NClos_rec n e' t :: e') t v ->

  trans_correct_prop e (NApply t1 tl) v.




Lemma constr_correct:

forall (e : list Nval) (tl : list Nterm) (vl : list Nval) (n : nat),

 Neval_list e tl vl ->

 trans_list_correct_prop e tl vl ->

 trans_correct_prop e (NConstr n tl) (Nconstr n vl).




Lemma match_correct:  

 forall (e : list Nval) (t : Nterm) (n : nat) (pl : list npat)

 (vl : list Nval) (m : nat) (tn : Nterm) (v : Nval),

 Neval e t (Nconstr n vl) ->

 trans_correct_prop e t (Nconstr n vl) ->

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

 length vl = m ->

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

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

 trans_correct_prop e (NMatch t pl) v.




Lemma nil_correct: 

   forall e : list Nval, trans_list_correct_prop e nil nil.




Lemma cons_correct:

forall (e : list Nval) (t : Nterm) (lt : list Nterm) (v : Nval) (lv : list Nval),

Neval e t v ->

trans_correct_prop e t v ->

Neval_list e lt lv ->

trans_list_correct_prop e lt lv ->

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




Theorem trans_correct:

  forall (l : list Nval) (n : Nterm) (n0 : Nval),

       Neval l n n0 -> trans_correct_prop l n n0.