Apprendre un langage de preuve est particuli\u00e8rement d\u00e9routant quand on est habitu\u00e9 aux langages de programmations \u00ab classiques \u00bb qu’ils soient fonctionnels ou non : la plupart des patterns classiques deviennent perdent leur pertinence pour du code qui ne sera pas ex\u00e9cut\u00e9, et il faut adopter une fa\u00e7on diff\u00e9rente de \u00ab penser \u00bb qui s’attachent aux propri\u00e9t\u00e9s des choses et non au comment de leur r\u00e9alisation. Cependant s’il est difficile de transposer les pratiques de programmation pour s’entrainer \u00e0 manipuler le langage, les maths fournissent beaucoup de mat\u00e9riau qui lui sied particuli\u00e8rement bien (ce qui n’est pas surprenant). J’ai choisi de m’int\u00e9resser \u00e0 la topologie dans cette s\u00e9rie de billets pour voir jusqu’o\u00f9 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\u00e9rie.<\/p>\n\n\n\n
Pour l’instant je m’inspire librement de https:\/\/github.com\/coq-contribs\/topology<\/a> et en particulier je vais utiliser comme lui le module https:\/\/github.com\/coq-contribs\/zorns-lemma<\/a> qui contient une impl\u00e9mentation des familles d\u00e9nombrables ou non d’ensembles, de propri\u00e9t\u00e9s sur les fonctions etc. Il existe peut-\u00eatre d’autres impl\u00e9mentation ailleurs mais je n’en ai pas trouv\u00e9.<\/p>\n\n\n\n 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\u00e9rant parfois requis par certains paquets opam.<\/p>\n\n\n\n On utilise ensuite opam, qui va installer les paquets dans le r\u00e9pertoire de l’utilisateur, et modifier le fichier profile pour que bash puisse trouver l’ex\u00e9cutable Coq.<\/p>\n\n\n\n Pour d\u00e9buter, j’ai pr\u00e9f\u00e9r\u00e9 rester modeste en choisissant un exercice relativement \u00ab tautologique \u00bb de topologie classique, trouv\u00e9 sur cette liste : http:\/\/math.univ-lille1.fr\/~bodin\/exolic1\/exolic.pdf<\/a> :<\/p>\n\n\n\n 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^{\u2212 1}(A)\\) est un ouvert de \\(X\\). V\u00e9rifier qu’on a d\u00e9fini ainsi une topologie sur \\(Y\\).<\/p><\/blockquote>\n\n\n\n Sur les 3 axiomes d\u00e9finissant une topologie, celui sur l’appartenance de l’ensemble vide et de Y est relativement \u00e9vident <\/p>\n\n\n<\/span>1<\/sup><\/a><\/span>\n\n\n\n , celui sur l’intersection fini est d\u00e9j\u00e0 d\u00e9fini dans zorns-lemma. Il reste donc l’axiome de stabilit\u00e9 par union.<\/p>\n\n\n\n La librairie standard de Coq propose une impl\u00e9mentation des ensembles https:\/\/coq.inria.fr\/library\/Coq.Sets.Ensembles.html<\/a> : ces derniers contiennent juste une fonction d’appartenance de leur \u00e9l\u00e9ment. On notera surtout la pr\u00e9sence de l’axiome d’extensionalit\u00e9 (deux ensembles sont \u00e9gaux s’ils sont inclus l’un dans l’autre) qu’on va utiliser dans la suite.<\/p>\n\n\n\nInstallation<\/h1>\n\n\n\n
opam init\nopam repo add coq-released http:\/\/coq.inria.fr\/opam\/released\nopam install coq<\/pre><\/pre>\n\n\n\n
Un premier exercice
<\/span><\/h1>\n\n\n\nD\u00e9finitions d’ensemble, de r\u00e9union quelconque etc
<\/span><\/h2>\n\n\n\n