Commit d0eddb9c by charguer

### attempt at CF with factorized local

parent d3e563ca
 ... ... @@ -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. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!