Library Fml_sem

Equivalence between Nml big-step semantics with environment and based on substitution

Author : Zaynah Dargaye

Created : 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import Fml.

Require Import Fml_subst.

Require Import f2cps_help.

Require Import f2cps.




Definition eval_env := Fml.eval_term.

Definition eval_subst:= Fml_subst.eval_term.

Definition eval_list_env := Fml.eval_list.

Definition eval_list_subst:= Fml_subst.eval_list.

Definition Subst:= fun x =>fun y => subst_rec x y O.

Definition Subst_list:= fun x=>fun y => subst_list_rec x y O.

I. Relation between "terms-values" and "semantics-values"





Inductive val_atom: val -> term->Prop:= 

| va_clos: forall n t vl  al, 

            val_atomlist vl al -> 

            val_atom (clos n t vl) (Lamb n (subst_rec (lift_list al (S n) )t (S n)))

| va_closr: forall n t vl  al, 

            val_atomlist vl al -> 

            val_atom (closr n t vl) (Mu n (subst_rec (lift_list al (S (S n))) t (S (S n))))

| va_con: forall n  vl al, 

            val_atomlist vl al ->

            val_atom (constr n vl) (Con n al)

with val_atomlist: list val -> list term -> Prop:= 

|va_nil: val_atomlist nil nil 

| va_cons: forall v a vl al , 

           val_atom v a ->

           val_atomlist vl al ->

           val_atomlist (v::vl) (a::al).




Scheme val_atom_ind6 := Minimality for  val_atom Sort Prop

 with val_atomlist_ind6 := Minimality for  val_atomlist Sort Prop.




Lemma val_atomlist_nth: 

 forall vl al, val_atomlist vl al ->

   forall n v (NTH: nth_error vl n= Some v), 

     exists a, nth_error al n = Some a /\ val_atom v a.




Lemma val_atomlist_nth2: 

 forall vl al, val_atomlist vl al ->

   forall n a (NTH: nth_error al n= Some a), 

     exists v, nth_error vl n = Some v /\ val_atom v a.




Lemma val_atom_app: 

 forall vl1 al1, val_atomlist vl1 al1 ->

  forall vl2 al2 (AV: val_atomlist vl2 al2) , 

    val_atomlist (vl1++vl2) (al1++al2).




Lemma val_atom_rev: 

 forall vl al , val_atomlist vl al -> 

   val_atomlist (rev vl) (rev al).




Lemma val_atom_length: 

 forall vl al , val_atomlist vl al -> length al = length vl.




Lemma val_atom_eval : 

 forall v a, val_atom v a -> eval_subst a a.




Lemma val_atom_atom: 

 forall v a, val_atom v a -> is_atom a=true.




Lemma val_atom_list: 

    forall v a, val_atomlist v a -> is_atom_list a=true.

II.Big-step with environment corresponds to big-step based on substitution


Definition eval_env_subst_equiv (e:list val) (t:term) (v:val):Prop:=

        forall al (VAL: val_atomlist e al) , 

        exists w, eval_subst (Subst al t) w /\

                       val_atom v w.




Definition eval_list_env_subst_equiv (e:list val) (t:list term) (v:list val):Prop:=

        forall al (VAL: val_atomlist e al) , 

        exists w, eval_list_subst (Subst_list al t) w /\

                       val_atomlist v w.




Lemma subst_rec_nth: 

 forall l n v m, nth_error l n = Some v ->

   subst_rec l (Var (n+m)) m =  v.




Lemma subst_nth: 

 forall l n v,  nth_error l n = Some v ->

   Subst l (Var n) =  v.




Lemma var_1: 

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

        nth_error e n = Some v -> 

        eval_env_subst_equiv e (Var n) v.




Lemma lamb_1:  

 forall (n : nat) (e : list val) (t : term),

  eval_env_subst_equiv e (Lamb n t) (clos n t e).




Lemma mu_1: 

 forall (n : nat) (e : list val) (t : term),

  eval_env_subst_equiv e (Mu n t) (closr n t e).




Lemma con_1:  

 forall (e : list val) (n : nat) (tl : list term) (vl : list val),

 Fml.eval_list e tl vl ->

 eval_list_env_subst_equiv e tl vl ->

 eval_env_subst_equiv e (Con n tl) (constr n vl).




Lemma app_1:

  forall (e : list val) (tf : term) (tl : list term) (n : nat)

  (v : val) (tb : term) (vl e1 : list val),

   Fml.eval_term e tf (clos n tb e1) ->

   eval_env_subst_equiv e tf (clos n tb e1) ->

   Fml.eval_list e tl vl ->

   eval_list_env_subst_equiv e tl vl ->

   length tl = S n ->

   Fml.eval_term (rev vl ++ e1) tb v ->

   eval_env_subst_equiv (rev vl ++ e1) tb v ->

   eval_env_subst_equiv e (App tf tl) v.




Lemma appr_1: 

forall (e : list val) (tf : term) (tl : list term) (n : nat)

 (v : val) (tb : term) (vl e1 : list val),

 Fml.eval_term e tf (closr n tb e1) ->

 eval_env_subst_equiv e tf (closr n tb e1) ->

 Fml.eval_list e tl vl ->

 eval_list_env_subst_equiv e tl vl ->

 length tl = S n ->

 Fml.eval_term (rev vl ++ closr n tb e1 :: e1) tb v ->

 eval_env_subst_equiv (rev vl ++ closr n tb e1 :: e1) tb v ->

 eval_env_subst_equiv e (App tf tl) v.




Lemma nth_psubst: 

