Commit 7224defa authored by charguer's avatar charguer

simplified_for

parent 17ca0ec3
......@@ -93,7 +93,6 @@ Qed.
Arguments hstar_hwand : clear implicits.
Arguments hstar_qwand [A]. (* H should be first *)
Lemma local_local : forall F,
local (local F) = local F.
Proof using.
......@@ -116,6 +115,13 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Elimination rules for [local] for WP *)
Lemma local_erase' : forall H F Q,
H ==> F Q ->
H ==> local F Q.
Proof using.
introv M. hchanges M. applys local_erase.
Qed.
Lemma local_weaken : forall Q' F H Q,
is_local F ->
H ==> F Q ->
......@@ -162,41 +168,93 @@ Qed.
(* TODO *)
(** Ramified frame rule with top *)
Lemma local_ramified_frame_htop : forall (Q1:val->hprop) H1 F H Q,
SepBasicSetup.is_local F ->
F H1 Q1 ->
H ==> H1 \* (Q1 \---* Q \*+ \Top) ->
F H Q.
Proof using.
introv L M W. applys~ SepBasicSetup.local_frame_htop (Q1 \---* Q \*+ \Top) M.
hchanges qwand_cancel.
Qed.
(*
Lemma is_local_weakestpre : forall B (F:~~B) Q,
SepBasicSetup.is_local F ->
is_local (weakestpre F).
Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed.
*)
Lemma rule_ramified_frame_htop_pre : forall t H Q Q',
triple t H Q' ->
triple t (H \* (Q' \---* Q \*+ \Top)) Q.
Proof using.
introv M. applys local_ramified_frame_htop M.
applys is_local_triple. hsimpl.
Qed.
(* TODO: stays here *)
Lemma is_local_weakestpre_triple : forall t,
is_local (weakestpre (triple t)).
Proof using.
intros. unfold is_local, weakestpre. applys fun_ext_1 ;=> Q.
applys himpl_antisym.
{ apply~ local_erase'. }
{ unfold local. hpull ;=> Q' H M. hsimpl (H \* (Q' \---* Q \*+ \Top)).
applys~ rule_ramified_frame_htop_pre. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Definition of CF blocks *)
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition wp_fail : formula := fun Q =>
\[False].
Definition wp_fail : formula := local (fun Q =>
\[False]).
Definition wp_val (v:val) : formula := fun Q =>
Q v.
Definition wp_val (v:val) : formula := local (fun Q =>
Q v).
Definition wp_seq (F1 F2:formula) : formula := fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q).
Definition wp_seq (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q)).
Definition wp_let (F1:formula) (F2of:val->formula) : formula := fun Q =>
F1 (fun X => F2of X Q).
Definition wp_let (F1:formula) (F2of:val->formula) : formula := local (fun Q =>
F1 (fun X => F2of X Q)).
Definition wp_if_val (v:val) (F1 F2:formula) : formula := fun Q =>
Hexists (b:bool), \[v = val_bool b] \* (if b then F1 Q else F2 Q).
Definition wp_if_val (v:val) (F1 F2:formula) : formula := local (fun Q =>
Hexists (b:bool), \[v = val_bool b] \* (if b then F1 Q else F2 Q)).
Definition wp_if (F0 F1 F2 : formula) : formula :=
wp_let F0 (fun v => local (wp_if_val v F1 F2)).
Definition wp_if (F0 F1 F2:formula) : formula :=
wp_let F0 (fun v => wp_if_val v F1 F2).
Definition wp_while (F1 F2:formula) : formula := fun Q =>
Definition wp_while (F1 F2:formula) : formula := local (fun Q =>
Hforall (R:formula),
let F := (local (wp_if F1 (local (wp_seq F2 R)) (local (wp_val val_unit)))) in
\[ is_local R /\ F ===> R] \--* (R Q).
let F := wp_if F1 (wp_seq F2 R) (wp_val val_unit) in
\[ is_local R /\ F ===> R] \--* (R Q)).
Definition wp_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
Definition wp_for_val (v1 v2:val) (F3:int->formula) : formula := local (fun Q =>
Hexists n1 n2, \[v1 = val_int n1 /\ v2 = val_int n2] \*
Hforall (S:int->formula),
let F i := local (If (i <= n2) then (local (wp_seq (F3 i) (S (i+1))))
else (local (wp_val val_unit))) in
\[ is_local_pred S /\ (forall i, F i ===> S i)] \--* (S n1 Q).
let F i := If (i <= n2) then (wp_seq (F3 i) (S (i+1)))
else (wp_val val_unit) in
\[ is_local_pred S /\ (forall i, F i ===> S i)] \--* (S n1 Q)).
Definition wp_for (F1 F2:formula) (F3:int->formula) : formula :=
wp_let F1 (fun v1 => wp_let F2 (fun v2 => wp_for_val v1 v2 F3)).
Definition wp_for' (F1 F2:formula) (F3:int->formula) : formula := local (fun Q =>
F1 (fun v1 => F2 (fun v2 => wp_for_val v1 v2 F3 Q))).
(* ---------------------------------------------------------------------- *)
......@@ -209,41 +267,26 @@ Definition wp_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
Definition wp_def wp (t:trm) :=
match t with
| trm_val v => local (wp_val v)
| trm_var x => local (wp_fail) (* unbound variable *)
| trm_fun x t1 => local (wp_val (val_fun x t1))
| trm_fix f x t1 => local (wp_val (val_fix f x t1))
| trm_if t0 t1 t2 => local (wp_if (wp t0) (wp t1) (wp t2))
| trm_seq t1 t2 => local (wp_seq (wp t1) (wp t2))
| trm_let x t1 t2 => local (wp_let (wp t1) (fun X => wp (subst x X t2)))
| trm_app t1 t2 => local (weakestpre (triple t))
| trm_while t1 t2 => local (wp_while (wp t1) (wp t2))
| trm_for x t1 t2 t3 => local (
match t1, t2 with
| trm_val v1, trm_val v2 => local (wp_for v1 v2 (fun X => wp (subst x X t3)))
| _, _ => wp_fail
end)
| trm_val v => wp_val v
| trm_var x => wp_fail (* unbound variable *)
| trm_fun x t1 => wp_val (val_fun x t1)
| trm_fix f x t1 => wp_val (val_fix f x t1)
| trm_if t0 t1 t2 => wp_if (wp t0) (wp t1) (wp t2)
| trm_seq t1 t2 => wp_seq (wp t1) (wp t2)
| trm_let x t1 t2 => wp_let (wp t1) (fun X => wp (subst x X t2))
| trm_app t1 t2 => weakestpre (triple t)
| trm_while t1 t2 => wp_while (wp t1) (wp t2)
| trm_for x t1 t2 t3 => wp_for' (wp t1) (wp t2) (fun X => wp (subst x X t3))
end.
Definition wp := FixFun wp_def.
Ltac fixfun_auto := try solve [
try fequals; auto; try apply fun_ext_1; auto ].
Lemma wp_unfold_iter : forall n t,
wp t = func_iter n wp_def wp t.
Proof using.
applys~ (FixFun_fix_iter (measure trm_size)). auto with wf.
intros f1 f2 t IH. unfold wp_def.
destruct t; fequals.
{ fequals~. }
{ fequals~. }
{ fequals~. applys~ fun_ext_1. }
{ fequals~. }
{ destruct t1; fequals~.
destruct t2; fequals~.
fequals. applys~ fun_ext_1. }
destruct t; try solve [ fequals~ | fequals~; applys~ fun_ext_1 ].
Qed.
Lemma wp_unfold : forall t,
......@@ -260,7 +303,9 @@ Proof using. applys (wp_unfold_iter 1). Qed.
Lemma is_local_cf : forall t,
is_local (wp t).
Proof.
intros. rewrite wp_unfold. destruct t; try apply is_local_local.
intros. rewrite wp_unfold.
destruct t; try solve [ apply is_local_local ].
{ simpl. applys is_local_weakestpre_triple. }
Qed.
Definition sound_for (t:trm) (F:formula) :=
......@@ -301,12 +346,13 @@ Lemma sound_for'_local' : forall t (F:formula) Q,
Proof using. introv M. applys sound_for'_local. applys M. Qed.
(*
Lemma remove_local_from_hyp : forall t (F:formula) H Q,
(H ==> local F Q) ->
(forall Q, triple t (F Q) Q) ->
triple t H Q.
Proof using. introv N M. xchanges N. applys* sound_for'_local'. Qed.
*)
......@@ -421,66 +467,25 @@ Lemma triple_weakestpre_pre : forall t Q,
Proof using. intros. applys weakestpre_pre. applys is_local_triple. Qed.
Lemma local_erase' : forall H F Q,
H ==> F Q ->
H ==> local F Q.
Proof using.
introv M. hchanges M. applys local_erase.
Qed.
(** Ramified frame rule with top *)
Lemma local_ramified_frame_htop : forall (Q1:val->hprop) H1 F H Q,
SepBasicSetup.is_local F ->
F H1 Q1 ->
H ==> H1 \* (Q1 \---* Q \*+ \Top) ->
F H Q.
Proof using.
introv L M W. applys~ SepBasicSetup.local_frame_htop (Q1 \---* Q \*+ \Top) M.
hchanges qwand_cancel.
Qed.
(*
Lemma is_local_weakestpre : forall B (F:~~B) Q,
SepBasicSetup.is_local F ->
is_local (weakestpre F).
Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed.
*)
Lemma rule_ramified_frame_htop_pre : forall t H Q Q',
triple t H Q' ->
triple t (H \* (Q' \---* Q \*+ \Top)) Q.
Proof using.
introv M. applys local_ramified_frame_htop M.
applys is_local_triple. hsimpl.
Qed.
(* TODO: stays here *)
Lemma is_local_weakestpre_triple : forall t,
is_local (weakestpre (triple t)).
Proof using.
intros. unfold is_local, weakestpre. applys fun_ext_1 ;=> Q.
applys himpl_antisym.
{ apply~ local_erase'. }
{ unfold local. hpull ;=> Q' H M. hsimpl (H \* (Q' \---* Q \*+ \Top)).
applys~ rule_ramified_frame_htop_pre. }
Qed.
Lemma weaken_formula_trans : forall (F1 F2:formula),
(forall H' Q', (H' ==> F1 Q') -> (H' ==> F2 Q')) ->
F1 ===> F2.
Proof using. introv M. intros Q. applys~ M (F1 Q). Qed.
Lemma weakestpre_intro : forall B (F:~~B) H Q,
Lemma himpl_weakestpre : forall B (F:~~B) H Q,
F H Q ->
H ==> weakestpre F Q.
Proof using. introv M. unfold weakestpre. hsimpl~ H. Qed.
Lemma qimpl_weakestpre_triple : forall t F,
(forall Q, triple t (F Q) Q) ->
F ===> weakestpre (triple t).
Proof using.
introv M. intros Q'. applys himpl_weakestpre. applys M.
Qed.
(*
Lemma triple_local_pre : forall t F Q,
......@@ -499,78 +504,142 @@ Qed.
rewrite~ hstar_comm.
*)
(*
Lemma triple_of_wp_fail : forall t H Q,
H ==> wp_fail Q ->
triple t H Q.
Proof using. introv M. unfolds wp_fail. xchanges M. intros. false. Qed.
Proof using.
introv M. xchanges M. applys sound_for'_local'. clears Q; intros Q.
xpull. intros; false.
Qed.
*)
Lemma wp_if_val_false : forall v F1 F2 Q,
~ is_val_bool v ->
wp_if_val v F1 F2 Q ==> \[False].
Proof using.
introv M. applys local_extract_false. intros Q'.
hpull ;=> v' E. inverts E. false* M. hnfs*.
Qed.
Lemma triple_of_wp : forall (t:trm) H Q,
H ==> wp t Q ->
triple t H Q.
(** [remove_local] applies to goal of the form [triple t (local F Q) Q] *)
Ltac remove_local :=
match goal with |- triple _ _ ?Q =>
applys sound_for'_local'; try (clear Q; intros Q); xpull end.
Definition is_val_int (v:val) :=
exists n, v = val_int n.
Lemma rule_for_trm_int : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v, ~ is_val_int v -> (Q1 v) ==> \[False]) ->
(forall (n1:int), exists Q2,
triple t2 (Q1 (val_int n1)) Q2
/\ (forall v, ~ is_val_int v -> (Q2 v) ==> \[False])
/\ (forall (n2:int), triple (trm_for x n1 n2 t3) (Q2 (val_int n2)) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using.
intros t. induction_wf: trm_size t.
rewrite wp_unfold. destruct t; simpl;
try (applys sound_for_local; intros H Q P).
{ unfolds wp_val. applys~ rule_val. }
{ applys~ triple_of_wp_fail. }
{ unfolds wp_val. applys~ rule_fun. }
{ unfolds wp_val. applys~ rule_fix. }
{ unfolds wp_if. applys rule_if.
introv M1 nQ1 M2. intros HF h Hf. forwards (h1'&v1&R1&K1): (rm M1) Hf.
tests C1: (is_val_int v1).
{ destruct C1 as (n1&E). subst. lets (Q2&M2'&nQ2&M3): ((rm M2) n1).
forwards* (h2'&v2&R2&K2): (rm M2') h1'.
rewrite <- (hstar_assoc \Top \Top) in K2. rewrite htop_hstar_htop in K2.
tests C2: (is_val_int v2).
{ destruct C2 as (n2&E). subst.
forwards* (h'&v'&R'&K'): ((rm M3) n2) h2'.
exists h' v'. splits~.
{ applys* red_for_arg. }
{ rewrite <- htop_hstar_htop. rew_heap~. } }
{ specializes nQ2 C2.
asserts Z: ((\[False] \* \Top \* HF) h2').
{ applys himpl_trans K2. hchange nQ2. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } } (* LATER: shorten *)
{ specializes nQ1 C1.
asserts Z: ((\[False] \* \Top \* HF) h1').
{ applys himpl_trans K1. hchange nQ1. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } (* LATER: shorten *)
Qed.
Lemma rule_for_trm : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v1, exists Q2,
triple t2 (Q1 v1) Q2
/\ (forall v2, triple (trm_for x v1 v2 t3) (Q2 v2) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using.
introv M1 M2. intros HF h Hf. forwards (h1'&v1&R1&K1): (rm M1) Hf.
lets (Q2&M2'&M3): ((rm M2) v1).
forwards* (h2'&v2&R2&K2): (rm M2') h1'.
rewrite <- (hstar_assoc \Top \Top) in K2. rewrite htop_hstar_htop in K2.
forwards* (h'&v'&R'&K'): ((rm M3) v2) h2'.
exists h' v'. splits~.
{ applys* red_for_arg. }
{ rewrite <- htop_hstar_htop. rew_heap~. }
Qed.
Lemma triple_wp : forall (t:trm) Q,
triple t (wp t Q) Q.
Proof using.
intros t. induction_wf: trm_size t. intros Q.
rewrite wp_unfold. destruct t; simpl.
{ remove_local. applys~ rule_val. }
{ remove_local ;=> E. false. }
{ remove_local. applys~ rule_fun. }
{ remove_local. applys~ rule_fix. }
{ remove_local. applys rule_if.
{ applys* IH. }
{ intros b. simpl. applys sound_for'_local'. clears Q; intros Q.
unfold wp_if_val. xpull ;=> b' E. inverts E. case_if.
{ intros b. simpl. remove_local ;=> b' E. inverts E. case_if.
{ applys* IH. }
{ applys* IH. } }
{ simpl. intros v N. applys local_extract_false. intros Q'.
unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ unfolds wp_seq. applys rule_seq'. { applys* IH. } { applys* IH. } }
{ unfolds wp_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } }
{ xchanges~ P. apply triple_weakestpre_pre. }
{ unfolds wp_while. xchange (rm P); rew_heap.
set (R := weakestpre (triple (trm_while t1 t2))).
{ intros. applys~ wp_if_val_false. } }
{ remove_local. applys rule_seq'. { applys* IH. } { applys* IH. } }
{ remove_local. applys rule_let. { applys* IH. } { intros X. applys* IH. } }
{ apply triple_weakestpre_pre. }
{ remove_local. set (R := weakestpre (triple (trm_while t1 t2))).
apply rule_extract_hforall. exists R.
apply rule_extract_hwand_hpure_l. split; [ split | ].
apply rule_extract_hwand_hpure_l. split; [split|].
{ apply~ is_local_weakestpre_triple. }
{ clear H Q. applys weaken_formula_trans. intros H Q P.
apply weakestpre_intro. applys rule_while_raw.
applys sound_for_local (rm P). clear H Q. intros H Q P.
applys rule_if.
{ applys qimpl_weakestpre_triple. clears Q; intros Q.
applys rule_while_raw. remove_local. applys rule_if.
{ applys* IH. }
{ intros b. simpl. applys sound_for'_local'. clears Q; intros Q.
unfold wp_if_val. xpull ;=> v' E. inverts E. case_if as C.
{ applys sound_for'_local'. clears Q. intros Q.
unfold wp_seq. applys rule_seq'.
{ simpl. intros b. remove_local ;=> v' E. inverts E. case_if as C.
{ remove_local. applys rule_seq'.
{ applys* IH. }
{ unfold R. apply triple_weakestpre_pre. } }
{ applys sound_for'_local'. clears Q; intros Q.
unfold wp_val. applys~ rule_val. } }
{ simpl. intros v N. applys local_extract_false. intros Q'.
unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ remove_local. applys~ rule_val. } }
{ intros. applys~ wp_if_val_false. } }
{ apply triple_weakestpre_pre. } }
{ rename v into x. destruct t1; try solve [ applys triple_of_wp_fail P ].
destruct t2; try solve [ applys triple_of_wp_fail P ].
xchanges (rm P). applys sound_for'_local'. clear Q; intros Q.
unfold wp_for. xpull ;=> n1 n2 (E1&E2).
{ rename v into x. remove_local. applys rule_for_trm.
applys* IH. intros v1. esplit. split.
applys* IH. intros v2. simpl.
remove_local ;=> n1 n2 (E1&E2).
invert E1. invert E2. intros _ _.
set (S := fun i => weakestpre (triple (trm_for x i n2 t3))).
apply rule_extract_hforall. exists S.
apply rule_extract_hwand_hpure_l. split; [ split | ].
{ intros i. applys is_local_weakestpre_triple. }
{ intros i. clear H Q. applys weaken_formula_trans. intros H Q P.
apply weakestpre_intro. applys rule_for_raw.
applys sound_for_local (rm P). clear H Q. intros H Q P. case_if.
{ xchanges (rm P). applys sound_for'_local'. clears Q. intros Q.
unfold wp_seq. applys rule_seq'.
{ applys* IH. }
{ unfold S. apply triple_weakestpre_pre. } }
{ xchanges (rm P). applys sound_for'_local'. clears Q; intros Q.
unfold wp_val. applys~ rule_val. } }
{ intros i. applys qimpl_weakestpre_triple. clears Q; intros Q.
applys rule_for_raw. case_if.
{ remove_local. applys rule_seq'.
{ applys* IH. }
{ unfold S. apply triple_weakestpre_pre. } }
{ remove_local. applys~ rule_val. } }
{ apply triple_weakestpre_pre. } }
Qed.
Lemma triple_of_wp : forall (t:trm) H Q,
H ==> wp t Q ->
triple t H Q.
Proof using. introv M. xchanges M. applys triple_wp. Qed.
Lemma triple_trm_of_wp_iter : forall (n:nat) t H Q,
H ==> func_iter n wp_def wp t Q ->
triple t H Q.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment