3 0 Les types dépendants à l'ouvrage

Suite et fin de l'Introduction express aux types dépendants.

Prérequis.

Il est entendu que vous avez lu attentivement Introduction express aux types dépendants et qu'éventuellement vous êtes allé un peu plus loin. Par exemple en lisant le manuel Coq ainsi que d'autres tutoriels sur le net.

De la Turing complétude et de la misère de la condition humaine.

On pourrait penser qu'avec un langage aussi sérieux que OCaml on est à l'abri des turpitudes qui empoissent la vie des pauvres mortels que nous sommes.

 Hélas ça n'est qu'une illusion dont je vais rapidement vous délivrer.

OCaml est Turing-complet. D'un côté c'est rassurant. Au premier abord c'est même un avantage :

D'après la thèse de Church cela ne limite pas vos ambitions en matière de calculabilité.

Et de l'ambition vous en avez à revendre. Par exemple pourquoi ne pas créer une intelligence supérieure et la lancer à la conquête de l'univers ? Ou bien transformer le plomb en or ?

Bon, on va commencer par quelque chose de simple, on va se contenter de transformer le plomb en or.

(* 1Kg de plomb et 1Kg d'or *)
type lead_1Kg = Lead_1Kg
type gold_1Kg = Gold_1Kg

(* une fonction magique *)
let rec magic abracadabra = magic abracadabra

(* une fonction qui utilise la magie pour transformer 1Kg de plomb en 1Kg d'or *)
# let transmute : lead_1Kg -> gold_1Kg = magic;;
val transmute : lead_1Kg -> gold_1Kg = <fun>

Et nous voilà virtuellement riches comme Nicolas Flamel, car pour produire 1Kg d'or il nous suffit de transmuter 1Kg de plomb transmute Lead_1Kg.

On est bien parti. Pourquoi s'arrêter en si bon chemin ? Être riche c'est bien mais à la longue on s'y habitue.

Alors on va se lancer un nouveau défi, plus grandiose : conquérir l'univers à l'aide d'une simple cacahuète.

(* une cacahuète *)
type peanut = Peanut

(* un plan diabolique qui utilise la magie pour transformer une cacahuète *)
(* en une super-intelligence qu'on va lancer à la conquête de l'univers   *)
# let my_space_conquest_plan : peanut -> <conquer_the_universe:unit> = magic;;
val my_space_conquest_plan : peanut -> <conquer_the_universe:unit> = <fun>

Zut, j'ai mangé tout le paquet de cacahuètes.

Ha oui. J'ai oublié de vous dire. La fonction magic ne termine pas

C'est un des désagréments de la Turing-complétude.

Moins de promesses, plus de preuves !

Et si on abandonnait carrément la Turing-complétude ?

On perdrait (éventuellement) quelques possibilités délirantes (ou pas, mais là n'est pas la question qui nous préoccupe ici). C'est l'inconvénient.

Cependant l'avantage est considérable :

Si notre programme n'est pas Turing-complet on peut vérifier sa terminaison.

Si notre programme n'est pas Turing-complet on peut rédiger sa spécification et prouver qu'il la respecte en tous points.

Le peuple réclame un exemple concret !

Soit. On va abandonner OCaml.

On passe en Coq, et on revoit nos classiques.
Par exemple l'indémodable arbre binaire de recherche.

On va y stocker des entiers naturels, certes on y perd en généricité mais le code sera plus lisible et le principe reste le même :

Ou bien l'arbre est vide.

Ou bien l'arbre possède une racine qui contient un élément pivot, les éléments strictement plus petits sont dans la branche gauche, les éléments strictement plus grands sont dans la branche droite.

L'arbre est un ensemble et pas un multi-ensemble, chaque élément est inclus une fois et une seule.

On ne va pas se prendre la tête : notre arbre binaire de recherche ne sera pas équilibré.

On envoie la sauce en Coq :

(* c'est là qu'est définie nat_compare *)
Require Import Arith.Arith_base.

(* un arbre est soit vide soit une séparation en deux *)
Inductive tree : Type :=
  | Empty: tree
  | Split: tree -> nat -> tree -> tree.

(* recherche d'un entier n dans un arbre t *)
Fixpoint find t n :=
  match t with
  | Empty => false     (* absent *)
  | Split l m r =>
      match nat_compare n m with
      | Eq => true     (* on l'a trouvé *)
      | Lt => find l n (* on cherche à gauche *)
      | Gt => find r n (* on cherche à droite *)
      end
  end.

(* insertion d'un entier n dans un arbre t *)
Fixpoint insert t n :=
  match t with
  | Empty => Split Empty n Empty     (* on crée un singleton *)
  | Split l m r =>
      match nat_compare n m with
      | Eq => t                      (* déjà présent *)
      | Lt => Split (insert l n) m r (* on insère à gauche *)
      | Gt => Split l m (insert r n) (* on insère à droite *)
      end
  end.

Quelle différence avec une source équivalente en OCaml ?

Hé bien très peu sinon qu'ici il n'y a pas d'arnaque, on est certain que les fonctions find et insert terminent bien. Coq nous l'annonce par les messages suivants :

find is recursively defined (decreasing on 1st argument)
insert is recursively defined (decreasing on 1st argument)

Néanmoins nous ne baissons pas la garde. Nos fonctions terminent mais jusque là rien ne nous garantie qu'elles se comportent selon nos attentes.

Foin de la démagogie ! Le peuple réclame une politique de transparence !

Soit. Examinons en détail le programme de notre candidat au statut d'arbre totalement ordonné :

L'évidence voudrait qu'on puisse retrouver un élément une fois qu'il a été inséré.

La politesse voudrait qu'un élément admis dans l'ensemble n'entraine pas l'expulsion d'un ou plusieurs éléments déjà présents.

Le protocole exige que l'insertion d'un élément laisse l'arbre dans son état ordonné qui précédait l'insertion.

Qu'est-ce que vous en pensez ? Ça paraît honnête, non ?

Bon, après vous me direz : c'est de la politique, il va nous dire 'héritage désastreux légué par mon prédécesseur', 'crise', 'croissance molle'...

Il dit ce qu'il fait.

Parce que jusque là le programme est un peu vague. C'est sujet à interprétation. Et puis il ne va pas appliquer toutes ses mesures mais seulement les moins coûteuses et celles qui arrangent ses partisans.

Alors on va réécrire tout ça plus proprement.
En commençant par la propriété d'appartenance d'un entier à un arbre ordonné :

Inductive member : tree -> nat -> Prop :=
  | root_member :
      forall l n r,
      member (Split l n r) n
  | left_member :
      forall m n l r,
      member l n ->
      member (Split l m r) n 
  | right_member :
      forall m n l r,
      member r n ->
      member (Split l m r) n. 

Il y a comme qui dirait de la redite. Malgré une nouvelle syntaxe, dans l'esprit ça ressemble furieusement à la fonction find. Attendez une minute ! J'ai un mot d'excuse. find est une fonction, alors que member est une proposition (d'où son type Prop). find est faite pour s'exécuter, alors que member ne s'exécutera jamais. Pour faire nos démonstrations nous n'exécutons rien, nous avons besoin de propositions.

À commencer par member que nous allons mettre au charbon pas plus tard que tout de suite :

La première mesure de notre candidat peut maintenant se reformuler comme ceci : 

forall t n, member (insert t n) n.

La seconde mesure de notre candidat peut maintenant se reformuler comme ceci : 

forall t m n, member t m -> member (insert t n) m.

La troisième mesure de notre candidat peut maintenant se reformuler comme ceci est reportée au prochain mandat.

Il a la tactique.

La tactique principale c'est l'induction.

Il s'agit d'une généralisation du raisonnement par récurrence.

Soit une propriété P à démontrer sur un type T :

Démontrez cette propriété pour les constructeurs non récursifs (O pour ℕ, Empty pour une liste ou un ensemble,...).

Faites l'hypothèse d'induction que P est vraie pour les composantes récursives (P(n) pour S n, P(t) pour Cons h t,...) et démontrez qu'alors P est vraie pour les constructeurs récursifs (P(S n), P(Cons h t),...).

Il fait ce qu'il dit.

On peut retrouver un élément une fois qu'il a été inséré :

Theorem insert_is_inclusive :
  forall t n, member (insert t n) n.
Proof.
  intros t n. induction t.
  (* Empty *)
  simpl.
    apply root_member.
  (* Split *)
  simpl. remember (nat_compare n n0) as cmp.
  destruct cmp.
    (* Eq *)
    symmetry in Heqcmp.
    apply (nat_compare_eq n n0) in Heqcmp.
    subst n0. apply root_member.
    (* Lt *)
    apply left_member. exact IHt1.
    (* Gt *)
    apply right_member. exact IHt2.
Qed.

Un élément inséré dans l'ensemble n'entraine pas l'expulsion d'un ou plusieurs éléments déjà présents :

Theorem insert_is_conservative :
  forall t m n, member t m -> member (insert t n) m.
Proof.
  intros t m n H. induction t.  
  (* Empty *)
  simpl.
    apply left_member. exact H.
  (* Split *)
  remember (Split t1 n0 t2) as node.
  destruct H.
  (* root_member *)
  simpl. destruct (nat_compare n n1).
    apply root_member.
    apply root_member.
    apply root_member.
  (* left_member *)
  inversion Heqnode. rewrite H1 in H.
  simpl. destruct (nat_compare n n0).
    apply left_member. exact H.
    apply IHt1 in H. apply left_member. exact H.
    apply left_member. exact H.
  (* right_member *)
  inversion Heqnode. rewrite H3 in H.
  simpl. destruct (nat_compare n n0).
    apply right_member. exact H.
    apply right_member. exact H.
    apply IHt2 in H. apply right_member. exact H.
Qed.

Il termine le travail. 

Merci de m'avoir renouvelé votre confiance.

Il me reste un dernière promesse à tenir : l'insertion d'un élément doit laisser l'arbre dans son état ordonné qui précédait l'insertion.

Pour ça il nous faudrait une proposition tree_ordered qui dirait si un arbre binaire est totalement ordonné ou non.

Votre serviteur avait proposé ceci :

Inductive tree_between : tree -> nat -> nat -> Prop :=
  | leaf_tree_between :
      forall a b,
      tree_between Leaf a b
  | node_tree_between :
      forall l m r, forall a b,
      tree_between l a m -> a < m < b -> tree_between r m b ->
      tree_between (Node l m r) a b
with tree_less : tree -> nat -> Prop :=
  | leaf_tree_less :
      forall b,
      tree_less Leaf b
  | node_tree_less :
      forall l m r, forall b,
      tree_less l m -> m < b -> tree_between r m b ->
      tree_less (Node l m r) b
with tree_more : tree -> nat -> Prop :=
  | leaf_tree_more :
      forall a,
      tree_more Leaf a
  | node_tree_more :
      forall l m r, forall a,
      tree_between l a m -> a < m -> tree_more r m ->
      tree_more (Node l m r) a.
  
Inductive tree_ordered : tree -> Prop :=
  | leaf_tree_ordered :
      tree_ordered Leaf
  | node_tree_ordered :
      forall l m r,
      tree_less l m -> tree_more r m ->
      tree_ordered (Node l m r).

Heureusement que je suis entouré des meilleurs conseillers Il se trouve que ma proposition pour tree_ordered est sous-optimale.

Explication. Il y a deux écueils possibles dans l'activité de spécification :

La sous-spécification. La spécification donne certaines garanties mais pas toutes les garanties qu'on est en droit d'attendre. Tout n'est pas prouvé, il peut rester une ou plusieurs failles.

La sur-spécification. La spécification donne plus de garanties que celles qu'on attend. Le logiciel est correct. Mais la preuve est sans doute plus longue, laborieuse et alambiquée que nécessaire.

Le problème de mon tree_ordered c'est qu'il n'est pas récursif. Il ne fait qu'utiliser tree_between-tree_less-tree_more. C'est un cas de sur-spécification. La preuve serait plus compliquée que strictement nécessaire.

à Ptival et à dividee pour cette remarque pertinente.

en plus de diagnostiquer le problème dividee a également élaboré une solution.

Bravo à lui, c'est un bel exemple de proof-engineering.

Voici la solution proposée par dividee  :

Inductive tree_less : tree -> nat -> Prop :=
  | empty_tree_less :
      forall b, tree_less Empty b
  | split_tree_less :
      forall l m r b,
      tree_less l b -> tree_less r b -> m < b ->
      tree_less (Split l m r) b.

Inductive tree_more : tree -> nat -> Prop :=
  | empty_tree_more :
      forall a, tree_more Empty a
  | split_tree_more :
      forall l m r a,
      tree_more l a -> tree_more r a -> m > a ->
      tree_more (Split l m r) a.

Inductive tree_ordered : tree -> Prop :=
  | empty_tree_ordered :
      tree_ordered Empty
  | split_tree_ordered :
      forall l m r,
      tree_ordered l -> tree_ordered r ->
      tree_less l m -> tree_more r m ->
      tree_ordered (Split l m r).

Avec cette solution la proposition tree_ordered est maintenant récursive. Ça va faciliter la preuve par induction.

Du coup "l'insertion d'un élément doit laisser l'arbre dans son état ordonné" peut maintenant s'écrire ainsi : forall t, tree_ordered t -> forall n, tree_ordered (insert t n).

à dividee pour avoir développé la preuve qui suit.

dividee commence par caractériser les sous-arbres à gauche : ce sont les arbres majorés par un entier.

Fact tree_less_upper_bound:
  forall t n, tree_less t n <-> forall m, member t m -> m < n.
Proof.
  split.
  (* -> *)
  intros Hless m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hless; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Et, symétriquement, les sous-arbres à droite sont les arbres minorés par un entier.

Fact tree_more_lower_bound: 
  forall t n, tree_more t n <-> forall m, member t m -> m > n.
Proof.
  split.
  (* -> *)
  intros Hmore m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hmore; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Puis dividee introduit deux lemmes, l'un dit qu'un élément plus petit que le pivot est présent dans le sous-arbre gauche, l'autre dit qu'un élément plus grand que le pivot est présent dans le sous-arbre droit.

Lemma member_left:
  forall l m r n, tree_ordered (Split l m r) -> member (Split l m r) n -> n < m -> member l n.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    contradict Hlt. apply lt_irrefl.
    assumption.
    apply tree_more_lower_bound with (m:=n) in H5.
      contradict H5. apply gt_asym. assumption.
      assumption.
Qed.

Lemma member_right:
  forall l m r n, tree_ordered (Split l m r) -> member (Split l m r) n -> n > m -> member r n.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    contradict Hlt. apply lt_irrefl.
    apply tree_less_upper_bound with (m:=n) in H4.
      contradict H4. apply lt_asym. assumption. assumption.
    assumption.
Qed.

Ensuite dividee ajoute encore deux lemmes, l'un dit que l'insertion d'un élément plus petit préserve le majorant, l'autre dit que l'insertion d'un élément plus grand préserve le minorant. 

Lemma insert_preserves_less:
  forall t n m, tree_less t n -> m < n -> tree_less (insert t m) n.
Proof.
  induction t; intros; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (nat_compare m n); constructor; auto.
Qed.

Lemma insert_preserves_more:
  forall t n m, tree_more t n -> m > n -> tree_more (insert t m) n.
Proof.
  induction t; intros; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (nat_compare m n); constructor; auto.
Qed.

Finalement dividee prouve que l'insertion préserve un arbre totalement ordonné.

Theorem insert_preserves_order :
  forall t, tree_ordered t ->
  forall n, tree_ordered (insert t n).
Proof.
  induction t; intros.
  (* Empty *)
  simpl. repeat constructor.
  (* Split *)
  simpl. remember (nat_compare n0 n) as cmp. symmetry in Heqcmp.
  destruct cmp.
    assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_lt in Heqcmp. apply insert_preserves_less; assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_gt in Heqcmp. apply insert_preserves_more; assumption.
Qed.

Il contente même les grognons.

Certains grincheux pourraient penser que les "bons" théorèmes à prouver ne devraient pas utiliser la proposition member mais plutôt la fonction find, par exemple comme ceci :

forall t n, find (insert t n) n = true

forall t m n, (find t m = true) -> (find (insert t n) m = true)

dividee a pensé à eux. Il prouve que member (dans le monde des propositions) est rigoureusement équivalent à find (dans le monde des fonctions).

Theorem find_iff_member :
  forall t, tree_ordered t ->
  forall n, find t n = true <-> member t n.
Proof.
  intros t ord n.
  split; intro H.
    (* -> *)
    induction t.
      (* Empty *)
      inversion H.
      (* Split *)
      inversion_clear ord.
      simpl in H. remember (nat_compare n n0) as cmp.
      symmetry in Heqcmp. destruct cmp.
        (* n = n0 *)
        apply nat_compare_eq in Heqcmp. subst.
        apply root_member.
        (* n < n0 *)
        apply left_member. apply IHt1.
          assumption. assumption.
        (* n > n0 *)
        apply right_member. apply IHt2.
          assumption. assumption.
    (* <- *)
    induction t.
      (* Empty *)
      inversion H.
      (* Split *)
      simpl. remember (nat_compare n n0) as cmp.
      symmetry in Heqcmp. destruct cmp.
        (* n = m *)
        reflexivity.
        (* n < m *)
        apply IHt1.
          inversion ord. assumption.
          apply nat_compare_lt in Heqcmp.
            apply member_left with (n:=n) in ord.
              assumption. assumption. assumption.
        (* n > m *)
        apply IHt2.
          inversion ord. assumption.
          apply nat_compare_gt in Heqcmp.
            apply member_right with (n:=n) in ord.
              assumption. assumption. assumption.
Qed.

Son bilan.

Avantages :

Bye-bye UML. Bye-bye les méthodes agiles. Bye-bye l'extreme programming. Bye-bye les diagrammes de conception. Bye-bye la documentation. Bye-bye le cycle de développement en fontaine, en cascade ou en spirale. Bye-bye stderr. Bye-bye le QA (Quality Assurance). Bye-bye le bug-tracker. Bye-bye la maintenance.

Inconvénients :

Le code à prouver fait 25 lignes. La preuve de ce code fait 230 lignes. On n'est pas du tout dans les proportions du principe de Pareto En fait on en est plus éloigné qu'il n'y paraît. Même en utilisant CoqIDE, vous constaterez rapidement qu'une ligne preuve est bien plus difficile à écrire qu'une ligne de programme.

Dans l'absolu on est pas encore dans la perfection puisqu'on peut encore tomber dans l'erreur de la sous-spécification ou dans la galère de la sur-spécification.

À l'heure d'aujourd'hui cette méthodologie "deluxe" ne s'applique pas encore (partiellement et/ou très difficilement) à des logiciels fortement interactifs / parallélisés / multi-utilisateurs.

Pis encore : même si votre fonction possède une définition simple et rigoureuse il n'est pas garanti que vous puissiez prouver telle ou telle propriété.