Proving that euclidian algorithm complexity is at most logarithmic

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 1 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: 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: ""
homepage: ""
bug-reports: ""
dev-repo: "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"

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 known2 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).
    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:


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.
    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).
    move ->.

Frontières en topologie et coq

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).
  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.

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).
  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.

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.
  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.

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

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

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).
  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.
    + apply closure_inflationary.
    + rewrite closure_fixes_closed.  eauto with sets. assumption.

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).
  autounfold. autorewrite with sets_helper.
  unfold Included. 
  intros _ [x xInClosureInteriorA xInComplementClosureInteriorA].
  autounfold with sets.
  - 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.

Theorem incl_frontier2 (X:TopologicalSpace) (A:Ensemble (point_set X)):
  Included (frontier X (closure A)) (frontier X A).
  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.

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)).
  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.

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

Intérieurs et adhérences en Coq

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).
   unfold alpha. unfold Included. intros A B H x.
   apply interior_increasing. apply closure_increasing.
   unfold Included. apply H.

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.

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

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).
   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.

Encore un peu de topologie en Coq

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)). 

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).


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).

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.

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.

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.

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 :

  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.

Un peu de topologie en Coq

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 et en particulier je vais utiliser comme lui le module 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é.


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
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 : :

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


, 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 : 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, 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-&amp;gt;Y) (A: Ensemble Y) : Ensemble X:=

fun x =&amp;gt; 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-&amp;gt;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-&amp;gt;Y) : Ensemble X :=

FamilyUnion (fun S =&amp;gt; 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-&amp;gt;Y),

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


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 =&amp;gt; S (f x1)). unfold In. exists S. split. apply H. trivial.

unfold In. rewrite &amp;lt;- Heqfx. apply H0.