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.