From 57845bb37eda5e2bcb94c198c007ef3b75e818a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 24 Jul 2021 10:32:50 +0200
Subject: [PATCH] Add lemmas that say that `curry{3,4}?` and `uncurry{3,4}?`
 are inverses.

---
 theories/base.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index ebd343af..ad373c01 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -705,6 +705,24 @@ Global Instance prod_inhabited {A B} (iA : Inhabited A)
     (iB : Inhabited B) : Inhabited (A * B) :=
   match iA, iB with populate x, populate y => populate (x,y) end.
 
+(** Note that we need eta for products for the [uncurry_curry] lemmas to hold
+in non-applied form ([uncurry (curry f) = f]). *)
+Lemma curry_uncurry {A B C} (f : A → B → C) : curry (uncurry f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry_curry {A B C} (f : A * B → C) p : uncurry (curry f) p = f p.
+Proof. destruct p; reflexivity. Qed.
+Lemma curry3_uncurry3 {A B C D} (f : A → B → C → D) : curry3 (uncurry3 f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry3_curry3 {A B C D} (f : A * B * C → D) p :
+  uncurry3 (curry3 f) p = f p.
+Proof. destruct p as [[??] ?]; reflexivity. Qed.
+Lemma curry4_uncurry4 {A B C D E} (f : A → B → C → D → E) :
+  curry4 (uncurry4 f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry4_curry4 {A B C D E} (f : A * B * C * D → E) p :
+  uncurry4 (curry4 f) p = f p.
+Proof. destruct p as [[[??] ?] ?]; reflexivity. Qed.
+
 Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
 Proof. injection 1; auto. Qed.
 Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
-- 
GitLab