Library Cml_sem

Correspondence between different semantics definition of EpsilonML



Author: Zaynah Dargaye <dargaye@ensiie.fr>

Created: 29th April 2009.

Definition of EpsilonML for substitution (with mu). Definition of semantics in small-step based on substitution, big-step based on substitution and big-step with environment.

Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Cml.
Open Scope nat_scope.

I. Syntax of EpsilonML with mu

Inductive term:Set :=
  | Var : nat -> term
  | Llet : term -> term -> term
  | Fun : term -> term
  | Mu : term->term
  | Apply : term -> term -> term
  | Constr : ident -> list term -> term
  | Match : term -> list pat -> term
with pat :Set :=
  | Pat : ident -> nat -> term -> pat.

II. Induction Scheme
Section term_ind_sect.
Variable
 (P: term->Prop)
 (Pl: list term -> Prop)
 (Pp: pat->Prop)
 (Ppl: list pat ->Prop).

Hypothesis
(Hv: forall n, P (Var n))
(Hl:forall t, P t -> P (Fun t))
(Hmu:forall t, P t-> P(Mu t))
(Hlet: forall t1 t2, P t1 ->P t2 -> P (Llet t1 t2))
(Happ: forall t1 t2, P t1 -> P t2 -> P (Apply t1 t2))
(Hconstr: forall n l, Pl l -> P (Constr n l))
(Hm: forall t pl, P t -> Ppl pl -> P (Match t pl))
(Hnil : Pl nil)
(Hcons: forall t tl, P t -> Pl tl -> Pl (t::tl))
(Hpat: forall x n t, P t -> Pp (Pat x n t))
(Hpnil: Ppl nil)
(Hpcons: forall p pl, Pp p -> Ppl pl-> Ppl (p::pl)).


Fixpoint term_ind2 (t:term): P t:=
 match t as x return P x with
 |Var n => Hv n
 |Llet t1 t2=> Hlet t1 t2 (term_ind2 t1) (term_ind2 t2)
 |Fun t => Hl t (term_ind2 t)
 |Mu t => Hmu t (term_ind2 t)
 |Apply t1 t2 => Happ t1 t2 (term_ind2 t1) (term_ind2 t2)
 |Constr n l => Hconstr n l ((fix l_ind(tl: list term): Pl tl :=
             match tl as x return Pl x with
             | nil => Hnil
             | a::m => Hcons a m (term_ind2 a) (l_ind m)end) l)
 |Match t pl =>Hm t pl (term_ind2 t)
            ((fix pl_ind (pl:list pat) {struct pl}: Ppl pl:=
            match pl as x return Ppl x with
            | nil => Hpnil
            |a::m => Hpcons a m (pat_ind2 a) (pl_ind m)end)pl)
 end
with pat_ind2 (p:pat) {struct p}:Pp p:=
 match p as x return Pp x with
 |Pat y n t => Hpat y n t (term_ind2 t)
 end.
End term_ind_sect.

III. Substitutions and lift

Fixpoint lift_rec (t:term) (n:nat) (ari:nat){struct t}: term:=
 match t with
 | Var i => if lt_ge_dec i n then Var i else Var (i+ari)
 | Fun b => Fun (lift_rec b (S n) ari)
 | Mu b => Mu (lift_rec b (S (S n)) ari)
 | Apply t1 t2 =>
     Apply (lift_rec t1 n ari) (lift_rec t2 n ari)
 |Llet t1 t2 => Llet (lift_rec t1 n ari) (lift_rec t2 (S n) ari)
 |Constr m tl =>
     let fix lift_list_rec (tl:list term) (n:nat) (ari:nat) {struct tl}:list term:=
     match tl with
     | nil => nil
     | a::m => (lift_rec a n ari)::(lift_list_rec m n ari)
     end in Constr m (lift_list_rec tl n ari)
 |Match t pl =>
      let fix lift_patlist_rec (tl:list pat) (n:nat) (ari:nat) {struct tl}:list pat:=
     match tl with
     | nil => nil
     | a::m => (lift_pat_rec a n ari)::(lift_patlist_rec m n ari)
     end in
     Match (lift_rec t n ari) (lift_patlist_rec pl n ari)
 end
