topology.v

Require Import Coq.Unicode.Utf8.
Require Import List.

Global Obligation Tactic := compute; firstorder.

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.
Definition singleton {A : Type} (x : A) :=
  fun y => x = y.

(* Definition and notation for subset relation. *)
Definition subset {A : Type} (u v : P A) :=
  forall x : A, u x -> v x.

Infix "⊆" := subset (at level 40, left associativity).
(* Notation "x ∈ U" := (U x) (at level 20).*)

Definition subset_compose {A : Type} : forall {u v w : P A} (i : u ⊆ v) (j : v ⊆ w), u ⊆ w.
  firstorder.
Defined.

Infix "∘" := subset_compose (at level 40, left associativity).

(* Disjointness. *)
Definition disjoint {A : Type} (u v : P A) :=
  ∀ x, ¬ (u x /\ v x).

(* We are going to write a lot of statements of the form
   [forall x : A, U x -> P] and we'd like to write
   them in a less verbose manner. We introduce a notation
   that lets us write [all x : U, P] -- Coq will figure
   out what [A] is. *)
Notation "∀[ x ∈ U ] , P" := (forall x, U x -> P) (at level 20, x at level 99).

(* Similarly for existence. *)
Notation "∃[ x ∈ U ] , P" := (exists x, U x /\ P) (at level 20, x at level 99).


Section SetOperations.
  Variable A : Type.
  (* Arbitrary unions and binary intersections *)
  Definition union (S : P (P A)) :=
    fun x => ∃[U ∈ S], U x.
  
  Definition inter {A : Type} (u v : P A) :=
    fun x => u x /\ v x.
  
  (* The intersection of a finite list of subsets. *)
  Definition inters (us : list (P A)) : P A :=
    fun x => Forall (fun u => u x) us.
  
  
  (* The closure of a family of sets by finite intersections. *)
  Definition inter_close (S : P (P A)) :=
    fun v => ∃[ us ∈  Forall S], ∀ x, v x ↔ inters us x.

End SetOperations.

Notation "⋂" := inters.
Notation "⋃" := union.
Infix "∩" := inter (at level 20).
Infix "∪" := union (at level 20).

Arguments union [A] S x.
Arguments inter [A] u v x.
Arguments inter_close [A] S v.

(* The empty and the full set. *)
Definition empty {A} (_ : A) := False.
Definition full {A} (_ : A) := True.

(* A topology in a type [A] is a structure which consists
   of a family of subsets (called the opens), satisfying
   the usual axioms. In Coq this amounts to the following
   definition. The mysterious [:>] means "automatically
   coerce from the topology structure to its opens". This
   is useful as it lets us write [U : T] instead of
   [U : opens T].
*)

Structure Topology (A : Type) := {
  open :> P A -> Prop ;
  empty_open : open empty;
  full_open : open full ;
  inter_open : ∀[u ∈ open], ∀[v ∈ open], open (u ∩ v) ;
  union_open : forall S, S ⊆ open -> open (⋃ S)
}.

Section ListLemmas.
  Variable A : Type.
  Lemma Forall_app (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 (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 (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.
End ListLemmas.  

Section Topologies.
  Variable A : Type.
  
  (* The discrete topology on a type. *)
  Program Definition discrete : Topology A :=
    {| open := full |}.

  (* 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. *)
  Program Definition indiscrete : Topology A :=
    {| open := fun u => ∀ x, u x -> ∀ y, u y |}.

  (* Particular point topology, see
     http://en.wikipedia.org/wiki/Particular_point_topology, but of course
     without unecessary excluded middle.
  *)
  Program Definition particular (x : A) : Topology A :=
    {| open := fun u => (∃ y, u y) → u x |}.

  (* The topology generated by a family B of subsets that are
     closed under finite intersections. *)
  Program Definition base (B : P (P A)) (H : B full) (G : ∀[u ∈ B], ∀[v ∈ B], B (u ∩ v)) :  Topology A :=
    {| open := fun u => ∀ x, u x ↔ ∃[v ∈ B], (v x /\ v ⊆ u) |}.
  Next Obligation.
    destruct (proj1 (H0 x) H2) as [u' [? [? ?]]].
    destruct (proj1 (H1 x) H3) as [v' [? [? ?]]].
    exists (u' ∩ v'); firstorder.
  Defined.
  Next Obligation.
    destruct (H0 x0 H1 x) as [L1 _].
    destruct (L1 H2) as [v ?].
    exists v; firstorder.
  Defined.

  (* The topology generated by a subbase S. *)
  Definition subbase (S : P (P A)) : 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.

  (* The cofinite topology on A. *)
  Definition cofinite : Topology A :=
    subbase (fun u => ∃ x, ∀ y, (u y ↔ y ≠ x)).
End Topologies.

Arguments subbase [A] S.

Section TopologyLemmas.
  Variable A : Type.
  Variable T : Topology A.

  (* The definition of a T_1 space. *)
  Definition T₁ :=
    ∀ x y : A,
      x ≠ y →
      ∃[ u ∈ T], (u x /\ ¬ u y).
  
  (* The definition of Hausdorff space. *)
  Definition hausdorff :=
    ∀ x y : A,
      x ≠ y →
      ∃[ u ∈ T ], ∃[ v ∈ T ],
         (u x /\ v y /\ disjoint u v).

  (* Every Hausdorff space is T1. *)
  Lemma hausdorff_is_T₁ : hausdorff → 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.

  (* Let us prove that the indiscrete topology is the least one.
     We seem to need extensionality for propositions. *)
  Lemma indiscrete_least : (forall X (s t : P X), s ⊆ t -> t ⊆ s -> s = t) -> 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 = ⋃ (fun v => T v /\ ∃[x ∈ v], 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.
End TopologyLemmas.

Arguments hausdorff [A] T.
Arguments T₁ [A] T.

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

(* A subbasic set is open. *)
Lemma subbase_open {A : Type} (S : P (P A)) (u : P A) :
  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 is T1. *)
Lemma cofinite_T₁ (A : Type) : T₁ (cofinite A).
Proof.
  intros x y N.
  exists (fun z => z ≠ y).
  split ; auto.
  apply subbase_open.
  exists y ; firstorder.
Qed.

Structure Presheaf {X : Type} (T : Topology X) := {
  apply :> sigT (open X T) -> Type;
  contramap : forall {u v}, projT1 u ⊆ _ v -> apply v -> apply u;
  id_law : forall u x, @contramap u _ (fun _ x => x) x = x;
  comp_law : forall u v w (i : _ u ⊆ _ v) (j : _ v ⊆ _ w) x, contramap (i ∘ j) x = contramap i (contramap j x)
}.

Section Records.
  Variable X : Type.
  Variable T : Topology X.
  Variable El : X -> Type.
  Program Definition R : Presheaf T :=
    {| apply := fun U => forall x, projT1 U x -> El x |}.
End Records.

Arguments R [X] T El.

Section Examples.
  Inductive Bool := tt | ff.
  
  Inductive Cat := Emma.
  Inductive Dog := Tucker | Rover.
  
  Definition El (b : Bool) : Type :=
    match b with
      | tt => Cat
      | ff => Dog
    end.
  
  Program Definition allbools : sigT (indiscrete Bool) := existT _ full _.
  Program Definition nobools : sigT (indiscrete Bool) := existT _ empty _.

  Definition RTest1 : R (indiscrete Bool) El allbools :=
    fun x _ =>
      match x with
        | tt => Emma
        | ff => Tucker
      end.
  
  Program Definition RTest2 : R (indiscrete Bool) El nobools := _.
End Examples.