From 84a6c1562bd6f039ca92a86bbe9676dcddbea76b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 26 Sep 2021 16:12:55 -0400
Subject: [PATCH] f_equiv: slightly better support for function relations

---
 tests/proper.v     | 12 ++++++++++++
 theories/tactics.v |  8 ++++----
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/tests/proper.v b/tests/proper.v
index 58f68d1e..2d7b8119 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -21,6 +21,18 @@ Section tests.
     baz (bar (f 0)) (f 2).
   Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3.
   Proof. solve_proper. Qed.
+
+  (* We mirror [discrete_fun] from Iris to have an equivalence on a function
+  space. *)
+  Definition discrete_fun {A} (B : A → Type) `{!∀ x, Equiv (B x)} := ∀ x : A, B x.
+  Local Instance discrete_fun_equiv  {A} {B : A → Type} `{!∀ x, Equiv (B x)} :
+      Equiv (discrete_fun B) :=
+    λ f g, ∀ x, f x ≡ g x.
+  Notation "A -d> B" :=
+    (@discrete_fun A (λ _, B) _) (at level 99, B at level 200, right associativity).
+  Definition test4 x (f : A -d> A) := f x.
+  Goal ∀ x, Proper ((≡) ==> (≡)) (test4 x).
+  Proof. solve_proper. Qed.
 End tests.
 
 Global Instance from_option_proper_test1 `{Equiv A} {B} (R : relation B) (f : A → B) :
diff --git a/theories/tactics.v b/theories/tactics.v
index 78dbd978..62f8ff4a 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -406,12 +406,12 @@ Ltac f_equiv :=
   | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
   | |- ?R (?f _ _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> _ ==> R) f)
   (* In case the function symbol differs, but the arguments are the same,
-     maybe we have a pointwise_relation in our context. *)
+     maybe we have a relation about those functions in our context. *)
   (* TODO: If only some of the arguments are the same, we could also
-     query for "pointwise_relation"'s. But that leads to a combinatorial
+     query for such relations. But that leads to a combinatorial
      explosion about which arguments are and which are not the same. *)
-  | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
-  | H : pointwise_relation _ (pointwise_relation _ ?R) ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => simple apply H
+  | H : _ ?f ?g |- ?R (?f ?x) (?g ?x) => solve [simple apply H]
+  | H : _ ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => solve [simple apply H]
   end;
   try simple apply reflexivity.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
-- 
GitLab