lock allows applying equivalences

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 35551d40f927c1d567993ff27eeb46f64788efca
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1edf71ef9809456c29454d8ad60c34ea10e36fe8

theories/lang/lib/lock.v

@@ -28,16 +28,13 @@ Section proof.
     (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
 
   Definition is_lock (γ : lockname) (l : loc) (R : iProp Σ) : iProp Σ :=
-    (cinv N (γ.1) (lock_inv (γ.2) l R))%I.
+    cinv N (γ.1) (lock_inv (γ.2) l R).
 
   Definition own_lock (γ : lockname) : frac → iProp Σ :=
     cinv_own (γ.1).
 
   Definition locked (γ : lockname): iProp Σ := own (γ.2) (Excl ()).
 
-  Lemma locked_exclusive (γ : lockname) : locked γ -∗ locked γ -∗ False.
-  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
-
   Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
   Proof. solve_proper. Qed.
   Global Instance is_lock_contractive γ l : Contractive (is_lock γ l).
@@ -50,6 +47,18 @@ Section proof.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
 
+  Lemma locked_exclusive (γ : lockname) : locked γ -∗ locked γ -∗ False.
+  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+
+  Lemma is_lock_iff γ l R R' :
+    □ ▷ (R ↔ R') -∗ is_lock γ l R -∗ is_lock γ l R'.
+  Proof.
+    iIntros "#HRR' Hlck". iApply cinv_iff; last done. iNext. iAlways.
+    iSplit; iIntros "Hinv"; iDestruct "Hinv" as (b) "[Hl HR]"; iExists b;
+      iFrame "Hl"; (destruct b; first done); iDestruct "HR" as "[$ HR]";
+      by iApply "HRR'".
+  Qed.
+
   (** The main proofs. *)
   Lemma newlock_inplace (E : coPset) (R : iProp Σ) l (b : bool) :
     l ↦ #b -∗ (if b then True else ▷ R) ={E}=∗ ∃ γ, is_lock γ l R ∗ own_lock γ 1%Qp.