Library curry

(* https://www.youtube.com/watch?v=i2Q5GJhgsjA *)
(* https://www.youtube.com/watch?v=2SjM5f3GkV0 *)
(* http://math.andrej.com/2011/02/22/video-tutorials-for-the-coq-proof-assistant/ *)

Parameters A B C : Set.

(* A function f : A * B -> C is equivalent to a function A -> (B -> C). *)
Definition curry (f : A × B → C) := fun a ⇒ fun b ⇒ f (a, b).
Definition uncurry (g : A → B → C) := fun p ⇒ g (fst p) (snd p).

(* "extensional equality" *)
Theorem Left_Inverse : ∀ f a b, uncurry (curry f) (a, b) = f (a, b).
Proof.
  intros.
  unfold curry, uncurry.
  simpl.
  reflexivity.
Qed.

(* Prove that curry (uncurry g) is extensionally equivalent to g. *)
Theorem Right_Inverse : ∀ g a b, curry (uncurry g) a b = g a b.
Proof.
  intros.
  unfold curry, uncurry.
  simpl.
  reflexivity.
Qed.

(* There exist bijections back and forth. *)
Definition Isomorphic (X Y : Set) :=
  ∃ f : X → Y,
    ∃ g : Y → X,
      (∀ x, g(f(x)) = x ∧ (∀ y, f(g(y)) = y)).

Axiom Extensionality : ∀ (X Y : Set) (f g : X → Y),
  (∀ x, f x = g x) → f = g.

(* When you see your goal is going to fall apart into several cases,
  `split` is usually the proper tactic. *)
Theorem IsoFunSpace : Isomorphic (A × B → C) (A → B → C).
Proof.
  ∃ curry, uncurry.
  split.
  apply Extensionality. intros [a b].
  apply Left_Inverse. intro g.
  apply Extensionality. intro a.
  apply Extensionality. intro b.
  apply Right_Inverse.
Qed.