Require Import ZArith String List Zwf Omega. Open Scope Z_scope. Open Scope list_scope. Open Scope string_scope. Inductive ml : Type := var (x:string) | app (f a : ml) | letrec (x:string)(e1 e2:ml) | num (n:Z) | ml_bool(b:bool) | ml_if (e1 e2 e3 : ml) | lam(x:string)(body:ml). Inductive value : Type := vnum (n:Z) | vbool (b:bool) | native (f:Z->Z->value) | closure (x:string)(body:ml)(env:list (string*value)) | fclosure (f x:string)(body:ml)(env:list (string*value)). Definition is_fclosure (x:value) : bool := match x with fclosure _ _ _ _ => true | _ => false end. Inductive ml_ds : list (string*value) -> ml -> value -> Prop := dnum : forall r n, ml_ds r (num n) (vnum n) | dbool : forall r b, ml_ds r (ml_bool b) (vbool b) | dif_t : forall r e1 e2 e3 v, ml_ds r e1 (vbool true) -> ml_ds r e2 v -> ml_ds r (ml_if e1 e2 e3) v | dif_f : forall r e1 e2 e3 v, ml_ds r e1 (vbool false) -> ml_ds r e3 v -> ml_ds r (ml_if e1 e2 e3) v | dlam : forall r x body, ml_ds r (lam x body) (closure x body r) | drec : forall r f x e1 e2 v, ml_ds ((f,(fclosure f x e1 r))::r) e2 v -> ml_ds r (letrec f (lam x e1) e2) v | dvar1 : forall x v l, is_fclosure v = false -> ml_ds ((x,v)::l)(var x) v | dvar2 : forall f x y body r' l, ml_ds ((x,fclosure f y body r')::l) (var x) (closure y body ((f, fclosure f y body r')::r')) | dvar3 : forall x y l v v', x <> y -> ml_ds l (var y) v' -> ml_ds ((x,v)::l) (var y) v' | dapp1 : forall r e1 e2 x body r' v2 v, ml_ds r e1 (closure x body r') -> ml_ds r e2 v2 -> ml_ds ((x, v2)::r') body v -> ml_ds r (app e1 e2) v | dapp_native : forall r fsym f e1 e2 n1 n2, ml_ds r fsym (native f) -> ml_ds r e1 (vnum n1) -> ml_ds r e2 (vnum n2) -> ml_ds r (app (app fsym e1) e2) (f n1 n2) | dapp_native1 : forall r fsym f e1 n1, ml_ds r fsym (native f) -> ml_ds r e1 (vnum n1) -> ml_ds r (app fsym e1) (closure "x" (app (app (var "f") (num n1)) (var "x")) (("f",native f)::nil)). Definition native_env := ("plus", native (fun x y => vnum (x+y))):: ("lt", native (fun x y => vbool (if Z_lt_le_dec x y then true else false))):: ("mult", native (fun x y => vnum(x*y)))::nil. Definition fact_body := (ml_if (app (app (var "lt") (var "x")) (num 1)) (num 1) (app (app (var "mult") (var "x")) (app (var "fact") (app (app (var "plus") (var "x"))(num (-1)))))). Definition fact (n:Z) := letrec "fact" (lam "x" fact_body) (app (var "fact")(num n)). Ltac easy_ml := match goal with | |- ml_ds _ (num _) _ => apply dnum | |- ml_ds ((?a,_)::_) (var ?a) _ => apply dvar2 | |- ml_ds ((?a,_)::_) (var ?a) _ => apply dvar1; solve [auto] | |- ml_ds _ _ _ => apply dvar3;[discriminate | easy_ml] | |- _ => idtac end. Lemma compute_fact_body_rec : forall n factnm1, 0 < n -> ml_ds (("x", vnum (n-1)):: ("fact", fclosure "fact" "x" fact_body native_env)::native_env) fact_body (vnum factnm1) -> ml_ds (("x", vnum n):: ("fact", fclosure "fact" "x" fact_body native_env)::native_env) fact_body (vnum (factnm1*n)). unfold fact_body, native_env; intros n factnm1 zln H; apply dif_f. replace (vbool false) with (vbool (if Z_lt_le_dec n 1 then true else false)). apply dapp_native with (n1:=n) (n2:=1) (f:=(fun x y => vbool (if Z_lt_le_dec x y then true else false))); easy_ml. apply f_equal with (f:=vbool); case (Z_lt_le_dec n 1); auto; intro; elimtype False; omega. replace (factnm1*n) with (n*factnm1) by ring. apply dapp_native with (n1:=n)(n2:=factnm1)(f:=fun x y=>vnum(x*y)); easy_ml. eapply dapp1 with (v2 := (vnum (n-1))); easy_ml. apply dapp_native with (n1:=n)(n2:=-1)(f:= fun x y=>vnum(x+y)); easy_ml. apply H. Qed. Lemma compute_fact_body_0 : ml_ds (("x", vnum 0):: ("fact", fclosure "fact" "x" fact_body native_env)::native_env) fact_body (vnum 1). unfold fact_body, native_env; apply dif_t; easy_ml. apply dapp_native with (n1:=0)(n2:=1) (f:=(fun x y => vbool (if Z_lt_le_dec x y then true else false)));easy_ml. Qed. Lemma example_fact_6 : ml_ds native_env (fact 6) (vnum 720). unfold fact, fact_body. constructor. eapply dapp1; easy_ml. replace 720 with (1*1*2*3*4*5*6) by ring. repeat (apply compute_fact_body_0 || (apply compute_fact_body_rec; auto with zarith)). Qed.