## Stream: Coq users

### Topic: building a simple topology

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

End TopSpaceEx1.

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

#### 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

#### 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?

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

#### 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

#### Ali Caglayan (Aug 01 2021 at 13:35):

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

#### Ali Caglayan (Aug 01 2021 at 13:35):

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

#### Ali Caglayan (Aug 01 2021 at 13:35):

Build_TopologicalSpace_from_open_basis

#### Ali Caglayan (Aug 01 2021 at 13:35):

This might be slightly more tractable

#### Ali Caglayan (Aug 01 2021 at 13:36):

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

#### 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

#### 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?

#### 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 _ _ _).
- 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.

End TopSpaceEx1.

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

#### Stéphane Desarzens (Aug 09 2021 at 05:27):

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

#### 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: Jun 23 2024 at 23:01 UTC