Stream: Coq users

Topic: building a simple topology


view this post on Zulip Ben Siraphob (Jul 31 2021 at 14:49):

I tried using the coq-community/topology library but it seems very hard to work with Ensembles, I want to make a topological space on a type X={a,b,c} with the open sets T={{b},{b,c},{a,b},X,∅}, but I'm having great difficulty in doing so (code below). In particular, I'm stuck on this goal:

1 subgoal (ID 70)

  F : Family X
  HF : forall S : Ensemble X, In F S -> T S
  ============================
  T (FamilyUnion F)
From Topology Require Import TopologicalSpaces.
Require Import Ensembles.

Section TopSpaceEx1.

Inductive X : Type := a | b | c.
From ZornsLemma Require Export EnsemblesImplicit.

Definition T (x : Ensemble X) : Prop := Same_set x (Singleton b)
                                  \/ Same_set x (Couple b c)
                                  \/ Same_set x (Couple a b)
                                  \/ Same_set x Full_set.
Ltac destruct_ensembles_in :=
 match goal with
   | [H : Ensembles.In _ _ |- _] => destruct H
 end.

Ltac destruct_ensembles :=
  split; red; intros;
    repeat destruct_ensembles_in.

Ltac inversion_ensembles_in :=
 match goal with
   | [H : Ensembles.In _ _ |- _] => inversion H; clear H
 end.

Ltac ensembles_inv :=
  let x := fresh "x" in
  let H := fresh "H" in
  split; red; intros x H; destruct x;
    repeat inversion_ensembles_in.

Lemma T_is_topology : TopologicalSpace.
Proof with auto with sets.
refine (Build_TopologicalSpace X T _ _ ltac:(firstorder)).
- intros F HF.
  admit.
- intros.
  destruct H as [? | [? | [? | ?]]];
  destruct H0 as [? | [? | [? | ?]]];
  apply Extensionality_Ensembles in H;
  apply Extensionality_Ensembles in H0; subst; unfold T.
  + left...
  + left; repeat destruct_ensembles; constructor.
  + left; repeat destruct_ensembles; constructor.
  + left; repeat destruct_ensembles; constructor.
  + left; repeat destruct_ensembles; constructor.
  + right; left; repeat destruct_ensembles; constructor.
  + left; ensembles_inv...
  + right; left; repeat destruct_ensembles; constructor.
  + left; repeat destruct_ensembles; constructor.
  + left; ensembles_inv...
  + right; right; left...
  + right; right; left; repeat destruct_ensembles; constructor.
  + left; red; repeat destruct_ensembles; constructor.
  + right; left; repeat destruct_ensembles; constructor.
  + right; right; left; repeat destruct_ensembles; constructor.
  + right; right; right...
Admitted.

End TopSpaceEx1.

view this post on Zulip Ali Caglayan (Jul 31 2021 at 17:42):

Perhaps it might be useful to write your T more directly as an inductive type?

Inductive T : Ensemble X -> Prop :=
| t_sing : T (Singleton b)
| t_coup_b_c : T (Couple b c)
| t_coup_a_b : T (Couple b c)
| t_X : T X.

Obviously you can change the names of the constructors.

view this post on Zulip Ben Siraphob (Aug 01 2021 at 08:11):

I get similar goals if I do that, e.g. T (Intersection (Singleton b) (singleton b)) which is obviously true but can't be discharged automatically because of the lack of reflection with ensembles

view this post on Zulip Ali Caglayan (Aug 01 2021 at 12:42):

I'm having a go at this now, however I noticed that the empty set isn't in your opens. Shouldn't you also include that?

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:35):

I was able to get coq to automatically solve the later parts of the topology, however the first goal is quite difficult as you say. On paper I would do this by trying every element since everything is finite in X and the powerset etc. But this requires a lot of excluded middle I believe and I am not sure if it is constructively true... thought perhaps since X is decidable we can get away with it.

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:35):

Something else to try is that every finite top space has a basis given by its opens

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:35):

Here is the stuff you would need to do it this way:

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:35):

https://github.com/coq-community/topology/blob/master/theories/Topology/OpenBases.v

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:35):

Build_TopologicalSpace_from_open_basis

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:35):

This might be slightly more tractable

view this post on Zulip Ali Caglayan (Aug 01 2021 at 13:36):

I made some progress but became a bit disinterested 0:-)

view this post on Zulip Ben Siraphob (Aug 01 2021 at 15:54):

Ali Caglayan said:

I'm having a go at this now, however I noticed that the empty set isn't in your opens. Shouldn't you also include that?

This is fine because it's proved in TopologicalSpaces.v https://github.com/coq-community/topology/blob/b59526221debf2b5f55e8439cc9f9fec42d82339/theories/Topology/TopologicalSpaces.v#L24

view this post on Zulip Ben Siraphob (Aug 01 2021 at 15:55):

Ali Caglayan said:

I was able to get coq to automatically solve the later parts of the topology, however the first goal is quite difficult as you say. On paper I would do this by trying every element since everything is finite in X and the powerset etc. But this requires a lot of excluded middle I believe and I am not sure if it is constructively true... thought perhaps since X is decidable we can get away with it.

How did you get Coq to automatically solve the later parts?

view this post on Zulip Ali Caglayan (Aug 01 2021 at 18:22):

Something like this. When you define the topology inductively, you can add its constructors as hints to a hint database. Then auto can solve these.

From Topology Require Import TopologicalSpaces OpenBases.
Require Import Ensembles.
Import Powerset_facts.

Section TopSpaceEx1.

Inductive X : Type := a | b | c.
From ZornsLemma Require Export EnsemblesImplicit.

Inductive T : Ensemble X -> Prop :=
| t_empty : T Empty_set
| t_sing : T (Singleton b)
| t_coup_b_c : T (Couple b c)
| t_coup_a_b : T (Couple a b)
| t_full : T Full_set.

(** We create a hint database for dealing with this topology. *)
Create HintDb mytopology_hints.

(** We add the constructors of T as hints. *)
Hint Constructors T : mytopology_hints.

(** Inclusion of singleton into couple *)
Lemma Included_Singleton_Couple {U : Type} (x y : U)
  : Included (Singleton x) (Couple x y).
Proof.
  intros z.
  apply Singleton_ind.
  apply Couple_l.
Defined.

(** We add this as an immediate hint to coq. Immediate meaning it won't elaborate on it much. *)
Hint Immediate Included_Singleton_Couple : mytopology_hints.

(** Some ensemble lemmas *)

Lemma Intersection_Included {X : Type} {U V : Ensemble X}
  : Included U V -> Intersection U V = U.
Proof.
  intros p.
  apply Extensionality_Ensembles.
  split.
  - apply Intersection_decreases_l.
  - intros x v.
    apply Intersection_intro, p; assumption.
Defined.

Lemma Intersection_self {X : Type} {U : Ensemble X}
  : Intersection U U = U.
Proof.
  apply Intersection_Included.
  cbv; trivial.
Defined.

Lemma T_is_topology : TopologicalSpace.
Proof.
  refine (Build_TopologicalSpace X T _ _ _).
  - admit.
  - intros U V u v.
    destruct u, v.
    (** Do some rewriting passes (these can be done much more compactly). *)
    (** We need to rewrite the intersection in these cases *)
    4,5,8,9,12: rewrite Intersection_commutative.
    (** Intersections with full sets *)
    all: rewrite ?Intersection_Full_set, ?Intersection_Full_set'.
    (** Intersections with self *)
    all: rewrite ?Intersection_self.
    (** The rest of the intersections are intersections with subsets *)
    all: rewrite ?Intersection_Included.
    (** Finally, coq can solve the rest with our hints. *)
    all: auto with mytopology_hints.
  - auto with mytopology_hints.
Admitted.

End TopSpaceEx1.

view this post on Zulip Stéphane Desarzens (Aug 09 2021 at 05:26):

Ali Caglayan said:

I'm having a go at this now, however I noticed that the empty set isn't in your opens. Shouldn't you also include that?

This is fine because it's proved in TopologicalSpaces.v https://github.com/coq-community/topology/blob/b59526221debf2b5f55e8439cc9f9fec42d82339/theories/Topology/TopologicalSpaces.v#L24

No, this is not fine. Since the empty set is the union of the empty family, you'd fail to satisfy open_family_union.

To solve your initial problem, you could try to destruct FamilyUnion F somehow. Maybe doing case-analysis on which sets are elements of F.

view this post on Zulip Stéphane Desarzens (Aug 09 2021 at 05:27):

That's how I'd try to do it on paper.

view this post on Zulip Ben Siraphob (Aug 15 2021 at 18:38):

No, this is not fine. Since the empty set is the union of the empty family, you'd fail to satisfy open_family_union.

Ah, right. Thanks.


Last updated: Feb 06 2023 at 12:04 UTC