Commit edea7903 authored by charguer's avatar charguer

formally

parent 443ed16c
Program Definition normally' H h1 := (* alternative *)
exists h2, heap_compat h1 h2
/\ h1^r = fmap_empty
/\ h2^f = fmap_empty
/\ H (h1 \u h2).
Lemma normally_of_normally' : forall H,
normally' H ==> normally H.
Proof using.
intros H h1 (h2&M1&M2&M3&M4).
hnf. exists (=h1) (=h2).
rewrite hstar_pure. split.
{ intros h' E. subst h'. auto. }
{ exists h1 h2. splits~.
Tactic Notation "exists_dep" "as" ident(E) :=
match goal with |- exists (_:?T), _ =>
assert (E:T); [ | exists E ] end.
......
......@@ -658,12 +658,25 @@ Definition normal_post A (Q:A->hprop) :=
Arguments normal_post [A].
Lemma normal_empty :
normal hempty.
normal \[].
Proof using.
Transparent hempty hpure.
introv M. unfolds hempty, hpure. autos*.
Qed.
Lemma normal_pure : forall P,
normal \[P].
Proof using.
Transparent hpure.
introv (p&(M1&M2)). auto.
Qed.
Lemma normal_empty' : (* simpler proof *)
normal \[].
Proof using.
intros. rewrite hempty_eq_hpure_true. applys~ normal_pure.
Qed.
Lemma normal_single : forall l v,
normal (hsingle l v).
Proof using.
......@@ -704,6 +717,17 @@ Lemma normal_himpl : forall H1 H2,
normal H1.
Proof using. introv HS HI M. lets: HI M. applys* HS. Qed.
Lemma normal_pure_star_hprop : forall (P:Prop) H,
(P -> normal H) ->
normal (\[P] \* H).
Proof using.
introv N (h1&h2&P1&P2&M1&EQ).
lets (_&E): heap_eq_forward EQ. simpls. rewrite E.
rewrite~ heap_union_r.
lets (MP&ME): hpure_inv P1. rewrites (>> hempty_inv (rm ME)).
rewrites~ (>> N P2). rew_fmap~.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Definitions and properties of [ROl] *)
......@@ -743,6 +767,30 @@ Proof using.
{ rewrite M2. fmap_eq. } }
Qed.
Lemma RO_empty :
RO \[] = \[].
Proof using.
intros. apply pred_ext_1. intros h.
iff (h'&(M1f&M1r)&M2&M3) (M1&M2).
{ rewrite M1f,M1r in M3. rew_fmap. split~. }
{ exists h. rewrite M1,M2. splits~. { split~. } { rew_fmap~. } }
Qed.
Lemma RO_pure : forall P,
RO \[P] = \[P].
Proof using.
intros. apply pred_ext_1. intros h.
iff (h'&(M1p&(M1f&M1r))&M2&M3) (MP&(M1&M2)).
{ rewrite M1f,M1r in M3. rew_fmap. split~. split~. }
{ exists h. rewrite M1,M2. splits~. { split~. split~. } { rew_fmap~. } }
Qed.
Lemma RO_empty' : (* simpler proof *)
RO \[] = \[].
Proof using.
intros. rewrite hempty_eq_hpure_true. rewrite~ RO_pure.
Qed.
Lemma RO_hexists : forall A (J:A->hprop),
RO (hexists J)
= Hexists x, RO (J x).
......@@ -781,6 +829,7 @@ Lemma heap_ro_pred : forall (H:hprop) h,
RO H (heap_ro h).
Proof using. introv N. exists h. split~. Qed.
Arguments RO_star : clear implicits.
(* ********************************************************************** *)
......@@ -1205,6 +1254,81 @@ Proof using.
{ applys~ on_rw_sub_base. applys~ himpl_hprop_r (l ~~~> w). split~. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ********************************************************************** *)
(* * Extension: [normally] modality (WORK IN PROGRESS) *)
Module Normally.
Definition normally H :=
Hexists H1 H2, \[normal H1] \* H1 \* \[H1 \* RO H2 ==> H].
Lemma normally_intro : forall H,
normal H ->
H ==> normally H.
Proof using.
introv N. unfold normally. hsimpl H \[].
{ rewrite RO_empty. hsimpl. }
{ auto. }
Qed.
Lemma normal_normally : forall H,
normal (normally H).
Proof using.
intros H. applys normal_hexists. intros H1.
applys normal_hexists. intros H2.
applys normal_pure_star_hprop. intros N1.
applys normal_star. auto.
applys normal_pure.
Qed.
Lemma normally_himpl : forall H1 H2,
(H1 ==> H2) ->
normally H1 ==> normally H2.
Proof using.
introv M. unfold normally. hpull ;=> H1a H1b N1 R1.
hsimpl~ H1a H1b. hchanges~ R1.
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 ==> normally (H1 \* H2).
Proof using.
intros. unfold normally. hpull ;=> H1a H1b N1 R1 H2a H2b N2 R2.
hsimpl (H1a \* H2a) (H1b \* H2b).
{ rew_heap. hchange (RO_star H1b H2b). hchange R1. hchanges R2. }
{ applys~ normal_star. }
Qed.
Lemma normally_idempotent1 : forall H,
normally H ==> normally (normally H).
Proof using.
intros. applys normally_intro. applys normal_normally.
Qed.
Lemma normally_idempotent2 : forall H,
normally (normally H) ==> normally H.
Proof using.
intros. unfold normally at 1. hpull ;=> H1 H2 N1 R.
asserts E: (\[] ==> RO H2). (* equivalent to [RO H2 hempty] *)
{ intros h M. rewrites (hempty_inv (rm M)).
(* This is almost true. I think we would need to know that H2 is not [False],
i.e. that at least one heap satisfies [RO H2] in order to conclude.
We might try to add \[exists h2, RO H2 h2], or equivalently
\[ ~ (RO H2 ==> \[False]) ] to the definition. *)
admit.
}
hchange E. hchanges R.
Abort.
(* It this was true, we would have a proper idempotence result:
[(normally (normally H)) = normally H]
*)
End Normally.
(* ---------------------------------------------------------------------- *)
End TripleLowLevel.
......
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