Merge branch 'robbert/params' into 'master'

`Params` and `Proper` instances for `curry` and friends

See merge request iris/stdpp!302

CHANGELOG.md

@@ -113,9 +113,12 @@ API-breaking change is listed.
   for Coq's `evar` tactic).
 - Make `solve_ndisj` able to solve more goals of the form `_ ⊆ ⊤ ∖ _`,
   `_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`.
-- Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
-  `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
-  Haskell and friends.
+- Improvements to curry:
+  + Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
+    `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
+    Haskell and friends.
+  + Add `Params` and `Proper` instances for `curry`/`uncurry`,
+    `curry3`/`uncurry3`, and `curry4`/`uncurry4`.
 - Rename `map_union_subseteq_l_alt` → `map_union_subseteq_l'` and
   `map_union_subseteq_r_alt` → `map_union_subseteq_r'` to be consistent with
   `or_intro_{l,r}'`.

tests/proper.v

-From stdpp Require Import prelude fin_maps.
+From stdpp Require Import prelude fin_maps propset.
 
 (** Some tests for solve_proper. *)
 Section tests.
@@ -69,3 +69,7 @@ Section map_tests.
     Proper ((≡) ==> (≡@{M _})) (omap f).
   Proof. solve_proper. Qed.
 End map_tests.
+
+Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
+  X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
+Proof. intros H1 H2. by rewrite H1, <-H2. Qed.

theories/base.v

@@ -675,17 +675,23 @@ Global Instance: Params (@snd) 2 := {}.
 https://github.com/coq/coq/pull/12716/ 
 FIXME: Remove this workaround once the lowest Coq version we support is 8.13. *)
 Notation curry := prod_uncurry.
+Global Instance: Params (@curry) 3 := {}.
 Notation uncurry := prod_curry.
+Global Instance: Params (@uncurry) 3 := {}.
 
 Definition uncurry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
   let '(a,b,c) := p in f a b c.
+Global Instance: Params (@uncurry3) 4 := {}.
 Definition uncurry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
   let '(a,b,c,d) := p in f a b c d.
+Global Instance: Params (@uncurry4) 5 := {}.
 
 Definition curry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
   f (a, b, c).
+Global Instance: Params (@curry3) 4 := {}.
 Definition curry4 {A B C D E} (f : A * B * C * D → E)
   (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).
+Global Instance: Params (@curry4) 5 := {}.
 
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
   (f (p.1), g (p.2)).
@@ -710,37 +716,95 @@ Qed.
 
 Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
   relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2).
+
 Section prod_relation.
-  Context `{R1 : relation A, R2 : relation B}.
+  Context `{RA : relation A, RB : relation B}.
   Global Instance prod_relation_refl :
