diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v index 8e075e5c3bcd53c0618af49f1f887a843ad0af2b..96ad668e269c688a9dd57c4ec5e541deea158367 100644 --- a/theories/logic/compatibility.v +++ b/theories/logic/compatibility.v @@ -89,5 +89,24 @@ Section compatibility. rel_rec_l. rel_rec_r. iApply "H". Qed. + Lemma refines_store e1 e2 e1' e2' A : + (REL e1 << e1' : ref A) -∗ + (REL e2 << e2' : A) -∗ + REL e1 <- e2 << e1' <- e2' : (). + Proof. + iIntros "IH1 IH2". + rel_bind_ap e2 e2' "IH2" w w' "IH2". + rel_bind_ap e1 e1' "IH1" v v' "IH1". + iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=. + rel_store_l_atomic. + iInv (relocN .@ "ref" .@ (l,l')) as (v v') "[Hv1 [>Hv2 #Hv]]" "Hclose". + iModIntro. iExists _; iFrame "Hv1". + iNext. iIntros "Hw1". + rel_store_r. + iMod ("Hclose" with "[Hw1 Hv2 IH2]"). + { iNext; iExists _, _; simpl; iFrame. } + value_case. + Qed. + End compatibility. diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v index 4aee02cd4620f918adeb270f2a1b701931d942fe..9d49a034feb00b7bb928bbd56eced967b0e7a688 100644 --- a/theories/typing/fundamental.v +++ b/theories/typing/fundamental.v @@ -278,17 +278,9 @@ Section fundamental. Proof. iIntros "IH1 IH2". intro_clause. - rel_bind_ap e2 e2' "IH2" w w' "IH2". - rel_bind_ap e1 e1' "IH1" v v' "IH1". - iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=. - rel_store_l_atomic. - iInv (relocN .@ "ref" .@ (l,l')) as (v v') "[Hv1 [>Hv2 #Hv]]" "Hclose". - iModIntro. iExists _; iFrame "Hv1". - iNext. iIntros "Hw1". - rel_store_r. - iMod ("Hclose" with "[Hw1 Hv2 IH2]"). - { iNext; iExists _, _; simpl; iFrame. } - value_case. + iApply (refines_store with "[IH1] [IH2]"). + - by iApply "IH1". + - by iApply "IH2". Qed. Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