add some test cases by Robbert

tests/proper.v

@@ -42,6 +42,41 @@ Global Instance from_option_proper_test2 `{Equiv A} {B} (R : relation B) (f : A
   Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
 Proof. solve_proper. Qed.
 
+(** The following tests are inspired by Iris's [ofe] structure (here, simplified
+to just a type an arbitrary relation), and the discrete function space [A -d> B]
+on a Type [A] and OFE [B]. The tests occur when proving [Proper]s for
+higher-order functions, which typically occurs while defining functions using
+Iris's [fixpoint] operator. *)
+Record setoid :=
+  Setoid { setoid_car :> Type; setoid_equiv : relation setoid_car }.
+Arguments setoid_equiv {_} _ _.
+
+Definition myfun (A : Type) (B : setoid) := A → B.
+Definition myfun_equiv {A B} : relation (myfun A B) :=
+  pointwise_relation _ setoid_equiv.
+Definition myfunS (A : Type) (B : setoid) := Setoid (myfun A B) myfun_equiv.
+
+Section setoid_tests.
+  Context {A : setoid} (f : A → A) (h : A → A → A).
+  Context `{!Proper (setoid_equiv ==> setoid_equiv) f,
+            !Proper (setoid_equiv ==> setoid_equiv ==> setoid_equiv) h}.
+
+  Definition setoid_test1 (rec : myfunS nat A) : myfunS nat A :=
+    λ n, h (f (rec n)) (rec n).
+  Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test1.
+  Proof. solve_proper. Qed.
+
+  Definition setoid_test2 (rec : myfunS nat (myfunS nat A)) : myfunS nat A :=
+    λ n, h (f (rec n n)) (rec n n).
+  Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test2.
+  Proof. solve_proper. Qed.
+
+  Definition setoid_test3 (rec : myfunS nat A) : myfunS nat (myfunS nat A) :=
+    λ n m, h (f (rec n)) (rec m).
+  Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test3.
+  Proof. solve_proper. Qed.
+End setoid_tests.
+
 Section map_tests.
   Context `{FinMap K M} `{Equiv A}.