...
 
Commits (1)
......@@ -95,22 +95,22 @@ Definition cf_for (v1 v2:val) (F3:int->formula) : formula := fun H Q =>
Subsequently, the fixed-point equation is established. *)
Definition cf_def cf (t:trm) :=
match t with
| trm_val v => local (cf_val v)
| trm_var x => local (cf_fail) (* unbound variable *)
| trm_fun x t1 => local (cf_val (val_fun x t1))
| trm_fix f x t1 => local (cf_val (val_fix f x t1))
| trm_if t0 t1 t2 => local (cf_if (cf t0) (cf t1) (cf t2))
| trm_seq t1 t2 => local (cf_seq (cf t1) (cf t2))
| trm_let x t1 t2 => local (cf_let (cf t1) (fun X => cf (subst x X t2)))
| trm_app t1 t2 => local (triple t)
| trm_while t1 t2 => local (cf_while (cf t1) (cf t2))
| trm_for x t1 t2 t3 => local (
local (match t with
| trm_val v => cf_val v
| trm_var x => cf_fail (* unbound variable *)
| trm_fun x t1 => cf_val (val_fun x t1)
| trm_fix f x t1 => cf_val (val_fix f x t1)
| trm_if t0 t1 t2 => cf_if (cf t0) (cf t1) (cf t2)
| trm_seq t1 t2 => cf_seq (cf t1) (cf t2)
| trm_let x t1 t2 => cf_let (cf t1) (fun X => cf (subst x X t2))
| trm_app t1 t2 => triple t
| trm_while t1 t2 => cf_while (cf t1) (cf t2)
| trm_for x t1 t2 t3 =>
match t1, t2 with
| trm_val v1, trm_val v2 => cf_for v1 v2 (fun X => cf (subst x X t3))
| _, _ => cf_fail
end)
end.
end
end).
Definition cf := FixFun cf_def.
......@@ -121,8 +121,8 @@ Lemma cf_unfold_iter : forall n t,
cf t = func_iter n cf_def cf t.
Proof using.
applys~ (FixFun_fix_iter (measure trm_size)). auto with wf.
intros f1 f2 t IH. unfold cf_def.
destruct t; fequals.
intros f1 f2 t IH. unfold cf_def. fequal.
destruct t; try solve [fequals].
{ fequals~. }
{ fequals~. }
{ fequals~. applys~ fun_ext_1. }
......@@ -163,8 +163,8 @@ Lemma sound_for_cf : forall (t:trm),
sound_for t (cf t).
Proof using.
intros t. induction_wf: trm_size t.
rewrite cf_unfold. destruct t; simpl;
try (applys sound_for_local; intros H Q P).
rewrite cf_unfold. unfold cf_def.
applys sound_for_local. intros H Q P. destruct t.
{ unfolds in P. applys~ rule_val. hchanges~ P. }
{ false. }
{ unfolds in P. applys rule_fun. hchanges~ P. }
......
......@@ -31,7 +31,6 @@ Implicit Types n : int.
(* ********************************************************************** *)
(* * Derived basic functions *)
(* ---------------------------------------------------------------------- *)
(** Increment function *)
......@@ -48,7 +47,7 @@ Lemma rule_incr : forall p n,
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
xcf. unfold cf_def. simpl. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_spec val_incr) => Provide rule_incr.
......