with lift_pat_rec (p:pat) (n ari:nat) {struct p}: pat:=
 match p with
 | Pat y k t => Pat y k (lift_rec t (n+ k) ari)
 end.

Definition liftn (t:term) (ari:nat) := lift_rec t O ari .
Definition lift (t:term) := liftn t 1.
Definition lift2 (t:term):= liftn t 2.

Definition liftn_list (tl:list term) (ari:nat) :=
       List.map (fun t =>lift_rec t O ari) tl .
Definition lift_list (tl:list term) := List.map (fun t =>liftn t 1) tl.
Definition lift2_list (tl:list term):= List.map (fun t => liftn t 2) tl.

The simultaneous substitution
Fixpoint subst_rec
  (tl : list term) (t:term) (n : nat) {struct t}: term:=
 match t with
 |Var m =>
 let u:= length tl+n in
     match compare_bd_dec m n u with
      | INF _ => Var m
      | IN _ _ =>
   match nth_error tl (m-n) with |Some w => w | None =>Var m end
      | SUP _=> Var (m+n-u)
    end
 | Fun b =>
       Fun (subst_rec (lift_list tl) b (S n) )
 | Mu b =>
      Mu (subst_rec (lift2_list tl) b (S (S n)))
| Apply t1 t2 =>
       Apply (subst_rec tl t1 n) (subst_rec tl t2 n)
 |Llet t1 t2 =>
       Llet (subst_rec tl t1 n) (subst_rec (lift_list tl) t2 (S n))
 |Constr k l =>
   let fix subst_list_rec
       (tl :list term) (l : list term) (n :nat) {struct l}: list term:=
       match l with
      | nil => nil
      | a::m => (subst_rec tl a n )::(subst_list_rec tl m n)
      end in
       Constr k (subst_list_rec tl l n)
 |Match t1 pl =>
     let fix subst_patlist_rec
      (tl :list term) (l: list pat) (n : nat) {struct l}: list pat:=
      match l with
      | nil => nil
      | a::m => (subst_pat_rec tl a n )::(subst_patlist_rec tl m n )
      end in Match (subst_rec tl t1 n) (subst_patlist_rec tl pl n)
 end
with subst_pat_rec (tl :list term) (p:pat) (n:nat) {struct p}:pat:=
 match p with
 |Pat y m t => Pat y m (subst_rec (liftn_list tl m) t (n+m))
end.

Definition substn (tl:list term) (t:term):= subst_rec tl t O.
Definition Subst (v:term) (t:term):= substn (v::nil) t.
Definition substn_list (tl:list term) (l:list term):=
     List.map (fun t =>substn tl t) l.
Definition Subst_list (v:term) (l:list term):=
      List.map (fun t =>Subst v t) l.

IV. values

Fixpoint is_valeur (t:term) : bool:=
match t with
| Fun t => true
| Mu t => true
| Constr k l =>
      let fix is_valeur_list (tl:list term):bool:=
        match tl with
        |nil => true
        | t::l => if (is_valeur t) then is_valeur_list l else false
        end
       in is_valeur_list l
| _ => false
end.

Fixpoint is_valeur_list (tl:list term):=
 match tl with
        |nil => true
        | t::l => if (is_valeur t) then is_valeur_list l else false
        end.

Inductive abstract:term->Prop:=
|Afun : forall t, abstract (Fun t)
|Amu : forall t, abstract (Mu t).

Definition is_abstract (t:term):{abstract t}+{~abstract t}.

V. evaluation of data types
Definition GMenv:= list ((list ident)).

Fixpoint extract_constr_match (pl : list pat) {struct pl}: list ident:=
 match pl with
 | nil => nil
 | a::l => match a with
              | Pat x m t => x::(extract_constr_match l)
              end
 end.

Definition exists_constr (c:ident) (g:GMenv):Prop:=
 exists l , In l g /\ In c l.

Definition wf_match (pl : list pat) (g:GMenv) :Prop:=
 exists l , In l g /\
  list_permut_norepet (ident) l (extract_constr_match pl).

