冪

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.A: Type
forall x : A, x ∈ empty_set -> False
  Proof.A: Type
forall x : A, x ∈ empty_set -> False
    intros.A: Type
x: A
H: x ∈ empty_set
False
    unfold mem in H.A: Type
x: A
H: empty_set x
False
    unfold empty_set in H.A: Type
x: A
H: False
False
    exact H.
  Qed.

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

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

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

  Lemma inclusion_refl :
    forall {S : power A},
    S ⊆ S.A: Type
forall S : power A, S ⊆ S
  Proof.A: Type
forall S : power A, S ⊆ S
    intros.A: Type
S: power A
S ⊆ S
    unfold inclusion.A: Type
S: power A
forall x : A, x ∈ S -> x ∈ S
    intros.A: Type
S: power A
x: A
H: x ∈ S
x ∈ S
    assumption.
  Qed.

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

  Lemma inclusion_is_preorder :
    is_preorder (power A) inclusion.A: Type
is_preorder (power A) inclusion
  Proof.A: Type
is_preorder (power A) inclusion
    constructor.A: Type
forall x : power A, x ⊆ x
A: Type
forall x y z : power A, x ⊆ y -> y ⊆ z -> x ⊆ z
    -A: Type
forall x : power A, x ⊆ x
      exact @inclusion_refl.
    -A: Type
forall x y z : power A, x ⊆ y -> y ⊆ z -> x ⊆ z
      exact @inclusion_trans.
  Qed.

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

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

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

  Lemma bin_inter_subset_left :
    forall {S T : power A},
    S ∩ T ⊆ S.A: Type
forall S T : power A, S ∩ T ⊆ S
  Proof.A: Type
forall S T : power A, S ∩ T ⊆ S
    intros.A: Type
S, T: power A
S ∩ T ⊆ S
    unfold inclusion.A: Type
S, T: power A
forall x : A, x ∈ S ∩ T -> x ∈ S
    intros.A: Type
S, T: power A
x: A
H: x ∈ S ∩ T
x ∈ S
    destruct H.A: Type
S, T: power A
x: A
H: x ∈ S
H0: x ∈ T
x ∈ S
    assumption.
  Qed.

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

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

  Lemma bin_inter_of_subset_left :
    forall {S T : power A},
    S ⊆ T ->
    S ∩ T = S.A: Type
forall S T : power A, S ⊆ T -> S ∩ T = S
  Proof.A: Type
forall S T : power A, S ⊆ T -> S ∩ T = S
    intros.A: Type
S, T: power A
H: S ⊆ T
S ∩ T = S
    apply inclusion_antisymmetric.A: Type
S, T: power A
H: S ⊆ T
S ∩ T ⊆ S
A: Type
S, T: power A
H: S ⊆ T
S ⊆ S ∩ T
    -A: Type
S, T: power A
H: S ⊆ T
S ∩ T ⊆ S
      apply bin_inter_subset_left.
    -A: Type
S, T: power A
H: S ⊆ T
S ⊆ S ∩ T
      unfold inclusion.A: Type
S, T: power A
H: S ⊆ T
forall x : A, x ∈ S -> x ∈ S ∩ T
      intros.A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ S ∩ T
      unfold mem.A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
(S ∩ T) x
      unfold bin_inter.A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ S /\ x ∈ T
      split.A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ S
A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ T
      +A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ S
        assumption.
      +A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ T
        apply H.A: Type
S, T: power A
H: S ⊆ T
x: A
H0: x ∈ S
x ∈ S
        assumption.
  Qed.

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

  Lemma bin_inter_left_unit :
    forall {S : power A},
    whole_set ∩ S = S.A: Type
forall S : power A, whole_set ∩ S = S
  Proof.A: Type
forall S : power A, whole_set ∩ S = S
    intros.A: Type
S: power A
whole_set ∩ S = S
    extensionality x.A: Type
S: power A
x: A
(whole_set ∩ S) x = S x
    apply propositional_extensionality.A: Type
S: power A
x: A
(whole_set ∩ S) x <-> S x
    split.A: Type
S: power A
x: A
(whole_set ∩ S) x -> S x
A: Type
S: power A
x: A
S x -> (whole_set ∩ S) x
    -A: Type
S: power A
x: A
(whole_set ∩ S) x -> S x
      intro.A: Type
