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.
```

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.

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

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?

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.

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

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

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

Build_TopologicalSpace_from_open_basis

This might be slightly more tractable

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

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

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?

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.
```

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`

.

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

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: Sep 30 2023 at 05:01 UTC