Retrospective on learning Haskell

Mar1

It’s been something like 6 months that I started using Haskell for real and I think I’ve got past the point where I can say that I’m comfortable with it ; it’s usually the good time to take a halt and look back and identify the things that weren’t as smooth as one could have hoped.

The good part

At its core Haskell is an amazingly simple language: after you know how to define and call functions and how to define new types and type classes, there aren’t a lot of feature left to understand. I made a small presentation in my company saying that you can learn Haskell syntax in 10 minutes, it actually took 20. That’s still way below the time it takes to learn all the oddities of a language like C++.

The IDE support is quite good. Yes I know there are all kind of memes around this fact on Internet, yet there’s now a Langage Server Protocol for it which is very decent. It still struggles for big projects, for some reason it doesn’t work if there is a compilation failure when I start VS Code and may lack some refactoring tool (like renaming symbols) but other than that I can’t complain: it’s able to show the type of each variable and function in the code, and even with documentation when available, and jumping to definition just works. It also shows unused imports and language imports, something I wish was available for more mature language like C++.

Writing in Haskell helps practice Category Theory concept. Category Theory defines a lot of concepts which I often met with a « so what ? » mood at first read, but their relevance becomes so much more obvious when using them. For fun I ported a 300 lines code that parsed a specific CSV file from Python, and I ended up with something like 15 occurrences of a functor and 11 occurrences of a monad. I have yet to see how some other concepts like Adjunction translate in Haskell and read all the paper about the Categorical Language Query language which uses fibration.

The bad part

Haskell libraries are real beasts. Most of them have very useful features but it always feels like I’m learning a whole new subject each time I just want to use something. The lens libraries are really satisfying to use but there are tons of operators to discover. When reading about parsing in Haskell (one of it’s strengths) I encountered lot of daunting terms like Alternative functor and monadPlus, the former apparently being « just a monoid in a (non canonical) monoidal category »… It’s always challenging.

I can’t mention having 2 build tools is confusing a lot when beginning. As far as I understand Cabal is handling dependencies and Stack is handling the versioning of these dependencies, but apparently Cabal seem to have gained some functionalities lately in this department.

I discovered the hard way that the base library is unsafe which is non-diegetic for a langage that focus so much on safety. The (!!) function for instance doesn’t return a Maybe but an object, and if it fails it crashes. The solution is to use another base library (called relude) in the Stack/Cabal dependencies. It’s something that’s not emphasized enough in my opinion (I discovered it while browsing Zulip funprog channel).

Equality in type theory

Jan11

I’m always amazed by how many subtle assumptions we often make when doing day-to-day maths, and how challenging these assumptions yield to some interesting construct.

I’m currently trying to read the Homotopy Type Theory (« Hott ») book. HoTT is an extension of type theory which is the underlying logic foundation of most proof assistant.
It uses the « proposition as type » idea which identifies some usual logical building block like conjunction, disjunctions, implications, quantifiers… with usual (and sometimes less usual) programming type constructs like algebraic types, functions…

One of the most important logical building block covered by type theory is the equality. To be honest I never really thought what « being equals to » really mean before reading the book, besides the usual « it’s just another equivalence relation between things ». But that’s neither a definition nor a satisfying properly, as for instance you can name several other equivalence like isomorphism which wouldn’t act as a good replacement for equality in most context.

Type theory gives two answers to this question : the first one is the definitional equality, or equality by definition. This equality comes from the fact that some composite type can be « reduced » : breaking a tuple into its component, or applying an argument to a function yield simpler syntaxical construct ; for instance in this framework (\x -> x + x)(1) (applying « 1 » to the lambda function which transforms « x » to « x + x ») is definitionally equals to 2, or fst (x, y) is definitionally equals to x. It’s just a matter of « following your nose » and determining if 2 objects are definitionally equal should better be decidable.
Unfortunatly not every equality is decidable in the day to day maths world : equality for reals is not decidable, there is no magic method to determine if 2 sides of an equation are equals. This means we need another kind of equality and here lie the second answer provided by type theory.
Type theory introduce an identity type, sometimes called « judgemental equality ». It’s a proposition and not merely a syntaxical rewriting. However the computation and uniqueness principle are designed to capture the defining property of equality which was hinted by the definitional equality : If two objects x and y are equals, then you can replace x by y in any proposition containing y (it’s a bit more involving but it’s the overall idea). Note that identity type is a generalisation of the definitional equality : an introduction rule for the identity type is equality by reflexivity, ie an object x is equals to itself. Since two definitionnaly equals objects are really just the same object in this framework, 2 definitionnally equals object are also judgmentally equals. But what are the others way to introduce equality then ?

That’s where Homotopy type theory comes into play. There are several answer to this question : one is that reflexivity is always the only way to introduce equality, and thus if 2 objects are equals one can consider that they are really the same. This is the logic under the Extensional Type Theory. There are several consequence to this design choice that I won’t cover.
On the other hand, homotopy type theory allows other kinds of « equalities » with root in homotopy (a subfield of topology as far as I understand which studies continuous path, path between path, and so on). It gives rise to a whole new interpretation of equality that is at the hearth of the book : objects are not merely « element in a set » but become « points in a space » whose path between point are equality relation.

I will write more on it later.

Proving that euclidian algorithm complexity is at most logarithmic

Oct2

I’m helping lately with C++ teaching for students with some mathematical background; obviously, you can’t avoid the topic of recursion at some point and it comes with the stereotypical exercises about factorial, Fibonacci sequences and computation of the Greatest Common Denominator.

The students are asked to write a naive (eg not tail recursive) recursive Fibonacci algorithm and to witness that it triggers a stack overflow for index like 60. We then ask them to write the GCD algorithm and to explain why it is robust even with big input.

It boils down to the argument that every two step the size of the input is halved, that is if $a$ and $b$ are natural numbers then $a \mod b \leq \frac{a}{2} $. The proof is quite simply and involves a case analysis so I thought it would be a nice opportunity to write a coq proof.

I’m using mathcomp and ssrnat type for this task. Manipulating equations in Coq is cumbersome since it involves issuing all intermediate steps including the most trivial ones like reassociating operators or commutating operands. That’s why vanilla Coq provides a couple of tactics that help proving that some equation hold, namely:

lia (previously omega) which stands for linear integer arithmetic. It tries to prove equations or inequalities where both left hand side and right hand side are of the form $\sum C_i x_i \geq 0$ where the $C_i$ are some integer constants.
lra which stands for linear rational arithmetic, which is the same, except that it works for real numbers.
nia which stands for nonlinear integer arithmetic. I’m not sure which kind of equations it covers, according to the doc ¹ it uses lia under the hood.
nra which is the same as nia but for rational number.

These tactics are not available to mathcomp natively but fortunately latest Coq version (from 8.11 I think) provides a Zify module which allows to add support for custom type for these tactics. Kazuhiko Sakaguchi wrote a lib, mczify (for MathComp Zify), which add supports for at least ssrbool and ssrnat; this lib is not on opam yet but we can build it and add it to our opam installation quite easily:

