From 6348c6aaf50aed9ee7d97048ef37c5dd585021f0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Jul 2021 17:20:04 +0200
Subject: [PATCH] Swap `curry` and `uncurry` to be consistent with Haskell and
 friends.

This also applies to `(un)curry{3,4}`, `gmap_(un)curry`, and `h(un)curry`.

This fixes issue #76.

The code includes a horrible hack that should removed once support for Coq versions prior
to 8.13 is dropped.
---
 theories/base.v      | 16 +++++++++------
 theories/decidable.v |  6 +++---
 theories/fin_maps.v  | 24 +++++++++++------------
 theories/gmap.v      | 46 ++++++++++++++++++++++----------------------
 theories/hlist.v     | 11 ++++++-----
 theories/list.v      |  6 +++---
 6 files changed, 57 insertions(+), 52 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 31f5a474..f7cf5110 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -671,16 +671,20 @@ Global Instance: Params (@pair) 2 := {}.
 Global Instance: Params (@fst) 2 := {}.
 Global Instance: Params (@snd) 2 := {}.
 
-Notation curry := prod_curry.
-Notation uncurry := prod_uncurry.
-Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
+(** The Coq standard library swapped the names of curry/uncurry, see
+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.
+Notation uncurry := prod_curry.
+
+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.
-Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
+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.
 
-Definition uncurry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
+Definition curry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
   f (a, b, c).
-Definition uncurry4 {A B C D E} (f : A * B * C * D → E)
+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).
 
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
diff --git a/theories/decidable.v b/theories/decidable.v
index 63c7a376..0fa06809 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -206,9 +206,9 @@ Proof. solve_decision. Defined.
 Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
 Proof. solve_decision. Defined.
 
-Global Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
-    Decision (curry P p) :=
-  match p as p return Decision (curry P p) with
+Global Instance uncurry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
+    Decision (uncurry P p) :=
+  match p as p return Decision (uncurry P p) with
   | (x,y) => P_dec x y
   end.
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 1ed4cf3b..920b9426 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -80,7 +80,7 @@ Global Instance map_size `{FinMapToList K A M} : Size M := λ m,
 
 Definition map_to_set `{FinMapToList K A M,
     Singleton B C, Empty C, Union C} (f : K → A → B) (m : M) : C :=
-  list_to_set (curry f <$> map_to_list m).
+  list_to_set (uncurry f <$> map_to_list m).
 Definition set_to_map `{Elements B C, Insert K A M, Empty M}
     (f : B → K * A) (X : C) : M :=
   list_to_map (f <$> elements X).
@@ -131,7 +131,7 @@ Global Instance map_difference `{Merge M} {A} : Difference (M A) :=
 of the elements. Implemented by conversion to lists, so not very efficient. *)
 Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
     ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
-  list_to_map (omap (λ ix, (fst ix ,.) <$> curry f ix) (map_to_list m)).
+  list_to_map (omap (λ ix, (fst ix ,.) <$> uncurry f ix) (map_to_list m)).
 
 (** Given a function [f : K1 → K2], the function [kmap f] turns a maps with
 keys of type [K1] into a map with keys of type [K2]. The function [kmap f]
@@ -152,7 +152,7 @@ Notation map_zip := (map_zip_with pair).
 (* Folds a function [f] over a map. The order in which the function is called
 is unspecified. *)
 Definition map_fold `{FinMapToList K A M} {B}
-  (f : K → A → B → B) (b : B) : M → B := foldr (curry f) b ∘ map_to_list.
+  (f : K → A → B → B) (b : B) : M → B := foldr (uncurry f) b ∘ map_to_list.
 
 Global Instance map_filter
     `{FinMapToList K A M, Insert K A M, Empty M} : Filter (K * A) M :=
@@ -1172,9 +1172,9 @@ Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R}
   R (map_fold f b (<[i:=x]> m)) (f i x (map_fold f b m)).
 Proof.
   intros Hf_proper Hf Hi. unfold map_fold; simpl.
