diff --git a/CHANGELOG.md b/CHANGELOG.md
index e9f7cefa6d182c70d56f4dc538611b5953fd6c55..c8934aea512fb23e6baee70eb1466ab1151bb7d2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -83,6 +83,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Make use of `ofe_iso` in the COFE solver.
 * The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
   `{o,r,ur}Functor_apply` to better match their intent.
+* Change `inv_iff`, `cinv_iff` and `na_inv_iff` to make order of arguments
+  consistent and more convenient for `iApply`. They are now of the form
+  `inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q` and (similar for `na_inv_iff` and
+  `cinv_iff`), following e.g., `inv_alter` and `wp_wand`.
+* Add lemma `is_lock_iff` and show that `is_lock` is contractive.
 
 **Changes in heap_lang:**
 
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 6eb3ef0248d1e6258dd99c4c8adac475c83b7300..234123b5737f249edd5ed8f37b9881a652932c19 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -53,11 +53,10 @@ Section proofs.
     iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
   Qed.
 
-  Lemma cinv_iff N γ P P' :
-    ▷ □ (P ↔ P') -∗ cinv N γ P -∗ cinv N γ P'.
+  Lemma cinv_iff N γ P Q : cinv N γ P -∗ ▷ □ (P ↔ Q) -∗ cinv N γ Q.
   Proof.
-    iIntros "#HP". iApply inv_iff. iIntros "!> !>".
-    iSplit; iIntros "[?|$]"; iLeft; by iApply "HP".
+    iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
+    iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
   Qed.
 
   (*** Allocation rules. *)
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index c8e996fa20a3b9a7fd56d1a6ba3f0dc217010379..a1af8026d410b62d13f0ff9232f5ff606fd0f020 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -97,18 +97,17 @@ Section inv.
   Global Instance inv_persistent N P : Persistent (inv N P).
   Proof. rewrite inv_eq. apply _. Qed.
 
-  Lemma inv_alter N P Q:
-    inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
+  Lemma inv_alter N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
   Proof.
-    rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
+    rewrite inv_eq. iIntros "#HI #HPQ !>" (E H).
     iMod ("HI" $! E H) as "[HP Hclose]".
-    iDestruct ("Acc" with "HP") as "[$ HQP]".
+    iDestruct ("HPQ" with "HP") as "[$ HQP]".
     iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
   Qed.
 
-  Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q.
+  Lemma inv_iff N P Q : inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q.
   Proof.
-    iIntros "#HPQ #HI". iApply (inv_alter with "HI").
+    iIntros "#HI #HPQ". iApply (inv_alter with "HI").
     iIntros "!> !> HP". iSplitL "HP".
     - by iApply "HPQ".
     - iIntros "HQ". by iApply "HPQ".
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 25c749dad1368289f22bdcb1c11afe8e6c3173cb..00d4452b89f0ce61aeb6ba950d4555544d19b1e9 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -43,10 +43,10 @@ Section proofs.
   Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
-  Lemma na_inv_iff p N P Q : ▷ □ (P ↔ Q) -∗ na_inv p N P -∗ na_inv p N Q.
+  Lemma na_inv_iff p N P Q : na_inv p N P -∗ ▷ □ (P ↔ Q) -∗ na_inv p N Q.
   Proof.
-    iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
-    iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
+    iIntros "HI #HPQ". rewrite /na_inv. iDestruct "HI" as (i ?) "HI".
+    iExists i. iSplit; first done. iApply (inv_iff with "HI").
     iIntros "!> !>".
     iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 1bd35bf56ea661b99240d01eeff0dee87739a9f8..184b62fd4b524fff8033ef918d05b9b7137c4996 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -13,8 +13,10 @@ Structure lock Σ `{!heapG Σ} := Lock {
   is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
   locked (γ: name) : iProp Σ;
   (* -- general properties -- *)
-  is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
+  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 -- *)
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index f0aab59b4d1bec01bcbc8cf1f3d7010dad81db56..d9be8c585c60044a9b962465a22be0df15ec8453 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -36,8 +36,8 @@ Section proof.
 
   Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
-  Proof. solve_proper. Qed.
+  Global Instance is_lock_contractive γ l : Contractive (is_lock γ l).
+  Proof. solve_contractive. Qed.
 
   (** The main proofs. *)
   Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
@@ -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 |}.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 8296258b676ba98bded79e7d42069bc1bb72abac..93b60961cb81a53bdeded9d0b0f49c7a058dc1ad 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -54,11 +54,10 @@ Section proof.
 
   Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, GSet ∅)))%I.
 
-  Global Instance lock_inv_ne γ lo ln :
-    NonExpansive (lock_inv γ lo ln).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
+  Global Instance lock_inv_ne γ lo ln : NonExpansive (lock_inv γ lo ln).
   Proof. solve_proper. Qed.
+  Global Instance is_lock_contractive γ lk : Contractive (is_lock γ lk).
+  Proof. solve_contractive. Qed.
   Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
   Proof. apply _. Qed.
   Global Instance locked_timeless γ : Timeless (locked γ).
@@ -70,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.
@@ -163,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 |}.