Library Topology


Require Import Utf8 Setoid.
Require Import ProofIrrelevance.
Require Import Classical.
Require Export Ensembles.
Require Export Morphism.
Require Import Notations Common Morphism.

Set Implicit Arguments.

Generalizable All Variables.

Topology


Create HintDb topology discriminated.

Delimit Scope topology_scope with topology.

Local Open Scope topology_scope.

Section inclusion.
  Variable T : Type.

  Global Instance Included_refl : RelationClasses.Reflexive (@Included T).
  Proof.
    firstorder.
  Qed.

  Global Instance Included_trans : RelationClasses.Transitive (@Included T).
  Proof.
    firstorder.
  Qed.
End inclusion.

Add Parametric Relation T : _ (@Included T)
    reflexivity proved by (@Included_refl _)
    transitivity proved by (@Included_trans _)
      as Included_rel.

Local Ltac inter_t :=
  repeat intro;
  destruct_head_hnf @Intersection;
  constructor; firstorder.

Add Parametric Morphism T A : (@Intersection T A)
with signature (@Included T) ==> (@Included T)
  as Intersection_Included_morl.
  inter_t.
Qed.

Add Parametric Morphism T A : (fun B ⇒ @Intersection T B A)
with signature (@Included T) ==> (@Included T)
  as Intersection_Included_morr.
  inter_t.
Qed.

Add Parametric Morphism T : (@Intersection T)
with signature (@Included T) ==> (@Included T) ==> (@Included T)
  as Intersection_Included_mor_both.
  inter_t.
Qed.

Section topology.
  Variable X : Type.

  Inductive ArbitraryUnion (XjP : Ensemble (Ensemble X)) : Ensemble X :=
  | ArbitraryUnion_inJ (Xj : Ensemble X)
    : x, Xj XjPx Xjx (ArbitraryUnion XjP).

  Definition ArbitraryIntersection (XjP : Ensemble (Ensemble X)) : Ensemble X :=
    Complement _ (ArbitraryUnion (fun U(Complement _ U) XjP)).

  Class Topology :=
    {
      Open : Ensemble (Ensemble X);
      OpenSet :> _ := { U | Open U };
      ContainsSpace : Open (Full_set _);
      ContainsEmpty : Open (Ensembles.Empty_set _);
      ArbitraryUnionOpen : (XjP : Ensemble (Ensemble X)),
                             ( Xj, Xj XjPOpen Xj) → Open (ArbitraryUnion XjP);
      FiniteIntersectionOpen : A B,
                                 Open AOpen BOpen (A B)
    }.

  Definition Closed {T : Topology} (U : Ensemble X) := @Open T (Complement _ U).
End topology.

Notation "⋃ S" := (ArbitraryUnion S) (at level 50, no associativity) : topology_scope.
Notation "⋂ S" := (ArbitraryIntersection S) (at level 50, no associativity) : topology_scope.

