From ec383775f171ed3427b98978044d12b28c7146de Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Tue, 17 Oct 2023 09:26:06 -0400
Subject: [PATCH] New lemma data_at_conflict_glb

---
 floyd/field_at.v | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/floyd/field_at.v b/floyd/field_at.v
index e4ef2939d..13b54dbbe 100644
--- a/floyd/field_at.v
+++ b/floyd/field_at.v
@@ -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,