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.