Commit 6348c6aa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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.
parent 7d502178
......@@ -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' :=
......
......@@ -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.
......
......@@ -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 (?&->&->)].
......
......@@ -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.
......
......@@ -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 :=
......
......@@ -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).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment