Library Fml
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.