Inductive valeur : GMenv -> term->Prop:=
| VFun : forall g t, valeur g (Fun t)
| VMu : forall g t, valeur g (Mu t)
| Vconst : forall g k vl, exists_constr k g->
     valeur_list g vl -> valeur g (Constr k vl)
with valeur_list:GMenv -> list term->Prop:=
|Vnil : forall g, valeur_list g nil
|Vcons:forall g v l,
       valeur g v -> valeur_list g l -> valeur_list g (v::l).

VI. small-step based on substitution semantics
Section CSEMred.

Variable g : GMenv.

Inductive red:term->term->Prop:=
|red_fun : forall t, red (Fun t) (Fun t)
|red_mu: forall t, red (Mu t) (Mu t)
|red_cstrval : forall k vl,
       exists_constr k g -> valeur_list g vl ->
       red (Constr k vl) (Constr k vl)
|red_cstr: forall k tl l,exists_constr k g ->
        red_list tl l ->
        red (Constr k tl) (Constr k l)
|red_let : forall v t2,
        valeur g v -> red (Llet v t2) (Subst v t2)
| red_letctxt: forall t1 t2 t,
        red t1 t ->
        red (Llet t1 t2) (Llet t t2)
|red_betaf : forall t v,
        valeur g v -> red (Apply (Fun t) v) (Subst v t)
| red_betam: forall t v,
        valeur g v -> red (Apply (Mu t) v) (substn (v::Mu t::nil) t)
| red_left: forall t1 t2 t,
        red t1 t -> red (Apply t1 t2) (Apply t t2)
| red_right: forall t1 t2 t,
        abstract t1-> red t2 t -> red (Apply t1 t2) (Apply t1 t)
|red_sujet: forall t1 t pl,
        red t1 t ->
        wf_match pl g ->
        red (Match t1 pl) (Match t pl)
|red_filtr: forall pl c m tn vl,
             wf_match pl g ->
             valeur_list g vl ->
             In (Pat c m tn) pl ->
             length vl = m ->
             red (Match (Constr c vl) pl) (substn (rev vl) tn)
with
red_list:list term -> list term->Prop:=
|rednil: red_list nil nil
|redcons : forall v l l',
        valeur g v -> red_list l l' -> red_list (v::l) (v::l')
|redcons2: forall t t' l ,
        red t t'->red_list (t::l)(t'::l).

Inductive red_star: term->term->Prop:=
|red_sym : forall t , red_star t t
|red_trans : forall t t' t1,
      red t t' -> red_star t' t1-> red_star t t1.

Inductive red_star_list: list term->list term->Prop:=
|red_sym_list : forall t , red_star_list t t
|red_trans_list : forall t t' t1,
      red_list t t' -> red_star_list t' t1-> red_star_list t t1.

End CSEMred.

VII. Big-step based on substitution semantics
Section CSEMeval.

Variable g : GMenv.

Inductive eval: term->term->Prop:=
| eval_fun: forall t, eval (Fun t) (Fun t)
| eval_mu: forall t, eval (Mu t) (Mu t)
| eval_cst: forall k tl vl,
            exists_constr k g ->
            eval_list tl vl ->
            eval (Constr k tl) (Constr k vl)
| eval_let: forall t1 t2 v1 v,
            eval t1 v1 -> eval (Subst v1 t2) v ->
            eval (Llet t1 t2) v
