Simplify the relational rules for locks

F_mu_ref_conc/examples/lock.v

@@ -93,22 +93,12 @@ Section proof.
   Qed.
 
   Lemma bin_log_related_newlock_r Γ K t τ :
-    (∀ (l : loc), l ↦ₛ (#♭v false) -∗ Γ ⊨ t ≤log≤ fill K (Loc l) : τ)%I
+    (∀ l : loc, l ↦ₛ (#♭v false) -∗ Γ ⊨ t ≤log≤ fill K (Loc l) : τ)%I
     -∗ Γ ⊨ t ≤log≤ fill K newlock : τ.
   Proof.
     iIntros "Hlog".
-    pose (Φ := (fun w => ∃ l, ⌜w = (LocV l)⌝ ∗ l ↦ₛ (#♭v false))%I).
-    iApply (bin_log_related_step_r Φ with "[]").
-    { autosubst.  }
-    { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
-      tp_apply j steps_newlock.
-      iDestruct "Hj" as (l) "[Hj Hl]".
-      iExists (LocV l). simpl. iFrame.
-      iModIntro. iSplitL; eauto. }
-    iIntros (v') "He'". iDestruct "He'" as (l) "[% Hl]". subst.
-    iApply "Hlog".
-    done.
+    unfold newlock.
+    iApply (bin_log_related_alloc_r); auto.
   Qed.
 
   Global Opaque newlock.
@@ -125,6 +115,29 @@ Section proof.
     by iFrame.
   Qed.
 
+  (* TODO: those should be accompaied by lemmas; preferably so that 
+     [change] does not change too much *)
+  Tactic Notation "rel_bind_l" open_constr(efoc) :=
+    iStartProof;
+    lazymatch goal with
+    | [ |- (_ ⊢ bin_log_related _ _ _ (fill _ ?e) _ _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e'))
+    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e'))
+    end.
+  Tactic Notation "rel_bind_r" open_constr(efoc) :=
+    iStartProof;
+    lazymatch goal with
+    | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+    | [ |- (_ ⊢ bin_log_related _ _ _ _ ?e _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+    end.
+
   Lemma bin_log_related_acquire_r Γ E1 E2 K l t τ
     (Hspec : nclose specN ⊆ E1) :
     l ↦ₛ (#♭v false) -∗
@@ -132,17 +145,13 @@ Section proof.
     -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
-    pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ (#♭v true))%I).
-    iApply (bin_log_related_step_r Φ with "[Hl]").
-    { autosubst.  }
-    { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
-      tp_apply j steps_acquire with "Hl" as "Hl".
-      iExists UnitV. simpl. iFrame.
-      iModIntro. iSplitL; eauto. }
-    iIntros (v') "[% Hl]". subst.
-    iApply "Hlog".
-    done.
+    unfold acquire.
+    iApply bin_log_related_rec_r; auto. asimpl.
+    rel_bind_r (CAS _ _ _).
+    iApply (bin_log_related_cas_suc_r with "Hl"); auto.
+    iIntros "Hl". rewrite fill_app /=.
+    iApply bin_log_related_if_true_r; auto.
+    by iApply "Hlog".
   Qed.
   
   Global Opaque acquire.
@@ -165,17 +174,9 @@ Section proof.
     -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
-    pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ (#♭v false))%I).
-    iApply (bin_log_related_step_r Φ with "[Hl]").
-    { autosubst.  }
-    { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
-      tp_apply j steps_release with "Hl" as "Hl".
-      iExists UnitV. simpl. iFrame.
-      iModIntro. iSplitL; eauto. }
-    iIntros (v') "[% Hl]". subst.
-    iApply "Hlog".
-    done.
+    unfold release.
+    iApply (bin_log_related_rec_r); auto. simpl.
+    iApply (bin_log_related_store_r with "Hl"); auto.
   Qed.
 
   Global Opaque release.
@@ -207,22 +208,6 @@ Section proof.
     tp_normalise j. asimpl.
     by iFrame.
   Qed.
-
-  (* TODO: those should be accompaied by lemmas; preferably so that 
-     [change] does not change too much *)
-  Tactic Notation "rel_bind_l" open_constr(efoc) :=
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e'))
-    end.
-  Tactic Notation "rel_bind_r" open_constr(efoc) :=
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    end.
-
   
   Lemma bin_log_related_with_lock_r' Γ K E1 E2 Q e ev ew v w l t τ :
     (nclose specN ⊆ E1) →

F_mu_ref_conc/relational_properties.v

@@ -790,17 +790,18 @@ Section properties.
     done.
   Qed.
   
-  Lemma bin_log_related_cas_fail_r Γ K l e1 e2 v1 v2 v t τ
+  Lemma bin_log_related_cas_fail_r Γ E1 E2 K l e1 e2 v1 v2 v t τ
     (Hclosed1 : ∀ f, e1.[f] = e1)
     (Hclosed2 : ∀ f, e2.[f] = e2) :
+    (nclose specN ⊆ E1) →
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (v <> v1) →
     l ↦ₛ v -∗
-    (l ↦ₛ v -∗ Γ ⊨ t ≤log≤ fill K (#♭ false) : τ)
-    -∗ Γ ⊨ t ≤log≤ fill K (CAS (Loc l) e1 e2) : τ.
+    (l ↦ₛ v -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (#♭ false) : τ)
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (CAS (Loc l) e1 e2) : τ.
   Proof.
-    iIntros (???) "Hl Hlog".
+    iIntros (????) "Hl Hlog".
     pose (Φ := (fun w => ⌜w = BoolV false⌝ ∗ l ↦ₛ v)%I).
     iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
     rewrite_closed.
@@ -814,17 +815,18 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_cas_suc_r Γ K l e1 e2 v1 v2 v t τ
+  Lemma bin_log_related_cas_suc_r Γ E1 E2 K l e1 e2 v1 v2 v t τ
     (Hclosed1 : ∀ f, e1.[f] = e1)
     (Hclosed2 : ∀ f, e2.[f] = e2) :
+    (nclose specN ⊆ E1) →   
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (v = v1) →
     l ↦ₛ v -∗
-    (l ↦ₛ v2 -∗ Γ ⊨ t ≤log≤ fill K (#♭ true) : τ)
-    -∗ Γ ⊨ t ≤log≤ fill K (CAS (Loc l) e1 e2) : τ.
+    (l ↦ₛ v2 -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (#♭ true) : τ)
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (CAS (Loc l) e1 e2) : τ.
   Proof.
-    iIntros (???) "Hl Hlog".
+    iIntros (????) "Hl Hlog".
     pose (Φ := (fun w => ⌜w = BoolV true⌝ ∗ l ↦ₛ v2)%I).
     iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
     rewrite_closed.

prelude/base.v

@@ -28,7 +28,7 @@ Ltac properness :=
   | |- (_ ∨ _)%I ≡ (_ ∨ _)%I => apply or_proper
   | |- (_ → _)%I ≡ (_ → _)%I => apply impl_proper
   | |- (_ -∗ _)%I ≡ (_ -∗ _)%I => apply wand_proper
-  | |- (WP _ {{ _ }})%I ≡ (WP _ {{ _ }})%I => apply wp_proper =>?
+  | |- (WP _ @ _ {{ _ }})%I ≡ (WP _ @ _ {{ _ }})%I => apply wp_proper =>?
   | |- (▷ _)%I ≡ (▷ _)%I => apply later_proper
   | |- (□ _)%I ≡ (□ _)%I => apply always_proper
   | |- (|={_,_}=> _ )%I ≡ (|={_,_}=> _ )%I => apply fupd_proper