-  assert (∀ kz, Proper (R ==> R) (curry f kz)) by (intros []; apply _).
-  trans (foldr (curry f) b ((i, x) :: map_to_list m)); [|done].
-  eapply (foldr_permutation R (curry f) b), map_to_list_insert; auto.
+  assert (∀ kz, Proper (R ==> R) (uncurry f kz)) by (intros []; apply _).
+  trans (foldr (uncurry f) b ((i, x) :: map_to_list m)); [|done].
+  eapply (foldr_permutation R (uncurry f) b), map_to_list_insert; auto.
   intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
   - intros ->.
     eapply Hj, NoDup_lookup; [apply (NoDup_fst_map_to_list (<[i:=x]> m))| | ].
@@ -1199,7 +1199,7 @@ Lemma map_fold_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b :
 Proof.
   intros Hemp Hinsert.
   cut (∀ l, NoDup l →
-    ∀ m, (∀ i x, m !! i = Some x ↔ (i,x) ∈ l) → P (foldr (curry f) b l) m).
+    ∀ m, (∀ i x, m !! i = Some x ↔ (i,x) ∈ l) → P (foldr (uncurry f) b l) m).
   { intros help ?. apply help; [apply NoDup_map_to_list|].
     intros i x. by rewrite elem_of_map_to_list. }
   induction 1 as [|[i x] l ?? IH]; simpl.
@@ -1399,7 +1399,7 @@ Section map_Forall.
   Context {A} (P : K → A → Prop).
   Implicit Types m : M A.
 
-  Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m).
+  Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (uncurry P) (map_to_list m).
   Proof.
     rewrite Forall_forall. split.
     - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
@@ -1457,7 +1457,7 @@ Section map_Forall.
   Context `{∀ i x, Decision (P i x)}.
   Global Instance map_Forall_dec m : Decision (map_Forall P m).
   Proof.
-    refine (cast_if (decide (Forall (curry P) (map_to_list m))));
+    refine (cast_if (decide (Forall (uncurry P) (map_to_list m))));
       by rewrite map_Forall_to_list.
   Defined.
   Lemma map_not_Forall (m : M A) :
@@ -1687,7 +1687,7 @@ Proof.
 Qed.
 
 Lemma map_zip_with_map_zip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) :
-  map_zip_with f m1 m2 = curry f <$> map_zip m1 m2.
+  map_zip_with f m1 m2 = uncurry f <$> map_zip m1 m2.
 Proof.
   apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with.
   by destruct (m1 !! i), (m2 !! i).
@@ -2640,7 +2640,7 @@ Section setoid.
   Qed.
 
   Global Instance map_filter_proper (P : K * A → Prop) `{!∀ kx, Decision (P kx)} :
-    (∀ k, Proper ((≡) ==> iff) (uncurry P k)) →
+    (∀ k, Proper ((≡) ==> iff) (curry P k)) →
     Proper ((≡@{M A}) ==> (≡)) (filter P).
   Proof.
     intros ? m1 m2 Hm i. rewrite !map_filter_lookup.
