From 92eaf4f9c4294a0c3d0e2cf21e19f50323726635 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 17:44:08 +0200
Subject: [PATCH] Prove that `is_lock` is contractive.

---
 theories/heap_lang/lib/lock.v        | 2 +-
 theories/heap_lang/lib/spin_lock.v   | 4 ++--
 theories/heap_lang/lib/ticket_lock.v | 7 +++----
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 1bd35bf56..5ed577320 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -13,7 +13,7 @@ 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);
   locked_timeless γ : Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index f0aab59b4..c7e2cbc84 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).
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 8296258b6..603984a5a 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 γ).
-- 
GitLab