notation for declaring a function non-expansive

theories/algebra/agree.v

@@ -271,12 +271,12 @@ Proof.
   split; rewrite Hxy; done.
 Qed.
 
-Instance: ∀ x : agree A, Proper (dist n ==> dist n) (op x).
+Instance: ∀ x : agree A, NonExpansive (op x).
 Proof.
-  intros n x y1 y2. rewrite /dist /agree_dist /agree_list /=. 
+  intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=. 
   rewrite !app_comm_cons. apply: list_setequiv_app.
 Qed.
-Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
+Instance: NonExpansive2 (@op (agree A) _).
 Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
 Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
 Instance: Assoc (≡) (@op (agree A) _).
@@ -347,7 +347,7 @@ Qed.
 Definition to_agree (x : A) : agree A :=
   {| agree_car := x; agree_with := [] |}.
 
-Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
+Global Instance to_agree_ne : NonExpansive to_agree.
 Proof.
   intros x1 x2 Hx; rewrite /= /dist /agree_dist /=.
   exact: list_setequiv_singleton.
@@ -420,11 +420,11 @@ Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
 Proof. rewrite /agree_map /= list_fmap_compose. done. Qed.
 
 Section agree_map.
-  Context {A B : ofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}.
   Collection Hyps := Type Hf.
-  Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
+  Instance agree_map_ne : NonExpansive (agree_map f).
   Proof using Hyps.
-    intros x y Hxy.
+    intros n x y Hxy.
     change (list_setequiv (dist n)(f <$> (agree_list x))(f <$> (agree_list y))).
     eapply list_setequiv_fmap; last exact Hxy. apply _. 
   Qed.
@@ -452,9 +452,9 @@ End agree_map.
 
 Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
   CofeMor (agree_map f : agreeC A → agreeC B).
-Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
+Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B).
 Proof.
-  intros f g Hfg x. apply: list_setequiv_ext.
+  intros n f g Hfg x. apply: list_setequiv_ext.
   change (f <$> (agree_list x) ≡{n}≡ g <$> (agree_list x)).
   apply list_fmap_ext_ne. done.
 Qed.

theories/algebra/auth.v

@@ -23,15 +23,15 @@ Instance auth_equiv : Equiv (auth A) := λ x y,
 Instance auth_dist : Dist (auth A) := λ n x y,
   authoritative x ≡{n}≡ authoritative y ∧ auth_own x ≡{n}≡ auth_own y.
 
-Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
+Global Instance Auth_ne : NonExpansive2 (@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).
+Global Instance authoritative_ne: NonExpansive (@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) (@auth_own A).
+Global Instance own_ne : NonExpansive (@auth_own A).
 Proof. by destruct 1. Qed.
 Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
 Proof. by destruct 1. Qed.
