From 7f04cf65ad82a12e7e50662f3bdfba42b5f65a05 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Feb 2017 20:51:41 +0100
Subject: [PATCH] Proper instances for types classes over ofe and cmra
 elements, and upreds.

---
 theories/algebra/cmra.v       | 13 +++++++++++++
 theories/algebra/ofe.v        | 11 +++++++----
 theories/base_logic/derived.v |  8 +++++++-
 3 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 444f4c89c..a8aeb26dc 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -139,23 +139,27 @@ Infix "â‹…?" := opM (at level 50, left associativity) : C_scope.
 Class Persistent {A : cmraT} (x : A) := persistent : pcore x ≡ Some x.
 Arguments persistent {_} _ {_}.
 Hint Mode Persistent + ! : typeclass_instances.
+Instance: Params (@Persistent) 1.
 
 (** * Exclusive elements (i.e., elements that cannot have a frame). *)
 Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
 Arguments exclusive0_l {_} _ {_} _ _.
 Hint Mode Exclusive + ! : typeclass_instances.
+Instance: Params (@Exclusive) 1.
 
 (** * Cancelable elements. *)
 Class Cancelable {A : cmraT} (x : A) :=
   cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
 Arguments cancelableN {_} _ {_} _ _ _ _.
 Hint Mode Cancelable + ! : typeclass_instances.
+Instance: Params (@Cancelable) 1.
 
 (** * Identity-free elements. *)
 Class IdFree {A : cmraT} (x : A) :=
   id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
 Arguments id_free0_r {_} _ {_} _ _.
 Hint Mode IdFree + ! : typeclass_instances.
+Instance: Params (@IdFree) 1.
 
 (** * CMRAs whose core is total *)
 (** The function [core] may return a dummy when used on CMRAs without total
@@ -313,6 +317,15 @@ Proof. destruct 2; by ofe_subst. Qed.
 Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
 Proof. destruct 2; by setoid_subst. Qed.
 
+Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent A).
+Proof. solve_proper. Qed.
+Global Instance Exclusive_proper : Proper ((≡) ==> iff) (@Exclusive A).
+Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
+Global Instance Cancelable_proper : Proper ((≡) ==> iff) (@Cancelable A).
+Proof. intros x y Hxy. rewrite /Cancelable. by setoid_rewrite Hxy. Qed.
+Global Instance IdFree_proper : Proper ((≡) ==> iff) (@IdFree A).
+Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
+
 (** ** Op *)
 Lemma cmra_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
 Proof. destruct mz; by rewrite /= -?assoc. Qed.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f374a62ee..4055a245e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -102,6 +102,7 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
 Class Timeless {A : ofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
 Arguments timeless {_} _ {_} _ _.
 Hint Mode Timeless + ! : typeclass_instances.
+Instance: Params (@Timeless) 1.
 
 Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
 
@@ -152,15 +153,17 @@ Section ofe.
   Qed.
   Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
   Proof. by apply dist_proper. Qed.
+  Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless A).
+  Proof. intros x y Hxy. rewrite /Timeless. by setoid_rewrite Hxy. Qed.
+
   Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y.
   Proof. induction 2; eauto using dist_S. Qed.
   Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
   Proof. intros; eauto using dist_le. Qed.
-  Instance ne_proper {B : ofeT} (f : A → B)
-    `{!NonExpansive f} : Proper ((≡) ==> (≡)) f | 100.
+  Instance ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
+    Proper ((≡) ==> (≡)) f | 100.
   Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
-  Instance ne_proper_2 {B C : ofeT} (f : A → B → C)
-    `{!NonExpansive2 f} :
+  Instance ne_proper_2 {B C : ofeT} (f : A → B → C) `{!NonExpansive2 f} :
     Proper ((≡) ==> (≡) ==> (≡)) f | 100.
   Proof.
      unfold Proper, respectful; setoid_rewrite equiv_dist.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index bb4f7fa2a..387a09362 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -32,11 +32,12 @@ Typeclasses Opaque uPred_except_0.
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
 Arguments timelessP {_} _ {_}.
 Hint Mode TimelessP + ! : typeclass_instances.
+Instance: Params (@TimelessP) 1.
 
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
-Hint Mode PersistentP - ! : typeclass_instances.
 Arguments persistentP {_} _ {_}.
 Hint Mode PersistentP + ! : typeclass_instances.
+Instance: Params (@PersistentP) 1.
 
 Module uPred.
 Section derived.
@@ -746,6 +747,8 @@ Proof.
 Qed.
 
 (* Timeless instances *)
+Global Instance TimelessP_proper : Proper ((≡) ==> iff) (@TimelessP M).
+Proof. solve_proper. Qed.
 Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
 Proof.
   rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
@@ -811,6 +814,9 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
 Proof. destruct mx; apply _. Qed.
 
 (* Derived lemmas for persistence *)
+Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M).
+Proof. solve_proper. Qed.
+
 Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
 Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
-- 
GitLab