{"id":43,"date":"2018-11-30T23:25:35","date_gmt":"2018-11-30T22:25:35","guid":{"rendered":"http:\/\/pinkieduck.net\/?p=43"},"modified":"2019-02-22T22:54:23","modified_gmt":"2019-02-22T21:54:23","slug":"encore-un-peu-de-topologie-en-coq","status":"publish","type":"post","link":"https:\/\/pinkieduck.net\/?p=43","title":{"rendered":"Encore un peu de topologie en Coq"},"content":{"rendered":"\n

Seconde partie sur la s\u00e9rie autour de quelques preuves d’exercices classiques de topologie en Coq, on va s’attaquer cette fois encore \u00e0 un exercice de \u00ab\u00a0r\u00e9\u00e9criture\u00a0\u00bb de d\u00e9finitions, toujours tir\u00e9 de la m\u00eame feuille d’exercice :<\/p>\n\n\n\n

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\u00e9e par \\(\\Sigma\\)) est constitu\u00e9e des unions d\u2019ensembles de \\(\\Sigma\\), ou, de fa\u00e7on \u00e9quivalente,
\\(A\\in T \\iff \\forall x\\in A, \\exists S \\in \\Sigma, x\\in S \\subset A\\)
Montrer que l\u2019on peut affaiblir l\u2019hypoth\u00e8se de stabilit\u00e9 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\\).<\/p><\/blockquote>\n\n\n\n

L\u00e0 encore on va faire son march\u00e9 parmi les choses qu’on veut d\u00e9montrer : en particulier la premi\u00e8re partie me semble pas particuli\u00e8rement passionnante (c’est compliqu\u00e9 pour toutes les topologies y compris la plus petite de pas contenir au moins les unions d’ensemble) et donc on va passer directement \u00e0 l’hypoth\u00e8se affaiblie ; il suffit <\/span>1<\/sup><\/a><\/span> de prouver que cette hypoth\u00e8se combin\u00e9e \u00e0 la stabilit\u00e9 par union implique la stabilit\u00e9 par intersection finie.
<\/p>\n\n\n\n

En Coq<\/h1>\n\n\n\n

\nDans le code on utilisera la lettre S pour d\u00e9signer \\(\\Sigma\\)<\/span>2<\/sup><\/a><\/span>.\n\n<\/p>\n\n\n\n

\nLa stabilit\u00e9 par union est relativement simple \u00e0 \u00e9crire:\n\n<\/p>\n\n\n