First you need to clone the repository: https://github.com/math-comp/mczify with the branch corresponding to your coq version (coq-8.11 or coq-8.12 at the time of writing, master doesn’t work with coq 8.12) and add an opam file whose content is given below.
Then you can call « opam install . » to make it build mczify and install it in our opam folder.

opam-version: "2.0"
maintainer: "pi8027@gmail.com"
homepage: "https://github.com/math-comp/mczify"
bug-reports: "https://github.com/math-comp/mczify/issues"
dev-repo: "git+https://github.com/math-comp/mczify.git"
license: "CECILL-C"
authors: [
  "Kazuhiko Sakaguchi"
]
build: [
  [make "INSTMODE=global"]
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
depends: [
  "coq" { ((>= "8.10" & < "8.13~") | = "dev") }
  "coq-mathcomp-field"       {(>= "1.11.0" & < "1.12~")}
  "coq-mathcomp-finmap"      {(>= "1.5.0" & < "1.6~")}
]
synopsis: "An analysis library for mathematical components"
description: """
This repository contains an experimental library for real analysis for
the Coq proof-assistant and using the Mathematical Components library.

It is inspired by the Coquelicot library.
"""
tags: [
  "category:Mathematics/Real Calculus and Topology"
  "keyword: analysis"
  "keyword: topology"
  "keyword: real numbers"
  "logpath: mathcomp.analysis"
  "date:2020-08-11"
]

Now we can check that we correctly installed zify by importing it as well as all the ssrnat and div libs:

From mathcomp Require Import ssreflect ssrnat div ssrbool.
From mathcomp Require Import zify.

Now we can start proving our proof script. Formulating the lemma isn’t complicated. I added some hypotheses ($ b \neq 0$ and $ a \ge b$) that I found necessary while writing the proof. They really don’t change the scope of what we’re trying to prove though.

Lemma half: forall a b : nat, 0 < b -> a >= b -> a %% b <= a %/ 2.

Now the proof. We will follow the proof by case here. The first step is to move all our hypotheses from the goal to the context:

move => a b H0 H1.

And then do the case analysis. While this may sound trivial in classical logic, we’re working with constructive mathematic, where the excluded middle lemma doesn’t hold in general. This is however the case for our example : the comparison function on nat ($\leq$) is actually a decision procedure, meaning that there is an algorithm that can compute a result for $a \leq b$ where $a$ and $b$ are natural number. Note that this isn’t true for every type: for instance, it is known² that equality on the real type isn’t decidable and so inequality isn’t either.

This means that the case tactic requires us to provide a proof that there is actually two cases (and thus as the expression is decidable). For reference in vanilla Coq one would look for something of the form :

forall (a b:nat), {a <= b} + {a > b}

In mathcomp however the lemma is a little less obvious : it’s leqP whose type is :

Lemma leqP m n : leq_xor_gtn m n (minn n m) (minn m n) (maxn n m) (maxn m n) (m <= n) (n < m).

It’s a common trick used in several place of mathcomp where some lemma use an intermediate inductive type which embeds various consequences of a case analysis. Here we see what’s happening if we look at what leq_xor_gtn embeds :

Variant leq_xor_gtn m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
  | LeqNotGtn of m <= n : leq_xor_gtn m n m m n n true false
  | GtnNotLeq of n < m  : leq_xor_gtn m n n n m m false true.

This reads as : there is two case (LeqNotGtn and GtnNotLeq), and for instance in the first case (min n m) and (min m n) is m, (max n m) and (max m n) is n, (m <= n) is true and (m < n) is false.

So now we can do our case analysis and put the case in the context :

case (leqP b (a %/2)) => H.

First case is trivial: it’s $b \le \frac{a}{2}$. We just need to notice that $a \mod b \le b$ which is provided by ltn_pmod lemma :

    apply: leq_trans.
    apply: ltnW.
    apply: ltn_pmod.
    by []. by [].

Second case is a little more involving: we will use the fact that the quotient of $a$ per $b$ is at least $1$ so $a\mod b \leq a – b$ which in turns is less than $\frac{a}{2}$ due to the hypothesis.

First let’s prove that $a / b\leq b$, it relies on the lemma leq_divRL which proves : (m <= n %/ d) = (m * d <= n).

    have: 1 <= a %/b.
        rewrite leq_divRL.
        by rewrite mul1n. by [].

Now let’s transform the goal into $ a – (a / b) * b \leq \frac{a}{2}$ ; for that we will use the lemma divn_eq (which expand $a$ into $a = (a / b) * b + a \mod b$) but it’s not enough : we want to substitute $a \mod b $ so we need to have an expression of the form $ a\mod b = \cdots$. This can be tedious to do manually and that’s where the tactic presented earlier comes in handy. Since it’s just substracting a term on both side of the equation, lia is enough.

    have: a %% b = a -  a %/ b * b.
        move: (divn_eq a b).
        lia.
    move ->.

Now all the elements are in place. An opportunistic call to the tactic nia (since this time there is a little more than moving integers expression between sides of an equation) finishes the proof:

    nia.

For reference here is the complete script proof:

From mathcomp Require Import ssreflect ssrnat div ssrbool.
From mathcomp Require Import zify.

Lemma half: forall a b : nat, 0 < b -> a >= b -> a %% b <= a %/ 2.
Proof.
    move => a b H0 H1.
    case (leqP b (a %/2)) => H.
        apply: leq_trans.
        apply: ltnW.
        apply: ltn_pmod.
        by []. by [].

    have: 1 <= a %/b.
        Check leq_divRL.
        rewrite leq_divRL.
        by rewrite mul1n. by [].

    have: a %% b = a -  a %/ b * b.
        move: (divn_eq a b).
        lia.
    move ->.
    nia.
Qed.

Yoneda lemma and Cayley theorem

Sep2

On Wikipedia’s page for Yoneda lemma (https://en.wikipedia.org/wiki/Yoneda_lemma) the authors mentions that the lemma is a vast generalization of the Cayley’s theorem. Whoever has ever seen the usual proof of these theorems has the intuition that there is a kind of similitude between them.

In Cayley’s theorem case you take a function that composes its input by a constant $g$ and discover that it shifts the element of the group, it sort of rearranges the elements of this group which is another way to say that it’s a member of the symmetric group of $G$. By varying the $g$ you end up with a group of functions and this group is included in the group of all symmetric group.

In Yoneda’s lemma case if we consider the Yoneda embedding functor, lifting a morphism yields a function which postpend this morphism to the input of the function, transforming a homset into another homset. If the source and destination homset are the same, we’re again somehow rearranging a set.

While this handwavy explanation suffices to give some intuition, let us dive into a more solid proof.

Group definitions

We recall some basic definitions so that everyone gets to the same point.

A group is a set G with a composition law which we may call $\otimes$ that has the following properties:

It has a neutral element $e$ on the left- and right-hand side: for all element $g$ of $G$, $e \otimes g = g \otimes e = g$.
It is associative : for all $x, y, z$ we have $(x \otimes y) \otimes z = x \otimes (y \times z)$ which we may abbreviate by omitting the parenthesis as $x \otimes y \otimes z$.
And for all element $x$ there is an inverse noted $x^{-1}$ such that $ x \otimes x^{-1} = e$.

The symmetric group over $X$ is the group of function from $X$ to $X$ that are bijective: an element of this group can be seen as a « permutation » of all elements of $X$. We may also call it the group of automorphism of $X$.

Given a group $G$ and a set $X$, an action on group is a function $\phi: G\times X\to X$ such that :

For the identity element, $\phi(e, x) = x$.
For any element $x, y\in G$, we say that the composition is compatible: $\phi ( x \otimes y, z) = \phi (x, \phi (y, z))$.

In a way an action on group is « applying » a group structure to a set. It is obviously an automorphism as an action $\phi(g, .)$ has an inverse $\phi(g^{-1}, .)$.

The group of all actions of a group on $X$ is included in the group of automorphism of $X$.

Then the Cayley theorem states that a group $G$ is isomorphic to a subgroup of the symmetric group over $G$.

Category theory definitions

We recall some basic definitions.

Given a (small) category $\mathcal{C}$, a homset between x and y is the set of all arrow between object x and y and is noted $Hom(x, y)$. This is really a set, that is an object of the category $\textbf{Set}$.

Given an object $X$, the Hom functor $Hom(X, -)$ is a functor from $\mathcal{C}$ to $\textbf{Set}$ which maps an object $Y$ to $Hom(X,Y)$ and which maps an arrow $f:A\to B$ to a function $Hom(X,f): Hom(X, A)\to Hom(X, B)$ such that forall arrow $g$ in $Hom(X,A)$, we have $Hom(X,f)(g) = g.f$ (we postpend the function).

The Yoneda embedding $Y$ takes a step back: it’s a functor that maps an object $X$ to the Hom functor $Hom(X, -)$. Any arrow $f:Y\to X$ maps a functor $Hom(X, -)$ to a functor $Hom(Y, -)$ (note that we take the reverse arrow) ; this mapping happens to be a natural transformation.

A functor $F$ between a category $\mathcal{C}$ and $\mathcal{D}$ induces a mapping on homsets : if $X$ and $Y$ are objects in $\mathcal{C}$, there is a mapping $Hom(X,Y)\to Hom(F(X), F(Y))$. We say that this functor is faithfull if this mapping is injective, full if this mapping is surjective.

There are two versions of the Yoneda lemma available: the first one states that the Yoneda functor is full and faithful. The second one is a bit more generic and states that $Nat(Hom(X, .), F(.))$ and $F(X)$ are naturally isomorphic for all X but we won’t use it.

Group in a category

Now we will look at group with a categorical point of view.

A group $G$ can be regarded as a category with a single arbitrary object and all elements as arrows. Composition, associativity, and existence of an identity morphism are respected by virtue of the group laws. In the following the arbitrary object will be represented by $\bullet$.

A functor $F$ between a group and the $\textbf{Set}$ category is an action on group :

For every arrow $f:\bullet\to\bullet$, $F(f)$ is an arrow from $F(\bullet)$ in $\textbf{Set}$ to $F(\bullet)$, which means it’s a function from a set to itself.
The identity arrow $Id_{\bullet}$ is lifted to $Id_{F(\bullet)}$.
For all arrow x and y $\bullet\to\bullet$, $x . y$ is lifted to $F(x . y) = F(x) . F(y)$ which is the compatibility property of the action on law.

The converse is also true : given a group action $\phi: G \times X \to X$, we can build a functor $F$ by taking $F(\bullet) = X$, and for $x\in G, F(x) = \phi(x, .)$. If we got another $y$ then the compatibility property ensures that $F(x).F(y) = \phi(x, \phi(y, .)) = \phi(x\otimes y, .) = F(x.y)$.

Proving the connection

We already saw some functors between a group and the $\textbf{Set}$ category: the hom functors. We even got the Yoneda embedding $Y$ which is a functor that provides us with such functor.

Let’s apply the Yoneda lemma on our group category’s object: $Hom(\bullet, \bullet)\to Hom(Y(\bullet), Y(\bullet))$ is an isomorphism.

Now let’s have a closer look at the mapping: the left hand-side is $Hom(\bullet, \bullet)$, that is all the morphisms of our group as a category. If you remember how we built our group as a category this means this set consists of all the elements of our group.

If we look at the right hand-side of the mapping, $Hom(Y(\bullet), Y(\bullet))$ are the morphisms of a functor from the group as a category to $\textbf{Set}$, that is the action of the group on a set.
And this is not any set : the expression of the Yoneda embedding tells us that $Y(\bullet) = Hom(\bullet, -)$ and again, there is only a single object of the category so we’re talking about $Hom(\bullet, \bullet)$ here that is the group itself.

If we recap the Yoneda lemma on a group as a category tells us that a group is isomorphic to the group of action of this group on itself. Since the group of action of this group on itself is a subgroup of the group of automorphism of the group, we have proven that a group is isomorphic to a subgroup of the symmetric group of this group.

References

In french : http://www.les-mathematiques.net/phorum/read.php?16,2085554

Produit de topologie en Coq

Jan27

Voici l’exercice qu’on va abordé dans ce billet :

Soit $(X, T )$ un espace topologique séparé. Montrer que la diagonale $\Delta$ de $X ×X$ est fermée dans
$X × X$.
http://math.univ-lille1.fr/~bodin/exolic1/exolic.pdf

Aparté sur les topologies initiales

Mon livre de topologie définit les produits de topologies comme la topologie initiale des fonctions de projections $p_i = (x_1, x_2) \in X, X \to x_i$. Ce qui nous amène à regarder ce qu’est une topologie initiale.

Pour être transparent, je vois également le terme de « topologie faible » utilisé ; c’est justement le terme utilisé par coq-topology… Je n’ai pour l’instant pas trouvé s’il y a une différence entre les 2 concepts, dans la suite je pars du principe qu’il s’agit de la même chose.

Une topologie initiale permet de construire une topologie sur un espace qui n’en dispose pas à partir de fonctions de cet espace sur un espace qui, lui, est topologique. Ainsi, si on dispose d’un espace X, et de fonctions $f_i:X \to Y_i$ avec $Y_i$ topologique, on définit une topologie sur X comme étant l’ensemble des intersections des $f_i^{-1}(O_i)$ avec $O_i$ ouvert de $Y_i$. Ceci permet d’assurer que, par construction, ces fonctions sont continues.

Dans le cas des fonctions produits, les ouverts sont donc de la forme $O_1 x O_2$ avec $O_1$ un ouvert de $Y_1$ et $O_2$ un ouvert de $Y_2$.

Preuve en Coq

Le module coq-topology dispose d’un module ProductTopology qui lui-même se base sur le module WeakTopology qui implémente les définitions du paragraphe précédent.

Comme souvent la principale difficulté n’est pas à trouver dans les mathématiques, il ne s’agit que de dérouler des définitions ; en revanche, ces définitions sont particulièrement peu digestes en Coq.

On va utiliser également les axiomes de séparations déjà définis dans coq-topology.

From Topology Require Import TopologicalSpaces.
From Topology Require Import InteriorsClosures.
From Topology Require Import Neighborhoods.
From Topology Require Import ProductTopology.
From Topology Require Import SeparatednessAxioms.

On dispose de quelques fonctions dans coq-topology pour faciliter l’écriture de produit de 2 topologies, qui se basent sur les fonctions built-in fst et snd de Coq. L’énoncé devient :


Theorem exo (X:TopologicalSpace):
  Hausdorff X -> closed (fun x:point_set (ProductTopology2 X X) => fst x = snd x).
Proof.

On va déplier les définitions :

  unfold Hausdorff.
  intros HypSep.
  unfold closed.

Pour plus de lisibilité, on va associer à l’ensemble $\Delta$ une variable :

  remember (Complement (fun x : point_set (ProductTopology2 X X) => fst x = snd x)) as ExtDiagonale.

On passe ensuite par un résultat intermédiaire sur cette diagonale pour caractériser les éléments qui y appartiennent :

  assert (forall x y, not (x=y) <-> In ExtDiagonale (x,y)).
  split;intros.
  - rewrite HeqExtDiagonale. eauto with sets.
  - rewrite HeqExtDiagonale in H. eauto with sets.

Pour résoudre l’exercice, on va utiliser une base des ouverts sur le produit de topologie.

  - refine (coverable_by_open_basis_impl_open (ProductTopology2_basis X X) _ _ _). apply ProductTopology2_basis_is_basis.
    intros x0 x0inExtDiag. assert (x0 = (fst x0, snd x0)). apply surjective_pairing. rewrite H0 in x0inExtDiag. pose (tmp:=H (fst x0) (snd x0)). rewrite <- tmp in x0inExtDiag. destruct (HypSep (fst x0) (snd x0) x0inExtDiag) as [U [V ]].
    exists (fun x => In U (fst x) /\ In V (snd x)). inversion H1 as [openU [openV [x0InU [x0inV InterUVEmpty]]]].
    split.
    + replace (fun x : point_set X * point_set X => In U (fst x) /\ In V (snd x)) with [p : point_set (ProductTopology2 X X) | let (x, y) := p in In U x /\ In V y]. constructor ; repeat assumption. simpl. apply functional_extensionality. intros. Search ([_:_ | _]). rewrite characteristic_function_to_ensemble_is_identity. autounfold with *. assert (x=(fst x, snd x)). apply surjective_pairing. rewrite H2. simpl. trivial.
    + split.
      * autounfold with *. intros. pose (tmp2:=surjective_pairing x). rewrite tmp2. rewrite <- H. unfold In in H2. inversion H2. unfold not. intro. rewrite H5 in H3. assert(In (Intersection U V) (snd x)). eauto with *. rewrite InterUVEmpty in H6. Search Empty_set. apply Noone_in_empty in H6. assumption.
      * autounfold with *. eauto with *.
Qed.

Séparation en Coq

Jan19

On continue dans la série des espaces topologiques avec un exercice sur les axiomes de séparation :

Soit $(X, T )$ un espace topologique.
Montrer que les conditions suivantes sont équivalentes :
(i) $\forall x, y \in X, x \neq y, \exists V \text{voisinage de}x, y \notin V .$
(ii) $\forall x \in X, {x} fermé.$
(iii) $\forall x \in X, {V ; V \text{voisinage de }x} = {x}.$
Soit $(X, T )$ ainsi et $A \subset X$ tel que $\overline{A} \neq A$. Montrer que si $x \in \overline{A}\backslash A$, tout voisinage de $x$ coupe A en une infinité de points.

Apparté sur la séparation

Cet exercice m’a donné l’occasion de découvrir le concept de séparation en topologie que je ne connaissais que très vaguement. L’idée derrière la séparation est de caractériser le niveau d’ « indépendance » des voisinages de deux points distincts. Plus exactement, on distingue 3 niveaux de séparations notés T0, T1 et T2:

T0 signifie que si on prend deux points distincts, on a au moins un voisinage de l’un qui ne contient pas l’autre,
T1 signifie que si on prend deux points distincts, chacun a au moins un voisinage ne contenant pas l’autre,
Enfin T2 est le niveau au dessus : si on prend deux points distincts, on a au moins un couple de voisinage respectif qui sont disjoints.

La plupart des espaces usuels (les réels, complexes, espaces vectoriels…) sont T2. Parmi les espaces qui ne sont pas séparés il y a les topologies grossières (ie l’ensemble entier et l’ensemble vide). J’avoue que je ne connais pas la motivation derrière les niveaux T0 et T1 et je n’ai pas d’exemples d’espace vérifiant ces niveaux mais pas les suivants.

Le trio d’équivalence est semble-t-il une propriété fondamentale des axiomes de séparation puisqu’il est directement présenté comme propriété dans mon livre de topologie, qui le démontre de bas en haut. J’ai essayé d’effectuer la démonstration en Coq de haut en bas mais je me suis retrouvé bloquer en cherchant à passer de (ii) à (iii) ; ayant ensuite décidé qu’il était peut-être plus sage de suivre une voie connue, j’ai finalement opté pour la démonstration de bas en haut. Il s’avère que le passage de (iii) à (ii) est aussi compliqué et que dans les autres cas les preuves sont plus ou moins des « miroirs » de celles que j’avais faite dans ma première tentative, j’imagine aisément qu’il est malgré tout possible d’effectuer la preuve dans n’importe quel sens.

Préalable

Une propriété particulièrement utile pour cette exercice est la caractérisation de l’adhérence d’un ensemble, appelé closure_impl_meets_every_open_neighborhood dans coq-topology : un point est dans l’adhérence d’un ensemble si tous ses voisinages rencontrent cet ensemble, ou dit autrement si l’intersection de ses voisinages avec cet ensemble n’est jamais vide.

Du point de vue plus pratique, on continue à utiliser quelques astuces qui simplifient la vie sur le long terme : on définit une tactic ensemble_proof_intro pour automatiquement nous fournir les 2 inclusions de l’égalité de l’ensemble à prouver, on se sert d’inversion plutôt que de destruct, et on nomme autant que possible les hypothèses/variables pour faciliter la lecture.

A noter qu’à un moment j’ai eu besoin de définir un axiome sur la décidabilité sur l’égalité de 2 éléments d’un ensemble. Par défaut si deux éléments d’un ensemble ne sont pas égaux, Coq ne déduit pas automatiquement qu’ils sont différents ; en effet la logique constructive sur laquelle est basée Coq se passe de l’axiome du tiers exclu qui stipule qu’une propriété (comme ici l’égalité) est vraie ou sa négation est vraie. Il faut donc manuellement indiqué que dans notre cas, c’est vrai.

Trio d’équivalence

On commence par les imports de circonstances et l’écriture des propriétés :

From Topology Require Import TopologicalSpaces.
From Topology Require Import InteriorsClosures.
From Topology Require Import Neighborhoods.
Require Import Decidable.

Definition P1 (X:TopologicalSpace) :=
  forall x y:point_set X, not (x = y) -> exists N, neighborhood N x /\ not (In N y).

Definition P2 (X:TopologicalSpace) :=
  forall x:point_set X, closed (Singleton x).

Definition P3 (X:TopologicalSpace) :=
  forall x:point_set X, FamilyIntersection [V:Ensemble (point_set X) | neighborhood V x] = Singleton x.

Ltac ensemble_proof_intro:=apply Extensionality_Ensembles; unfold Same_set; split.

On aura également besoin de montrer que si un singleton est contenu dans un autre, alors leur élément est égal :

Theorem Singleton_Inclusion (T:Type): forall x y:T, Included (Singleton x) (Singleton y) -> x = y.
Proof.
  intros.
  unfold Included in H. symmetry. apply Singleton_inv. apply H. eauto with sets.
Qed.

On commence ensuite par l’implication la plus compliqué, P3 vers P2 :

Theorem P3_implies_P2 {X:TopologicalSpace}:
  P3 X -> P2 X.
Proof.
  unfold P3. unfold P2.
  
  intros P3 x0.

La stratégie pour montrer que le singleton x est fermé, est de montrer qu’il est égal à son adhérence. Cette stratégie part de l’intuition que l’écriture de l’ensemble des voisinages est proche d’une intersection en ensemble de fermé contenant un ensemble.

  assert (Included (closure (Singleton x0)) (Singleton x0)).

  unfold Included.
  intros x xInClosure.

On va se servir de la propriété sur la caractérisation des adhérences. Quand on regarde les hypothèses de cette propriété, on voit qu’il va falloir trouver un ouvert, qui contient x, et on en déduira que x0 est dans V (car l’intersection du singleton x0 et V est non vide).

pose (tmp2:=closure_impl_meets_every_open_neighborhood  _ (Singleton x0) x xInClosure).

  assert (forall V, open_neighborhood V x -> Inhabited (Intersection (Singleton x0) V)).
  intros V VNeighbor. inversion VNeighbor. unfold open_neighborhood in VNeighbor.
  apply tmp2. 
  assumption. assumption.
  assert(forall V, open_neighborhood V x -> In V x0).
  intros. pose (tmp3:=H V H0). inversion tmp3. inversion H1. inversion H2. subst. assumption.

Pour rappel, on cherche à montrer ici que x est dans le singleton x0, ie que x = x0. Pour l’instant on n’a pas encore utilisé l’hypothèse P3. Pour se simplifier la vie on peut remarquer qu’on peut se servir des voisinages ouverts plutôt que des voisinages quelconques :


  assert( forall x : point_set X,  FamilyIntersection [V : Ensemble (point_set X) | neighborhood V x] =
                              FamilyIntersection [V : Ensemble (point_set X) | open_neighborhood V x]).
  {
    intros x1. ensemble_proof_intro.
   - intros  S SinInters. inversion SinInters.
    constructor. intros. apply H1. inversion H3. constructor. apply open_neighborhood_is_neighborhood. apply H4.
  - intros y yinIntersOpen. inversion yinIntersOpen.
    constructor. intros S SInInters. inversion SInInters as [[S' [OpenS' S'InS]]].
    refine (S'InS _ _). apply H1. split. assumption.
  }

Muni de ce résultat on peut prouver l’égalité:


  assert(Included (Singleton x0) (Singleton x)).
  unfold Included. intros y yisx0. inversion yisx0.
  rewrite <- (P3 x).
  rewrite (H1 x).
  constructor.
  intros. inversion H3. subst. eauto.

et donc l’inclusion inverse :

  apply Singleton_intro.
  refine (Singleton_Inclusion _ _ _ _). assumption.

La suite est relativement directe:


  assert (closure (Singleton x0) = Singleton x0).
  ensemble_proof_intro.
  apply H. apply closure_inflationary.
  rewrite <- H0. apply closure_closed.
Qed.

L’inclusion P2 vers P1 est plus simple:

Theorem P2_implies_P1 {X:TopologicalSpace}:
  P2 X -> P1 X.
Proof.
  unfold P1, P2.
  intros P2 x y xNeqy.
  unfold closed in P2.

  exists (Complement (Singleton y)). split.
  unfold neighborhood. exists (Complement (Singleton y)). split. unfold open_neighborhood. split. apply (P2 y).
  unfold Complement. unfold not. unfold In. intros. destruct xNeqy. inversion H. trivial.
  eauto with sets.
  eauto with sets.
Qed.

Celle de P1 vers P3 n’est pas beaucoup plus compliqué, mais nécessite quand même la décidabilité dont on a préalablement parlé, pour faire une disjonction de cas :

Theorem P1_implies_P3 {X:TopologicalSpace}:
  P1 X -> P3 X.
Proof.
  unfold P1. unfold P3.
  intros P1 x0.
  ensemble_proof_intro.
  - unfold Included. intros x xInIntersNeigh.
    destruct (decT X x0 x).
    + eauto with sets.
    + inversion xInIntersNeigh. destruct (P1 x0 x H). inversion H2. pose (tmp:= H0 x2). autounfold with sets in tmp.
      assert([V : Ensemble (point_set X) | neighborhood V x0] x2).
      constructor. assumption.
      apply tmp in H5. destruct (H4 H5).
  - unfold Included. intros x xIsx0.
    inversion xIsx0.
    constructor. intros. inversion H0. inversion H1. inversion H2. unfold Included in H4. apply H4. inversion H3. assumption.
Qed.

Seconde propriété

Alors là c’est vraiment costaud à démontrer, la faute à la démonstration de l’infinité. Coq dispose de quelques résultats sur les ensembles infinis, mais malheureusement peu nombreux et que nous n’utiliserons donc pas.
En revanche il est beaucoup plus simple de travailler sur les ensembles finis, on va donc procéder par l’absurde.

En particulier une propriété des ouverts qui est vraie dans le cas des ensembles finies mais qui ne l’est plus dans les ensembles infinis est la stabilité par intersection. On va donc prouver cette propriété, par récursion sur la taille de l’ensemble :

Theorem intersection_finite (X:TopologicalSpace):
  forall F:Family (point_set X), Finite _ F /\ (forall S, In F S -> open S) -> open (FamilyIntersection  F).
Proof.
  intros F [F_Finite F_Set_Of_Opens].
  apply finite_cardinal in F_Finite.
  destruct F_Finite as [n cardFn].
  generalize dependent F.
  induction n ; intros F cardFn F_Set_Of_Opens.
  - inversion cardFn. Search FamilyIntersection. rewrite empty_family_intersection.
    Print TopologicalSpace. apply open_full.
  - inversion cardFn. pose (tmp:= IHn A H0).
    assert(FamilyIntersection (Add A x) = Intersection (FamilyIntersection A) x).
    ensemble_proof_intro; unfold Included; intros x0.
    + intros x0InIntersAx.
      inversion x0InIntersAx.
      constructor.
      * constructor. eauto with sets.
      * eauto with sets.
    + intros x0InInters. inversion x0InInters. inversion H3. constructor. unfold Add.
      intros. inversion H8.
      * eauto with sets.
      *  inversion H9. subst. eauto with sets.

    + rewrite H3. apply open_intersection2.

      * apply tmp. intros. apply F_Set_Of_Opens. Search Add.
        unfold Add in H1. rewrite <- H1. eauto with sets.
      * apply F_Set_Of_Opens. rewrite <- H1. unfold Add. eauto with sets.
Qed.

Un autre résultat qui m’a été utile est que l’égalité est conservée par passage au complément :


Theorem Complement_inv (X:Type) : forall (S1 S2: Ensemble X), Complement S1 = Complement S2 -> S1 = S2.
Proof.
  intros. ensemble_proof_intro; rewrite <- Complement_Complement with (A:=S1); rewrite <- Complement_Complement with (A:=S2); apply complement_inclusion; rewrite H; eauto with sets.
Qed.

On peut ensuite passer à la démonstration en elle-même :

Theorem part2 (X:TopologicalSpace): P2 X -> forall A: Ensemble (point_set X), forall x, In (Setminus (closure A) A) x -> forall N, neighborhood N x -> not (Finite _ (Intersection N A)).
Proof.
  intros P2 A x0 x0inclAminA.
  unfold Top.P2 in P2.
  destruct x0inclAminA as [x0InClA x0NotInA].
  intros N [O [[OpenO x0inO] OInN]].
  
  pose (tmp:=closure_impl_meets_every_open_neighborhood _ A x0 x0InClA).

  unfold not. intros NInterAFinite.
  
  remember (fun E => exists x, In (Intersection N A) x /\ E = Complement (Singleton x)) as SetOfElems.
  (**pose (tmp3:=intersection_finite _ SetOfElems).**)
  assert(Finite _ SetOfElems).
  generalize dependent SetOfElems.
  induction NInterAFinite; intros.
  - assert (SetOfElems = Empty_set). rewrite HeqSetOfElems. ensemble_proof_intro.
    + unfold Included. intros. unfold In in H. destruct H. destruct H. destruct H.
    + eauto with sets.
    + rewrite H. eauto with sets.


  - assert (SetOfElems = Add (fun E : Ensemble (point_set X) => exists x0 : point_set X, In A0 x0 /\ E = Complement (Singleton x0)) (Complement (Singleton x))).
    ensemble_proof_intro ; unfold Included; rewrite HeqSetOfElems.
    + intros. inversion H0. inversion H1.  unfold In. inversion H2 as [x2InA0|]. 
      * left. exists x2. split. assumption. assumption.
      * right. inversion H4. subst. eauto with sets.
    + intros. unfold In. inversion H0.
      * inversion H1. inversion H3. exists x3. split. left. assumption. assumption.
      * exists x. inversion H1. split. right. eauto with sets. trivial.


    + rewrite H0. constructor.
      * remember (fun E : Ensemble (point_set X) => exists x1 : point_set X, In A0 x1 /\ E = Complement (Singleton x1)) as P0.
        apply IHNInterAFinite. trivial.
      * unfold In. unfold not. intros. inversion H1. inversion H2.
        apply Complement_inv in H4. 
        apply Singleton_equal in H4. subst. destruct (H H3).
    
   
  - remember (FamilyIntersection SetOfElems) as ContraGen.
    assert (open ContraGen).
    rewrite HeqContraGen.
    apply intersection_finite. split.
    + assumption.
    + intros S SInSetOfElems. rewrite HeqSetOfElems in SInSetOfElems. unfold In in SInSetOfElems. inversion SInSetOfElems.
      inversion H0. rewrite H2. refine (P2 _).
    + pose (contra:= tmp (Intersection ContraGen O) (open_intersection2 ContraGen O H0 OpenO)).
      assert (In (Intersection ContraGen O) x0).
      rewrite HeqContraGen.
      constructor. constructor. rewrite HeqSetOfElems. intros. unfold In in H1. inversion H1. inversion H2. rewrite H4. Search Intersection. apply Intersection_decreases_r in H3. unfold In. unfold Complement. unfold not. intros. inversion H5. subst. contradiction.
      assumption.

      apply contra in H1. inversion H1. inversion H2. inversion H4. rewrite HeqContraGen in H6. rewrite HeqSetOfElems in H6. unfold In in H6. inversion H6. pose (contra2:= H9 (Complement (Singleton x))). unfold In in contra2.
      assert(exists x0 : point_set X, Intersection N A x0 /\ Complement (Singleton x) = Complement (Singleton x0)). exists x. split. constructor.
      eauto with sets. eauto with sets. trivial. apply contra2 in H11. destruct H11. constructor.
Qed.

Frontières en topologie et coq

Jan2

Alors celui là, il est costaud malgré son apparente simplicité. Commençons par l’énoncé :

Dans un espace topologique, on définit la frontière d’une partie A comme étant $\partial A = \overline{A}\backslash \mathring{A}$.

Montrer que $
\partial A =
\partial (A^c )$ et que $A =
\partial A \Leftrightarrow A$ fermé d’intérieur vide.

Montrer que $
\partial (\overline{A})$ et $
\partial (\mathring{A})$ sont toutes deux incluses dans $
\partial A$, et donner un exemple où ces inclusions sont strictes.

Montrer que $
\partial (A \cup B) \subset
\partial A \cup
\partial B$, et que l’inclusion peut-être stricte ; montrer qu’il y a égalité lorsque $\overline{A} \cup \overline{B} = ∅$ (établir $\mathring{A \cup B} \subset \mathring{A} \cup \mathring{B}$).

Montrer que $\mathring{A \cup B} = \mathring{A} \cup \mathring{B}$ reste vrai lorsque $
\partial A \cap
\partial B = ∅$ (raisonner par l’absurde)

Il s’agit d’un exercice relativement classique pour un étudiant en topologie, qui permet surtout de manipuler les définitions d’intérieur et d’adhérence et quelques formules sur les ensembles. Oui mais voilà, la plupart des résultats « intuitifs » sur les ensembles ont besoin d’être prouvé, ce qui donne lieu à des preuves fastidieuses. Pire, il n’est pas rare de se précipiter dans de fausses pistes, en substituant une définition de trop. Bref, cet exercice m’a demandé mine te rien plusieurs jours à effectuer, et surtout à passer par la case papier + crayon alors que je m’en étais passé jusque là. Il est néanmoins très formateur puisqu’il invite à chercher des moyens d’abréger l’écriture de preuve, à découper quelques résultats intermédiaires.

Quelques préalables

On évacue déjà la définition d’une frontière :

Definition frontier (X:TopologicalSpace) (A:Ensemble (point_set X)) :=
  Setminus (closure A) (interior A).

La taille de l’exercice est un bon prétexte pour s’autoriser à essayer les possibilités d’automation que propose Coq. On commence modeste avec une tactique personnalisée « ensemble_proof_intro » qui n’est qu’une espèce de macro sur un enchainement qu’on trouve souvent lorsqu’on travaille avec des ensembles : la réécriture en double inclusion et la génération des 2 objectifs associés.

Ltac ensemble_proof_intro:=
  apply Extensionality_Ensembles; unfold Same_set; split.

Premier point

Muni de ce petit raccourci, le premier résultat est assez direct à prouver :

Theorem frontier_comp (X:TopologicalSpace) (A:Ensemble (point_set X)):
  frontier X A = frontier X (Complement A).
Proof.
  unfold frontier. apply Extensionality_Ensembles. unfold Same_set. split; unfold Included; unfold Setminus in *; rewrite interior_complement; rewrite closure_complement; unfold In in * ;intros; destruct H.
  - split ; unfold Complement.
    + apply H0.
    + unfold not. intros. destruct (H1 H).
  - unfold In.  split. Search (Complement). Print Complement. pose (tmp:= (Complement_Complement _ (closure A))). unfold Complement in tmp. rewrite <- tmp. unfold In. unfold Complement in H0. apply H0. apply H.
Qed.

En revanche pour l’équivalence j’ai eu beaucoup plus de mal. La tentation est grande de remplacer A par sa définition en terme de frontière partout dès le début mais est contre-productive : une façon de prouver est de montrer que si on est dans l’intérieur de A on est aussi dans le complémentaire de l’intérieur de A.

Un autre écueil, certes moins bloquant, est d’unfolder les Included ce qui va rajouter pas mal de « bruits » dans les hypothèses ; une hypothèse de type Included S (interior A) s’est retrouvée « diluée » lors de mes premières tentatives et m’a obligé à la recréer via assert.

La définition de Setminus est toutefois assez peu pratique à utiliser, on va donc utiliser une écriture intermédiaire à base d’intersection et de complémentaire. Une occasion également d’utiliser la tactic eauto (pour une raison que j’ignore, elle fonctionne beaucoup mieux que la tactique auto).

D’après la documentation Coq, cette tactique va essayer d’appliquer la tactique apply (et non des rewrite !) avec des théorèmes groupées dans une base de donnée qui peut être étendue. En pratique, cette tactique marche bien si on a des hypothèses de type « In S x » dans le contexte et peu de Complement.

Theorem setminus_as_intersection (X:Type):
  forall A B:Ensemble X, Setminus A B = Intersection A (Complement B).
Proof.
  intros A B.
  ensemble_proof_intro;  unfold Setminus; unfold Included; unfold Complement; unfold In; intros; destruct H.
  - constructor ; eauto with sets.
  - split; eauto with sets.
Qed.

Quelques mini résultats sur les ensembles qui simplifient la démonstration de la seconde partie du premier point. Bien entendu je n’ai pas planifié à l’avance, j’ai extrait ces résultats quand le besoin s’en ait fait ressentir.

Theorem include_intersection (T:Type): forall (S1 S2 S3:Ensemble T), Included S3 (Intersection S1 S2) <-> Included S3 S1 /\ Included S3 S2.
Proof.
  intros. split.
  - intros. split ; unfold Included in *; intros; pose (tmp:= H x H0); destruct tmp.
    + apply H1.
    + apply H2.
  -  intros.  destruct H. unfold Included in *. intros. constructor. apply H. apply H1. apply H0. apply H1.
Qed.

Theorem Empty_set_intersection (T:Type): forall A: Ensemble T, Intersection A (Complement A) = Empty_set.
Proof.
  intros. ensemble_proof_intro.
  - unfold Included. unfold Complement. intros. destruct H. destruct (H0 H).
  - apply Included_Empty.
Qed.

Theorem Intersection_Complement_Empty_set (T:Type): forall S:Ensemble T,
    Intersection S (Complement Empty_set) = S.
Proof.
  intros. ensemble_proof_intro ;autounfold with sets; intros.
  - destruct H. eauto.
  - constructor.
    * eauto.
    * unfold Complement. unfold In. repeat autounfold in *. intros. destruct H0.
Qed.

Afin de me faciliter la vie j’ai également créé une base de donnée de réécriture ne contenant que le théorème remplaçant Setminus par une intersection. L’intérêt n’est pas de rendre la preuve automatique (autant écrire rewrite setminus_as_intersection directement) mais permet surtout d’effectuer plusieurs réécriture en une seule fois (ce qu’on aurait pu faire avec repeat).

Hint Rewrite -> setminus_as_intersection : sets_helper.

Sur ce voici comment prouver la seconde partie du résultat :

Theorem frontier_equiv (X:TopologicalSpace) (A:Ensemble (point_set X)):
  A = frontier X A <-> closed A /\ (interior A = Empty_set).
Proof.
  autounfold in *. autorewrite with sets_helper. split.
  - intro HypFrontierEgalite. split.
    + rewrite HypFrontierEgalite. apply closed_intersection2; try (rewrite <- closure_complement); apply closure_closed.
    + ensemble_proof_intro.
      * unfold Included. intros x xInInteriorA. destruct xInInteriorA as [S x0 HypS x0InS]. destruct HypS. destruct H as [openS SInA].
         assert (Included S (interior A)).
         unfold Included. intros. unfold interior. eapply family_union_intro with (S:=S). split. split. apply openS. apply SInA. apply H.

         assert (Included S (Complement (interior A))).
         rewrite HypFrontierEgalite in SInA. rewrite include_intersection in SInA. destruct SInA. apply H1.

         assert (Included S (Intersection (interior A) (Complement (interior A)))).
         unfold Included. intros. constructor. apply (H x H1). apply (H0 x H1).

         rewrite Empty_set_intersection in H1. destruct (H1 x0 x0InS).
         * apply Included_Empty.
  - intros [HypClosed HypInteriorEmpty]. rewrite HypInteriorEmpty.
    autorewrite with sets_helper.
    ensemble_proof_intro.
    + apply closure_inflationary.
    + rewrite closure_fixes_closed.  eauto with sets. assumption.
Qed.

Second point

Les inclusions des frontières des intérieurs et des adhérences ne sont pas très compliquées à démontrer, il s’agit surtout d’utiliser les théorèmes de croissance et d’inflation/déflation de ces objets mathématiques :

Theorem incl_frontier (X:TopologicalSpace) (A:Ensemble (point_set X)):
  Included (frontier X (interior A)) (frontier X A).
Proof.
  autounfold. autorewrite with sets_helper.
  unfold Included. 
  intros _ [x xInClosureInteriorA xInComplementClosureInteriorA].
  autounfold with sets.
  constructor.
  - refine (closure_increasing _ _ _ x xInClosureInteriorA).
    apply interior_deflationary.
  - refine (complement_inclusion  _ _ _ x xInComplementClosureInteriorA).
    rewrite <- interior_fixes_open with (S:=interior A) at 1.
    eauto with sets.
    apply interior_open.
Qed.

Theorem incl_frontier2 (X:TopologicalSpace) (A:Ensemble (point_set X)):
  Included (frontier X (closure A)) (frontier X A).
Proof.
  autounfold. autorewrite with sets_helper. autounfold with sets.
  rewrite closure_fixes_closed. intros _ [x xInClosureA xInComplementInteriorClosureA]. constructor.
  + apply xInClosureA.
  + refine (complement_inclusion _ _ _ x xInComplementInteriorClosureA). refine (interior_increasing _ _ _).
    apply closure_inflationary.
  + apply closure_closed.
Qed.

L’inclusion de la frontière de l’union dans l’union des frontières est également assez directe (surtout si on s’autorise des eauto) :

Theorem front_union (X:TopologicalSpace): forall A B, Included (frontier X (Union A B)) (Union (frontier X A) (frontier X B)).
Proof.  
  intros. autounfold. autorewrite with sets_helper.
  rewrite closure_union.

  unfold Included.
  intros _ [x xInUClAClB xInComplementIntUAB].
  destruct xInUClAClB as [x0  xInClosureA | x0 xInClosureB].
  - left. constructor.
    * apply xInClosureA.
    * refine (complement_inclusion _ _ _ x0 xInComplementIntUAB).
      apply interior_increasing. eauto with sets.
  - right. constructor.
    * apply xInClosureB.
    * refine (complement_inclusion _ _ _ x0 xInComplementIntUAB).
      apply interior_increasing. eauto with sets.
Qed.

En revanche les choses se corsent pour démontrer l’inclusion inverse dans le cas de la disjonction des adhérences.

Clang-tidy

Déc29

Au bureau, on nous a cédé le code source d’un logiciel relativement ancien et dont le précédent propriétaire ne souhaitait pas continuer la maintenance.Si d’ m point de vue business il s’ agissait d’une opportunité des plus lucratives, puisqu’on a hérité d’une base de clients colossales, travailler sur du code qui a dormi parfois pendant près de 10 ans est particulièrement difficile.

Pour dresser une image plus précise, le projet utilise une version antédiluvienne de WxWidgets et de boost, en réimplémentant toutefois les smart pointers (qui étaient probablement encore à l’état de standardisation à l’époque ). On ressent assez rapidement le fait que plusieurs personnes sont passés dessus, avec un étrange mélange de pratique douteuses de développement logiciel (des fichiers entiers copié et collés) qui côtoient les design pattern classiques d’une base de code de taille respectable.

Et bien entendu, il n’y a pas ou peu de tests unitaires rendant chaque tentative de refactoring hasardeuse.

La récente série de posts autour de la customisation de clang-tidy sur le blog de visual c++ tombe à bien nommé :

https://blogs.msdn.microsoft.com/vcblog/2018/10/19/exploring-clang-tooling-part-1-extending-clang-tidy/
https://blogs.msdn.microsoft.com/vcblog/2018/10/23/exploring-clang-tooling-part-2-examining-the-clang-ast-with-clang-query/
https://blogs.msdn.microsoft.com/vcblog/2018/11/06/exploring-clang-tooling-part-3-rewriting-code-with-clang-tidy/

Pour référence pour plus tard je partage le bout de code qui permet de détecter les types std::string, qu’ils apparaissent explicitement ou via un using ou typedef:

auto typeParamMatcher =
		varDecl(hasType(hasUnqualifiedDesugaredType(
     recordType(hasDeclaration(cxxRecordDecl(hasName("basic_string")))))));

Si on supprime le hasUnqualifiedDesugaredType, on peut ne matcher que l’apparition explicite de ce type:

varDecl(hasType(cxxRecordDecl(matchesName("string"))))

Intérieurs et adhérences en Coq

Déc5

On continue dans la série d’exercice autour de la topologie, cette fois-ci en rentrant un peu plus dans le sujet en manipulant les concepts d’intérieur et d’adhérence.
Le module coq topology fournit une définition de ces concepts, ainsi que plusieurs propriétés usuelles (inclusions diverses, relation avec les compléments, caractérisation par la rencontre non vide etc) ; j’ai senti moins d’absences étranges que dans le cas des unions de familles comme dans les 2 exercices précédents.

Le sujet, toujours tiré de la même feuille d’exercice :

Si $A$ est une partie de l’espace topologique $X$, on pose $\alpha(A) = \mathring{\overline{A}}$ et $\beta(A) = \overline{\mathring{A}}$.
Montrer que $\alpha$ et $\beta]$ sont des applications croissantes pour l’inclusion de $\mathcal{P}(X)$ dans $\mathcal{P}(X)$.
Montrer que si $A$ est ouvert, $A\subset\alpha(A)$ et si $A$ est fermé, $\beta(A)\subset A$. En déduire que
$\alpha^2 = \alpha$ et $\beta^2 = \beta$.

On va traduire les définitions en Coq :

From Topology Require Import InteriorsClosures. 

Definition alpha (X:TopologicalSpace) (A:Ensemble (point_set X)) :=
interior (closure A). 

Definition beta (X:TopologicalSpace) (A:Ensemble (point_set X)) := 
closure (interior A).

La croissance est relativement facile à prouver à partir de la croissance des intérieurs fourni par le module topology et adhérences et en tripatouillant les définitions :

Theorem croiss (X:TopologicalSpace) :
    forall A B, Included A B -> Included (alpha X A) (alpha X B).
Proof.
   unfold alpha. unfold Included. intros A B H x.
   apply interior_increasing. apply closure_increasing.
   unfold Included. apply H.
Qed.

Prouver les inclusions est également relativement simple :

Theorem open_alpha (X:TopologicalSpace) :
    forall A: Ensemble (point_set X), open A -> Included A (alpha X A). Proof.
    unfold alpha. intros. Search (interior). apply interior_maximal.
    apply H. apply closure_inflationary.
Qed.

Theorem closure_beta (X:TopologicalSpace) :
    forall A: Ensemble (point_set X), closed A -> Included (beta X A) A.
Proof.
   unfold beta. intros. Search (closure). apply closure_minimal.
   apply H. Search (interior). apply interior_deflationary.
Qed.

La dernière propriété est un peu plus délicate à prouver. Déplier les définitions n’est pas suffisant… Il faut en effet reconnaitre $\alpha$ dans l’expression de $\beta^2$ et réciproqement pour appliquer la propriété précédente.

Require Import Coq.Logic.FunctionalExtensionality. 

Theorem alpha_square (X:TopologicalSpace):
    alpha X = fun A => alpha X (alpha X A).
Proof.
   apply functional_extensionality. intros.
   apply Extensionality_Ensembles. unfold Same_set. split.
   - apply open_alpha. Search (interior). apply interior_open.
   - unfold alpha in *. pose(tmp:=closure_beta X (closure x)).
       unfold beta in tmp. Search (interior).
       apply interior_increasing. apply tmp. apply closure_closed.
 Qed.

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 ³ 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$⁴.

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.

Pinkie Duck

Random programming thoughs, RSX emulation…