Library Closure


Require Import Utf8 Setoid.
Require Import Classical.
Require Export Topology.
Require Import Notations Common.

Set Implicit Arguments.

Generalizable All Variables.

Closure


Local Open Scope topology_scope.

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

The closure of a set is the intersection of all closed sets containing that set.

  Definition closure (S : Ensemble X) : Ensemble X :=
     (fun US U Closed U).

  Lemma closure_closed S : Closed (closure S).
    repeat unfold Closed, closure, ArbitraryIntersection.
    rewrite complement_idempotent.
    apply ArbitraryUnionOpen.
    firstorder.
    match goal with
      | [ H : _ |- _ ] ⇒ rewrite complement_idempotent in H
    end.
    assumption.
  Qed.

  Lemma closure_superset S : S closure S.
    repeat intro;
    destruct_head_hnf ArbitraryUnion;
    firstorder.
  Qed.

  Local Ltac t0 :=
    repeat match goal with
             | _eassumption
             | _progress (repeat (split || intro))
             | _progress (repeat unfold closure, ArbitraryIntersection, Closed, In in *; trivial)
             | _progress destruct_head_hnf ArbitraryUnion
             | _progress destruct_head_hnf and
             | [ H : _ |- _ ] ⇒ rewrite complement_idempotent in H
             | [ H : _ |- _ ] ⇒ hnf in H; rewrite complement_idempotent in H
             | _apply Extensionality_Ensembles
             | _progress (hnf; repeat rewrite complement_idempotent)
             | _progress intuition
             | _progress firstorder
           end.

  Local Ltac t1' tac := repeat ((progress t0) || (progress tac)).
  Local Ltac t1'' tac :=
    t1' tac;
    try match goal with
          | [ H : _ |- _ ] ⇒ apply H; solve [ t1' tac ]
        end.
  Local Ltac t1 tac :=
    t1' tac;
    match goal with
      | _apply NNPP; solve [ t1'' tac ]
    end.

  Lemma closure_closed_same S : Closed Sclosure S = S.
    t1 ltac:( (Complement X S)).
  Qed.

  Lemma closure_respect_subset U V : U Vclosure U closure V.
    t1'' ltac:(eexists; [ | eassumption ]).
  Qed.
End closure.