| eval_app: forall t1 t2 t v v',
      eval t1 (Fun t) -> eval t2 v' ->
      eval (Subst v' t) v ->
      eval (Apply t1 t2) v
| eval_apprec: forall t1 t2 t v v',
      eval t1 (Mu t) -> eval t2 v' ->
      eval (substn (v'::Mu t::nil) t) v ->
      eval (Apply t1 t2) v
| eval_match : forall t pl c vl m tn v,
             eval t (Constr c vl) ->
             wf_match pl g ->
             In (Pat c m tn) pl ->
             length vl = m ->
             eval (substn (rev vl) tn) v ->
             eval (Match t pl) v
with
eval_list:list term->list term->Prop:=
|enil : eval_list nil nil
|econs:forall t l v l', eval t v -> eval_list l l' ->eval_list (t::l) (v::l').
End CSEMeval.

Scheme eval_term_ind6 := Minimality for eval Sort Prop
 with eval_terml_ind6 := Minimality for eval_list Sort Prop.

Lemma eval_valeur:
 forall g t v, eval g t v ->valeur g v.

Lemma eval_valeur_list:
 forall g t v, eval_list g t v ->valeur_list g v.

VIII. big_step to small_step equivalence

Lemma red_star_constr:
 forall g l l2, red_star_list g l l2 ->
 forall k, exists_constr k g->red_star g (Constr k l) (Constr k l2).

Lemma red_star_star:
 forall g t1 t2 , red_star g t1 t2 ->
  forall t3, red_star g t2 t3 ->red_star g t1 t3.

Lemma red_star_star_list:
 forall g t1 t2 , red_star_list g t1 t2 ->
  forall t3, red_star_list g t2 t3 ->red_star_list g t1 t3.

Lemma red_star_let:
 forall g t t', red_star g t t' ->
     forall t2, red_star g (Llet t t2) (Llet t' t2).

Lemma red_star_appleft:
 forall g t t', red_star g t t' ->
     forall t2, red_star g (Apply t t2) (Apply t' t2).

Lemma red_star_appright:
 forall g t t', red_star g t t' ->
     forall t2, abstract t2->red_star g (Apply t2 t) (Apply t2 t').

Lemma red_star_match:
 forall g t t', red_star g t t' ->
  forall pl, wf_match pl g->red_star g (Match t pl) (Match t' pl).

Lemma red_star_cons:
 forall g t t', red_star g t t'->
    forall l , red_star_list g (t::l) (t'::l).

Lemma red_star_cons2:
 forall g l l', red_star_list g l l'->
    forall t , valeur g t ->red_star_list g (t::l) (t::l').

Theorem eval_red:
 forall g t v, eval g t v-> red_star g t v.



Scheme valeur_ind6 := Minimality for valeur Sort Prop
 with valeur_list_ind6 := Minimality for valeur_list Sort Prop.

IX. small step to big step equivalence
Lemma eval_value:
 forall g v, valeur g v -> eval g v v.

Scheme red_term_ind6 := Minimality for red Sort Prop
 with red_terml_ind6 := Minimality for red_list Sort Prop.

Lemma inter1:
forall pl c m l,
In (Pat c m l) pl-> In c (extract_constr_match pl).
Lemma wf_match_exist_constr:
 forall pl g c m l , In (Pat c m l) pl -> wf_match pl g ->
   exists_constr c g.

Lemma red_eval:
 forall g a b, red g a b ->
     forall v (V:valeur g v) (E: eval g b v),
      eval g a v.





Theorem small_big:
 forall g a v, red_star g a v ->
   forall (V:valeur g v), eval g a v.

X. Equivalence between small and big step

Theorem equivalence_small_big:
 forall g t v, eval g t v <-> (red_star g t v/\valeur g v).


Semantics values
Inductive val :Set:=
  | Clos : list val ->term ->val
  | Clos_rec: list val ->term ->val
  | constr: ident -> list val -> val
.

Section CSEM.

Variable g : GMenv.

Inductive Eeval: list val ->term->val->Prop:=
  | Eeval_var : forall n e v,
           nth_error e n = (Some v)-> Eeval e (Var n) v
  | Eeval_fun : forall e t , Eeval e (Fun t) (Clos e t)
 | Eeval_mu : forall e t , Eeval e (Mu t) (Clos_rec e t)
  | Eeval_let : forall e t1 t2 v1 v ,
           Eeval e t1 v1 ->
           Eeval (v1::e) t2 v ->
           Eeval e (Llet t1 t2) v
  | Eeval_app : forall e e' t t1 t2 v v2,
           Eeval e t1 (Clos e' t) ->
           Eeval e t2 v2 ->
           Eeval (v2::e') t v ->
           Eeval e (Apply t1 t2) v
  | Eeval_appr : forall e e' t t1 t2 v v2,
           Eeval e t1 (Clos_rec e' t) ->
           Eeval e t2 v2 ->
           Eeval (v2::(Clos_rec e' t)::e') t v ->
           Eeval e (Apply t1 t2) v
  | Eeval_constr : forall e tl vl n ,
            exists_constr n g ->
            Eeval_list e tl vl ->
            Eeval e (Constr n tl) (constr n vl)
  | Eeval_match : forall e t c pl vl m tn v,
             Eeval e t (constr c vl) ->
             wf_match pl g ->
             In (Pat c m tn) pl ->
             length vl = m ->
             Eeval ((rev vl)++e) tn v ->
             Eeval e (Match t pl) v
with
Eeval_list : list val->list term-> list val ->Prop:=
   | Eeval_nil : forall e , Eeval_list e nil nil
   | Eeval_cons : forall e t lt v lv ,
            Eeval e t v ->
            Eeval_list e lt lv ->
            Eeval_list e (t::lt) (v::lv)
.

End CSEM.

Scheme eeval_term_ind6 := Minimality for Eeval Sort Prop
 with eeval_terml_ind6 := Minimality for Eeval_list Sort Prop.

XII Relation between "term-values" and semantics values
Inductive val_atom: GMenv->val -> term->Prop:=
| va_clos: forall g t vl al,
            val_atomlist g vl al ->
            val_atom g (Clos vl t) ( Fun (subst_rec (lift_list al ) t (S O)))
| va_closr: forall g t vl al,
            val_atomlist g vl al ->
            val_atom g (Clos_rec vl t) (Mu (subst_rec (lift2_list al) t (S (S O))))
| va_con: forall g n vl al,
            val_atomlist g vl al -> exists_constr n g ->
            val_atom g (constr n vl) (Constr n al)
with val_atomlist: GMenv->list val -> list term -> Prop:=
|va_nil: forall g, val_atomlist g nil nil
| va_cons: forall g v a vl al ,
           val_atom g v a ->
           val_atomlist g vl al ->
           val_atomlist g (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 g vl al, val_atomlist g vl al ->
   forall n v (NTH: nth_error vl n= Some v),
     exists a, nth_error al n = Some a /\ val_atom g v a.

Lemma val_atomlist_nth2:
 forall g vl al, val_atomlist g vl al ->
   forall n a (NTH: nth_error al n= Some a),
     exists v, nth_error vl n = Some v /\ val_atom g v a.

Lemma val_atom_app:
 forall g vl1 al1, val_atomlist g vl1 al1 ->
  forall vl2 al2 (AV: val_atomlist g vl2 al2) ,
    val_atomlist g (vl1++vl2) (al1++al2).

Lemma val_atom_rev:
 forall g vl al , val_atomlist g vl al ->
   val_atomlist g (rev vl) (rev al).

Lemma val_atom_length:
 forall g vl al , val_atomlist g vl al -> length al = length vl.

Lemma val_atom_valeur:
 forall g v a, val_atom g v a ->valeur g a.

 Lemma val_atom_valeur_list:
 forall g v a, val_atomlist g v a ->valeur_list g a.

XIII Big-step with environment to big-step based on substitution equivalence
Definition eval_env_subst_equiv (e:list val) (t:term) (v:val):Prop:=
        forall g al (VAL: val_atomlist g e al) ,
        exists w, eval g (substn al t) w /\
                       val_atom g v w.

Definition eval_list_env_subst_equiv (e:list val) (t:list term) (v:list val):Prop:=
        forall g al (VAL: val_atomlist g e al) ,
        exists w, eval_list g (substn_list al t) w /\
                       val_atomlist g 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 ->
   substn 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 (e : list val) (t : term),
  eval_env_subst_equiv e ( Fun t) (Clos e t).

Lemma mu_1:
 forall (e : list val) (t : term),
  eval_env_subst_equiv e (Mu t) (Clos_rec e t).

Lemma con_1:
 forall (e : list val) (n : nat) (tl : list term) (vl : list val),
 eval_list e tl vl ->
 eval_list_env_subst_equiv e tl vl ->
 eval_env_subst_equiv e (Constr 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.

XIV. Big-step based on substitution to big-step with environment equivalence
Definition eval_subst_env_equiv (t:term) (v:term):Prop:=
 forall al b e
    (VAL: val_atomlist e al)
    (SE: substn 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: substn_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.