Merge branch 'ralf/f_equiv_ho' into 'master'

f_equiv: slightly better support for function relations

See merge request iris/stdpp!326

CHANGELOG.md

@@ -162,6 +162,9 @@ API-breaking change is listed.
 - Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
   `Forall2_cons_2` being the original one-directional versions (matching
   `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
+- Enable `f_equiv` (and by extension `solve_proper`) to handle goals of the form
+  `f x ≡ g x` when `f ≡ g` is in scope, where `f` has a type like Iris's `-d>`
+  and `-n>`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

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) :
@@ -30,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}.
 

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.