Seconde partie sur la série autour de quelques preuves d’exercices classiques de topologie en Coq, on va s’attaquer cette fois encore à un exercice de « réécriture » de définitions, toujours tiré de la même feuille d’exercice :
Soit \(X\) un ensemble non vide et \(\Sigma\) une famille de parties de \(X\) stable par intersection finie et contenant \(X\). Montrer que la plus petite topologie \(T\) contenant \(\Sigma\) (la topologie engendrée par \(\Sigma\)) est constituée des unions d’ensembles de \(\Sigma\), ou, de façon équivalente,
\(A\in T \iff \forall x\in A, \exists S \in \Sigma, x\in S \subset A\)
Montrer que l’on peut affaiblir l’hypothèse de stabilité par intersection finie en :
\(\forall S_1, S_2 \in \Sigma, \forall S \in S_1 \cap S_2, \exists S_3 \in \Sigma, x\in S_3 \subset S_1 \cap S_2\).
Là encore on va faire son marché parmi les choses qu’on veut démontrer : en particulier la première partie me semble pas particulièrement passionnante (c’est compliqué pour toutes les topologies y compris la plus petite de pas contenir au moins les unions d’ensemble) et donc on va passer directement à l’hypothèse affaiblie ; il suffit 1 de prouver que cette hypothèse combinée à la stabilité par union implique la stabilité par intersection finie.
En Coq
Dans le code on utilisera la lettre S pour désigner \(\Sigma\)2.
La stabilité par union est relativement simple à écrire:
Definition hypothese_union (T:Type) (S:Family T) :=
forall S', Included S' S -> S (FamilyUnion S').
De même que l’hypothèse affaiblie de l’énoncé, qui n’est qu’une traduction avec les mots clés Coq qui vont bien :
Definition hypothese_afaiblie (T:Type) (S:Family T) :=
forall (S1 S2:Ensemble T),
In S S1 ->
In S S2 ->
forall x, In (Intersection S1 S2) x ->
(exists S3, In S S3 /\ In S3 x /\ Included S3 (Intersection S1 S2)).
Il faut cependant se méfier de l’apparente simplicité de ces définitions, un des écueils auxquels j’ai été confronté en rédigeant la preuve qui va suivre est la facilité avec laquelle on oublie d’expliciter une appartenance ou une inclusion dans un théorème, et donc casse les preuves qui en découlent.
Le théorème que l’on souhaite prouver :
Theorem exo:
forall (T:Type) (S:Family T),
hypothese_union T S ->
hypothese_afaiblie T S ->
(forall S1 S2, In S S1 -> In S S2 -> In S (Intersection S1 S2)).
Proof.
Il peut être utile de prendre un peu de recul sur ce qu’on cherche à montrer : l’hypothèse affaiblie nous dit que, à défaut de stabilité « globale » par intersection finie, cette propriété vaut au moins localement. On peut alors s’en sortir en « découpant » une intersection en morceaux de S, et en réunissant ces morceaux grâces à l’hypothèse de stabilité par union.
Malheureusement je n’ai pas trouvé la plupart des théorèmes « intuitifs » sur les ensembles et leurs éléments dans le module zorns-lemma et il va donc falloir les écrire. Trouver quels sont les théorèmes dont on va avoir besoin est pas forcément facile et j’ai dû passer par pas mal de trial and errors avant de trouver comment m’en sortir, malgré l’apparente facilité de l’exercice.
Le premier de ces théorèmes : si pour tout élément d’un ensemble E, on peut trouver un ensemble de S l’incluant, alors E est la réunion des éléments de S inclus dans E (si on n’avait pas l’hypothèse de l’implication, il aurait été possible d’avoir des « bouts qui manquent » dans E).
Qed.
Theorem union_of_elem (T:Type) (S:Family T) (E:Ensemble T):
(forall x, In E x -> exists S', In S S' /\ In S' x /\ Included S' E) ->
E=FamilyUnion (fun S' => In S S' /\ Included S' E).
Proof.
Là encore on est dans des manipulations de définition donc on va pas mal spammer la tactique unfold. La preuve se déroule alors relativement linéairement.
intros. apply Extensionality_Ensembles. unfold Same_set. unfold Included in *. split.
- unfold In. intros. destruct (H x H0). destruct H1. destruct H2.
apply family_union_intro with (S:=x0). intros. split.
+ apply H1.
+ intros. apply H3. apply H4.
+ apply H2.
- intros. destruct H0. unfold In in *. destruct H0. apply H2. apply H1.
Qed.
Le second théorème est peut-être plus dispensable, je pense qu’il est possible de démontrer directement le résultat sur les intersections. Néanmoins par souci de clarté je le reproduis ici : il s’agit de montrer que rajouter l’hypothèse de stabilité des unions au théorème précédent fait que E est dans S :
Theorem function_app (T:Type) (S:Family T) (E:Ensemble T):
hypothese_union T S -> (forall x, In E x -> exists S', In S S' /\ In S' x /\ Included S' E) -> In S E.
Proof.
C’est surtout une application du théorème précédent:
unfold hypothese_union. intros. pose (tmp:= union_of_elem T S E).
rewrite tmp. apply H. unfold Included at 1. intros. destruct H1. apply H1. apply H0.
Qed.
Enfin la démonstration de l’exercice : ici il suffit de constater que le résultat précédent s’applique à une intersection d’éléments de S, sachant que l’hypothèse affaiblie est vérifiée. La preuve devient :
Proof.
intros. apply function_app. apply H. intros. unfold hypothese_afaiblie in *. pose (tmp:= H0 S1 S2 H1 H2 x H3). destruct tmp. exists x0. apply H4.
Qed.