From 386b91b5a4d1c6a28fd68735c574e5474377a6bf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 18:03:31 +0100
Subject: [PATCH] LeibnizEquiv instances for Modures.

---
 iris/resources.v | 4 ++--
 modures/auth.v   | 2 ++
 modures/cofe.v   | 3 +++
 modures/excl.v   | 2 ++
 4 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/iris/resources.v b/iris/resources.v
index 632a15d30..725d36f32 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -41,8 +41,8 @@ Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Σ A).
 Proof.
   intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia.
 Qed.
-Global Instance pst_proper : Proper ((≡) ==> (≡)) (@pst Σ A).
-Proof. by destruct 1. Qed.
+Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Σ A).
+Proof. by destruct 1; unfold_leibniz. Qed.
 Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Σ A).
 Proof. by destruct 1. Qed.
 Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Σ A).
diff --git a/modures/auth.v b/modures/auth.v
index eedff6979..c821b5de3 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -45,6 +45,8 @@ Canonical Structure authC := CofeT auth_cofe_mixin.
 Instance Auth_timeless (x : excl A) (y : A) :
   Timeless x → Timeless y → Timeless (Auth x y).
 Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
+Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
+Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
 End cofe.
 
 Arguments authC : clear implicits.
diff --git a/modures/cofe.v b/modures/cofe.v
index 1b8913b96..f8d32d84a 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -300,6 +300,9 @@ End discrete_cofe.
 Arguments discreteC _ {_ _}.
 
 Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
+Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
+Proof. by intros A x y. Qed.
+
 Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
 
diff --git a/modures/excl.v b/modures/excl.v
index 638290684..fcac96f26 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -75,6 +75,8 @@ Proof. by inversion_clear 1; constructor. Qed.
 Global Instance excl_timeless :
   (∀ x : A, Timeless x) → ∀ x : excl A, Timeless x.
 Proof. intros ? []; apply _. Qed.
+Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
+Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 (* CMRA *)
 Instance excl_valid : Valid (excl A) := λ x,
-- 
GitLab