Section intersection.
  Variable X : Type.
  Variables C C' : Ensemble (Ensemble X).

  Inductive PairwiseIntersection : Ensemble (Ensemble X) :=
    PairwiseIntersection_intro
    : U U',
        U CU' C'(U U') PairwiseIntersection.
End intersection.

Ltac destruct_sets := repeat (
                          (destruct_head_hnf ArbitraryUnion)
                            || (destruct_head_hnf PairwiseIntersection)
                            || (destruct_head_hnf Intersection)
                            || match goal with
                                 | [ |- ?G ] ⇒ match type of G with
                                                  | Propdestruct_head_hnf @ex;
                                                  destruct_head_hnf @ex2
                                                end
                               end
                        ).

Hint Extern 0 ⇒ econstructor; hnf in *; eassumption.
Hint Extern 1 ⇒ econstructor; solve [ trivial ].

Section intersection_union_commute.
  Variable X : Type.
  Variables C C' : Ensemble (Ensemble X).

  Lemma intersection_arbitrary_union_commute
  : (PairwiseIntersection C C')
    = ( C) ( C').
  Proof.
    apply Extensionality_Ensembles;
    split; hnf; intros;
    destruct_sets; eauto.
  Qed.
End intersection_union_commute.

Hint Immediate ContainsSpace ContainsEmpty ArbitraryUnionOpen FiniteIntersectionOpen : topology.

Coercion OpenSet : Topology >-> Sortclass.

Definition ensemble2sig {X} (E : Ensemble X) := { x | x E }.

Coercion ensemble2sig : Ensemble >-> Sortclass.

Definition subset_ensemble {U} {V : Ensemble U} (W : Ensemble (sig V)) : Ensemble U
  := fun xx V ( H, (exist _ x H) W).

Lemma subset_ensemble_included U V W : (@subset_ensemble U V W) V.
Proof.
  hnf; intros;
  hnf in *;
  destruct_hypotheses; trivial.
Qed.

Lemma subset_ensemble_iff1 U V W
: x H, x (@subset_ensemble U V W)(exist _ x H) W.
Proof.
  intros; hnf in ×.
  destruct_hypotheses; unfold Ensembles.In in *; intuition.
Qed.

Lemma subset_ensemble_iff2 U V W
: x, x W(proj1_sig x) (@subset_ensemble U V W).
Proof.
  intros; hnf in *; destruct_sig; intuition.
  hnf;
    match goal with
      | [ H : ?f (exist ?V ?x ?H0) |- ?f (exist ?V ?x ?H1) ] ⇒
        cut (f (exist V x H0) = f (exist V x H1));
          [ let H := fresh in intro; rewrite <- H; assumption | repeat f_equal ]
    end;
    apply ProofIrrelevance.proof_irrelevance.
Qed.

Ltac do_proof_irrelevance :=
  repeat match goal with
           | [ H : ?P, H' : ?P |- _ ] ⇒ match type of P with
                                           | Proplet H'' := fresh in assert (H'' : H = H') by (apply ProofIrrelevance.proof_irrelevance);
                                                                        rewrite H'' in *; clear H''; clear H
                                         end
         end.

Local Ltac generalize_sig_then_destruct_sets :=
  repeat match goal with
           | [ H : context[exist ?P ?x ?H] |- ?f ?x ] ⇒
             match goal with
               | [ _ := exist P x H |- _ ] ⇒ fail 1
               | _let x' := fresh "x'" in pose (exist P x H) as x';
                                             assert (proj1_sig x' = x) by reflexivity
             end
         end;
  destruct_sets; subst_body; repeat subst.

Section subset_ensemble_union_intersection.
  Variable X : Type.
  Variable U : Ensemble X.

  Local Ltac pre_union_intersection :=
    repeat (repeat subst; hnf in *; intros; generalize_sig_then_destruct_sets;
            do_proof_irrelevance;
            (split ||
                   constructor ||
                   split_and ||
                   intuition)).

  Local Ltac union_intersection :=
    repeat (pre_union_intersection; specialize_all_ways; intuition; hnf in *; destruct_sig; simpl in *; hnf).

  Lemma subset_ensemble_intersection (A B : Ensemble (sig U))
  : (subset_ensemble A) (subset_ensemble B) = subset_ensemble (A B).
  Proof.
    apply Extensionality_Ensembles; union_intersection.
  Qed.

  Lemma subset_ensemble_union (A : Ensemble (Ensemble (sig U)))
  : ArbitraryUnion (fun SS U A (fun x(proj1_sig x) S)) = subset_ensemble ( A).
  Proof.
    apply Extensionality_Ensembles; pre_union_intersection;
    specialize_all_ways; intuition; hnf in ×.
    generalize_sig_then_destruct_sets.
    unfold Ensembles.In in ×.
    destruct_sig; simpl in *; do_proof_irrelevance.
     (subset_ensemble Xj); pre_union_intersection;
    match goal with
      | [ |- A ?f ] ⇒ cut (f = Xj); [ let H := fresh in intro H; rewrite H; assumption | ]
    end;
    apply Extensionality_Ensembles; union_intersection.
  Qed.
End subset_ensemble_union_intersection.

Section inclusion2.
  Variable X : Type.
  Variable E : Ensemble X.

  Definition inclusion : EX := @proj1_sig _ _.
End inclusion2.

Section inclusion3.
  Variable X : Type.

  Definition include_subset (U V : Ensemble X) : U VEnsemble { x : X | x V }
    := (fun _ xH(proj1_sig xH) U).
End inclusion3.

Notation "p ⁻¹" := (inverse_image p) (at level 10) : topology_scope.

Section complement_idempotent.
  Context `(T : Topology X).

  Lemma complement_idempotent S : Complement X (Complement X S) = S.
    clear T.
    apply Extensionality_Ensembles.
    repeat (intro || split);
    try match goal with
          | [ H : _ |- _ ] ⇒ apply NNPP in H
        end;
    firstorder.
  Qed.

  Local Ltac t :=
    repeat match goal with
             | _apply Extensionality_Ensembles
             | _progress (repeat (intro || split))
             | _progress destruct_head_hnf ArbitraryUnion
             | _progress (repeat unfold Complement, Ensembles.In in *; trivial)
             | _eassumption
             | _eexists; try eassumption; []
             | [ H : _ |- _ ] ⇒ apply H
             | [ H : _ |- _ ] ⇒ apply NNPP in H
             | [ H : ?XjP ?Xj |- ?XjP ?Xj' ] ⇒ cut (Xj = Xj');
                                               [ let H := fresh in intro H; rewrite <- H; assumption
                                               | apply Extensionality_Ensembles ]
             | _progress intuition
             | _progress firstorder
           end.

  Lemma complement_union XjP : Complement T ( XjP)
                               = (fun U(Complement T U) XjP).
    t.
  Qed.

  Lemma complement_intersection XjP : Complement T ( XjP)
                               = (fun U(Complement T U) XjP).
    t.
  Qed.
End complement_idempotent.

Section disjoint_union.
  Variable X : Type.

  Record IsDisjointUnion (U : Ensemble X) := {
                                              DisjointUnionSets :> Ensemble (Ensemble X);
                                              DisjointUnionSetsDisjoint : A B,
                                                                            A B
                                                                            → A DisjointUnionSets
                                                                            → B DisjointUnionSets
                                                                            → Disjoint _ A B;
                                              DisjointUnionIsUnion : DisjointUnionSets = U
                                            }.

  Lemma disjoint_union_in (U : Ensemble X) (DU : IsDisjointUnion U) : (Ux : DU), (proj1_sig Ux) U.
  Proof.
    intros Ux x H;
    destruct_sig;
    simpl in ×.
    let H := fresh in pose proof (DisjointUnionIsUnion DU) as H;
                     rewrite <- H.
    hnf.
    econstructor; unfold Ensembles.In in *; simpl in *; eassumption.
  Qed.
End disjoint_union.

Section intersection_lemmas.
  Variable X : Type.

  Lemma IntersectionAAA (A : Ensemble X) : A A = A.
  Proof.
    apply Extensionality_Ensembles; split; intros x H; destruct_head_hnf Intersection; try constructor; trivial.
  Qed.
End intersection_lemmas.