Ben Siraphob (Jul 31 2021 at 14:49): 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.
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 _ _ _).
- 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.
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: Oct 13 2024 at 01:02 UTC