rw_lock: add Proper instances

iris_heap_lang/lib/rw_lock.v

 From iris.base_logic.lib Require Export invariants.
 From iris.bi.lib Require Export fractional.
-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 reader-writer lock.
@@ -63,3 +63,27 @@ Class rwlock `{!heapGS_gen hlc Σ} := RwLock {
     {{{ RET #(); True }}};
 }.
 Global Hint Mode rwlock + + + : typeclass_instances.
+
+Global Instance is_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock} γ lk :
+  ∀ n, Proper (pointwise_relation _ (dist_later n) ==> dist n) (is_rw_lock γ lk).
+Proof.
+  intros n Φ1 Φ2 HΦ.
+  set (Φ1' := λne (q : leibnizO Qp), Φ1 q).
+  set (Φ2' := λne (q : leibnizO Qp), Φ2 q).
+  assert (Next Φ1' ≡{n}≡ Next Φ2') as HΦ'.
+  { constructor => m ? q /=. specialize (HΦ q). by eapply dist_later_dist_lt. }
+  clear HΦ. revert n HΦ'. eapply (uPred.internal_eq_entails (M:=iResUR Σ)).
+  rewrite later_equivI. iIntros "#HΦ". iApply prop_ext. iModIntro.
+  iSplit; iIntros "H"; iApply (is_rw_lock_iff with "H"); iIntros "!> !> %q".
+  all: rewrite ofe_morO_equivI; iSpecialize ("HΦ" $! q).
+  all: change (Φ1 q) with (Φ1' q); change (Φ2 q) with (Φ2' q).
+  all: iRewrite "HΦ"; auto.
+Qed.
+
+Global Instance is_rw_lock_proper `{!heapGS_gen hlc Σ, !rwlock} γ lk :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (is_rw_lock γ lk).
+Proof.
+  intros Φ1 Φ2 HΦ.
+  apply equiv_dist=>n. apply is_rw_lock_contractive=>q.
+  constructor=>m _. move: (HΦ q) => /equiv_dist. auto.
+Qed.