@@ -295,8 +295,8 @@ Proof.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).
-Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
-Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
+Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
+Proof. intros n f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
 
 Program Definition authRF (F : urFunctor) : rFunctor := {|
   rFunctor_car A B := authR (urFunctor_car F A B);

theories/algebra/cmra.v

@@ -37,7 +37,7 @@ Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
 Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
   (* setoids *)
-  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
+  mixin_cmra_op_ne (x : A) : NonExpansive (op x);
   mixin_cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
@@ -93,7 +93,7 @@ Canonical Structure cmra_ofeC.
 Section cmra_mixin.
   Context {A : cmraT}.
   Implicit Types x y : A.
-  Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
+  Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
   Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
   Lemma cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
@@ -211,7 +211,7 @@ Class CMRADiscrete (A : cmraT) := {
 
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
-  cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
+  cmra_monotone_ne :> NonExpansive f;
   cmra_monotone_validN n x : ✓{n} x → ✓{n} f x;
   cmra_monotone x y : x ≼ y → f x ≼ f y
 }.
@@ -221,7 +221,7 @@ Arguments cmra_monotone {_ _} _ {_} _ _ _.
 (* Not all intended homomorphisms preserve validity, in particular it does not
 hold for the [ownM] and [own] connectives. *)
 Class CMRAHomomorphism {A B : cmraT} (f : A → B) := {
-  cmra_homomorphism_ne n :> Proper (dist n ==> dist n) f;
+  cmra_homomorphism_ne :> NonExpansive f;
   cmra_homomorphism x y : f (x ⋅ y) ≡ f x ⋅ f y
 }.
 Arguments cmra_homomorphism {_ _} _ _ _ _.
@@ -239,9 +239,9 @@ Implicit Types x y z : A.
 Implicit Types xs ys zs : list A.
 
 (** ** Setoids *)
-Global Instance cmra_pcore_ne' n : Proper (dist n ==> dist n) (@pcore A _).
+Global Instance cmra_pcore_ne' : NonExpansive (@pcore A _).
 Proof.
-  intros x y Hxy. destruct (pcore x) as [cx|] eqn:?.
+  intros n x y Hxy. destruct (pcore x) as [cx|] eqn:?.
   { destruct (cmra_pcore_ne n x y cx) as (cy&->&->); auto. }
   destruct (pcore y) as [cy|] eqn:?; auto.
   destruct (cmra_pcore_ne n y x cy) as (cx&?&->); simplify_eq/=; auto.
@@ -255,8 +255,8 @@ Proof.
 Qed.
 Global Instance cmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _).
 Proof. apply (ne_proper _). Qed.
-Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
-Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
+Global Instance cmra_op_ne' : NonExpansive2 (@op A _).
+Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
 Global Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
 Proof. apply (ne_proper_2 _). Qed.
 Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
@@ -287,7 +287,7 @@ Proof.
   intros x x' Hx y y' Hy.
   by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
 Qed.
-Global Instance cmra_opM_ne n : Proper (dist n ==> dist n ==> dist n) (@opM A).
+Global Instance cmra_opM_ne : NonExpansive2 (@opM A).
 Proof. destruct 2; by cofe_subst. Qed.
 Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
 Proof. destruct 2; by setoid_subst. Qed.
@@ -448,9 +448,9 @@ Section total_core.
     by rewrite /core /= Hcx Hcy.
   Qed.
 
-  Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
+  Global Instance cmra_core_ne : NonExpansive (@core A _).
   Proof.
-    intros x y Hxy. destruct (cmra_total x) as [cx Hcx].
+    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
     by rewrite /core /= -Hxy Hcx.
   Qed.
   Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
@@ -616,8 +616,8 @@ End ucmra_leibniz.
 Section cmra_total.
   Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
   Context (total : ∀ x, is_Some (pcore x)).
-  Context (op_ne : ∀ n (x : A), Proper (dist n ==> dist n) (op x)).
-  Context (core_ne : ∀ n, Proper (dist n ==> dist n) (@core A _)).
+  Context (op_ne : ∀ (x : A), NonExpansive (op x)).
+  Context (core_ne : NonExpansive (@core A _)).
   Context (validN_ne : ∀ n, Proper (dist n ==> impl) (@validN A _ n)).
   Context (valid_validN : ∀ (x : A), ✓ x ↔ ∀ n, ✓{n} x).
   Context (validN_S : ∀ n (x : A), ✓{S n} x → ✓{n} x).
