From 2b0886b93fa448828dfd228669444d5ef3724d82 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 17:20:45 +0200
Subject: [PATCH] Derive `is_lock_contractive`.

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

diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 10e87b49d..ed80e9ca4 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Import primitive_laws notation.
+From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 (** A general interface for a lock.
@@ -28,7 +28,6 @@ Class lock `{!heapGS_gen hlc Σ} := Lock {
   is_lock (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ;
   locked (γ: lock_name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_lock_ne γ lk :> Contractive (is_lock γ lk);
   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;
@@ -44,5 +43,14 @@ Class lock `{!heapGS_gen hlc Σ} := Lock {
 }.
 Global Hint Mode lock + + + : typeclass_instances.
 
-Global Instance is_lock_proper hlc Σ `{!heapGS_gen hlc Σ} (L : lock) γ lk :
-  Proper ((≡) ==> (≡)) (L.(is_lock) γ lk) := ne_proper _.
+Global Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock} γ lk :
+  Contractive (is_lock γ lk).
+Proof.
+  apply (uPred.contractive_internal_eq (M:=iResUR Σ)).
+  iIntros (P Q) "#HPQ". iApply prop_ext. iIntros "!>".
+  iSplit; iIntros "H"; iApply (is_lock_iff with "H");
+    iNext; iRewrite "HPQ"; auto.
+Qed.
+
+Global Instance is_lock_proper `{!heapGS_gen hlc Σ, !lock} γ lk :
+  Proper ((≡) ==> (≡)) (is_lock γ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 07cd3721b..30753ba19 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -92,8 +92,7 @@ Section proof.
   Qed.
 End proof.
 
-Program Definition spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
+Definition spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
   {| 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 |}.
-Next Obligation. intros. rewrite /is_lock /lock_inv. solve_contractive. Qed.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 5095a766b..609560364 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -163,8 +163,7 @@ Section proof.
   Qed.
 End proof.
 
-Program Definition ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
+Definition ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
   {| 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 |}.
-Next Obligation. intros. rewrite /is_lock /lock_inv. solve_contractive. Qed.
-- 
GitLab