(* TP4 exercice 1 *)

Parameter Ens: Type.
Parameter someset: Ens.
Parameter elt: Ens -> Ens -> Prop.  (* elt A B se lit A \in B *)

Definition subset (a b:Ens) := (forall (x:Ens), elt x a -> elt x b).

Lemma subset_refl: forall a, subset a a.
intros a x H; assumption.
Qed.

Lemma subset_trans: forall a b c, subset a b -> subset b c -> subset a c.
intros a b c H1 H2 x H.
apply H2.
now apply H1.
Qed.

Lemma extensionality_reciprocal: forall (a b:Ens),
  a = b -> (forall x, elt x a <-> elt x b).
intros a b H x.
rewrite H.
now split.
Qed.

Lemma elt_antisym_implies_extensionality:
   (forall a b, subset a b -> subset b a -> a=b) -> 
    (forall (a b:Ens), (forall x, elt x a <-> elt x b) -> a = b).
intros H a b H1.
apply H.
intros x Hx.
destruct (H1 x).
now apply H0.
intros x Hx.
destruct (H1 x).
now apply H2.
Qed.

Axiom extensionality : forall (a b:Ens), (forall x, elt x a <-> elt x b) -> a = b.

Lemma elt_antisym: forall a b, subset a b -> subset b a -> a=b.
intros a b H1 H2.
apply extensionality.
intros x; split; intros H.
now apply H1.
now apply H2.
Qed.

(* TP4 exercice 2 *)

Parameter pair: Ens -> Ens -> Ens.
Axiom pair_axiom: forall a b x:Ens, elt x (pair a b) <-> x=a \/ x = b.

Goal forall a a' b b', a=a' -> b=b' -> pair a b = pair a' b'.
intros.
apply extensionality.
intros x.
apply iff_trans with (1:=pair_axiom _ _ _).
apply iff_sym.
apply iff_trans with (1:=pair_axiom _ _ _).
split; intros H1; case H1; intros H2.
left; apply trans_eq with (1:=H2); apply sym_eq; exact H.
right; apply trans_eq with (1:=H2); apply sym_eq; exact H0.
left; apply trans_eq with (1:=H2); exact H.
right; apply trans_eq with (1:=H2); exact H0.
Qed.

Lemma pair_implies: forall a b c d, pair a b = pair c d -> (a=c/\ b=d) \/ (a=d /\ b=c).
intros a b c d H.
assert (c=a \/ c=b).
  apply -> pair_axiom.
  rewrite H.
  apply <- pair_axiom.
  now left.
assert (d=a \/ d=b).
  apply -> pair_axiom.
  rewrite H.
  apply <- pair_axiom.
  now right.
assert (a=c \/ a=d).
  apply -> pair_axiom.
  rewrite <- H.
  apply <- pair_axiom.
  now left.
assert (b=c \/ b=d).
  apply -> pair_axiom.
  rewrite <- H.
  apply <- pair_axiom.
  now right.
destruct H0; rewrite H0 in * |- *.
(* . *)
destruct H1; rewrite H1 in * |- *.
left; split.
reflexivity.
now destruct H3.
left; split; reflexivity.
(* . *)
destruct H1; rewrite H1 in * |- *.
right; split; reflexivity.
left; split.
now destruct H2.
reflexivity.
Qed.

Definition single (a:Ens) := pair a a.

Lemma single_is: forall a x, elt x (single a) <-> x=a.
intros a x.
apply iff_trans with (1:=pair_axiom _ _ _).
split; intros.
now case H.
now left.
Qed.


Definition couple (a b:Ens) := pair (single a) (pair a b).

Lemma single_pair: forall a b c, single a = pair b c -> a=b /\ a = c.
intros a b c H.
case pair_implies with (1:=H); intros (H1,H2).
split; assumption.
split; assumption.
Qed.


Goal forall a b c d, couple a b = couple c d <-> a=c /\ b=d.
intros; unfold couple.
split; intros H.
(* . *)
case pair_implies with (1:=H); intros (H1,H2).
(* . . *)
assert (a=c).
case pair_implies with (1:=H1); intros (H3,_); assumption.
case pair_implies with (1:=H2); intros (H5,H4).
split; assumption.
split; try assumption.
rewrite H4; rewrite <- H5; apply sym_eq; assumption.
(* . . *)
destruct (single_pair a c d); try assumption.
destruct (single_pair c a b).
now apply sym_eq.
split; try assumption.
rewrite <- H5; now rewrite <- H0.
(* . *)
destruct H.
rewrite H; now rewrite H0.
Qed.


(* TP4 exercice 3 *)

Parameter separ : Ens -> (Ens->Prop) -> Ens.
Axiom separ_axiom: forall (P:Ens -> Prop),
    forall (a x :Ens), elt x (separ a P) <-> elt x a /\ P x.

Definition emptyset := separ someset (fun x:Ens=> False).

Lemma emptyset_false: forall x:Ens, elt x emptyset -> False.
unfold emptyset; intros x H.
assert (elt x someset /\ False).
destruct (separ_axiom (fun x:Ens=> False) someset x).
now apply H0.
now destruct H0.
Qed.

Goal forall x, (forall y, elt y x -> False) -> x = emptyset.
intros.
apply extensionality.
intros.
split; intros.
absurd (elt x0 x); try assumption.
intro; now apply H with x0.
absurd (elt x0 emptyset); try assumption.
intro; now apply emptyset_false with x0.
Qed.

Goal (exists x, forall y, elt y x) -> False.
intros (x,H).
pose (russell_ens := separ x (fun t => ~(elt t t))).
destruct (separ_axiom (fun y : Ens => ~ elt y y) x russell_ens).
fold russell_ens in H0, H1.
assert (~(elt russell_ens russell_ens)).
intro.
destruct H0; try assumption.
apply H3; assumption.
apply H2.
apply H1.
split; try assumption.
apply H.
Qed.

(* TP4 exercice 4 *)

Parameter union: Ens -> Ens.

Axiom union_axiom: forall (a x : Ens), elt x (union a) <-> exists y, elt y a /\ elt x y.

Definition cup (a b:Ens) := union (pair a b).

Lemma cup_elt: forall (a b x:Ens), elt x (cup a b) <-> elt x a \/ elt x b.
intros a b x.
unfold cup.
apply iff_trans with (B:=exists y, elt y (pair a b) /\ elt x y).
apply union_axiom.
split.
intros (y,(H1,H2)).
destruct (pair_axiom a b y).
case H; try assumption.
intros Y; rewrite <- Y; now left.
intros Y; rewrite <- Y; now right.
intros H; case H; intros H1;[exists a|exists b]; split; try assumption.
apply <- pair_axiom; now left.
apply <- pair_axiom; now right.
Qed.


(* TP4 exercice 5 *)

Parameter power: Ens -> Ens.
Axiom power_axiom: forall (a x : Ens), elt x (power a) <-> subset x a.

Goal forall a, elt emptyset (power a).
intros.
apply <- power_axiom.
intros x H.
absurd (elt x emptyset); try assumption.
intro; now apply emptyset_false with x.
Qed.


Lemma power_a: forall a, elt a (power a).
intros.
apply <- power_axiom.
intros x H; assumption.
Qed.


Goal forall a, union (power a) = a.
intros a.
apply extensionality.
intros x.
apply iff_trans with (1:=union_axiom _ _).
split.
intros (y,(H1,H2)).
assert (subset y a).
apply -> power_axiom; assumption.
now apply H.
intros H; exists a; split; trivial.
apply power_a.
Qed.


Goal forall (a:Ens), (exists x:Ens, ~ elt x a).
intros.
exists (power (union a)).
intro.
assert (Hu : subset (power (union a)) (union a)).
intros x H1.
apply <- union_axiom.
exists (power (union a)); split; trivial.
pose (r := separ (union a) (fun x => ~ elt x x)).
assert (forall x,  elt x r <-> elt x (union a) /\ ~ elt x x).
intros x; unfold r.
apply separ_axiom with (P:=(fun x => ~ elt x x)).
destruct (H0 r).
assert (~ elt r r).
intro.
absurd (elt r r); try assumption.
now apply H1.
apply H3.
apply H2.
split; try assumption.
apply Hu.
apply (power_axiom (union a) r).
intros x Hx.
now apply -> H0.
Qed.

(* TP4 exercice 6 *)

Definition zero := emptyset.
Definition succ (x:Ens) := cup x (single x).

Goal forall x, succ x <> zero.
intros; unfold zero, succ; intro.
apply emptyset_false with x.
rewrite <- H.
apply <- cup_elt.
right.
now apply <- single_is.
Qed.

Parameter big:Ens.
Axiom big_axiom: elt zero big /\ forall x, elt x big -> elt (succ x) big.

Definition Nat (x : Ens) :=
  forall a, elt zero a -> (forall y, elt y a -> elt (succ y) a) -> elt x a.

Definition N := separ big Nat.

Lemma N_zero: elt zero N.
destruct (separ_axiom Nat big zero) as [h1 h2]; apply h2; split.
destruct big_axiom as [h3 h4]; assumption.
unfold Nat in |- *; intros; assumption.
Qed.


Lemma N_succ: forall x, elt x N -> elt (succ x) N.
Proof.
unfold N in |- *; intros x h.
destruct (separ_axiom Nat big x) as [h1 h2].
destruct (separ_axiom Nat big (succ x)) as [h3 h4].
apply h4; split.
 destruct big_axiom as [h6 h7]; apply h7; destruct (h1 h); assumption.
unfold Nat in |- *; intros h5 h6 h7; apply h7; destruct (h1 h) as [h8 h9]; apply h9; assumption.
Qed.


Lemma N_rec :
  forall P : Ens -> Prop,
    P zero -> (forall x, elt x N -> P x -> P (succ x)) ->
      forall x, elt x N -> P x.
Proof.
intros; destruct (separ_axiom Nat big x).
destruct (H2 H1); assert (elt x (separ N P)).
 apply H5.
  destruct (separ_axiom P N zero).
  apply H7; split; [ exact N_zero | assumption ].
 intros; destruct (separ_axiom P N y).
 destruct (separ_axiom P N (succ y)); apply H10; split.
   apply N_succ; destruct (H7 H6); assumption.
   apply H0; destruct (H7 H6); assumption.
 destruct (separ_axiom P N x); destruct (H7 H6); assumption.
Qed.