Commit 17ca0ec3 authored by charguer's avatar charguer

for_wp

parent 3966de5d
...@@ -194,8 +194,8 @@ Definition wp_while (F1 F2:formula) : formula := fun Q => ...@@ -194,8 +194,8 @@ Definition wp_while (F1 F2:formula) : formula := fun Q =>
Definition wp_for (v1 v2:val) (F3:int->formula) : formula := fun Q => Definition wp_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
Hexists n1 n2, \[v1 = val_int n1 /\ v2 = val_int n2] \* Hexists n1 n2, \[v1 = val_int n1 /\ v2 = val_int n2] \*
Hforall (S:int->formula), Hforall (S:int->formula),
let F i := local (If (i <= n2) then (wp_seq (F3 i) (S (i+1))) let F i := local (If (i <= n2) then (local (wp_seq (F3 i) (S (i+1))))
else (wp_val val_unit)) in else (local (wp_val val_unit))) in
\[ is_local_pred S /\ (forall i, F i ===> S i)] \--* (S n1 Q). \[ is_local_pred S /\ (forall i, F i ===> S i)] \--* (S n1 Q).
...@@ -301,6 +301,13 @@ Lemma sound_for'_local' : forall t (F:formula) Q, ...@@ -301,6 +301,13 @@ Lemma sound_for'_local' : forall t (F:formula) Q,
Proof using. introv M. applys sound_for'_local. applys M. Qed. 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.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
...@@ -408,12 +415,10 @@ Lemma weakestpre_pre : forall B (F:~~B) Q, ...@@ -408,12 +415,10 @@ Lemma weakestpre_pre : forall B (F:~~B) Q,
F (weakestpre F Q) Q. F (weakestpre F Q) Q.
Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed. Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed.
(* corollary of weakestpre_pre. *)
Lemma triple_weakestpre_pre : forall t Q, Lemma triple_weakestpre_pre : forall t Q,
triple t (weakestpre (triple t) Q) Q. triple t (weakestpre (triple t) Q) Q.
Proof using. Proof using. intros. applys weakestpre_pre. applys is_local_triple. Qed.
intros. unfold weakestpre. xpull ;=> H. auto.
Qed.
Lemma local_erase' : forall H F Q, Lemma local_erase' : forall H F Q,
...@@ -495,6 +500,10 @@ Qed. ...@@ -495,6 +500,10 @@ Qed.
*) *)
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.
...@@ -506,12 +515,12 @@ Proof using. ...@@ -506,12 +515,12 @@ Proof using.
rewrite wp_unfold. destruct t; simpl; rewrite wp_unfold. destruct t; simpl;
try (applys sound_for_local; intros H Q P). try (applys sound_for_local; intros H Q P).
{ unfolds wp_val. applys~ rule_val. } { unfolds wp_val. applys~ rule_val. }
{ unfolds wp_fail. xchanges (rm P). intros; false. } { applys~ triple_of_wp_fail. }
{ unfolds wp_val. applys~ rule_fun. } { unfolds wp_val. applys~ rule_fun. }
{ unfolds wp_val. applys~ rule_fix. } { unfolds wp_val. applys~ rule_fix. }
{ unfolds wp_if. applys rule_if. { unfolds wp_if. applys rule_if.
{ applys* IH. } { applys* IH. }
{ intros b. simpl. applys sound_for'_local'. clears Q. intros Q. { intros b. simpl. applys sound_for'_local'. clears Q; intros Q.
unfold wp_if_val. xpull ;=> b' E. inverts E. case_if. unfold wp_if_val. xpull ;=> b' E. inverts E. case_if.
{ applys* IH. } { applys* IH. }
{ applys* IH. } } { applys* IH. } }
...@@ -519,57 +528,47 @@ Proof using. ...@@ -519,57 +528,47 @@ Proof using.
unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } } unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ unfolds wp_seq. applys rule_seq'. { applys* IH. } { applys* IH. } } { unfolds wp_seq. applys rule_seq'. { applys* IH. } { applys* IH. } }
{ unfolds wp_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } } { unfolds wp_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } }
{ unfolds weakestpre. xchanges~ P. } { xchanges~ P. apply triple_weakestpre_pre. }
{ unfolds wp_while. xchange (rm P); rew_heap. { unfolds wp_while. xchange (rm P); rew_heap.
apply rule_extract_hforall. exists (weakestpre (triple (trm_while t1 t2))). 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. } { apply~ is_local_weakestpre_triple. }
{ clear H Q. set (R := weakestpre (triple (trm_while t1 t2))). { clear H Q. applys weaken_formula_trans. intros H Q P.
applys weaken_formula_trans. intros H Q P. apply weakestpre_intro. applys rule_while_raw.
unfold R. apply weakestpre_intro. applys rule_while_raw.
applys sound_for_local (rm P). clear H Q. intros H Q P. applys sound_for_local (rm P). clear H Q. intros H Q P.
applys rule_if. applys rule_if.
{ applys* IH. } { applys* IH. }
{ intros b. simpl. applys sound_for'_local'. clears Q. intros Q. { intros b. simpl. applys sound_for'_local'. clears Q; intros Q.
unfold wp_if_val. xpull ;=> v' E. inverts E. case_if. unfold wp_if_val. xpull ;=> v' E. inverts E. case_if as C.
{ applys sound_for'_local'. clears Q. intros Q. { applys sound_for'_local'. clears Q. intros Q.
unfold wp_seq. applys rule_seq'. unfold wp_seq. applys rule_seq'.
{ applys* IH. } { applys* IH. }
{ unfold R. apply weakestpre_pre. apply is_local_triple. } } { unfold R. apply triple_weakestpre_pre. } }
{ applys sound_for'_local'. clears Q. intros Q. { applys sound_for'_local'. clears Q; intros Q.
unfold wp_val. applys~ rule_val. } } unfold wp_val. applys~ rule_val. } }
{ simpl. intros v N. applys local_extract_false. intros Q'. { simpl. intros v N. applys local_extract_false. intros Q'.
unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } } unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ apply weakestpre_pre. apply is_local_triple. } } { apply triple_weakestpre_pre. } }
{ skip. } { rename v into x. destruct t1; try solve [ applys triple_of_wp_fail P ].
(* destruct t2; try solve [ applys triple_of_wp_fail P ].
{ hnf in P. simpls. applys P. { xlocal. } clears H Q. intros H Q P. xchanges (rm P). applys sound_for'_local'. clear Q; intros Q.
applys rule_while_raw. applys sound_for_local (rm P). unfold wp_for. xpull ;=> n1 n2 (E1&E2).
clears H Q. intros H Q (Q1&P1&P2). applys rule_if. invert E1. invert E2. intros _ _.
{ applys* IH. } set (S := fun i => weakestpre (triple (trm_for x i n2 t3))).
{ intros b. specializes P2 b. applys sound_for_local (rm P2). apply rule_extract_hforall. exists S.
clears H Q1 Q. intros H Q (b'&P1&P2&P3). inverts P1. case_if. apply rule_extract_hwand_hpure_l. split; [ split | ].
{ forwards~ P2': (rm P2). applys sound_for_local (rm P2'). { intros i. applys is_local_weakestpre_triple. }
clears H Q b'. intros H Q (H1&P1&P2). applys rule_seq'. { intros i. clear H Q. applys weaken_formula_trans. intros H Q P.
{ applys* IH. } apply weakestpre_intro. applys rule_for_raw.
{ applys P2. } } applys sound_for_local (rm P). clear H Q. intros H Q P. case_if.
{ forwards~ P3': (rm P3). applys sound_for_local (rm P3'). { xchanges (rm P). applys sound_for'_local'. clears Q. intros Q.
clears H Q b'. intros H Q P. hnf in P. applys rule_val. unfold wp_seq. applys rule_seq'.
{ hchanges* P. } } } { applys* IH. }
{ intros v N. specializes P2 v. applys local_extract_false P2. { unfold S. apply triple_weakestpre_pre. } }
intros H' Q' (b&E&S1&S2). subst. applys N. hnfs*. } } { xchanges (rm P). applys sound_for'_local'. clears Q; intros Q.
{ destruct t1; tryfalse. destruct t2; tryfalse. unfold wp_val. applys~ rule_val. } }
hnf in P. destruct P as (n1&n2&E1&E2&P). subst v0 v1. { apply triple_weakestpre_pre. } }
simpls. applys P. { xlocal. }
clears H Q. intros i H Q P. applys sound_for_local (rm P).
clears H Q. intros H Q P. applys rule_for. case_if as C.
{ destruct P as (H1&P1&P2). exists (fun r => \[r = val_unit] \* H1).
splits.
{ applys* IH. }
{ xpull ;=> _. applys P2. }
{ intros v' N. hpull. } }
{ hnf in P. hchanges* P. } }
*)
Qed. Qed.
Lemma triple_trm_of_wp_iter : forall (n:nat) t H Q, Lemma triple_trm_of_wp_iter : forall (n:nat) t H Q,
...@@ -617,7 +616,6 @@ Notation "'`Fail'" := ...@@ -617,7 +616,6 @@ Notation "'`Fail'" :=
(local (wp_fail)) (local (wp_fail))
(at level 69) : charac. (at level 69) : charac.
(*
Notation "'`While' F1 'Do' F2 'Done'" := Notation "'`While' F1 'Do' F2 'Done'" :=
(local (wp_while F1 F2)) (local (wp_while F1 F2))
(at level 69, F2 at level 68, (at level 69, F2 at level 68,
...@@ -629,7 +627,6 @@ Notation "'`For' x '=' v1 'To' v2 'Do' F3 'Done'" := ...@@ -629,7 +627,6 @@ Notation "'`For' x '=' v1 'To' v2 'Do' F3 'Done'" :=
(at level 69, x ident, (* t1 at level 0, t2 at level 0, *) (at level 69, x ident, (* t1 at level 0, t2 at level 0, *)
format "'[v' '`For' x '=' v1 'To' v2 'Do' '/' '[' F3 ']' '/' 'Done' ']'") format "'[v' '`For' x '=' v1 'To' v2 'Do' '/' '[' F3 ']' '/' 'Done' ']'")
: charac. : charac.
*)
Open Scope charac. Open Scope charac.
......
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