From 70a6b2c8fe1f1975cd54841c0ef9bf4306eac122 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 3 May 2017 11:50:57 +0200 Subject: [PATCH] Add an ElimModal instance for the relational interpretation --- F_mu_ref_conc/examples/counter.v | 7 +------ F_mu_ref_conc/relational_properties.v | 19 ++++++++++++------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/F_mu_ref_conc/examples/counter.v b/F_mu_ref_conc/examples/counter.v index 647f715..a568b96 100644 --- a/F_mu_ref_conc/examples/counter.v +++ b/F_mu_ref_conc/examples/counter.v @@ -122,7 +122,6 @@ Section CG_Counter. iApply (steps_CG_increment E with "Hspec Hx"); auto. } Unshelve. all: trivial. Qed. - Lemma bin_log_related_CG_locked_increment Γ K E1 E2 t τ x n l : nclose specN ⊆ E1 → @@ -337,10 +336,9 @@ Section CG_Counter. iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto. { solve_ndisj. } { by compute. } iIntros "Hcnt'". - iApply fupd_logrel. iMod ("Hclose" with "[Hl Hcnt Hcnt']"). { iNext. iExists _. by iFrame. } - simpl. iModIntro. + simpl. iPoseProof (bin_log_related_nat [TArrow TUnit TNat; TUnit] ⊤ n) as "H". iFrame "H". (* TODO: iApply does not work in this case *) - Transparent CG_locked_increment. unfold CG_locked_increment. @@ -363,7 +361,6 @@ Section CG_Counter. iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". iModIntro. iExists (#nv n). iSplit; eauto. iFrame "Hcnt". iIntros "Hcnt". simpl. - iApply fupd_logrel. iMod ("Hclose" with "[Hl Hcnt Hcnt']"). { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". } iApply (bin_log_related_rec_l _ []); auto. iNext. asimpl. @@ -381,7 +378,6 @@ Section CG_Counter. iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl"); auto. solve_ndisj. iIntros "Hcnt' Hl". - iApply fupd_logrel. iMod ("Hclose" with "[Hl Hcnt Hcnt']"). { iNext. iExists (S m). iFrame. } iApply (bin_log_related_if_true_l _ []); auto. @@ -391,7 +387,6 @@ Section CG_Counter. iSplitL; eauto; last first. { iDestruct 1 as %Hfoo. injection Hfoo. intro. by exfalso. } iIntros "_ Hcnt". simpl. - iApply fupd_logrel. iMod ("Hclose" with "[Hl Hcnt Hcnt']"). { iNext. iExists m. iFrame. } iApply (bin_log_related_if_false_l [] []); auto. diff --git a/F_mu_ref_conc/relational_properties.v b/F_mu_ref_conc/relational_properties.v index 6528d2d..f65ebe6 100644 --- a/F_mu_ref_conc/relational_properties.v +++ b/F_mu_ref_conc/relational_properties.v @@ -26,6 +26,14 @@ Section properties. iApply ("H" with "* Hs [HΓ] * Hj"); auto. Qed. + Global Instance elim_modal_logrel E1 E2 Γ e e' P τ : + ElimModal (|={E1,E2}=> P) P + ({E1,E2;Γ} ⊨ e ≤log≤ e' : τ) ({E2,E2;Γ} ⊨ e ≤log≤ e' : τ) | 0. + Proof. + iIntros "[HP HI]". iApply fupd_logrel. + iMod "HP". iApply ("HI" with "HP"). + Qed. + Lemma bin_log_related_val Γ τ e e' v v' (Hclosed : ∀ f, e.[f] = e) (Hclosed' : ∀ f, e'.[f] = e') : @@ -355,11 +363,10 @@ Section properties. -∗ {E1,E1;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ. Proof. iIntros "Hlog". - iApply fupd_logrel. pose (Φ:=(fun (_ : unit) w => ∃ l, ⌜w = LocV l⌝ ∗ l ↦ᵢ v)%I). iApply (bin_log_related_step_atomic_l Φ); auto. { rewrite_closed. } - iMod "Hlog" as "Hlog". iModIntro. + iMod "Hlog". iModIntro. iExists (). iSplitR "Hlog". - iApply (wp_alloc _ _ v); auto. iNext. iIntros (l) "Hl". @@ -387,7 +394,6 @@ Section properties. -∗ {E1,E1;Γ} ⊨ fill K (Load (Loc l)) ≤log≤ t : τ. Proof. iIntros "Hlog". - iApply fupd_logrel. pose (Φ:=(fun v' w => ⌜w = v'⌝ ∗ l ↦ᵢ v')%I). iApply (bin_log_related_step_atomic_l Φ); auto. iMod "Hlog" as (v') "[% [Hl Hlog]]". iModIntro. @@ -423,7 +429,6 @@ Section properties. -∗ {E1,E1;Γ} ⊨ fill K (Store (Loc l) e) ≤log≤ t : τ. Proof. iIntros (?) "Hlog". - iApply fupd_logrel. pose (Φ:=(fun (_ : unit) w => ⌜w = UnitV⌝ ∗ l ↦ᵢ v')%I). iApply (bin_log_related_step_atomic_l Φ); auto. { rewrite_closed. } @@ -462,7 +467,6 @@ Section properties. -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ. Proof. iIntros (??) "Hlog". - iApply fupd_logrel. pose (Φ:=(fun v' w => (⌜v' <> v1⌝ -∗ ⌜w = BoolV false⌝ ∗ l ↦ᵢ v') ∗ (⌜v' = v1⌝ -∗ ⌜w = BoolV true⌝ ∗ l ↦ᵢ v2))%I). iApply (bin_log_related_step_atomic_l Φ); auto. @@ -505,7 +509,6 @@ Section properties. -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ. Proof. iIntros (??) "Hlog". - iApply fupd_logrel. pose (Φ:=(fun v' w => ⌜w = BoolV false⌝ ∗ l ↦ᵢ v')%I). iApply (bin_log_related_step_atomic_l Φ); auto. { rewrite_closed. } @@ -546,7 +549,6 @@ Section properties. -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ. Proof. iIntros (??) "Hlog". - iApply fupd_logrel. pose (Φ:=(fun (_ : unit) w => ⌜w = BoolV true⌝ ∗ l ↦ᵢ v2)%I). iApply (bin_log_related_step_atomic_l Φ); auto. { rewrite_closed. } @@ -807,4 +809,7 @@ Section properties. done. Qed. + (* To prevent accidental unfolding by iMod or other tactics *) + Typeclasses Opaque bin_log_related. + End properties. -- GitLab