Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

New lemma data_at_conflict_glb #732

Merged
merged 1 commit into from
Oct 17, 2023
Merged

New lemma data_at_conflict_glb #732

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 37 additions & 0 deletions floyd/field_at.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2193,6 +2193,43 @@ Lemma data_at__share_join{cs: compspecs}:
data_at_ sh1 t p * data_at_ sh2 t p = data_at_ sh t p.
Proof. intros. apply data_at_share_join; auto. Qed.

Lemma data_at_conflict_glb: forall {cs: compspecs} sh1 sh2 t v v' p,
sepalg.nonidentity (Share.glb sh1 sh2) ->
0 < sizeof t ->
data_at sh1 t v p * data_at sh2 t v' p |-- FF.
Proof.
intros.
pose (sh := Share.glb sh1 sh2).
assert (sepalg.join sh (Share.glb sh1 (Share.comp sh)) sh1). {
hnf. rewrite (Share.glb_commute sh1), <- Share.glb_assoc, Share.comp2.
rewrite Share.glb_commute, Share.glb_bot.
split; auto.
rewrite Share.distrib2, Share.comp1.
rewrite Share.glb_commute, Share.glb_top.
unfold sh. rewrite Share.lub_commute, Share.lub_absorb. auto.
}
assert (sepalg.join sh (Share.glb sh2 (Share.comp sh)) sh2). {
hnf. rewrite (Share.glb_commute sh2), <- Share.glb_assoc, Share.comp2.
rewrite Share.glb_commute, Share.glb_bot.
split; auto.
rewrite Share.distrib2, Share.comp1.
rewrite Share.glb_commute, Share.glb_top.
unfold sh. rewrite Share.glb_commute.
rewrite Share.lub_commute, Share.lub_absorb. auto.
}
rewrite <- (data_at_share_join _ _ _ _ _ _ H1).
rewrite <- (data_at_share_join _ _ _ _ _ _ H2).
rewrite sepcon_assoc.
rewrite <- (sepcon_assoc (data_at (Share.glb _ _) _ _ _)).
rewrite (sepcon_comm (data_at (Share.glb sh1 _) _ _ _)).
rewrite <- !sepcon_assoc.
rewrite (sepcon_assoc (_ * _)).
eapply derives_trans.
apply sepcon_derives; [ | apply derives_refl].
apply data_at_conflict; auto.
rewrite FF_sepcon. auto.
Qed.

Lemma nonreadable_memory_block_field_at:
forall {cs: compspecs}
sh t gfs v p,
Expand Down
Loading