From 5d66333ca9544f71d2b59cd6901e8dd8cb493287 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 16:12:09 +0200
Subject: [PATCH] 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     | 20 ++++++++++++++------
 program_logic/boxes.v |  2 +-
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index a9c3458e6..fabd259de 100644
--- a/prelude/tactics.v
+++ b/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? *)
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 8999eda05..b3532b64a 100644
--- a/program_logic/boxes.v
+++ b/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 γ).
-- 
GitLab