forall pl al k n p,

 nth_error pl n = Some p ->

nth_error (subst_patlist_rec al pl k) n = Some (subst_pat_rec al p k).




Lemma match_1:   

   forall (e : list val) (a : term) (n : nat) (vl : list val)

   (pl : list pat) (p : term) (m : nat) (v : val),

   Fml.eval_term e a (constr n vl) ->

   eval_env_subst_equiv e a (constr n vl) ->

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

   length vl = m ->

   Fml.eval_term (rev vl ++ e) p v ->

   eval_env_subst_equiv (rev vl ++ e) p v ->

   eval_env_subst_equiv e (Match a pl) v.




Lemma let_1:

 forall (e : list val) (a1 a2 : term) (v1 v : val),

  Fml.eval_term e a1 v1 ->

  eval_env_subst_equiv e a1 v1 ->

  Fml.eval_term (v1 :: e) a2 v ->

  eval_env_subst_equiv (v1 :: e) a2 v ->

  eval_env_subst_equiv e (tLet a1 a2) v.




Lemma nil_1:

  forall e : list val, eval_list_env_subst_equiv e nil nil.




Lemma cons_1:  

 forall (e : list val) (hd : term) (vhd : val) (tl : list term)

  (vtl : list val),

  Fml.eval_term e hd vhd ->

  eval_env_subst_equiv e hd vhd ->

  Fml.eval_list e tl vtl ->

  eval_list_env_subst_equiv e tl vtl ->

  eval_list_env_subst_equiv e (hd :: tl) (vhd :: vtl).




Theorem eval_env_subst_correct:   

    forall (l : list val) (t : term) (v : val),

       Fml.eval_term l t v -> eval_env_subst_equiv l t v.

III. Big-step based on substitution corresponds to big-step with environment


Definition eval_subst_env_equiv (t:term) (v:term):Prop:= 

 forall al b e

    (VAL: val_atomlist e al)

    (SE: Subst al b =  t) , 

   exists w, eval_env e b w /\ val_atom w v .




Definition eval_list_subst_env_equiv (t:list term) (v:list term):Prop:= 

 forall al b e

    (VAL: val_atomlist e al)

    (SE: Subst_list al b =  t) , 

   exists w, eval_list_env e b w /\ val_atomlist w v .




Lemma mu_2:

forall (ari : nat) (t : term),

 eval_subst_env_equiv (Mu ari t) (Mu ari t).







Lemma lamb_2:

   forall (ari : nat) (t : term),

   eval_subst_env_equiv (Lamb ari t) (Lamb ari t).







Lemma app_2:  

  forall (t1 : term) (t2 vb : list term) (t v : term) (ari : nat),

  eval_term t1 (Lamb ari t) ->

  eval_subst_env_equiv t1 (Lamb ari t) ->

  length t2 = S ari ->

  eval_list t2 vb ->

  eval_list_subst_env_equiv t2 vb ->

  eval_term (subst_rec (rev vb) t 0) v ->

  eval_subst_env_equiv (subst_rec (rev vb) t 0) v ->

  eval_subst_env_equiv (App t1 t2) v.







Lemma appr_2:   

 forall (t1 : term) (t2 vb : list term) (t v : term) (ari : nat),

 eval_term t1 (Mu ari t) ->

 eval_subst_env_equiv t1 (Mu ari t) ->

 length t2 = S ari ->

 eval_list t2 vb ->

 eval_list_subst_env_equiv t2 vb ->

 eval_term (subst_rec (rev vb ++ Mu ari t :: nil) t 0) v ->

 eval_subst_env_equiv (subst_rec (rev vb ++ Mu ari t :: nil) t 0) v ->

 eval_subst_env_equiv (App t1 t2) v.










Lemma let_2:   

 forall t1 t2 v1 v2 : term,

  eval_term t1 v1 ->

  eval_subst_env_equiv t1 v1 ->

  eval_term (subst_rec (v1 :: nil) t2 0) v2 ->

  eval_subst_env_equiv (subst_rec (v1 :: nil) t2 0) v2 ->

  eval_subst_env_equiv (tLet t1 t2) v2.




Lemma con_2:

 forall (n : nat) (l vl : list term),

  eval_list l vl ->

  eval_list_subst_env_equiv l vl ->

  eval_subst_env_equiv (Con n l) (Con n vl).







Lemma Pat_nth: 

forall l p l1 nt n ca,

  nth_error (subst_patlist_rec l1  l nt) p =

     Some (Patc n ca) -> 

 exists c , ca = subst_rec (lift_list l1 n) c  (nt+n) /\ 

                  nth_error l p = Some (Patc n c).




Lemma match_2:    

 forall (t : term) (n : nat) (lv : list term) (p : list pat)

  (ca v : term),

  eval_term t (Con n lv) ->

  eval_subst_env_equiv t (Con n lv) ->

  nth_error p n = Some (Patc (length lv) ca) ->

  eval_term (subst_rec (rev lv) ca 0) v ->

  eval_subst_env_equiv (subst_rec (rev lv) ca 0) v ->

  eval_subst_env_equiv (Match t p) v.










Lemma nil_2: 

    eval_list_subst_env_equiv nil nil.




Lemma cons_2: 

  forall (a va : term) (m vm : list term),

   eval_term a va ->

   eval_subst_env_equiv a va ->

   eval_list m vm ->

   eval_list_subst_env_equiv m vm ->

   eval_list_subst_env_equiv (a :: m) (va :: vm).




Theorem eval_subst_env_correct: 

 forall t t0 : term, eval_term t t0 -> 

 eval_subst_env_equiv t t0.