``` ```

Nml for substitution

Author : Zaynah Dargaye

created : 29th April 2009
``` Require Import List. Require Import Coqlib. Require Import Coqlib2. ```
I. Syntax
``` Inductive term:Set:= |Var :nat->term |Lamb: nat -> term->term |Mu : nat->term->term |App: term->list term->term |tLet : term->term->term |Con : nat->list term->term |Match : term-> list pat ->term with pat: Set:=  |Patc : 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) ) (Hlet: forall t1 t2, P t1 ->P t2 -> P (tLet t1 t2)) (Hmu:forall ari t, P t -> P(Mu ari t)) (Hl:forall ari t ,P t->P(Lamb ari t)) (Happ: forall t tl, P t -> Pl tl -> P (App t tl)) (Hconstr: forall n l, Pl l -> P (Con 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 n t, P t -> Pp (Patc 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  |tLet t1 t2=> Hlet t1 t2 (term_ind2 t1) (term_ind2 t2)  |Mu ari t => Hmu ari t (term_ind2 t)  |Lamb ari t => Hl ari t (term_ind2 t)  |App t tl => Happ t tl (term_ind2 t)           ((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) tl)  |Con 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  |Patc n t => Hpat n t (term_ind2 t)  end. End term_ind_sect. ```
III. Big-step semantics CBV with environment
``` Inductive val:Set:=  |clos: nat->term->list val->val  |closr: nat->term->list val->val  |constr: nat->list val->val. Inductive eval_term: list val-> term->val->Prop:= |evar: forall n e v, nth_error e n= Some v -> eval_term e (Var n) v |elamb: forall n e t, eval_term e (Lamb n t) (clos n t e) |emu: forall n e t, eval_term e (Mu n t) (closr n t e) |econ: forall e n tl vl, eval_list e tl vl->eval_term e (Con n tl) (constr n vl) |eapp : forall e tf tl n v tb vl e1,           eval_term e tf (clos n tb e1) ->           eval_list e tl vl ->           List.length tl = S n ->           eval_term ((List.rev vl)++e1) tb v ->           eval_term e (App tf tl) v |eappr : forall e tf tl n v tb vl e1,           eval_term e tf (closr n tb e1) ->           eval_list e tl vl ->           List.length tl = S n ->           eval_term ((List.rev vl)++(closr n tb e1)::e1) tb v ->           eval_term e (App tf tl) v |ematch: forall e a n vl pl p m v,           eval_term e a (constr n vl) ->           nth_error pl n = Some (Patc m p) ->           List.length vl = m ->           eval_term (rev vl++e) p v ->           eval_term e (Match a pl) v  |elet: forall e a1 a2 v1 v,              eval_term e a1 v1->eval_term (v1::e) a2 v->              eval_term e (tLet a1 a2) v with eval_list: list val->list term->list val->Prop:= |enil: forall e, eval_list e nil nil  |econs:forall e hd vhd tl vtl, eval_term e hd vhd->           eval_list e tl vtl->eval_list e (hd::tl) (vhd::vtl). Scheme eval_term_ind6 := Minimality for eval_term Sort Prop  with eval_terml_ind6 := Minimality for eval_list Sort Prop. ```