@@ -2739,7 +2739,7 @@ Section setoid_inversion.
   Qed.
 
   Lemma map_filter_equiv_eq (P : K * A → Prop) `{!∀ kx, Decision (P kx)} (m1 m2 : M A):
-    (∀ k, Proper ((≡) ==> iff) (uncurry P k)) →
+    (∀ k, Proper ((≡) ==> iff) (curry P k)) →
     m1 ≡ filter P m2 ↔ ∃ m2', m1 = filter P m2' ∧ m2' ≡ m2.
   Proof.
     intros HP. split; [|by intros (?&->&->)].
diff --git a/theories/gmap.v b/theories/gmap.v
index f0f72d2a..bea67cfd 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -144,11 +144,11 @@ Next Obligation.
 Qed.
 
 (** * Curry and uncurry *)
-Definition gmap_curry `{Countable K1, Countable K2} {A} :
+Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
     gmap K1 (gmap K2 A) → gmap (K1 * K2) A :=
   map_fold (λ i1 m' macc,
     map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') ∅.
-Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
+Definition gmap_curry `{Countable K1, Countable K2} {A} :
     gmap (K1 * K2) A → gmap K1 (gmap K2 A) :=
   map_fold (λ '(i1, i2) x,
     partial_alter (Some ∘ <[i2:=x]> ∘ default ∅) i1) ∅.
@@ -158,8 +158,8 @@ Section curry_uncurry.
 
   (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
   a consequence of Coq bug #5735 *)
-  Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
-    gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (.!! j).
+  Lemma lookup_gmap_uncurry (m : gmap K1 (gmap K2 A)) i j :
+    gmap_uncurry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (.!! j).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
     { by rewrite !lookup_empty. }
@@ -175,8 +175,8 @@ Section curry_uncurry.
     - by rewrite !lookup_insert_ne, IH', lookup_insert_ne by congruence.
   Qed.
 
-  Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
-    (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (.!! j) = m !! (i, j).
+  Lemma lookup_gmap_curry (m : gmap (K1 * K2) A) i j :
+    (gmap_curry m !! i : option (gmap K2 A)) ≫= (.!! j) = m !! (i, j).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
     { by rewrite !lookup_empty. }
@@ -188,8 +188,8 @@ Section curry_uncurry.
     - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
   Qed.
 
-  Lemma lookup_gmap_uncurry_None (m : gmap (K1 * K2) A) i :
-    gmap_uncurry m !! i = None ↔ (∀ j, m !! (i, j) = None).
+  Lemma lookup_gmap_curry_None (m : gmap (K1 * K2) A) i :
+    gmap_curry m !! i = None ↔ (∀ j, m !! (i, j) = None).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! i = None ↔ (∀ j, m !! (i, j) = None)));
       [done|].
@@ -201,34 +201,34 @@ Section curry_uncurry.
       intros j. rewrite lookup_insert_ne; [done|congruence].
   Qed.
 
-  Lemma gmap_curry_uncurry (m : gmap (K1 * K2) A) :
-    gmap_curry (gmap_uncurry m) = m.
+  Lemma gmap_uncurry_curry (m : gmap (K1 * K2) A) :
+    gmap_uncurry (gmap_curry m) = m.
   Proof.
-   apply map_eq; intros [i j]. by rewrite lookup_gmap_curry, lookup_gmap_uncurry.
+   apply map_eq; intros [i j]. by rewrite lookup_gmap_uncurry, lookup_gmap_curry.
   Qed.
 
-  Lemma gmap_uncurry_non_empty (m : gmap (K1 * K2) A) i x :
-    gmap_uncurry m !! i = Some x → x ≠ ∅.
+  Lemma gmap_curry_non_empty (m : gmap (K1 * K2) A) i x :
+    gmap_curry m !! i = Some x → x ≠ ∅.
   Proof.
     intros Hm ->. eapply eq_None_not_Some; [|by eexists].
-    eapply lookup_gmap_uncurry_None; intros j.
-    by rewrite <-lookup_gmap_uncurry, Hm.
+    eapply lookup_gmap_curry_None; intros j.
+    by rewrite <-lookup_gmap_curry, Hm.
   Qed.
 
-  Lemma gmap_uncurry_curry_non_empty (m : gmap K1 (gmap K2 A)) :
+  Lemma gmap_curry_uncurry_non_empty (m : gmap K1 (gmap K2 A)) :
     (∀ i x, m !! i = Some x → x ≠ ∅) →
-    gmap_uncurry (gmap_curry m) = m.
+    gmap_curry (gmap_uncurry m) = m.
   Proof.
     intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
-    - destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry.
+    - destruct (gmap_curry (gmap_uncurry m) !! i) as [m2'|] eqn:Hcurry.
       + f_equal. apply map_eq. intros j.
-        trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) ≫= (.!! j)).
+        trans ((gmap_curry (gmap_uncurry m) !! i : option (gmap _ _)) ≫= (.!! j)).
         { by rewrite Hcurry. }
-        by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm.
-      + rewrite lookup_gmap_uncurry_None in Hcurry.
+        by rewrite lookup_gmap_curry, lookup_gmap_uncurry, Hm.
+      + rewrite lookup_gmap_curry_None in Hcurry.
         exfalso; apply (Hne i m2), map_eq; [done|intros j].
-        by rewrite lookup_empty, <-(Hcurry j), lookup_gmap_curry, Hm.
-   - apply lookup_gmap_uncurry_None; intros j. by rewrite lookup_gmap_curry, Hm.
+        by rewrite lookup_empty, <-(Hcurry j), lookup_gmap_uncurry, Hm.
+   - apply lookup_gmap_curry_None; intros j. by rewrite lookup_gmap_uncurry, Hm.
   Qed.
 End curry_uncurry.
 
diff --git a/theories/hlist.v b/theories/hlist.v
index 51dc2a8c..ee3e4511 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -37,21 +37,22 @@ Definition hinit {B} (y : B) : himpl tnil B := y.
 Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
 Global Arguments hlam _ _ _ _ _ / : assert.
 
-Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
+Definition huncurry {As B} (f : himpl As B) (xs : hlist As) : B :=
   (fix go {As} xs :=
     match xs in hlist As return himpl As B → B with
     | hnil => λ f, f
     | hcons x xs => λ f, go xs (f x)
     end) _ xs f.
-Coercion hcurry : himpl >-> Funclass.
+Coercion huncurry : himpl >-> Funclass.
 
-Fixpoint huncurry {As B} : (hlist As → B) → himpl As B :=
+Fixpoint hcurry {As B} : (hlist As → B) → himpl As B :=
   match As with
   | tnil => λ f, f hnil
-  | tcons x xs => λ f, hlam (λ x, huncurry (f ∘ hcons x))
+  | tcons x xs => λ f, hlam (λ x, hcurry (f ∘ hcons x))
   end.
 
-Lemma hcurry_uncurry {As B} (f : hlist As → B) xs : huncurry f xs = f xs.
+Lemma huncurry_curry {As B} (f : hlist As → B) xs :
+  huncurry (hcurry f) xs = f xs.
 Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
 
 Fixpoint hcompose {As B C} (f : B → C) {struct As} : himpl As B → himpl As C :=
diff --git a/theories/list.v b/theories/list.v
index 98c9d5ee..c67c9c47 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2934,7 +2934,7 @@ Proof.
 Qed.
 
 Lemma Forall2_Forall {A} P (l1 l2 : list A) :
-  Forall2 P l1 l2 → Forall (curry P) (zip l1 l2).
+  Forall2 P l1 l2 → Forall (uncurry P) (zip l1 l2).
 Proof. induction 1; constructor; auto. Qed.
 
 Section Forall2.
@@ -4345,9 +4345,9 @@ Section zip_with.
   Lemma fmap_zip_with_r (g : C → B) l k :
     (∀ x y, g (f x y) = y) → length k ≤ length l → g <$> zip_with f l k = k.
   Proof. revert l. induction k; intros [|??] ??; f_equal/=; auto with lia. Qed.
-  Lemma zip_with_zip l k : zip_with f l k = curry f <$> zip l k.
+  Lemma zip_with_zip l k : zip_with f l k = uncurry f <$> zip l k.
   Proof. revert k. by induction l; intros [|??]; f_equal/=. Qed.
-  Lemma zip_with_fst_snd lk : zip_with f (lk.*1) (lk.*2) = curry f <$> lk.
+  Lemma zip_with_fst_snd lk : zip_with f (lk.*1) (lk.*2) = uncurry f <$> lk.
   Proof. by induction lk as [|[]]; f_equal/=. Qed.
   Lemma zip_with_replicate n x y :
     zip_with f (replicate n x) (replicate n y) = replicate n (f x y).
-- 
GitLab