Archive | novembre 2018

Encore un peu de topologie en Coq

Nov30

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.


Un peu de topologie en Coq

Nov27

Apprendre un langage de preuve est particulièrement déroutant quand on est habitué aux langages de programmations « classiques » qu’ils soient fonctionnels ou non : la plupart des patterns classiques deviennent perdent leur pertinence pour du code qui ne sera pas exécuté, et il faut adopter une façon différente de « penser » qui s’attachent aux propriétés des choses et non au comment de leur réalisation. Cependant s’il est difficile de transposer les pratiques de programmation pour s’entrainer à manipuler le langage, les maths fournissent beaucoup de matériau qui lui sied particulièrement bien (ce qui n’est pas surprenant). J’ai choisi de m’intéresser à la topologie dans cette série de billets pour voir jusqu’où il est possible d’aller. Je conseille fortement d’avoir lu au moins le premier tome de software foundation pour bien profiter de cette série.

Pour l’instant je m’inspire librement de https://github.com/coq-contribs/topology et en particulier je vais utiliser comme lui le module https://github.com/coq-contribs/zorns-lemma qui contient une implémentation des familles dénombrables ou non d’ensembles, de propriétés sur les fonctions etc. Il existe peut-être d’autres implémentation ailleurs mais je n’en ai pas trouvé.

Installation

Afin de pouvoir utiliser simplement les modules coq public, j’utilise le gestionnaire de paquets opam. Ce dernier n’est pas disponible nativement sur Windows actuellement, il faut donc passer par Windows Subsystem for Linux. L’installation se fait classiquement, via apt install m4 opam pour l’image Debian ou Ubuntu, m4 s’avérant parfois requis par certains paquets opam.

On utilise ensuite opam, qui va installer les paquets dans le répertoire de l’utilisateur, et modifier le fichier profile pour que bash puisse trouver l’exécutable Coq.

opam init
opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq

Un premier exercice

Pour débuter, j’ai préféré rester modeste en choisissant un exercice relativement « tautologique » de topologie classique, trouvé sur cette liste : http://math.univ-lille1.fr/~bodin/exolic1/exolic.pdf :

Soit \(X\) un espace topologique, et \(f\) une application quelconque de \(X\) dans un ensemble \(Y\). On dit qu’une partie \(A\) de \(Y\) est ouverte, si \(f^{− 1}(A)\) est un ouvert de \(X\). Vérifier qu’on a défini ainsi une topologie sur \(Y\).

Sur les 3 axiomes définissant une topologie, celui sur l’appartenance de l’ensemble vide et de Y est relativement évident

1

, celui sur l’intersection fini est déjà défini dans zorns-lemma. Il reste donc l’axiome de stabilité par union.

Définitions d’ensemble, de réunion quelconque etc

La librairie standard de Coq propose une implémentation des ensembles https://coq.inria.fr/library/Coq.Sets.Ensembles.html : ces derniers contiennent juste une fonction d’appartenance de leur élément. On notera surtout la présence de l’axiome d’extensionalité (deux ensembles sont égaux s’ils sont inclus l’un dans l’autre) qu’on va utiliser dans la suite.

Coté zorns-lemma existe une définition de famille d’ensembles https://github.com/coq-contribs/zorns-lemma/blob/master/Families.v, qui correspond, de façon plutôt prévisible, à un alias sur les ensembles d’ensembles. Le type qui nous intéresse en particulier est celui de FamilyUnion, qui va « réduire » une famille en un ensemble. A noter que zorns-lemma propose aussi une version « indexed » des familles, version indexed qui, contrairement à ce que je pensais initialement, peut être indexée par n’importe quoi, et pas seulement par des entiers, et est probablement plus simple à manipuler ; cependant, dans la suite, je me base seulement sur le FamilyUnion classique.

On se lance

Premier point : définir l’ensemble réciproque d’une fonction. On pourrait certes utiliser la définition fournie par zorns-lemma, mais, vu que ce module ne fournit que très peu de propriétés sur les fonctions réciproques, le gain est minime.

From Topology Require Import TopologicalSpaces.

Definition img_recip (X Y:Type) (f:X->Y) (A: Ensemble Y) : Ensemble X:=

fun x => In A (f x).

Seconde étape, formuler l’égalité de l’union des images réciproques et de l’image réciproque de l’union. Pour plus de lisibilité, on va définir les deux séparément. D’un coté, on a l’image réciproque d’une union, relativement immédiate :

Definition img_recip_union (X Y:Type) (Fa: Family Y) (f:X->Y) :=

img_recip X Y f (FamilyUnion Fa).

De l’autre, on a la réunion des images réciproques, et c’est là où les choses commencent à se gâter. Si une FamilyUnion est une ensemble en premier lieu, il faut donc écrire une fonction d’appartenance, sauf que les éléments sont ici eux-mêmes des ensembles…dont la description nécessite quelques circonvolutions : il faut à la fois exprimer qu’on a l’image réciproque de quelque chose, et que ledit quelque chose est dans la famille de départ. J’avoue avoir galéré quelques temps avant de parvenir à écrire la définition, dont l’inélégance augure quelques prises de tête dans les futures preuves qui y seront rattachées :

Definition img_recip_union_as_fu (X Y:Type) (Fa: Family Y) (f:X->Y) : Ensemble X :=

FamilyUnion (fun S => exists F, In Fa F /\ S = (img_recip X Y f F)).

Il aurait probablement été plus simple de passer par les familles indexées (la faculté de « nommer » les ensembles qu’on manipule par leurs indices plutôt que par un quantifieur d’existence doit plutôt aider).

On pose enfin le théorème d’égalité des deux quantités :

Theorem union_img_inverse : forall (X Y : Type) (Fa:Family Y) (f:X->Y),

(img_recip_union_as_fu X Y Fa f) = (img_recip_union X Y Fa f).

Proof.

Comme énoncé préalablement, on reste sur un exercice plutôt tautologique, où on ne fait guère que renommer les choses. Par conséquent une grosse partie de la preuve va consister à utiliser en boucle la tactique unfold, qui va juste expliciter les définitions :

unfold img_recip_union_as_fu. unfold img_recip_union.

intros. unfold img_recip. unfold In.

On se retrouve avec une égalité entre deux ensembles.

apply Extensionality_Ensembles. split.

- unfold Included. unfold In. intros. destruct H eqn:Heqn. unfold In in i. destruct i eqn:ieqn. destruct a.

apply family_union_intro with (S:=x0). subst. apply f0. unfold In in i0. unfold In. subst. apply i0.

- unfold Included. intros. unfold In in H. Print FamilyUnion. remember (f x) as fx. destruct H.

eapply family_union_intro with (S:=fun x1 : X => S (f x1)). unfold In. exists S. split. apply H. trivial.

unfold In. rewrite <- Heqfx. apply H0.

Qed.