Library SubspaceTopology


Require Import Utf8 Setoid.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import Finite_sets Classical IndefiniteDescription.
Require Import Classes.RelationClasses Morphisms.
Require Export Topology.
Require Import Notations Common Morphism.

Set Implicit Arguments.

Generalizable All Variables.

The Subspace Topology


Local Open Scope topology_scope.

Section subspace_topology.
  Variable X : Type.
  Variable T : Topology X.
  Variable P : XProp.

  Local Ltac subspace_t :=
    try apply Extensionality_Ensembles; hnf;
    repeat split; simpl in *; hnf in *;
    destruct_hypotheses; unfold Ensembles.In in *; simpl in *;
    destruct_head_hnf @Intersection;
    auto;
    specialize_all_ways;
    destruct_head_hnf @Ensembles.Empty_set;
    destruct_head_hnf .


  Local Ltac remove_proj1_sig_evar :=
    match goal with
      | [ |- context[proj1_sig ?x] ] ⇒
        has_evar x;
          let T := type of x in
          match eval hnf in T with
            | sig ?P
              match type of P with
                | ?AProp
                  let y := fresh "y" in
                  let H := fresh "H" in
                  evar (y : A);
                    evar (H : P y);
                    let H' := fresh in
                    assert (H' : x = exist P y H) by reflexivity;
                      clear H'; subst y; subst H; simpl
              end
          end
    end.

  Global Instance SubspaceTopology : Topology (sig P) :=
    {| Open := (fun U U' : T, subset_ensemble U = (proj1_sig U') P) |}.
  Proof with simpl; try abstract solve [ subspace_t ].
    - refine (ex_intro _ (exist _ (Full_set _) _) _)...
    - refine (ex_intro _ (exist _ (Ensembles.Empty_set _) _) _)...
    -
      admit.
    - setoid_rewrite <- subset_ensemble_intersection;
      intros A B HA HB; destruct HA as [ UA HA ], HB as [ UB HB ];
      rewrite HA, HB;
      refine (ex_intro _ (exist _ (Intersection _ _ _) _) _); simpl;
      apply Extensionality_Ensembles; split; intros ? ?; destruct_sets; unfold Ensembles.In in *; simpl in *;
      repeat constructor; try assumption; unfold Ensembles.In in *; [ | | eassumption | eassumption ]; assumption.
      Grab Existential Variables.
      abstract (destruct_sig; simpl; auto with topology).
      abstract (destruct_sig; simpl; auto with topology).
      abstract (destruct_sig; simpl; auto with topology).
  Defined.
End subspace_topology.