Commit 028fc1a6 authored by charguer's avatar charguer

normally

parent 96cc63fc
......@@ -1323,9 +1323,135 @@ Proof using.
{ split~. applys* fmap_union_eq_empty_inv_r. } }
Qed.
Lemma rule_frame_read_only' : forall t H1 Q1 H2,
triple t (H1 \* RO H2) Q1 ->
triple t (H1 \* normally H2) (Q1 \*+ normally H2).
Proof using.
introv M. intros h1 h2 D (h11&h12&P11&P12&R1&R2).
lets R1': heap_compat_ro_r R1.
destruct P12 as (N&E12).
subst h1. lets~ (D1&D2): heap_compat_union_l_inv (rm D).
asserts R12: (heap_state (heap_ro h12) = heap_state h12).
{ unstate. rewrite E12. fmap_eq. }
asserts C: (heap_compat (h11 \u heap_ro h12) h2).
{ apply~ heap_compat_union_l. applys~ heap_compat_ro_l. }
forwards~ (h1'&v&(N1&N2&N3&N4)): (rm M) (h11 \u (heap_ro h12)) h2.
{ exists h11 (heap_ro h12). splits~.
{ applys~ heap_ro_pred. } }
rew_heap~ in N3. rewrite E12 in N3.
lets G: heap_disjoint_components h1'.
forwards (h1''&F1&F2): heap_make (h1'^f \+ h12^f) (h11^r).
{ rewrite N3 in G. fmap_disjoint. }
asserts C': (heap_compat h1'' h2).
{ unfolds. rewrite F1,F2. split.
{ destruct~ D1. }
{ lets G2: heap_disjoint_components h2. rewrite N3 in G.
fmap_disjoint. } }
exists h1'' v. splits.
{ auto. }
{ fmap_red~.
{ rewrite~ R12. }
{ fequals. unstate. rewrite F1,F2,N3. fmap_eq. } }
{ rew_heap~. rewrite F2,E12. fmap_eq~. }
{ clears h2.
rename h1'' into hd. rename H2 into Hb. sets Ha: (Q1 v).
rename h1' into ha. rewrite~ fmap_union_empty_r in N3.
rename h12 into hb. rename h11 into hc.
(* LATER: begin separate lemma *)
destruct N4 as (hx&hy&V1&V2&V3&V4).
lets G': G. rewrite N3 in G'. rewrite V2 in G'. rew_heap~ in G'.
asserts C1: (heap_compat hx hb).
{ unfolds. rewrite E12. split.
{ auto. }
{ lets Gx: heap_disjoint_components hx. rewrite V3. auto. } }
forwards~ (hyf&W1&W2): heap_make (hy^f) (fmap_empty:state).
forwards~ (hcr&Y1&Y2): heap_make (fmap_empty:state) (hc^r).
(* LATER: find a way to automate these lemmas *)
(* LATER: automate disjoint_components use by fmap_disjoint *)
asserts C2: (heap_compat hcr hyf).
{ unfolds. split.
{ rewrite~ W2. }
{ rewrite Y1,Y2,W1,W2. fmap_disjoint. } }
asserts C3: (heap_compat hx hcr).
{ unfolds. split.
{ rewrite~ V3. }
{ rewrite Y1,Y2,V3. fmap_disjoint. } }
asserts C4: (heap_compat hx hyf).
{ unfolds. split.
{ rewrite~ W2. }
{ rewrite W1,W2,V3. fmap_disjoint. } }
asserts C5: (heap_compat hb hyf).
{ unfolds. split.
{ rewrite~ W2. }
{ rewrite W1,W2,E12. fmap_disjoint. } }
asserts C6: (heap_compat hb hcr).
{ unfolds. split.
{ rewrite~ E12. }
{ rewrite Y1,Y2,E12. fmap_disjoint. } }
exists (hx \u hb) (hcr \u hyf). splits.
{ auto. }
{ applys heap_eq. split.
{ rewrite F1,V2. rew_heap~. rewrite Y1,W1.
rewrite fmap_union_empty_l.
do 2 rewrite fmap_union_assoc. fequals.
applys fmap_union_comm_of_disjoint. auto. }
{ rew_heap~. rewrite V3,E12,W2,Y2,F2. fmap_eq. } }
{ rew_heap~. rewrite V3,E12. fmap_eq. }
{ exists~ hx hb. splits~. split~. } }
Qed.
Definition normal' H :=
(H ==> normally H).
Lemma normal_eq_normal' :
normal = normal'.
Proof using.
applys pred_ext_1. intros H. unfold normal, normal', normally. iff N.
{ intros h M. split~. }
{ intros h M. forwards~ (R&E): N h. }
Qed.
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