S: power A
x: A
H: (whole_set ∩ S) x
S x
      destruct H.A: Type
S: power A
x: A
H: x ∈ whole_set
H0: x ∈ S
S x
      assumption.
    -A: Type
S: power A
x: A
S x -> (whole_set ∩ S) x
      intro.A: Type
S: power A
x: A
H: S x
(whole_set ∩ S) x
      unfold bin_inter.A: Type
S: power A
x: A
H: S x
x ∈ whole_set /\ x ∈ S
      split.A: Type
S: power A
x: A
H: S x
x ∈ whole_set
A: Type
S: power A
x: A
H: S x
x ∈ S
      +A: Type
S: power A
x: A
H: S x
x ∈ whole_set
        apply whole_set_contains_everything.
      +A: Type
S: power A
x: A
H: S x
x ∈ S
        assumption.
  Qed.

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

  Lemma whole_set_top :
    forall {S : power A},
    S ⊆ whole_set.A: Type
forall S : power A, S ⊆ whole_set
  Proof.A: Type
forall S : power A, S ⊆ whole_set
    intros.A: Type
S: power A
S ⊆ whole_set
    unfold inclusion.A: Type
S: power A
forall x : A, x ∈ S -> x ∈ whole_set
    intros.A: Type
S: power A
x: A
H: x ∈ S
x ∈ whole_set
    apply whole_set_contains_everything.
  Qed.

  Lemma union_whole_set :
    forall {X : power (power A)},
    whole_set ∈ X ->
    ⋃ X = whole_set.A: Type
forall X : power (power A), whole_set ∈ X -> ⋃ X = whole_set
  Proof.A: Type
forall X : power (power A), whole_set ∈ X -> ⋃ X = whole_set
    intros.A: Type
X: power (power A)
H: whole_set ∈ X
⋃ X = whole_set
    apply inclusion_antisymmetric.A: Type
X: power (power A)
H: whole_set ∈ X
⋃ X ⊆ whole_set
A: Type
X: power (power A)
H: whole_set ∈ X
whole_set ⊆ ⋃ X
    -A: Type
X: power (power A)
H: whole_set ∈ X
⋃ X ⊆ whole_set
      apply whole_set_top.
    -A: Type
X: power (power A)
H: whole_set ∈ X
whole_set ⊆ ⋃ X
      unfold inclusion.A: Type
X: power (power A)
H: whole_set ∈ X
forall x : A, x ∈ whole_set -> x ∈ ⋃ X
      intros.A: Type
X: power (power A)
H: whole_set ∈ X
x: A
H0: x ∈ whole_set
x ∈ ⋃ X
      exists whole_set.A: Type
X: power (power A)
H: whole_set ∈ X
x: A
H0: x ∈ whole_set
whole_set ∈ X /\ x ∈ 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.A: Type
forall (X : power (power A)) (U : power A),
(forall S : power A, S ∈ X -> S ⊆ U) -> ⋃ X ⊆ U
  Proof.A: Type
forall (X : power (power A)) (U : power A),
(forall S : power A, S ∈ X -> S ⊆ U) -> ⋃ X ⊆ U
    intros.A: Type
X: power (power A)
U: power A
H: forall S : power A, S ∈ X -> S ⊆ U
⋃ X ⊆ U
    unfold inclusion.A: Type
X: power (power A)
U: power A
H: forall S : power A, S ∈ X -> S ⊆ U
forall x : A, x ∈ ⋃ X -> x ∈ U
    intros.A: Type
X: power (power A)
U: power A
H: forall S : power A, S ∈ X -> S ⊆ U
x: A
H0: x ∈ ⋃ X
x ∈ U
    destruct H0 as [S [H1 H2]].A: Type
X: power (power A)
U: power A
H: forall S : power A, S ∈ X -> S ⊆ U
x: A
S: power A
H1: S ∈ X
H2: x ∈ S
x ∈ U
    specialize (H S H1).A: Type
X: power (power A)
U, S: power A
H: S ⊆ U
x: A
H1: S ∈ X
H2: x ∈ S
x ∈ U
    apply H.A: Type
X: power (power A)
U, S: power A
H: S ⊆ U
x: A
H1: S ∈ X
H2: x ∈ S
x ∈ S
    assumption.
  Qed.

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