\nDefinition hypothese_union (T:Type) (S:Family T) :=\n    forall S', Included S' S -> S (FamilyUnion S').\n<\/pre><\/div>\n\n\n
De m\u00eame que l’hypoth\u00e8se affaiblie de l’\u00e9nonc\u00e9, qui n’est qu’une traduction avec les mots cl\u00e9s Coq qui vont bien :<\/p>\n\n\n
\nDefinition hypothese_afaiblie (T:Type) (S:Family T) :=\n    forall (S1 S2:Ensemble T), \n    In S S1 ->\n    In S S2 ->\n    forall x, In (Intersection S1 S2) x ->\n    (exists S3, In S S3 \/\\ In S3 x \/\\ Included S3 (Intersection S1 S2)).\n<\/pre><\/div>\n\n\n
Il faut cependant se m\u00e9fier de l’apparente simplicit\u00e9 de ces d\u00e9finitions, un des \u00e9cueils auxquels j’ai \u00e9t\u00e9 confront\u00e9 en r\u00e9digeant la preuve qui va suivre est la facilit\u00e9 avec laquelle on oublie d’expliciter une appartenance ou une inclusion dans un th\u00e9or\u00e8me, et donc casse les preuves qui en d\u00e9coulent.<\/p>\n\n\n\n
Le th\u00e9or\u00e8me que l’on souhaite prouver :<\/p>\n\n\n
\nTheorem exo:\n    forall (T:Type) (S:Family T),\n    hypothese_union T S ->\n    hypothese_afaiblie T S ->\n    (forall S1 S2, In S S1 -> In S S2 -> In S (Intersection S1 S2)). \nProof.\n<\/pre><\/div>\n\n\n
Il peut \u00eatre utile de prendre un peu de recul sur ce qu’on cherche \u00e0 montrer : l’hypoth\u00e8se affaiblie nous dit que, \u00e0 d\u00e9faut de stabilit\u00e9 \u00ab\u00a0globale\u00a0\u00bb par intersection finie, cette propri\u00e9t\u00e9 vaut au moins localement. On peut alors s’en sortir en \u00ab\u00a0d\u00e9coupant\u00a0\u00bb une intersection en morceaux de S, et en r\u00e9unissant ces morceaux gr\u00e2ces \u00e0 l’hypoth\u00e8se de stabilit\u00e9 par union.
<\/p>\n\n\n\n
Malheureusement je n’ai pas trouv\u00e9 la plupart des th\u00e9or\u00e8mes \u00ab\u00a0intuitifs\u00a0\u00bb sur les ensembles et leurs \u00e9l\u00e9ments dans le module zorns-lemma et il va donc falloir les \u00e9crire. Trouver quels sont les th\u00e9or\u00e8mes dont on va avoir besoin est pas forc\u00e9ment facile et j’ai d\u00fb passer par pas mal de trial and errors avant de trouver comment m’en sortir, malgr\u00e9 l’apparente facilit\u00e9 de l’exercice.
<\/p>\n\n\n\n
Le  premier de ces th\u00e9or\u00e8mes : si pour tout \u00e9l\u00e9ment d’un ensemble E, on peut trouver un ensemble de S l’incluant, alors E est la r\u00e9union des \u00e9l\u00e9ments de S inclus dans E (si on n’avait pas l’hypoth\u00e8se de l’implication, il aurait \u00e9t\u00e9 possible d’avoir des \u00ab\u00a0bouts qui manquent\u00a0\u00bb dans E).
<\/p>\n\n\n
\nQed.\n\nTheorem union_of_elem (T:Type) (S:Family T) (E:Ensemble T):\n  (forall x, In E x -> exists S', In S S' \/\\ In S' x \/\\ Included S' E) ->\n  E=FamilyUnion (fun S' => In S S' \/\\ Included S' E).\nProof.\n<\/pre><\/div>\n\n\n
L\u00e0 encore on est dans des manipulations de d\u00e9finition donc on va pas mal spammer la tactique unfold. La preuve se d\u00e9roule alors relativement lin\u00e9airement.
<\/p>\n\n\n
\n  intros. apply Extensionality_Ensembles. unfold Same_set. unfold Included in *. split.\n  - unfold In. intros. destruct (H x H0). destruct H1. destruct H2.\n    apply family_union_intro with (S:=x0). intros. split.\n    + apply H1.\n    + intros. apply H3. apply H4.\n    +  apply H2.\n  - intros. destruct H0. unfold In in *. destruct H0. apply H2. apply H1.\nQed.\n<\/pre><\/div>\n\n\n
Le second th\u00e9or\u00e8me est peut-\u00eatre plus dispensable, je pense qu’il est possible de d\u00e9montrer directement le r\u00e9sultat sur les intersections. N\u00e9anmoins par souci de clart\u00e9 je le reproduis ici : il s’agit de montrer que rajouter l’hypoth\u00e8se de stabilit\u00e9 des unions au th\u00e9or\u00e8me pr\u00e9c\u00e9dent fait que E est dans S :<\/p>\n\n\n\n

<\/p>\n\n\n
\nTheorem function_app (T:Type) (S:Family T) (E:Ensemble T): \n  hypothese_union T S -> (forall x, In E x -> exists S', In S S' \/\\ In S' x \/\\ Included S' E) -> In S E.\nProof.\n\n<\/pre><\/div>\n\n\n
C’est surtout une application du th\u00e9or\u00e8me pr\u00e9c\u00e9dent:
<\/p>\n\n\n
\n  unfold hypothese_union. intros. pose (tmp:= union_of_elem T S E).\n  rewrite tmp. apply H. unfold Included at 1. intros. destruct H1. apply H1. apply H0.\nQed.\n<\/pre><\/div>\n\n\n
Enfin la d\u00e9monstration de l’exercice : ici il suffit de constater que le r\u00e9sultat pr\u00e9c\u00e9dent s’applique \u00e0 une intersection d’\u00e9l\u00e9ments de S, sachant que l’hypoth\u00e8se affaiblie est v\u00e9rifi\u00e9e. La preuve devient :<\/p>\n\n\n
\nProof.\n  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.\nQed.\n<\/pre><\/div>\n\n\n

<\/p>\n","protected":false},"excerpt":{"rendered":"
Seconde partie sur la s\u00e9rie autour de quelques preuves d’exercices classiques de topologie en Coq, on va s’attaquer cette fois encore \u00e0 un exercice de \u00ab\u00a0r\u00e9\u00e9criture\u00a0\u00bb de d\u00e9finitions, toujours tir\u00e9 de la m\u00eame feuille d’exercice : Soit un ensemble non vide et une famille de parties de stable par intersection finie et contenant . Montrer […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[2],"tags":[],"_links":{"self":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/43"}],"collection":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=43"}],"version-history":[{"count":20,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/43\/revisions"}],"predecessor-version":[{"id":90,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/43\/revisions\/90"}],"wp:attachment":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=43"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=43"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=43"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}