Make f_equiv slightly more robust.

Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.

prelude/tactics.v

@@ -251,8 +251,10 @@ Ltac setoid_subst :=
   end.
 
 (** f_equiv works on goals of the form "f _ = f _", for any relation and any
-    number of arguments. It looks for an appropriate "Proper" instance, and
-    applies it. *)
+number of arguments. It looks for an appropriate "Proper" instance, and applies
+it. The tactic is somewhat limited, since it cannot be used to backtrack on
+the Proper instances that has been found. To that end, we try to ensure the
+trivial instance in which the resulting goals have an [eq]. *)
 Ltac f_equiv :=
   match goal with
   | _ => reflexivity
@@ -263,10 +265,16 @@ Ltac f_equiv :=
   | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
     destruct x
   (* First assume that the arguments need the same relation as the result *)
-  | |- ?R (?f ?x) (?f _) =>
-    apply (_ : Proper (R ==> R) f)
-  | |- ?R (?f ?x ?y) (?f _ _) =>
-    apply (_ : Proper (R ==> R ==> R) f)
+  | |- ?R (?f ?x) (?f _) => apply (_ : Proper (R ==> R) f)
+  (* For the case in which R is polymorphic, or an operational type class,
+  like equiv. *)
+  | |- (?R _) (?f ?x) (?f _) => apply (_ : Proper (R _ ==> _) f)
+  | |- (?R _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ ==> _) f)
+  | |- (?R _ _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ _ ==> _) f)
+  | |- (?R _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ ==> R _ ==> _) f)
+  | |- (?R _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
+  | |- (?R _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
+  | |- (?R _ _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ _ ==> R _ _ _ _ ==> _) f)
   (* Next, try to infer the relation. Unfortunately, there is an instance
      of Proper for (eq ==> _), which will always be matched. *)
   (* TODO: Can we exclude that instance? *)

program_logic/boxes.v

@@ -45,7 +45,7 @@ Implicit Types P Q : iProp.
 
 (* FIXME: solve_proper picks the eq ==> instance for Next. *)
 Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
-Proof. intros P P' HP. by rewrite /box_own_prop HP. Qed.
+Proof. solve_proper. Qed.
 Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_inv γ).
 Proof. solve_proper. Qed.
 Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ).