(*|
冪
==
|*)

Require Import preorder.
From Stdlib Require Import Logic.FunctionalExtensionality.
From Stdlib Require Import Logic.PropExtensionality.

Definition power (A : Type) : Type :=
  A -> Prop.

Definition mem {A : Type} (a : A) (S : power A) : Prop :=
  S a.

Notation "a ∈ S" := (mem a S) (at level 70).

Section Sets.
  Context {A : Type}.

  Definition whole_set : power A :=
    fun _ => True.

  Definition empty_set : power A :=
    fun _ => False.

  Definition singleton (a : A) : power A :=
    fun x => x = a.

  Definition bin_inter (S : power A) (T : power A) : power A :=
    fun x => x ∈ S /\ x ∈ T.

  Definition union (X : power (power A)) : power A :=
    fun x => exists S, S ∈ X /\ x ∈ S.

  Definition inclusion (S : power A) (T : power A) : Prop :=
    forall x, x ∈ S -> x ∈ T.

  Definition complement (S : power A) : power A :=
    fun x => ~ (x ∈ S).

  Definition overlap (S : power A) (T : power A) : Prop :=
    exists x, x ∈ S /\ x ∈ T.

  Definition disjoint (S : power A) (T : power A) : Prop :=
    forall x,
    x ∈ S ->
    x ∈ T ->
    False.
End Sets.

Notation "S ∩ T" := (bin_inter S T) (at level 50).
Notation "⋃ S" := (union S) (at level 50).

Notation "S ⊆ T" := (inclusion S T) (at level 60).

Notation "S ≬ T" := (overlap S T) (at level 60).

Section SetProperties.
  Context {A : Type}.

  Lemma empty_set_has_no_element :
    forall x : A,
    x ∈ empty_set ->
    False.
  Proof.
    intros.
    unfold mem in H.
    unfold empty_set in H.
    exact H.
  Qed.

  Lemma empty_set_subset :
    forall (S : power A),
    empty_set ⊆ S.
  Proof.
    intros.
    unfold inclusion.
    intros.
    contradict H.
  Qed.

  Lemma inclusion_antisymmetric :
    forall {S T : power A},
    S ⊆ T ->
    T ⊆ S ->
    S = T.
  Proof.
    intros.
    extensionality x.
    apply propositional_extensionality.
    split.
    -
      intro.
      apply H.
      assumption.
    -
      intro.
      apply H0.
      assumption.
  Qed.

  Lemma subset_of_empty_set :
    forall {S : power A},
    S ⊆ empty_set ->
    S = empty_set.
  Proof.
    intros.
    apply inclusion_antisymmetric.
    -
      assumption.
    -
      apply empty_set_subset.
  Qed.

  Lemma inclusion_refl :
    forall {S : power A},
    S ⊆ S.
  Proof.
    intros.
    unfold inclusion.
    intros.
    assumption.
  Qed.

  Lemma inclusion_trans :
    forall {S T U : power A},
    S ⊆ T ->
    T ⊆ U ->
    S ⊆ U.
  Proof.
    intros.
    unfold inclusion.
    intros.
    apply H0.
    apply H.
    assumption.
  Qed.

  Lemma inclusion_is_preorder :
    is_preorder (power A) inclusion.
  Proof.
    constructor.
    -
      exact @inclusion_refl.
    -
      exact @inclusion_trans.
  Qed.

  Lemma whole_set_contains_everything :
    forall x : A,
    x ∈ whole_set.
  Proof.
    intros.
    unfold whole_set, mem.
    trivial.
  Qed.

  Lemma bin_inter_subset :
    forall {S T U : power A},
    S ⊆ U ->
    T ⊆ U ->
    S ∩ T ⊆ U.
  Proof.
    intros.
    unfold inclusion.
    intros.
    destruct H1.
    apply H0.
    assumption.
  Qed.

  Lemma bin_inter_sym :
    forall {S T : power A},
    S ∩ T = T ∩ S.
  Proof.
    intros.
    extensionality x.
    unfold bin_inter.
    apply propositional_extensionality.
    split.
    -
      intro.
      destruct H.
      refine (conj H0 H).
    -
      intro.
      destruct H.
      refine (conj H0 H).
  Qed.

  Lemma bin_inter_subset_left :
    forall {S T : power A},
    S ∩ T ⊆ S.
  Proof.
    intros.
    unfold inclusion.
    intros.
    destruct H.
    assumption.
  Qed.

  Lemma bin_inter_empty_set_left :
    forall {S : power A},
    empty_set ∩ S = empty_set.
  Proof.
    intros.
    apply inclusion_antisymmetric.
    -
      apply bin_inter_subset_left.
    -
      apply empty_set_subset.
  Qed.

  Lemma bin_inter_empty_set_right :
    forall {S : power A},
    S ∩ empty_set = empty_set.
  Proof.
    intros.
    rewrite bin_inter_sym.
    apply bin_inter_empty_set_left.
  Qed.

  Lemma bin_inter_of_subset_left :
    forall {S T : power A},
    S ⊆ T ->
    S ∩ T = S.
  Proof.
    intros.
    apply inclusion_antisymmetric.
    -
      apply bin_inter_subset_left.
    -
      unfold inclusion.
      intros.
      unfold mem.
      unfold bin_inter.
      split.
      +
        assumption.
      +
        apply H.
        assumption.
  Qed.

  Lemma bin_inter_of_subset_right :
    forall {S T : power A},
    T ⊆ S ->
    S ∩ T = T.
  Proof.
    intros.
    rewrite bin_inter_sym.
    apply bin_inter_of_subset_left.
    assumption.
  Qed.

  Lemma bin_inter_left_unit :
    forall {S : power A},
    whole_set ∩ S = S.
  Proof.
    intros.
    extensionality x.
    apply propositional_extensionality.
    split.
    -
      intro.
      destruct H.
      assumption.
    -
      intro.
      unfold bin_inter.
      split.
      +
        apply whole_set_contains_everything.
      +
        assumption.
  Qed.

  Lemma bin_inter_right_unit :
    forall {S : power A},
    S ∩ whole_set = S.
  Proof.
    intros.
    rewrite bin_inter_sym.
    apply bin_inter_left_unit.
  Qed.

  Lemma whole_set_top :
    forall {S : power A},
    S ⊆ whole_set.
  Proof.
    intros.
    unfold inclusion.
    intros.
    apply whole_set_contains_everything.
  Qed.

  Lemma union_whole_set :
    forall {X : power (power A)},
    whole_set ∈ X ->
    ⋃ X = whole_set.
  Proof.
    intros.
    apply inclusion_antisymmetric.
    -
      apply whole_set_top.
    -
      unfold inclusion.
      intros.
      exists whole_set.
      exact (conj H H0).
  Qed.

  Lemma union_least_upper_bound :
    forall {X : power (power A)},
    forall U : power A,
    (forall S, S ∈ X -> S ⊆ U) ->
    ⋃ X ⊆ U.
  Proof.
    intros.
    unfold inclusion.
    intros.
    destruct H0 as [S [H1 H2]].
    specialize (H S H1).
    apply H.
    assumption.
  Qed.

  Lemma union_of_empty_set :
    ⋃ empty_set = empty_set (A := A).
  Proof.
    intros.
    apply subset_of_empty_set.
    intros x H.
    destruct H as [S [H0 H1]].
    unfold mem, empty_set in H0.
    contradiction.
  Qed.
End SetProperties.