proposition: Lemma writable_readable_share_common: forall rsh wsh, readable_share rsh -> writable_share wsh -> exists sh, nonunit sh /\ join_sub sh rsh /\ join_sub sh wsh.
proof: Proof. intros. assert (join (glb Lsh rsh) (glb Rsh rsh) rsh). { apply (comp_parts_join comp_Lsh_Rsh). - rewrite glb_twice, <- glb_assoc, glb_Lsh_Rsh, (glb_commute bot), glb_bot. apply join_comm, bot_join_eq. - rewrite <- glb_assoc, (glb_commute Rsh), glb_Lsh_Rsh, (glb_commute bot), glb_bot, glb_twice. apply bot_join_eq. } assert (join (glb Rsh rsh) (glb Rsh (comp rsh)) Rsh). { rewrite !(glb_commute Rsh). apply (@comp_parts_join rsh (comp rsh)); auto. - rewrite glb_twice, <- glb_assoc, comp2, (glb_commute bot), glb_bot. apply join_comm, bot_join_eq. - rewrite <- glb_assoc, (glb_commute (comp _)), comp2, (glb_commute bot), glb_bot, glb_twice. apply bot_join_eq. } exists (glb Rsh rsh). split; [|split]. - red in H. apply nonidentity_nonunit, H. - apply join_comm in H1. exists (glb Lsh rsh). assumption. - apply join_sub_trans with Rsh; [exists (glb Rsh (comp rsh))|destruct H0]; assumption. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List