Commit 0f47daa3 authored by charguer's avatar charguer

example_ro

parent 8c4b2deb
......@@ -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.
......
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