
Definition subset (A : Type) (u v : A -> Prop) := (forall x : A, u x -> v x).
Definition disjoint (A : Type) (u v : A -> Prop) := forall x, ~ (u x /\ v x).
Definition union (A : Type) (B : (A -> Prop) -> Prop) := fun x : A => exists U, B U /\ U x.
Definition inter (A : Type) (u v : A -> Prop) := fun x : A => u x /\ v x.
Definition empty (A: Type) := fun x : A => False.
Definition full (A: Type) := fun x : A => True.

Structure topology (A : Type) := {
          open :> (A -> Prop) -> Prop;
          empty_open: open (empty _);
          full_open: open (full _);
          inter_open: forall u, open u -> forall v, open v -> open (inter A u v) ;
          union_open: forall s, (subset _ s open) -> open (union A s) }.

(* The discrete topology on a type. *)
Definition discrete (A : Type) : topology A.
Proof.
  exists (full _); firstorder.
Defined.

(* The definition of a T_1 space. *)
Definition T1 {A : Type} (T : topology A) :=
  forall x y : A,
    x <> y ->
      exists u, T u /\ (u x /\ ~ (u y)).

(* The definition of Hausdorff space. *)
Definition hausdorff {A : Type} (T : topology A) :=
  forall x y : A,
  x <> y ->
    exists u, T u /\ exists v, T v /\
      (u x /\ v y /\ disjoint A u v).

(* A discrete space is Hausdorff. *)
Lemma discrete_hausdorff {A : Type} : hausdorff (discrete A).
Proof.
  intros x y N.
  exists (fun z : A => x = z ) ; split ; [exact I | idtac].
  exists (fun z : A => y = z ) ; split ; [exact I | idtac].
  repeat split ; auto.
  intros z [? ?].
  absurd (x = y) ; auto.
  transitivity z ; auto.
Qed.

(* Every Hausdorff space is T1. *)
Lemma hausdorff_is_T1 {A : Type} (T : topology A) :
  hausdorff T -> T1 T.
Proof.
  intros H x y N.
  destruct (H x y N) as [u [? [v [? [? [? G]]]]]].
  exists u ; repeat split ; auto.
  intro.
  absurd (u y /\ v y) ; auto.
Qed.

(* Indiscrete topology. A classical mathematician will be tempted to use
   disjunction: a set is open if it is either empty or the whole set. But
   that relies on excluded middle and generally causes trouble. Here is
   a better definition: a set is open iff as soon as it contains an element,
   it is the whole set. *)
Definition indiscrete (A : Type) : topology A.
Proof.
  exists (fun u : A -> Prop => forall x : A, u x -> (forall y : A, u y) ) ; firstorder.
Defined.

Notation "u <= v" := (subset u v).

(* Let us prove that the indiscrete topology is the least one.
   We seem to need extensionality for propositions. *)
Lemma indiscrete_least (A : Type) (T : topology A) :
  (forall (X : Type) (s t : X -> Prop), (subset _ s t) -> (subset _ t s) -> s = t) ->
  subset _ (indiscrete A) T.
Proof.
  intros ext u H.
  (* Idea: if u is in the indiscrete topology then it is the union of all T-opens v which it meets. *)
  assert (G : (u = union A (fun v : A -> Prop => T v /\ exists x, v x /\ u x ))).
  - apply ext.
    + intros x ?. exists (full _); firstorder using full_open.
    + intros x [v [[? [y [? ?]]] ?]] ; now apply (H y).
  - rewrite G ; apply union_open ; firstorder.
Qed.

(* Particular point topology, see
   http://en.wikipedia.org/wiki/Particular_point_topology, but of course
   without unecessary excluded middle.
*)
Definition particular {A : Type} (x : A) : topology A.
Proof.
  exists (fun u : A -> Prop => (exists y, u y) -> u x ) ; firstorder.
Qed.

(* The topology generated by a family B of subsets that are
   closed under finite intersections. *)

Require Import List.

(* The intersection of a finite list of subsets. *)
Definition inters {A : Type} (us : list (A -> Prop)) : A -> Prop :=
  (fun x : A => Forall (fun u =>  u x) us ).

(* The closure of a family of sets by finite intersections. *)
Definition inter_close {A : Type} (S : (A -> Prop) -> Prop) :=
  (fun v : A -> Prop => exists us, (Forall S) us /\ (forall x, v x <-> inters us x) ).

Lemma Forall_app {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).
Proof.
  induction l1 ; simpl ; auto.
  intros H G.
  constructor.
  - apply (Forall_inv H).
  - apply IHl1 ; auto.
    inversion H ; assumption.
Qed.

Lemma Forall_app1 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P (l1 ++ l2) -> Forall P l1.
Proof.
  induction l1 ; simpl ; auto.
  intro H.
  inversion H ; auto.
Qed.

Lemma Forall_app2 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P (l1 ++ l2) -> Forall P l2.
Proof.
  induction l1 ; simpl ; auto.
  intro H.
  inversion H ; auto.
Qed.

Definition base {A : Type} (B : (A->Prop) -> Prop) :
  B (full _) -> (forall u, B u -> forall v, B v -> B (inter A u v)) -> topology A.
Proof.
  intros H G.
  exists (fun u : A -> Prop => forall x, u x <-> exists v, B v /\ (v x /\ (subset _ v u))).
  - firstorder.
  - firstorder.
  - intros u Hu v Hv x.
    split.
    + intros [Gu Gv].
      destruct (proj1 (Hu x) Gu) as [u' [? [? ?]]].
      destruct (proj1 (Hv x) Gv) as [v' [? [? ?]]].
      exists (inter A u' v') ; firstorder.
    + intros [w [? [? ?]]].
      split ; now apply H2.
  - intros S K x.
    split.
    + intros [u [H1 H2]].
      destruct (K u H1 x) as [L1 _].
      destruct (L1 H2) as [v ?].
      exists v ; firstorder.
    + firstorder.
Defined.

(* The topology generated by a subbase S. *)
Definition subbase {A : Type} (S : (A -> Prop) -> Prop) : topology A.
Proof.
  apply (base (inter_close S)).
  - exists nil ; firstorder using Forall_nil.
  - intros u [us [Hu Gu]] v [vs [Hv Gv]].
    exists (us ++ vs).
    split ; [ (now apply Forall_app) | idtac ].
    split.
    + intros [? ?].
      apply Forall_app ; firstorder.
    + intro K ; split.
      * apply Gu.
        apply (Forall_app1 _ _ _ K).
      * apply Gv.
        apply (Forall_app2 _ _ _ K).
Defined.

(* A subbasic set is open. *)
Lemma subbase_open {A : Type} (S : (A -> Prop) -> Prop) (u : A -> Prop) :
  S u -> (subbase S) u.
Proof.
  intros H x.
  split.
  - intro G.
    exists u ; split ; [ idtac | firstorder ].
    exists (u :: nil).
    split ; [now constructor | idtac].
    intro y ; split.
    + intro ; now constructor.
    + intro K.
      inversion K ; auto.
  - firstorder.
Qed.

(* The cofinite topology on A. *)
Definition cofinite (A : Type) : topology A :=
  subbase (fun u : A -> Prop => exists x, forall y, (u y <-> y <> x) ).

(* The cofinite topology is T1. *)
Lemma cofinite_T1 (A : Type) : T1 (cofinite A).
Proof.
  intros x y N.
  exists (fun z : A => z <> y ).
  split ; auto.
  apply subbase_open.
   exists y ; firstorder.
Qed.

