Some forgotten Proper instances.

modures/auth.v

@@ -20,10 +20,16 @@ Instance auth_dist : Dist (auth A) := λ n x y,
 
 Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
 Proof. by split. Qed.
+Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A).
+Proof. by split. Qed.
 Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
 Proof. by destruct 1. Qed.
+Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
+Proof. by destruct 1. Qed.
 Global Instance own_ne : Proper (dist n ==> dist n) (@own A).
 Proof. by destruct 1. Qed.
+Global Instance own_proper : Proper ((≡) ==> (≡)) (@own A).
+Proof. by destruct 1. Qed.
 
 Instance auth_compl : Compl (auth A) := λ c,
   Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).

modures/cmra.v

@@ -143,12 +143,12 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
   ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z).
-Instance: Params (@cmra_updateP) 3.
+Instance: Params (@cmra_updateP) 1.
 Infix "⇝:" := cmra_updateP (at level 70).
 Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
   ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z).
 Infix "⇝" := cmra_update (at level 70).
-Instance: Params (@cmra_update) 3.
+Instance: Params (@cmra_update) 1.
 
 (** * Properties **)
 Section cmra.
@@ -193,6 +193,17 @@ Proof.
   intros x x' Hx y y' Hy.
   by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
 Qed.
+Global Instance cmra_update_proper :
+  Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
+Qed.
+Global Instance cmra_updateP_proper :
+  Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
+Proof.
+  intros x1 x2 Hx P1 P2 HP; split=>Hup z n;
+    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
+Qed.
 
 (** ** Validity *)
 Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.

modures/excl.v

@@ -27,6 +27,14 @@ Inductive excl_dist `{Dist A} : Dist (excl A) :=
   | ExclUnit_dist n : ExclUnit ={n}= ExclUnit
   | ExclBot_dist n : ExclBot ={n}= ExclBot.
 Existing Instance excl_dist.
+Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A).
+Proof. by constructor. Qed.
+Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
+Proof. by constructor. Qed.
+Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
+Proof. by inversion_clear 1. Qed.
+Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
+Proof. by inversion_clear 1. Qed.
 Program Definition excl_chain
     (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
   {| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
@@ -66,10 +74,6 @@ Proof.
 Qed.
 Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
 
-Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
-Proof. by inversion_clear 1. Qed.
-Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
-Proof. by inversion_clear 1. Qed.
 Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).