The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

I have translated in coq the French Wikipedia page  théorème de Cantor .
Most of the proof is written in the mathematical proof language, with exception of the tactics unfold and constructor.
Can you help me to write the proof completely in the mathematical proof language ?

Require Import Coq.Sets.Image.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Powerset.

Section Cantor.
Variable U : Type.

Definition surjective (U:Type)(V:Type)
(A : Ensemble U)(B : Ensemble V)
(f: U -> V):=
forall x: V, In V B x -> exists y:U  ,In U A y /\  f(y)=x.


(* there is no surjective function from
(A : Ensemble U) in (Power_set U A) *)
Theorem Cantor : forall (A : Ensemble U),
~ (exists (f : U -> Ensemble U),
(surjective U (Ensemble U) A (Power_set U A) f)).

proof.
assume A : (Ensemble U) and H :(exists (f : U -> Ensemble U),
(surjective U (Ensemble U) A (Power_set U A) f)).
consider f:(U -> Ensemble U)
such that fsurj :(surjective U (Ensemble U) A (Power_set U A) f) from H.
(* Proof coming from Wikipédia : Théorème_de_Cantor *)

(* Let D the set of x in A such that x is not in f x*)
define  D  as (fun x:U => In U A x /\ ~(In U (f x) x)).

(* D is in (Power_set U A) *)
claim SousEns : (In (Ensemble U) (Power_set U A) D).
unfold In.
constructor.
thus thesis .
end claim.

(* Because f is surjective, there exists y in A such that f(y) = D.*)
unfold surjective in fsurj.

then H1: (In (Ensemble U)(Power_set U A) D -> exists y : U, In U A y /\
f y = D) by (fsurj D).

then H2 : (exists y : U, In U A y /\ f y = D) by H1,SousEns.
consider y such that H3:(In U A y /\ f y = D) from H2.
then H4 : (f y = D).

(* Either y is in D or is not in D.
In the first case, y is not in D, in the second, y is in D : then False *)

then H5 : ((In U D y)\/ ~(In U D y)) by (classic (In U D y)).
per cases on H5.
suppose H6:(In U D y).
then H7 : (~(In U (f y) y)) by H6.
then H8 : (~(In U D y)) by H7,H4.
thus thesis by H6, H8.
suppose H6:(~(In U D y)).
then H7 : (~(In U (f y) y)) by H6, H4.
then H8 : (In U D y) by H3,H7.
thus thesis by H6,H8.
end cases.

end proof.

Qed.

End Cantor.

-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy