Require Import Utf8 Setoid Classical.

Notation "'∃!' x .. y , p" :=
 (ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
 (at level 0, x binder, y binder).
Notation "'p1'" := (proj1_sig) (at level 0).

Axiom set: Type.
Declare Scope set_scope.
Delimit Scope set_scope with set.
Open Scope set.

Definition set_sig (P: set → Prop) := sig P.
Definition proj1_set {P}: set_sig P → set := @proj1_sig _ _.
Coercion proj1_set: set_sig >-> set.


Axiom In: set → set → Prop.
Notation "x ∈ y" := (In x y) (at level 10): set_scope.
Infix "∉" := (λ x y, ¬ x ∈ y) (at level 10): set_scope.

Axiom empty_set: set_sig (λ X, ∀ x, x ∈ X ↔ False).
Notation "'Ø'" := empty_set: set_scope.
Notation " { } " := empty_set (only parsing): set_scope.

Definition subset X Y := ∀ a, a ∈ X → a ∈ Y.
Infix "⊆" := subset (at level 10): set_scope.

Axiom Extensionality:
    ∀ X Y, (∀ a, a ∈ X ↔ a ∈ Y) ↔ X = Y.
Axiom UnorderedPair:
    ∀ (X Y: set), set_sig (λ Z, ∀ a, a ∈ Z <-> a = X \/ a = Y).

Notation "{ x , y }" := (UnorderedPair x y) (at level 0): set_scope.

Definition singleton (X: set): set_sig (fun Y => ∀ a, a ∈ Y <-> a = X).
Proof.
    pose {X, X}. destruct UnorderedPair. simpl in *. exists x.
    setoid_rewrite i. tauto.
Defined.
Notation "{ x }" := (singleton x): set_scope.
Notation "{{ x }}" := (singleton x) (only parsing): set_scope.

Axiom Subsets:
    ∀ (P: set → Prop) X, set_sig (λ Y, ∀ a, a ∈ Y <-> a ∈ X ∧ P a).

Definition intersection X Y := Subsets (fun x => In x Y) X.
Infix "∩" := intersection (at level 55, right associativity): set_scope.

Definition difference X Y := Subsets (λ x, ~ x ∈ Y) X.
Infix "\" := difference (at level 50, no associativity): set_scope.

Axiom SumSet:
    ∀ X, set_sig (λ Y, ∀ a, a ∈ Y <-> ∃ z, z ∈ X ∧ a ∈ z).

Notation "∪ X" := (SumSet X) (at level 70): set_scope.
Definition union X Y: set_sig (λ Z, ∀ a, a ∈ Z <-> a ∈ X \/ a ∈ Y).
Proof.
    destruct (SumSet (p1 {X, Y})) as [sumset p]. destruct {X, Y} as [pair p0]. simpl in *.
    setoid_rewrite p0 in p. exists sumset. setoid_rewrite p.
    clear p p0. intuition.
    + destruct H. destruct H. destruct H. subst; auto. subst; auto.
    + exists X. auto.
    + exists Y. auto.
Qed.
Infix "∪" := union (at level 60, right associativity): set_scope.
Notation "{ x , y , z , .. , v }" := (union .. (union (UnorderedPair x y) (singleton z) ) .. (singleton v)) (at level 0): set_scope.

Axiom PowerSet:
    ∀ X, set_sig (λ Y, ∀ a, a ∈ Y <-> a ⊆ X).

Axiom Infinity:
    set_sig (λ S, In (p1 Ø) S ∧ ∀ x, In x S → In (p1 {{ x }}) S).

Axiom Replacement:
    ∀ (P: set → set → Prop) (H: ∀ x, ∃! y, (P x y)) X,
    set_sig (λ Y, ∀ b, b ∈ Y <-> ∃ a, a ∈ X ∧ P a b).

Definition disjoint_sets X Y := ¬ ∃ z, z ∈ X ∧ z ∈ Y.

Axiom AxiomOfFoundation:
    ∀ X, X ≠ p1 Ø → set_sig (λ a, a ∈ X ∧ disjoint_sets a X).

Axiom AxiomOfChoice:
    ∀ X, set_sig (λ Y, ∀ a, a ∈ X ∧ a ≠ p1 Ø → (∃! u, (u ∈ a ∧ u ∈ Y))).

Theorem T x y: @eq set ({x, y} ∩ {{x}}) {{x}}.
Proof.
    destruct singleton, UnorderedPair, intersection; simpl in *.
    apply Extensionality. setoid_rewrite i1. setoid_rewrite i.
    setoid_rewrite i0. tauto.
Qed.

Theorem T0 {Px Py} (X: set_sig Px) (Y: set_sig Py) a: a ∈ X -> a ∈ (X ∪ Y).
Proof.
 destruct X, union; simpl in *. pose (i a). intro. setoid_rewrite i0. auto.
Defined.

Theorem T1 (a: set) {Px Py} (X: set_sig Px) (Y: set_sig Py): a ∈ X -> a ∈ Y -> a ∈ (X ∩ Y).
Proof.
 destruct X, Y, intersection; simpl in *. pose (i a). intros. rewrite i0. auto.
Defined.

Theorem T2 {Px Py Pz} (X: set_sig Px) (Y: set_sig Py) (Z: set_sig Pz):
 subset X Y -> subset Y Z -> subset X Z.
Proof. unfold subset. intuition. Qed.

(* Exercises *)

Theorem E1213: ¬ ∃ x, ∀ y, y ∈ x.
Proof.
    intro. destruct H as [S H].
    destruct (Subsets (λ x, ¬ x ∈ x) S).
    pose (i x). pose (H x). intuition.
Qed.

Definition is_singleton A x := ∀ z, z ∈ A ↔ z = x.

Theorem E1214 x: ∃! A, (is_singleton A x).
Proof.
    intros. destruct {{x}}. exists x0. unfold unique, is_singleton. intuition.
    apply (Extensionality x0 x'). intuition.
    + rewrite i in H0. rewrite H. auto.
    + rewrite i. rewrite H in H0. auto.
Qed.

Definition E1214_0 x: ∃! A, (is_singleton A x).
Proof.
    intros. destruct (Subsets (λ p, p = x) (PowerSet x)).
    exists x0. unfold unique, is_singleton in *.
    setoid_rewrite i. intuition.
    + subst. clear i. destruct (PowerSet x). simpl. rewrite i. unfold subset. auto.
    + destruct (PowerSet x). simpl in *. apply Extensionality. intuition.
      - rewrite H. rewrite i in H0. tauto.
      - rewrite i. rewrite H in H0. subst. intuition. rewrite i0. unfold subset. tauto.
Qed.

Fixpoint F n: set :=
match n with
| O => Ø
| S m => PowerSet (F m)
end.

Theorem subset_of_empty_set x: subset x {} <-> x = {}.
Proof.
  unfold subset. destruct empty_set. simpl.
  setoid_rewrite <- Extensionality.
  setoid_rewrite i.
  + intuition; eauto. rewrite H in H0; auto.
Qed.

Theorem element_of_singleton x a: x ∈ {{a}} <-> x = a.
Proof. destruct {{a}}. exact (i x). Qed.

Theorem T3 X Y:
    subset X Y -> ( Y = union X (Y \ X) )%set.
Proof.
 intro. unfold subset in H. apply Extensionality.
 destruct (union X (Y \ X)) as [union H0]. destruct (Y \ X) as [difference H1]. simpl in *.
 setoid_rewrite H0. setoid_rewrite H1. clear union difference H1 H0.
 intuition. destruct (classic (a ∈ X)). auto. auto.
Qed.

Theorem T4 x a b (H: a <> b) S: let X := {a, b} ∪ S in subset X {{x}} -> False.
Proof.
 simpl. destruct union as [union H0]. simpl in *. destruct singleton as [singleton H1]. simpl in *.
 destruct {a, b} as [pair H2]. simpl in *. intro.
 unfold subset in *. setoid_rewrite H2 in H0. clear H2.
 setoid_rewrite H0 in H3. clear H0. setoid_rewrite H1 in H3. clear H1.
 apply H. clear H.
 assert (a = x). apply H3. auto.
 assert (b = x). apply H3. auto.
 congruence.
Qed.

Theorem subset_of_singleton x a: subset x {{a}} <-> x = {} \/ x = {{a}}.
Proof.
  destruct singleton as [singleton H]. simpl. destruct empty_set as [empty H0]. simpl.
  unfold subset. intuition.
  2:{ rewrite H2 in H1. exfalso. eapply H0. eauto. }
  2:{ rewrite <- H2. auto. }
Admitted.