The file 'curry.v' as Latin-1 text

  1 (* https://www.youtube.com/watch?v=i2Q5GJhgsjA *)
  2 (* https://www.youtube.com/watch?v=2SjM5f3GkV0 *)
  3 (* http://math.andrej.com/2011/02/22/video-tutorials-for-the-coq-proof-assistant/ *)
  4 
  5 Parameters A B C : Set.
  6 
  7 (* A function f : A * B -> C is equivalent to a function A -> (B -> C). *)
  8 Definition curry   (f : A * B -> C) := fun a => fun b => f (a, b).
  9 Definition uncurry (g : A -> B -> C) := fun p => g (fst p) (snd p).
 10 
 11 (* "extensional equality" *)
 12 Theorem Left_Inverse : forall f a b, uncurry (curry f) (a, b) = f (a, b).
 13 Proof.
 14   intros.
 15   unfold curry, uncurry.
 16   simpl.
 17   reflexivity.
 18 Qed.
 19 
 20 (* Prove that curry (uncurry g) is extensionally equivalent to g. *)
 21 Theorem Right_Inverse : forall g a b, curry (uncurry g) a b = g a b.
 22 Proof.
 23   intros.
 24   unfold curry, uncurry.
 25   simpl.
 26   reflexivity.
 27 Qed.
 28 
 29 (* There exist bijections back and forth. *)
 30 Definition Isomorphic (X Y : Set) :=
 31   exists f : X -> Y,
 32     exists g : Y -> X,
 33       (forall x, g(f(x)) = x /\ (forall y, f(g(y)) = y)).
 34 
 35 Axiom Extensionality : forall (X Y : Set) (f g : X -> Y),
 36   (forall x, f x = g x) -> f = g.
 37 
 38 (* When you see your goal is going to fall apart into several cases,
 39   `split` is usually the proper tactic. *)
 40 Theorem IsoFunSpace : Isomorphic (A * B -> C) (A -> B -> C).
 41 Proof.
 42   exists curry, uncurry.
 43   split.
 44   apply Extensionality.  intros [a b].
 45   apply Left_Inverse.  intro g.
 46   apply Extensionality.  intro a.
 47   apply Extensionality.  intro b.
 48   apply Right_Inverse.
 49 Qed.