@@ -693,8 +693,8 @@ Structure rFunctor := RFunctor {
   rFunctor_car : ofeT → ofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne A1 A2 B1 B2 n :
-    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
+  rFunctor_ne A1 A2 B1 B2 :
+    NonExpansive (@rFunctor_map A1 A2 B1 B2);
   rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
   rFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -726,8 +726,8 @@ Structure urFunctor := URFunctor {
   urFunctor_car : ofeT → ofeT → ucmraT;
   urFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
-  urFunctor_ne A1 A2 B1 B2 n :
-    Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2);
+  urFunctor_ne A1 A2 B1 B2 :
+    NonExpansive (@urFunctor_map A1 A2 B1 B2);
   urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x ≡ x;
   urFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -762,7 +762,7 @@ Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
 Section cmra_transport.
   Context {A B : cmraT} (H : A = B).
   Notation T := (cmra_transport H).
-  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
+  Global Instance cmra_transport_ne : NonExpansive T.
   Proof. by intros ???; destruct H. Qed.
   Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
   Proof. by intros ???; destruct H. Qed.
@@ -1178,7 +1178,7 @@ Section option.
   Proof.
     apply cmra_total_mixin.
     - eauto.
-    - by intros n [x|]; destruct 1; constructor; cofe_subst.
+    - by intros [x|] n; destruct 1; constructor; cofe_subst.
     - destruct 1; by cofe_subst.
     - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
     - intros [x|]; [apply cmra_valid_validN|done].

theories/algebra/cmra_big_op.v

@@ -76,8 +76,8 @@ Lemma big_op_Forall2 R :
   Proper (Forall2 R ==> R) (@big_op M).
 Proof. rewrite /Proper /respectful. induction 3; eauto. Qed.
 
-Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op M).
-Proof. apply big_op_Forall2; apply _. Qed.
+Global Instance big_op_ne : NonExpansive (@big_op M).
+Proof. intros ?. apply big_op_Forall2; apply _. Qed.
 Global Instance big_op_proper : Proper ((≡) ==> (≡)) (@big_op M) := ne_proper _.
 
 Lemma big_op_nil : [⋅] (@nil M) = ∅.

theories/algebra/cofe_solver.v

@@ -98,7 +98,7 @@ Qed.
 Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
 Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
 
-Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k).
+Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
 Proof. by intros X Y HX. Qed.
 Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k).
 
@@ -152,8 +152,8 @@ Program Definition embed (k : nat) (x : A k) : T :=
   {| tower_car n := embed_coerce n x |}.
 Next Obligation. intros k x i. apply g_embed_coerce. Qed.
 Instance: Params (@embed) 1.
-Instance embed_ne k n : Proper (dist n ==> dist n) (embed k).
-Proof. by intros x y Hxy i; rewrite /= Hxy. Qed.
+Instance embed_ne k : NonExpansive (embed k).
+Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
 Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
 Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
 Proof.
@@ -188,7 +188,7 @@ Next Obligation.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
 Definition unfold (X : T) : F T := compl (unfold_chain X).
-Instance unfold_ne : Proper (dist n ==> dist n) unfold.
+Instance unfold_ne : NonExpansive unfold.
 Proof.
   intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
     (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
@@ -201,7 +201,7 @@ Next Obligation.
   rewrite g_S -cFunctor_compose.
   apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
-Instance fold_ne : Proper (dist n ==> dist n) fold.
+Instance fold_ne : NonExpansive fold.
 Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.

theories/algebra/csum.v

@@ -39,7 +39,7 @@ Inductive csum_dist : Dist (csum A B) :=
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
 Existing Instance csum_dist.
 
-Global Instance Cinl_ne n : Proper (dist n ==> dist n) (@Cinl A B).
+Global Instance Cinl_ne : NonExpansive (@Cinl A B).
 Proof. by constructor. Qed.
 Global Instance Cinl_proper : Proper ((≡) ==> (≡)) (@Cinl A B).
 Proof. by constructor. Qed.
@@ -47,7 +47,7 @@ Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B).
 Proof. by inversion_clear 1. Qed.
 Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B).
 Proof. by inversion_clear 1. Qed.
-Global Instance Cinr_ne n : Proper (dist n ==> dist n) (@Cinr A B).
+Global Instance Cinr_ne : NonExpansive (@Cinr A B).
 Proof. by constructor. Qed.
 Global Instance Cinr_proper : Proper ((≡) ==> (≡)) (@Cinr A B).
 Proof. by constructor. Qed.
@@ -132,9 +132,9 @@ Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply
 Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
   csumC A B -n> csumC A' B' :=
   CofeMor (csum_map f g).
-Instance csumC_map_ne A A' B B' n :
-  Proper (dist n ==> dist n ==> dist n) (@csumC_map A A' B B').
-Proof. by intros f f' Hf g g' Hg []; constructor. Qed.
+Instance csumC_map_ne A A' B B' :
+  NonExpansive2 (@csumC_map A A' B B').
+Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
 
 Section cmra.
 Context {A B : cmraT}.
