From 6fabbbc1bbcdc98a760918430140723477b0cc9b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 17:22:34 +0200
Subject: [PATCH] =?UTF-8?q?Prefer=20`=E2=88=97-=E2=88=97`=20over=20`?=
 =?UTF-8?q?=E2=86=94`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris_heap_lang/lib/lock.v        | 2 +-
 iris_heap_lang/lib/spin_lock.v   | 2 +-
 iris_heap_lang/lib/ticket_lock.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index ed80e9ca4..5c66f9c7c 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -30,7 +30,7 @@ Class lock `{!heapGS_gen hlc Σ} := Lock {
   (** * General properties of the predicates *)
   is_lock_persistent γ lk R :> Persistent (is_lock γ lk R);
   is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2;
+    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2;
   locked_timeless γ :> Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (** * Program specs *)
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 30753ba19..c449f45c6 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -39,7 +39,7 @@ Section proof.
 
   (** The main proofs. *)
   Local Lemma is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk 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").
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 609560364..02c4e48d0 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -63,7 +63,7 @@ Section proof.
   Qed.
 
   Local Lemma is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk 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").
-- 
GitLab