Add rule `is_lock_iff` for locks.

theories/heap_lang/lib/lock.v

@@ -15,6 +15,8 @@ Structure lock Σ `{!heapG Σ} := Lock {
   (* -- general properties -- *)
   is_lock_ne N γ lk : Contractive (is_lock N γ lk);
   is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
+  is_lock_iff N γ lk R1 R2 :
+    is_lock N γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock N γ lk R2;
   locked_timeless γ : Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (* -- operation specs -- *)

theories/heap_lang/lib/spin_lock.v

@@ -45,6 +45,16 @@ Section proof.
   Global Instance locked_timeless γ : Timeless (locked γ).
   Proof. apply _. Qed.
 
+  Lemma is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2.
+  Proof.
+    iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
+    iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
+    iIntros "!> !#"; iSplit; iDestruct 1 as (b) "[Hl H]";
+      iExists b; iFrame "Hl"; destruct b;
+      first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
+  Qed.
+
   Lemma newlock_spec (R : iProp Σ):
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
@@ -92,5 +102,6 @@ End proof.
 Typeclasses Opaque is_lock locked.
 
 Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
-  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
+  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
+     lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.

theories/heap_lang/lib/ticket_lock.v

@@ -69,6 +69,16 @@ Section proof.
     iDestruct (own_valid_2 with "H1 H2") as %[[] _].
   Qed.
 
+  Lemma is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2.
+  Proof.
+    iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
+    iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
+    iIntros "!> !#"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
+      iExists o, n; iFrame "Ho Hn H●";
+      (iDestruct "H" as "[[H◯ H]|H◯]"; [iLeft; iFrame "H◯"; by iApply "HR"|by iRight]).
+  Qed.
+
   Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
@@ -162,5 +172,6 @@ End proof.
 Typeclasses Opaque is_lock issued locked.
 
 Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
-  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
+  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
+     lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.