@@ -189,7 +189,7 @@ Qed.
 Lemma csum_cmra_mixin : CMRAMixin (csum A B).
 Proof.
   split.
-  - intros n []; destruct 1; constructor; by cofe_subst.
+  - intros [] n; destruct 1; constructor; by cofe_subst.
   - intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
       destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.

theories/algebra/excl.v

@@ -32,7 +32,7 @@ Inductive excl_dist : Dist (excl A) :=
   | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
 Existing Instance excl_dist.
 
-Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
+Global Instance Excl_ne : NonExpansive (@Excl A).
 Proof. by constructor. Qed.
 Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
 Proof. by constructor. Qed.
@@ -152,7 +152,7 @@ Instance excl_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
 Instance excl_map_cmra_monotone {A B : ofeT} (f : A → B) :
-  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
+  NonExpansive f → CMRAMonotone (excl_map f).
 Proof.
   split; try apply _.
   - by intros n [a|].
@@ -161,8 +161,8 @@ Proof.
 Qed.
 Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
   CofeMor (excl_map f).
-Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
-Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
+Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).
+Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
 Program Definition exclRF (F : cFunctor) : rFunctor := {|
   rFunctor_car A B := (exclR (cFunctor_car F A B));

theories/algebra/gmap.v

@@ -43,8 +43,8 @@ Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 Global Instance gmapC_leibniz: LeibnizEquiv A → LeibnizEquiv gmapC.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
 
-Global Instance lookup_ne n k :
-  Proper (dist n ==> dist n) (lookup k : gmap K A → option A).
+Global Instance lookup_ne k :
+  NonExpansive (lookup k : gmap K A → option A).
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
@@ -54,19 +54,19 @@ Proof.
   intros ? m m' Hm k'.
   by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
 Qed.
-Global Instance insert_ne i n :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
+Global Instance insert_ne i :
+  NonExpansive2 (insert (M:=gmap K A) i).
 Proof.
-  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
+  intros n x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
 Qed.
-Global Instance singleton_ne i n :
-  Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
-Proof. by intros ???; apply insert_ne. Qed.
-Global Instance delete_ne i n :
-  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
+Global Instance singleton_ne i :
+  NonExpansive (singletonM i : A → gmap K A).
+Proof. by intros ????; apply insert_ne. Qed.
+Global Instance delete_ne i :
+  NonExpansive (delete (M:=gmap K A) i).
 Proof.
-  intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
+  intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
 Qed.
 
@@ -460,10 +460,10 @@ Proof.
 Qed.
 Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
   gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).
-Instance gmapC_map_ne `{Countable K} {A B} n :
-  Proper (dist n ==> dist n) (@gmapC_map K _ _ A B).
+Instance gmapC_map_ne `{Countable K} {A B} :
+  NonExpansive (@gmapC_map K _ _ A B).
 Proof.
-  intros f g Hf m k; rewrite /= !lookup_fmap.
+  intros n f g Hf m k; rewrite /= !lookup_fmap.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 Qed.
 

theories/algebra/iprod.v

@@ -43,10 +43,10 @@ Section iprod_cofe.
   Qed.
 
   (** Properties of iprod_insert. *)
-  Global Instance iprod_insert_ne n x :
-    Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
+  Global Instance iprod_insert_ne x :
+    NonExpansive2 (iprod_insert x).
   Proof.
-    intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
+    intros n y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
     by destruct (decide _) as [[]|].
   Qed.
   Global Instance iprod_insert_proper x :
@@ -188,9 +188,9 @@ Section iprod_singleton.
   Context `{Finite A} {B : A → ucmraT}.
   Implicit Types x : A.
 
-  Global Instance iprod_singleton_ne n x :
-    Proper (dist n ==> dist n) (iprod_singleton x : B x → _).
-  Proof. intros y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
+  Global Instance iprod_singleton_ne x :
+    NonExpansive (iprod_singleton x : B x → _).
+  Proof. intros n y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
   Global Instance iprod_singleton_proper x :
     Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
 
@@ -297,9 +297,9 @@ Qed.
 Definition iprodC_map `{Finite A} {B1 B2 : A → ofeT}
     (f : iprod (λ x, B1 x -n> B2 x)) :
   iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} n :
