Merge branch 'ralf/non-expansive' into 'master'

add NonExpansive3, NonExpansive4

See merge request iris/iris!721

iris/algebra/ofe.v

@@ -28,6 +28,10 @@ Global Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
 Global Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
 Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
 Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
+Notation NonExpansive3 f :=
+  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f).
+Notation NonExpansive4 f :=
+  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f).
 
 Tactic Notation "ofe_subst" ident(x) :=
   repeat match goal with
@@ -614,9 +618,9 @@ Proof. apply ne_proper_2; apply _. Qed.
 (* Function space maps *)
 Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
   (h : A -n> B) : A' -n> B' := g ◎ h ◎ f.
-Global Instance ofe_mor_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B').
-Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
+Global Instance ofe_mor_map_ne {A A' B B'} :
+  NonExpansive3 (@ofe_mor_map A A' B B').
+Proof. intros n ??? ??? ???. by repeat apply ccompose_ne. Qed.
 
 Definition ofe_morO_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
   (A -n> B) -n> (A' -n>  B') := OfeMor (ofe_mor_map f g).

tests/algebra.v

@@ -70,27 +70,21 @@ Definition gmap_view_check {K : Type} `{Countable K} {V : ofe} :
   gmap_view K V = gmap_viewO K V := eq_refl.
 
 Lemma uncurry_ne_test {A B C : ofe} (f : A → B → C) :
-  (∀ n, Proper (dist n ==> dist n ==> dist n) f) →
-  NonExpansive (uncurry f).
+  NonExpansive2 f → NonExpansive (uncurry f).
 Proof. apply _. Qed.
 Lemma uncurry3_ne_test {A B C D : ofe} (f : A → B → C → D) :
-  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f) →
-  NonExpansive (uncurry3 f).
+  NonExpansive3 f → NonExpansive (uncurry3 f).
 Proof. apply _. Qed.
 Lemma uncurry4_ne_test {A B C D E : ofe} (f : A → B → C → D → E) :
-  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f) →
-  NonExpansive (uncurry4 f).
+  NonExpansive4 f → NonExpansive (uncurry4 f).
 Proof. apply _. Qed.
 
 Lemma curry_ne_test {A B C : ofe} (f : A * B → C) :
-  NonExpansive f →
-  ∀ n, Proper (dist n ==> dist n ==> dist n) (curry f).
+  NonExpansive f → NonExpansive2 (curry f).
 Proof. apply _. Qed.
 Lemma curry3_ne_test {A B C D : ofe} (f : A * B * C → D) :
-  NonExpansive f →
-  ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) (curry3 f).
+  NonExpansive f → NonExpansive3 (curry3 f).
 Proof. apply _. Qed.
 Lemma curry4_ne_test {A B C D E : ofe} (f : A * B * C * D → E) :
-  NonExpansive f →
-  ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (curry4 f).
+  NonExpansive f → NonExpansive4 (curry4 f).
 Proof. apply _. Qed.