From 17ca0ec3fb9d9cd3ed3bf2471fd2167f120ed8dd Mon Sep 17 00:00:00 2001 From: charguer Date: Fri, 6 Apr 2018 15:27:30 +0200 Subject: [PATCH] for_wp --- model/LambdaWP.v | 95 +++++++++++++++++++++++------------------------- 1 file changed, 46 insertions(+), 49 deletions(-) diff --git a/model/LambdaWP.v b/model/LambdaWP.v index 01c6279..ea5c6ff 100644 --- a/model/LambdaWP.v +++ b/model/LambdaWP.v @@ -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 => Hexists n1 n2, \[v1 = val_int n1 /\ v2 = val_int n2] \* Hforall (S:int->formula), - let F i := local (If (i <= n2) then (wp_seq (F3 i) (S (i+1))) - else (wp_val val_unit)) in + 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). @@ -301,6 +301,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. + + (* ---------------------------------------------------------------------- *) @@ -408,12 +415,10 @@ Lemma weakestpre_pre : forall B (F:~~B) Q, F (weakestpre F Q) Q. Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed. -(* corollary of weakestpre_pre. *) + Lemma triple_weakestpre_pre : forall t Q, triple t (weakestpre (triple t) Q) Q. -Proof using. - intros. unfold weakestpre. xpull ;=> H. auto. -Qed. +Proof using. intros. applys weakestpre_pre. applys is_local_triple. Qed. Lemma local_erase' : forall H F Q, @@ -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. rewrite wp_unfold. destruct t; simpl; try (applys sound_for_local; intros H Q P). { 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_fix. } { unfolds wp_if. applys rule_if. { 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. { applys* IH. } { applys* IH. } } @@ -519,57 +528,47 @@ Proof using. 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. } } - { unfolds weakestpre. xchanges~ P. } + { xchanges~ P. apply triple_weakestpre_pre. } { 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~ is_local_weakestpre_triple. } - { clear H Q. set (R := weakestpre (triple (trm_while t1 t2))). - applys weaken_formula_trans. intros H Q P. - unfold R. apply weakestpre_intro. applys rule_while_raw. + { 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* IH. } - { intros b. simpl. applys sound_for'_local'. clears Q. intros Q. - unfold wp_if_val. xpull ;=> v' E. inverts E. case_if. + { 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'. { applys* IH. } - { unfold R. apply weakestpre_pre. apply is_local_triple. } } - { applys sound_for'_local'. clears Q. intros Q. + { 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*. } } - { apply weakestpre_pre. apply is_local_triple. } } - { skip. } -(* - { hnf in P. simpls. applys P. { xlocal. } clears H Q. intros H Q P. - applys rule_while_raw. applys sound_for_local (rm P). - clears H Q. intros H Q (Q1&P1&P2). applys rule_if. - { applys* IH. } - { intros b. specializes P2 b. applys sound_for_local (rm P2). - clears H Q1 Q. intros H Q (b'&P1&P2&P3). inverts P1. case_if. - { forwards~ P2': (rm P2). applys sound_for_local (rm P2'). - clears H Q b'. intros H Q (H1&P1&P2). applys rule_seq'. - { applys* IH. } - { applys P2. } } - { forwards~ P3': (rm P3). applys sound_for_local (rm P3'). - clears H Q b'. intros H Q P. hnf in P. applys rule_val. - { hchanges* P. } } } - { intros v N. specializes P2 v. applys local_extract_false P2. - intros H' Q' (b&E&S1&S2). subst. applys N. hnfs*. } } - { destruct t1; tryfalse. destruct t2; tryfalse. - hnf in P. destruct P as (n1&n2&E1&E2&P). subst v0 v1. - 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. } } -*) + { 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). + 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. } } + { apply triple_weakestpre_pre. } } Qed. Lemma triple_trm_of_wp_iter : forall (n:nat) t H Q, @@ -617,7 +616,6 @@ Notation "'`Fail'" := (local (wp_fail)) (at level 69) : charac. -(* Notation "'`While' F1 'Do' F2 'Done'" := (local (wp_while F1 F2)) (at level 69, F2 at level 68, @@ -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, *) format "'[v' '`For' x '=' v1 'To' v2 'Do' '/' '[' F3 ']' '/' 'Done' ']'") : charac. -*) Open Scope charac. -- 2.24.1