diff --git a/model/ExampleRO.v b/model/ExampleRO.v index 749eb92ef8799e28bcf58133e6df9188cb71e1c8..35b3c27d3410b58e4f3c6ae8601e706eecf68012 100644 --- a/model/ExampleRO.v +++ b/model/ExampleRO.v @@ -111,9 +111,85 @@ Hint Resolve Normal_hsingle. +(* ---------------------------------------------------------------------- *) +(* rebind xchange to work on triples, which are not [local] *) + +Lemma xchange_lemma' : forall H1 H1' H2 t H Q, + (H1 ==> H1') -> + (H ==> H1 \* H2) -> + triple t (H1' \* H2) Q -> + triple t H Q. +Proof using. + introv W1 W2 M. applys~ rule_consequence M. + hchange W2. hchanges W1. +Qed. + +Ltac xchange_apply L cont1 cont2 ::= + eapply xchange_lemma'; + [ applys L | cont1 tt | cont2 tt (*xtag_pre_post*) ]. + +Ltac xchange_with_core cont1 cont2 H H' ::= + eapply xchange_lemma' with (H1:=H) (H1':=H'); + [ | cont1 tt | cont2 tt (* xtag_pre_post*) ]. + + + +(* ---------------------------------------------------------------------- *) +(* ** rebind [xpull] *) + + +(** Lemmas *) + +Lemma xpull_hprop' : forall t H1 H2 (P:Prop) Q, + (P -> triple t (H1 \* H2) Q) -> triple t (H1 \* (\[P] \* H2)) Q. +Proof using. + intros. rewrite hstar_comm_assoc. apply~ rule_extract_hprop. +Qed. + +Lemma xpull_hexists' : forall t H1 H2 A (J:A->hprop) Q, + (forall x, triple t (H1 \* ((J x) \* H2)) Q) -> + triple t (H1 \* (hexists J \* H2)) Q. +Proof using. + intros. rewrite hstar_comm_assoc. rewrite hstar_hexists. + applys rule_extract_hexists. + intros. rewrite~ hstar_comm_assoc. +Qed. + +Ltac xpull_hprop tt ::= + apply xpull_hprop'; [ intro ]. + +Ltac xpull_hexists tt ::= + apply xpull_hexists'; [ intro ]. + +Ltac xpull_step tt ::= + let go HP := + match HP with _ \* ?HN => + match HN with + | ?H \* _ => + match H with + | \[] => apply xpull_empty + | \[_] => xpull_hprop tt + | hexists _ => xpull_hexists tt + | _ ~> Id _ => xpull_id tt + | _ \* _ => apply xpull_assoc + | _ => apply xpull_keep + end + | \[] => fail 1 + | _ => apply xpull_starify + end end in + on_formula_pre ltac:(go). + + (* ********************************************************************** *) (* * Formalisation of higher-order iterator on a reference *) +Tactic Notation "xdef" := + rew_nary; rew_vals_to_trms; + match goal with |- triple (trm_apps (trm_val ?f) _) _ _ => + applys rule_apps_funs; + [unfold f; rew_nary; reflexivity | auto | simpl] + end. + (* ---------------------------------------------------------------------- *) (** Apply a function to the contents of a reference *) @@ -131,15 +207,11 @@ Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop), PRE (RO(p ~~~> v) \* H) POST Q). Proof using. - introv M. - rew_nary; rew_vals_to_trms; applys rule_apps_funs; - [unfold val_ref_apply; rew_nary; reflexivity| auto | simpl]. - applys rule_xchange (@RO_himpl_RO_hstar_RO (p ~~~> v)); [ hsimpl |]. + introv M. xdef. xchange (@RO_himpl_RO_hstar_RO (p ~~~> v)). rew_heap. applys rule_let (RO (p ~~~> v)). { applys rule_get_ro. } - { intros x; simpl. - applys rule_extract_hprop ;=> E; subst x. - applys M. } + { intros x; simpl. xpull ;=> E. subst x. + applys rule_consequence M; hsimpl. } Qed. (* Note: this specification allows [f] to call [val_get] on [r], @@ -184,20 +256,122 @@ Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop), PRE (p ~~~> v \* H) POST (fun r => \[r = val_unit] \* Hexists w, (p ~~~> w) \* (Q w))). Proof using. - introv N M. - rew_nary; rew_vals_to_trms; applys rule_apps_funs; - [unfold val_ref_update; rew_nary; reflexivity| auto | simpl]. + introv N M. xdef. applys rule_let. { applys rule_get. } - { intros x; simpl; rew_heap. applys rule_extract_hprop ;=> E; subst x. + { intros x; simpl. xpull ;=> E. subst x. applys rule_let' \[]. { hsimpl. } - applys~ rule_frame_read_only_conseq (p ~~~> v). - { hsimpl. } { rew_heap. applys M. } { hsimpl. } - { intros y; simpl; rew_heap. clear M. - applys~ rule_frame_conseq (Q y). hsimpl. - rew_heap. applys rule_set. hsimpl~. } } + applys~ rule_frame_read_only_conseq (p ~~~> v). + { applys rule_consequence M; hsimpl. } + { hsimpl. } + { clear M. intros y; simpl. xpull. + applys~ rule_frame_conseq (Q y). + { applys rule_set. } + { hsimpl~. } } } +Qed. + + +(* ---------------------------------------------------------------------- *) +(** In-place update of a reference by invoking a function, with representation predicate *) + +Hint Rewrite RO_hexists RO_pure : rew_RO. + (* todo : rename to RO_hpure , RO_hstar. *) + +Tactic Notation "rew_RO" := + autorewrite with rew_RO. + +Lemma rule_htop_pre' : forall H2 H1 t H Q, + H ==> H1 \* H2 -> + triple t H1 Q -> + triple t H Q. +Proof using. + introv W M. applys rule_consequence; [| applys rule_htop_pre M |]. + { hchange W. hsimpl. } { auto. } +Qed. + + +(*---*) + + + +Definition Box (n:int) (p:loc) := + Hexists (q:loc), (p ~~~> q) \* (q ~~~> n). + +Lemma Box_unfold : forall p n, + (p ~> Box n) ==> Hexists (q:loc), (p ~~~> q) \* (q ~~~> n). +Proof using. intros. xunfold Box. hsimpl. Qed. + +Lemma Box_fold : forall p q n, + (p ~~~> q) \* (q ~~~> n) ==> (p ~> Box n). +Proof using. intros. xunfold Box. hsimpl. Qed. + +Lemma RO_Box_unfold : forall p n, + RO (p ~> Box n) ==> RO (p ~> Box n) \* Hexists (q:loc), RO (p ~~~> q) \* RO (q ~~~> n). +Proof using. + intros. hchange RO_duplicatable. xunfold Box at 1. + rew_RO. hpull ;=> q. hchanges (RO_star (p ~~~> q) (q ~~~> n)). Qed. +Arguments Box_fold : clear implicits. +Arguments Box_unfold : clear implicits. +Arguments RO_Box_unfold : clear implicits. + + +(*---*) + +Definition val_box_get := + ValFun 'p := + Let 'q := val_get 'p in + val_get 'q. + +Lemma rule_box_get : forall p n, + triple (val_box_get p) + PRE (RO (p ~> Box n)) + POST (fun r => \[r = val_int n]). +Proof using. + intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q. + applys rule_htop_pre' (RO (p ~> Box n)). hsimpl. (* not need, ideally *) + rew_heap. applys rule_let' __ (RO (p ~~~> q)). + { hsimpl. } + { applys rule_get_ro. } + { intros x; simpl; xpull ;=> E; subst x. applys rule_get_ro. } +Qed. + +(*---*) + +(* let box_twice f p = + let q = !p in + q := f !q + f !q +*) + +Definition val_box_twice := + ValFun 'f 'p := + Let 'q := val_get 'p in + Let 'n1 := val_get 'q in + Let 'a1 := 'f 'n1 in + Let 'n2 := val_get 'q in + Let 'a2 := 'f 'n2 in + Let 'm := 'a1 '+ 'a2 in + val_set 'q 'm. + +Lemma rule_box_twice : forall (f:val) p n (F:int->int), + (forall (x:int) H, triple (val_box_twice f x) + PRE (RO(p ~> Box n) \* H) + POST (fun r => \[r = val_int (F x)] \* H)) -> + triple (val_box_twice f p) + PRE (p ~> Box n) + POST (fun r => \[r = val_unit] \* p ~> Box (2 * F n)). +Proof using. + introv M. xdef. xchange (Box_unfold p). xpull ;=> q. + applys rule_let' __ (p ~~~> q). + { hsimpl. } + { rew_heap. applys rule_get. } + { intros x; simpl; xpull ;=> E; subst x. + applys rule_let' __ (q ~~~> n). + { hsimpl. } + { rew_heap. applys rule_get. } + { intros x; simpl; xpull ;=> E; subst x. +Abort.