-    Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
+    Reflexive RA → Reflexive RB → Reflexive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_sym :
-    Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
+    Symmetric RA → Symmetric RB → Symmetric (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_trans :
-    Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
+    Transitive RA → Transitive RB → Transitive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_equiv :
-    Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
+    Equivalence RA → Equivalence RB → Equivalence (prod_relation RA RB).
   Proof. split; apply _. Qed.
 
-  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
+  Global Instance pair_proper' : Proper (RA ==> RB ==> prod_relation RA RB) pair.
   Proof. firstorder eauto. Qed.
-  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
+  Global Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair.
   Proof. inversion_clear 1; eauto. Qed.
-  Global Instance fst_proper' : Proper (prod_relation R1 R2 ==> R1) fst.
+  Global Instance fst_proper' : Proper (prod_relation RA RB ==> RA) fst.
+  Proof. firstorder eauto. Qed.
+  Global Instance snd_proper' : Proper (prod_relation RA RB ==> RB) snd.
+  Proof. firstorder eauto. Qed.
+
+  Global Instance curry_proper' `{RC : relation C} :
+    Proper ((prod_relation RA RB ==> RC) ==> RA ==> RB ==> RC) curry.
   Proof. firstorder eauto. Qed.
-  Global Instance snd_proper' : Proper (prod_relation R1 R2 ==> R2) snd.
+  Global Instance uncurry_proper' `{RC : relation C} :
+    Proper ((RA ==> RB ==> RC) ==> prod_relation RA RB ==> RC) uncurry.
+  Proof. intros f1 f2 Hf [x1 y1] [x2 y2] []; apply Hf; assumption. Qed.
+
+  Global Instance curry3_proper' `{RC : relation C, RD : relation D} :
+    Proper ((prod_relation (prod_relation RA RB) RC ==> RD) ==>
+            RA ==> RB ==> RC ==> RD) curry3.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry3_proper' `{RC : relation C, RD : relation D} :
+    Proper ((RA ==> RB ==> RC ==> RD) ==>
+            prod_relation (prod_relation RA RB) RC ==> RD) uncurry3.
+  Proof. intros f1 f2 Hf [[??] ?] [[??] ?] [[??] ?]; apply Hf; assumption. Qed.
+
+  Global Instance curry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
+    Proper ((prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) ==>
+            RA ==> RB ==> RC ==> RD ==> RE) curry4.
   Proof. firstorder eauto. Qed.
+  Global Instance uncurry5_proper' `{RC : relation C, RD : relation D, RE : relation E} :
+    Proper ((RA ==> RB ==> RC ==> RD ==> RE) ==>
+            prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) uncurry4.
+  Proof.
+    intros f1 f2 Hf [[[??] ?] ?] [[[??] ?] ?] [[[??] ?] ?]; apply Hf; assumption.
+  Qed.
 End prod_relation.
 
-Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
-Global Instance pair_proper `{Equiv A, Equiv B} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _.
-Global Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
-Global Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
-Global Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
+Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) :=
+  prod_relation (≡) (≡).
+
+(** Below we make [prod_equiv] type class opaque, so we first lift all
+instances *)
+Section prod_setoid.
+  Context `{Equiv A, Equiv B}.
+
+  Global Instance prod_equivalence :
+    Equivalence (≡@{A}) → Equivalence (≡@{B}) → Equivalence (≡@{A * B}) := _.
+
+  Global Instance pair_proper : Proper ((≡) ==> (≡) ==> (≡@{A*B})) pair := _.
+  Global Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair := _.
+  Global Instance fst_proper : Proper ((≡@{A*B}) ==> (≡)) fst := _.
+  Global Instance snd_proper : Proper ((≡@{A*B}) ==> (≡)) snd := _.
+
+  Global Instance curry_proper `{Equiv C} :
+    Proper (((≡@{A*B}) ==> (≡@{C})) ==> (≡) ==> (≡) ==> (≡)) curry := _.
+  Global Instance uncurry_proper `{Equiv C} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{A*B}) ==> (≡@{C})) uncurry := _.
+
+  Global Instance curry3_proper `{Equiv C, Equiv D} :
+    Proper (((≡@{A*B*C}) ==> (≡@{D})) ==>
+            (≡) ==> (≡) ==> (≡) ==> (≡)) curry3 := _.
+  Global Instance uncurry3_proper `{Equiv C, Equiv D} :
+    Proper (((≡) ==> (≡) ==> (≡) ==> (≡)) ==>
+            (≡@{A*B*C}) ==> (≡@{D})) uncurry3 := _.
+
+  Global Instance curry4_proper `{Equiv C, Equiv D, Equiv E} :
+    Proper (((≡@{A*B*C*D}) ==> (≡@{E})) ==>
+            (≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) curry4 := _.
+  Global Instance uncurry4_proper `{Equiv C, Equiv D, Equiv E} :
+    Proper (((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) ==>
+            (≡@{A*B*C*D}) ==> (≡@{E})) uncurry4 := _.
+End prod_setoid.
+
 Typeclasses Opaque prod_equiv.
 
 Global Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} :