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.