-  Proper (dist n ==> dist n) (@iprodC_map A _ _ B1 B2).
-Proof. intros f1 f2 Hf g x; apply Hf. Qed.
+Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} :
+  NonExpansive (@iprodC_map A _ _ B1 B2).
+Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
 
 Program Definition iprodCF `{Finite C} (F : C → cFunctor) : cFunctor := {|
   cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);

theories/algebra/list.v

@@ -12,36 +12,36 @@ Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
 Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
 
-Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
-Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
+Global Instance cons_ne : NonExpansive2 (@cons A) := _.
+Global Instance app_ne : NonExpansive2 (@app A) := _.
 Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
-Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
-Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
-Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
-Global Instance list_lookup_ne n i :
-  Proper (dist n ==> dist n) (lookup (M:=list A) i).
-Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Global Instance tail_ne : NonExpansive (@tail A) := _.
+Global Instance take_ne : NonExpansive (@take A n) := _.
+Global Instance drop_ne : NonExpansive (@drop A n) := _.
+Global Instance list_lookup_ne i :
+  NonExpansive (lookup (M:=list A) i).
+Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
 Global Instance list_alter_ne n f i :
   Proper (dist n ==> dist n) f →
   Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
-Global Instance list_insert_ne n i :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
-Global Instance list_inserts_ne n i :
-  Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
-Global Instance list_delete_ne n i :
-  Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
-Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
-Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
+Global Instance list_insert_ne i :
+  NonExpansive2 (insert (M:=list A) i) := _.
+Global Instance list_inserts_ne i :
+  NonExpansive2 (@list_inserts A i) := _.
+Global Instance list_delete_ne i :
+  NonExpansive (delete (M:=list A) i) := _.
+Global Instance option_list_ne : NonExpansive (@option_list A).
+Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
-Global Instance replicate_ne n :
-  Proper (dist n ==> dist n) (@replicate A n) := _.
-Global Instance reverse_ne n : Proper (dist n ==> dist n) (@reverse A) := _.
-Global Instance last_ne n : Proper (dist n ==> dist n) (@last A).
-Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
+Global Instance replicate_ne :
+  NonExpansive (@replicate A n) := _.
+Global Instance reverse_ne : NonExpansive (@reverse A) := _.
+Global Instance last_ne : NonExpansive (@last A).
+Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.
+  NonExpansive2 (@resize A n) := _.
 
 Definition list_ofe_mixin : OfeMixin (list A).
 Proof.
@@ -97,8 +97,8 @@ Instance list_fmap_ne {A B : ofeT} (f : A → B) n:
 Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
   CofeMor (fmap f : listC A → listC B).
-Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
-Proof. intros f g ? l. by apply list_fmap_ext_ne. Qed.
+Instance listC_map_ne A B : NonExpansive (@listC_map A B).
+Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
 
 Program Definition listCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := listC (cFunctor_car F A B);
@@ -293,9 +293,9 @@ Section properties.
 
   Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
   Proof. apply Forall_replicate. Qed.
-  Global Instance list_singletonM_ne n i :
-    Proper (dist n ==> dist n) (@list_singletonM A i).
-  Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
+  Global Instance list_singletonM_ne i :
+    NonExpansive (@list_singletonM A i).
+  Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
   Global Instance list_singletonM_proper i :
     Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
 

theories/algebra/ofe.v

@@ -17,6 +17,8 @@ Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
 Hint Extern 0 (_ ≡{_}≡ _) => reflexivity.
 Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption.
+Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
+Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
 
 Tactic Notation "cofe_subst" ident(x) :=
   repeat match goal with
@@ -87,7 +89,7 @@ Arguments chain_car {_} _ _.
 Arguments chain_cauchy {_} _ _ _ _.
 
 Program Definition chain_map {A B : ofeT} (f : A → B