diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v index 1bd35bf56ea661b99240d01eeff0dee87739a9f8..5ed577320d8f3f4282f5d1f1c3800707fd16242e 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 f0aab59b4d1bec01bcbc8cf1f3d7010dad81db56..c7e2cbc8497522b7bb7bf0819b290e67dafe2a38 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 8296258b676ba98bded79e7d42069bc1bb72abac..603984a5a963340d8415aa1785720bf7a35669e9 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 γ).