Previous Up Next

Cours 7  Preuve de programmes fonctionnels

Dans ce cours, nous nous intéressons à la spécification et à la preuve de programmes purement fonctionnels. Nous montrons comment Coq peut être utilisé pour produire du code ML certifié. Ce chapitre est illustré par des programmes manipulant des arbres binaires de recherche, qui sont représentatifs des programmes purement fonctionnels à la fois complexes et très utiles en pratique.

Dans la suite, nous dénommons informatif tout ce qui se trouve dans la sorte Set et logique tout ce qui se trouve dans la sorte Prop. Cette distinction de sorte est exploitée par le mécanisme d’extraction [PM89a, PM89b, Let03a, Let03b] fourni par Coq. Ce mécanisme extrait le contenu informatif d’un terme Coq sous la forme d’un programme ML. Les parties logiques disparaissent (ou ne subsistent que sous la forme d’une valeur dégénérée sans aucun calcul associé). Les fondements théoriques de l’extraction ont été exposés au chapitre précédent.

7.1  Méthode directe

La façon la plus simple de certifier un programme purement fonctionnel consiste à l’écrire comme une fonction dans Coq puis à prouver des propriétés de cette fonction. C’est ce qui a été fait par exemple dès le début de ce cours avec la plus sur les entiers de Peano. Un grand nombre de programmes ML purement fonctionnels peuvent être écrits directement dans le Calcul des Constructions.

D’une manière générale, on commence par définir dans Coq une fonction << pure >>, c’est-à-dire avec un type à la ML (un type du système F) purement informatif. Supposons ici une fonction prenant un seul argument :

  f   :   τ1 → τ2

On montre alors que cette fonction réalise une certaine spécification S : τ1 → τ2Prop par un théorème de la forme

  ∀ x.   (S   x   (f   x))

La preuve de ce théorème se fait en suivant la définition de f.

Exemple.

On souhaite développer et certifier formellement une bibliothèque d’ensembles finis codés à l’aide d’arbres binaires de recherche.

On se donne un type d’arbres binaires contenant des entiers

Coq <   Inductive tree : Set := 
Coq <   | Empty
Coq <   | Node : tree -> Z -> tree -> tree.

et une relation d’appartenance In indiquant qu’un élément apparaît dans un arbre (indépendamment de tout choix de rangement des éléments dans les arbres) :

Coq <   Inductive In (x:Z) : tree -> Prop :=
Coq <   | In_left : forall l r y, (In x l) -> (In x (Node l y r))
Coq <   | In_right : forall l r y, (In x r) -> (In x (Node l y r))
Coq <   | Is_root : forall l r, (In x (Node l x r)).

Une fonction de test de l’ensemble vide peut alors s’écrire

Coq <   Definition is_empty (s:tree) : bool := match s with
Coq <   | Empty => true
Coq <   | _ => false end.

et sa preuve de correction s’énonce ainsi

Coq <   Theorem is_empty_correct : 
Coq <   forall s, (is_empty s)=true <-> (forall x, ~(In x s)).

La preuve suit la définition de is_empty et tient en trois lignes :

Coq < Proof.

Coq <   destruct s; simpl; intuition.

Coq <   inversion_clear H0.

Coq <   elim H with z; auto.

Coq < Qed. 

Venons-en au test d’occurrence dans un arbre binaire de recherche. On commence par se donner une relation d’ordre ternaire sur les entiers relatifs :

Coq <   Inductive order : Set := Lt | Eq | Gt.

Coq <   Hypothesis compare : Z -> Z -> order.

Puis on définit une fonction mem de recherche dans un arbre supposé être un arbre de recherche :

Coq <   Fixpoint mem (x:Z) (s:tree) {struct s} : bool := match s with
Coq <   | Empty => 
Coq <      false
Coq <   | Node l y r => match compare x y with
Coq <      | Lt => mem x l
Coq <      | Eq => true
Coq <      | Gt => mem x r
Coq <     end
Coq <   end.

La preuve de correction de cette fonction nécessite de définir la notion d’arbre binaire de recherche, sous la forme du prédicat inductif bst suivant :

Coq <   Inductive bst : tree -> Prop :=
Coq <   | bst_empty : 
Coq <      (bst Empty)
Coq <   | bst_node : 
Coq <      forall x (l r : tree),
Coq <      bst l -> bst r -> 
Coq <      (forall y, In y l -> y < x) ->
Coq <      (forall y, In y r -> x < y) -> bst (Node l x r).

La correction de la fonction mem peut alors s’écrire ainsi :

Coq <   Theorem mem_correct : 
Coq <     forall x s, (bst s) -> (mem x s=true <-> In x s).

On voit sur cet exemple que la spécification S prend la forme P xQ x (f x). P est ce que l’on appelle une précondition et Q une postcondition.

Modularité.

Si l’on cherche à faire la preuve de mem_correct on commence par induction s; simpl pour suivre la définition de mem. Le premier cas (Empty) est trivial. Avec le second (Node s1 z s2) on tombe alors sur un terme de la forme match compare x z with ... qui ne permet pas d’aller plus avant. En effet, on ne sait rien de la fonction compare utilisée ici par la fonction mem. Il nous faut la spécifier, par exemple sous la forme d’un axiome

Coq <   Hypothesis compare_spec :
Coq <     forall x y, match compare x y with
Coq <     | Lt => x<y
Coq <     | Eq => x=y
Coq <     | Gt => x>y
Coq <     end.

On peut alors utiliser cette spécification de la manière suivante :

Coq <    generalize (compare_spec x z); destruct (compare x z).

La preuve se poursuit alors sans difficulté.

Note.

Pour des fonctions purement informatives telles que is_empty ou mem, le programme extrait est identique au terme Coq. Ainsi la commande Extraction mem donne-t-elle le code ocaml

let rec mem x = function
  | Empty -> false
  | Node (l, y, r) ->
      (match compare x y with
         | Lt -> mem x l
         | Eq -> true
         | Gt -> mem x r)

7.1.1  Cas des fonctions partielles

Une première difficulté apparaît lorsque la fonction est partielle, i.e. a un type de la forme

  f : ∀ x1.   (P x) → τ2

Le cas typique est celui d’une fonction de division qui attend un diviseur non nul.

Dans notre exemple, on peut souhaiter définir une fonction min_elt retournant le plus petit élément d’un ensemble supposé non vide (c’est-à-dire l’élément rangé le plus à gauche dans l’arbre binaire de recherche). On peut donner à cette fonction le type suivant :

  min_elt : ∀ s:tree.   ¬ s=Empty → Z     (7.1)

où apparaît la précondition ¬ s=Empty. La spécification de min_elt peut alors s’écrire

    ∀ s.   ∀ h:¬ s=Empty.   bst s → In (min_elt  s   h)   s ∧  ∀ x.   In  x  s → min_elt  s   h ≤ x

avec une précondition reprenant naturellement celle de la fonction (hypothèse h) et ajoutant bst s. La présence de h est même nécessaire pour pouvoir appliquer la fonction min_elt. On voit que l’utilisation d’une fonction partielle en Coq n’est pas simple : il faut passer en argument des termes de preuve, souvent difficiles à construire.

La définition même d’une fonction partielle est souvent délicate. Écrivons une fonction min_elt ayant le type (7.1). Le code ML que l’on a en tête est le suivant :

let rec min_elt = function
  | Empty -> assert false
  | Node (Empty, x, _) -> x
  | Node (l, _, _) -> min_elt l

Malheureusement la définition en Coq est plus difficile. D’une part l’assert false dans le premier cas de filtrage correspond à un cas absurde (on a supposé l’arbre non vide). La définition en Coq exprime cette absurdité à l’aide du récurseur False_rec appliqué à une preuve de l’absurde. Il faut donc construire une telle preuve à partir de la précondition. De même le troisième cas de filtrage fait un appel récursif à min_elt et pour cela on doit construire une preuve que l’argument l n’est pas vide. C’est ici une conséquence du filtrage qui a éliminé le cas où l est Empty. Dans ces deux cas la nécessité de construire ces termes de preuve complique le filtrage, qui doit être dépendant. On obtient la définition suivante :

Coq < Fixpoint min_elt (s:tree) (h:~s=Empty) { struct s } : Z := 
Coq <   match s return ~s=Empty -> Z with
Coq <   | Empty => 
Coq <       (fun h => False_rec _ (h (refl_equal Empty)))
Coq <   | Node l x _ => 
Coq <       (fun h => match l as a return a=l -> Z with
Coq <                 | Empty => (fun _ => x)
Coq <                 | _ => (fun h => min_elt l 
Coq <                                   (Node_not_empty _ _ _ _ h))
Coq <                 end (refl_equal l))
Coq <   end h.  

La première preuve (argument de False_rec) est construite directement. La seconde fait appel au lemme suivant :

Coq < Lemma Node_not_empty : forall l x r s, Node l x r=s -> ~s=Empty.

On peut alors prouver la correction de cette fonction :

Coq < Theorem min_elt_correct :
Coq <   forall s (h:~s=Empty), bst s ->
Coq <     In (min_elt s h) s /\ 
Coq <     forall x, In x s -> min_elt s h <= x.

Là encore la preuve se fait en suivant la définition de la fonction et ne pose pas de problème.

On peut vérifier que le code extrait est bien celui que l’on avait en tête. Extraction min_elt donne en effet :

let rec min_elt = function
  | Empty -> assert false (* absurd case *)
  | Node (l, x, t) ->
      (match l with
         | Empty -> x
         | Node (t0, z0, t1) -> min_elt l)

Plusieurs points sont à noter : d’une part l’utilisation de False_rec est extraite en assert false, ce qui est exactement le comportement souhaité (on a fait une preuve que ce point de programme est inatteignable, il est donc légitime de dire qu’arriver là est absurde i.e. une << preuve >> de false) ; d’autre part on voit que les arguments logiques liés à la précondition qui compliquaient la définition ont disparu dans le code extrait (ils étaient dans la sorte Prop).


Une autre solution consiste à définir la fonction min_elt par une preuve plutôt que par une définition. Il est alors facile de construire les termes de preuve (on est dans l’éditeur de preuves). Ici la définition-preuve est relativement simple :

Coq < Definition min_elt : forall s, ~s=Empty -> Z.

Coq < Proof.

Coq < induction s; intro h.

Coq < elim h; auto.

Coq < destruct s1.

Coq < exact z.

Coq < apply IHs1; discriminate.

Coq < Defined.

Mais il est plus difficile de se persuader que l’on construit la bonne fonction (tant que l’on n’a pas montré la correction de cette fonction). Il faut en particulier prendre bien soin de ne pas utiliser à tort de tactiques automatiques telles que auto qui pourraient avoir pour effet de construire une fonction autre que celle que l’on a en tête ; sur cet exemple auto n’est utilisé que sur un but logique (Empty=Empty).

Une façon de se persuader que le code sous-jacent est bien le bon consiste à examiner le code extrait. Ici on retrouve exactement le même que précédemment.


La tactique refine aide à la définition de fonction partielle (mais pas seulement). Elle permet de donner partiellement un terme de preuve, certaines parties étant omises (dénotées par _) et donnant lieu à des sous-buts. Ainsi on peut redéfinir la fonction min_elt de la façon suivante :

Coq < Definition min_elt : forall s, ~s=Empty -> Z.

Coq < refine 
Coq <   (fix min (s:tree) (h:~s=Empty) { struct s } : Z := 
Coq <   match s return ~s=Empty -> Z with
Coq <   | Empty => 
Coq <       (fun h => _)
Coq <   | Node l x _ => 
Coq <       (fun h => match l as a return a=l -> Z with
Coq <                 | Empty => (fun _ => x)
Coq <                 | _ => (fun h => min_elt l _)
Coq <                 end _)
Coq <   end h).

On obtient alors deux sous-buts qu’il est aisé de prouver. On remarque tout de même que l’on n’échappe pas à un filtrage dépendant.


Enfin une dernière solution consiste à rendre la fonction totale en la complétant de manière arbitraire en dehors de son domaine de définition. Ici on peut choisir de retourner la valeur 0 lorsque l’ensemble est vide. On évite ainsi l’argument logique ¬ s=Empty et ses fâcheuses conséquences. Le type de min_elt << redevient>> treeZ et sa définition est très simple :

Coq < Fixpoint min_elt (s:tree) : Z := match s with
Coq <   | Empty => 0
Coq <   | Node Empty z _ => z
Coq <   | Node l _ _ => min_elt l
Coq < end.

Le théorème de correction reste le même, en revanche :

Coq < Theorem min_elt_correct :
Coq <   forall s, ~s=Empty -> bst s ->
Coq <     In (min_elt s) s /\ 
Coq <     forall x, In x s -> min_elt s <= x.

L’énoncé garde la précondition ¬ s=Empty, sans quoi il ne serait pas possible de montrer l’appartenance de min_elt s à s.

Note.

La fonction de division sur les entiers relatifs, Zdiv, est ainsi définie comme une fonction totale mais ces propriétés ne sont établies que sous l’hypothèse que le diviseur est non nul.

Note.

Une autre façon de rendre totale la fonction min_elt, plus générale, eût été de lui faire retourner un résultat de type option Z, c’est-à-dire None lorsque l’ensemble est vide, et Some m lorsqu’il existe un plus petit élément m. Mais on change alors légèrement le code ML sous-jacent (et l’énoncé du théorème de correction).

7.1.2  Cas des fonctions non structurellement récursives

Le problème de la définition (et de l’utilisation) d’une fonction partielle se retrouve également lorsque l’on cherche à définir (et à prouver) une fonction récursive mais dont la récurrence n’est pas structurelle.

En effet, une solution pour définir une telle fonction consiste à utiliser un principe de récurrence bien fondée, tel que well_founded_induction :

Coq < well_founded_induction
Coq <      : forall (A : Set) (R : A -> A -> Prop),
Coq <        well_founded R ->
Coq <        forall P : A -> Set,
Coq <        (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
Coq <        forall a : A, P a

Mais alors la définition nécessite de construire des preuves de R y x pour chaque appel récursif sur y ; on retrouve les difficultés — mais aussi les solutions — mentionnées dans la section précédente.

Supposons que l’on souhaite écrire une fonction subset qui teste l’inclusion sur nos ensembles comme arbres binaires de recherche. Un code ML possible est le suivant :

  let rec subset s1 s2 = match (s1, s2) with
    | Empty, _ ->
        true
    | _, Empty ->
        false
    | Node (l1, v1, r1), (Node (l2, v2, r2) as t2) ->
        let c = compare v1 v2 in
        if c = 0 then
          subset l1 l2 && subset r1 r2
        else if c < 0 then
          subset (Node (l1, v1, Empty)) l2 && subset r1 t2
        else
          subset (Node (Empty, v1, r1)) r2 && subset l1 t2

On voit que les appels récursifs se font sur des arbres qui ne sont pas toujours des sous-termes des arguments initiaux (sans compter la difficulté supplémentaire d’une récurrence simultanée sur les deux arguments). Il existe cependant un critère simple de terminaison, à savoir le nombre total d’éléments dans les deux arbres.

On commence donc par établir un principe de récurrence bien fondée sur deux arbres basé sur la somme de leur nombre d’éléments :

Coq < Fixpoint cardinal_tree (s:tree) : nat := match s with
Coq <   | Empty => O
Coq <   | Node l _ r => (S (plus (cardinal_tree l) (cardinal_tree r))) 
Coq < end.

Coq < 
Coq < Lemma cardinal_rec2 : 
Coq <   forall (P:tree->tree->Set),
Coq <   (forall (x x’:tree),
Coq <      (forall (y y’:tree),
Coq <        (lt (plus (cardinal_tree y) (cardinal_tree y’)) 
Coq <            (plus (cardinal_tree x) (cardinal_tree x’))) -> (P y y’)) 
Coq <      -> (P x x’)) ->
Coq <   forall (x x’:tree), (P x x’).

La preuve est facile : on se ramène à un principe de récurrence bien fondée sur le type nat, fourni dans la bibliothèque de Coq, à savoir well_founded_induction_type_2, et l’on prouve aisément que la relation est bien fondée car elle est de la forme lt (f y y′) (f x x′) et que lt est une relation bien fondée sur nat (autre résultat fourni par la bibliothèque) :

Coq < Proof.

Coq <   intros P H x x’.

Coq <   apply well_founded_induction_type_2 
Coq <       with (R:=fun (yy’ xx’:tree*tree) =>
Coq <               (lt (plus (cardinal_tree (fst yy’)) (cardinal_tree (snd yy’))) 
Coq <                   (plus (cardinal_tree (fst xx’)) (cardinal_tree (snd xx’)))));
Coq <     auto.                      

Coq <     apply (Wf_nat.well_founded_ltof _
Coq <            (fun (xx’:tree*tree) => 
Coq <                 (plus (cardinal_tree (fst xx’)) (cardinal_tree (snd xx’))))).

Coq < Save.

On peut alors définir la fonction subset par une définition-preuve utilisant la tactique refine :

Coq < Definition subset : tree -> tree -> bool.

Coq < Proof.

On commence par appliquer le principe de récurrence cardinal_rec2 :

Coq <   intros s1 s2; pattern s1, s2; apply cardinal_rec2.

Puis on filtre sur x et x’ les deux cas Empty étant triviaux :

Coq <   destruct x.

Coq <   (* x=Empty *)
Coq <   intros; exact true.

Coq <   (* x = Node x1 z x2 *)
Coq <   destruct x’.

Coq <   (* x’=Empty *)
Coq <   intros; exact false.

On procède ensuite par cas sur le résultat de compare z z0 :

Coq <   (* x’ = Node x’1 z0 x’2 *)
Coq <   intros; case (compare z z0).

Dans chacun des trois cas, les appels récursifs (hypothèse H) se font à l’aide de la tactique refine : on a alors une obligation de montrer la décroissance du nombre d’éléments, ce qui est automatiquement prouvé par simpl; omega (simpl est nécessaire pour déplier la définition de cardinal_tree) :

Coq <   (* z < z0 *)
Coq <   refine (andb (H (Node x1 z Empty) x’2 _)
Coq <                (H x2 (Node x’1 z0 x’2) _)); simpl; omega.

Coq <   (* z = z0 *)
Coq <   refine (andb (H x1 x’1 _) (H x2 x’2 _)); simpl ; omega.

Coq <   (* z > z0 *)
Coq <   refine (andb (H (Node Empty z x2) x’2 _)
Coq <                (H x1 (Node x’1 z0 x’2) _)); simpl ; omega.

Coq < Defined.
Note.

On aurait pu également faire une définition à l’aide d’un unique refine.

Note.

Il est intéressant d’examiner le code extrait d’une fonction définie à l’aide d’un récurseur tel que well_founded_induction. On peut commencer par regarder directement le code extrait pour well_founded_induction et l’on reconnaît un opérateur de point-fixe :

let rec well_founded_induction x a =
  x a (fun y _ -> well_founded_induction x y)

En dépliant cet opérateur et deux autres constantes

Coq < Extraction NoInline andb.

Coq < Extraction Inline cardinal_rec2 Acc_iter_2 well_founded_induction_type_2.

Coq < Extraction subset.

on obtient exactement le code ML souhaité :

let rec subset x x' =
  match x with
    | Empty -> True
    | Node (x1, z0, x2) ->
        (match x' with
           | Empty -> False
           | Node (x'1, z1, x'2) ->
               (match compare z0 z1 with
                  | Lt ->
                      andb (subset (Node (x1, z0, Empty)) x'2)
                        (subset x2 (Node (x'1, z1, x'2)))
                  | Eq -> andb (subset x1 x'1) (subset x2 x'2)
                  | Gt ->
                      andb (subset (Node (Empty, z0, x2)) x'2)
                        (subset x1 (Node (x'1, z1, x'2)))))

De nombreuses autres techniques pour définir des fonctions récursives non structurelles dans Coq sont décrites dans le chapitre 15 de l’ouvrage Interactive Theorem Proving and Program Development [BC04].

7.2  Utilisation de types dépendants

Une autre approche de la preuve de programmes fonctionnels dans Coq consiste à utiliser la richesse du système de types du Calcul des Constructions Inductives pour exprimer la spécification de la fonction dans son type même. En fait, un type est une spécification. Dans le cas de ML, c’est juste une spécification très pauvre — une fonction attend un entier et retourne un entier — mais dans Coq on peut exprimer qu’une fonction attend un entier positif et retourne un entier premier :

  f : { n:Z  |  n ≥ 0 } → { p:Z  |  premier p }

Nous allons montrer comment.

7.2.1  Type sous-ensemble sig

La notation Coq {x:A | P} désigne le << sous-type de A des valeurs vérifiant la propriété P >> ou, dans un vocabulaire plus théorie des ensembles, le << sous-ensemble de A des éléments vérifiant P >>. La notation {x:A | P} désigne l’application sig A (fun xP) où sig est l’inductif suivant :

Coq < Inductive sig (A : Set) (P : A -> Prop) : Set :=
Coq <   exist : forall x:A, P x -> sig P

Cet inductif est identique à l’existentielle ex, si ce n’est sa sorte, Set au lieu de Prop (on souhaite définir une fonction et donc que ses arguments et résultats soient informatifs).

En pratique, on souhaite lier l’argument au résultat par une postcondition Q et on préfère donc la forme plus générale suivante :

  f : ∀  (x1),  P x → { y2  |  Q x y }

Si l’on reprend l’exemple de la fonction min_elt, sa spécification peut être la suivante :

Coq < Definition min_elt :
Coq <   forall s, ~s=Empty -> bst s ->
Coq <     { m:Z | In m s /\ forall x, In x s -> m <= x }.

On a toujours les difficultés de définition directe mentionnées dans la section précédente et l’on préfère donc en général la définition par preuve (avec toujours la même mise en garde vis-à-vis des méthodes automatiques).

Note.

Le déplacement de la propriété bst s vers la précondition n’est pas nécessaire ; c’est juste plus naturel.

Note.

L’extraction de sig A Q oublie l’annotation logique Q et se réduit donc à l’extraction du type A. Dit autrement, le type sig peut disparaître à l’extraction ; de fait on a

Coq < Extraction sig.
type 'a sig = 'a
  (* singleton inductive, whose constructor was exist *)

7.2.2  Variantes de sig

On peut définir d’autres types similaires à sig. Ainsi si l’on souhaite écrire une fonction retournant deux entiers, telle que par exemple une division euclidienne, on a envie d’emboîter deux utilisation de sig de la même manière que l’on peut le faire pour deux existentielles ex :

  div : ∀ a   b,  b>0 → { q  |  { r  |  a=bq+r ∧ 0≤ r<b }}

Mais la seconde utilisation de sig a pour sorte Set et non Prop, ce qui rend cette écriture incorrecte. Coq introduit pour cela une variante de sig, sigS :

Coq < Inductive sigS (A : Set) (P : A -> Set) : Set :=
Coq <   existS : forall x:A, P x -> sig P

où la seule différence est la sorte de P (Set au lieu de Prop). sigS A (fun xP) se note {x:A & P}, ce qui permet d’écrire

  div : ∀ a   b,  b>0 → { q  &  { r  |  a=bq+r ∧ 0≤ r<b }}

L’extraction de sigS est naturellement une paire :

Coq < Extraction sigS.
type ('a, 'p) sigS =
  | ExistS of 'a * 'p


De même si l’on souhaite une spécification de la forme

  { x:A  |  P x ∧ Q x }

il existe un inductif << sur mesure >>, sig2, défini par

Coq < Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set :=
Coq <   exist2 : forall x : A, P x -> Q x -> sig2 P Q

Son extraction est identique à celle de sig.

7.2.3  Spécification d’une fonction booléenne : sumbool

Un type de spécification1 qui revient très souvent est celui de la spécification d’une fonction booléenne. Dans ce cas, on souhaite exprimer quelles sont les deux propriétés établies lorsque la fonction retourne false et true respectivement. Coq introduit un type inductif pour cela, sumbool, défini par

Coq < Inductive sumbool (A : Prop) (B : Prop) : Set :=
Coq <   | left : A -> sumbool A B
Coq <   | right : B -> sumbool A B

C’est un type semblable au type bool mais dont chaque constructeur contient une preuve, de A et de B respectivement. sumbool A B se note {A}+{B}. Une fonction de test de l’ensemble vide pourra se spécifier ainsi :

  is_empty :  ∀ s,   {s=Empty} + {¬ s=Empty}

Un cas plus général, et très fréquent, est celui d’une égalité décidable. En effet, si un type A est muni d’une égalité eq:AAProp, on peut spécifier une fonction de test de cette égalité sous la forme

  A_eq_dec :  ∀ x y,   {eq x y} + {¬(eq x y)}

C’est presque la même chose que donner une preuve de

  ∀ x y,   (eq x y) ∨ ¬(eq x y)

si ce n’est que la sorte n’est pas la même. Dans ce dernier cas, on a une disjonction dans Prop (un tiers-exclu pour le prédicat eq) alors que dans le précédent on a une << disjonction >> dans Set, c’est-à-dire un programme décidant de l’égalité.

L’extraction de sumbool est un type isomorphe à bool :

Coq < Extraction sumbool.
type sumbool =
  | Left
  | Right

En pratique on peut indiquer à l’extraction de Coq d’utiliser directement les booléens de ML au lieu de Left et Right (permet notamment d’utiliser if-then-else dans le code extrait).

Variante sumor

Il existe une variante à sumbool où les sortes ne sont pas les mêmes à gauche et à droite :

Coq < Inductive sumor (A : Set) (B : Prop) : Set :=
Coq <   | inleft : A -> A + {B} 
Coq <   | inright : B -> A + {B}

Cet inductif permet de spécifier une fonction ML qui retourne une valeur du type α option : le constructeur inright représente le cas None et lui associe la propriété B, et le constructeur inleft représente le cas Some et lui associe la spécification A. De fait, l’extraction de sumor est isomorphe au type option de ML :

Coq < Extraction sumor.
type 'a sumor =
  | Inleft of 'a
  | Inright


On peut ainsi combiner sumor et sig pour spécifier la fonction min_elt de la manière suivante :

Coq < Definition min_elt : 
Coq <   forall s, bst s ->
Coq <   { m:Z | In m s /\ forall x, In x s -> m <= x } + { s=Empty }.

Il s’agit là de la version correspondant à une fonction ML rendue totale avec un type option.

On peut de même combiner sumor et sumbool pour spécifier notre fonction de comparaison ternaire :

Coq < Hypothesis compare : forall x y, {x<y} + {x=y} + {x>y}.

On note que maintenant cette seule hypothèse remplace à elle seule l’inductif order et les deux hypothèses compare et compare_spec.

Reprenons l’exemple de la fonction de test d’appartenance dans un arbre binaire de recherche, mem. On peut maintenant la spécifier à l’aide d’un type dépendant :

Coq < Definition mem : 
Coq <   forall x s, bst s -> { In x s }+{ ~(In x s) }.

La définition-preuve commence par une induction sur s.

Coq < Proof.

Coq <   induction s; intros. 

Coq <   (* s = Empty *)
Coq <   right; intro h; inversion_clear h.

Le cas s=Empty est trivial. Dans le cas s=Node s1 z s2, il s’agit de procéder par cas sur le résultat de compare x z. C’est maintenant plus simple qu’avec la méthode précédente : plus besoin de faire appel au lemme compare_spec, car compare x z contient sa spécification dans son type.

Coq <   (* s = Node s1 z s2 *)
Coq <   case (compare x z); intro.

De même chaque hypothèse de récurrence (sur s1 et s2) est une fonction contenant sa spécification. On l’utilise, le cas échéant, en lui appliquant la tactique case. Le reste de la preuve est aisé.

Note.

Il est possible de retrouver la fonction pure comme projection de la fonction spécifiée à l’aide d’un type dépendant :

Coq < Definition mem_bool x s (h:bst s) := match mem x s h with
Coq <   | left _ => true
Coq <   | right _ => false
Coq <   end.

Il est alors aisé de montrer la correction de cette fonction pure (car la preuve est contenue dans le type de la fonction d’origine) :

Coq < Theorem mem_bool_correct :
Coq <   forall x s, forall (h:bst s), 
Coq <   (mem_bool x s h)=true <-> In x s.

Coq < Proof.

Coq <   intros.

Coq <   unfold mem_bool; simpl; case (mem x s h); intuition.

Coq <   discriminate H.

Coq < Qed.

Mais cette projection a peu d’intérêt en pratique.

Note.

Il est important de noter que chaque fonction se voit maintenant donner sa spécification dès sa définition : il n’est plus aussi facile de montrer plusieurs propriétés d’une même fonction que dans le cas d’une fonction pure.

7.2.4  Spécification dans les types de données

L’ajout de spécification dans les types ML peut également s’appliquer aux types récursifs. Ainsi on peut introduire le type dépendant des arbres ayant la propriété d’être des arbres binaires de recherche :

Coq < Inductive bst_tree : Set :=
Coq <   | Bst_tree : forall t, bst t -> bst_tree.

Il s’agit là d’un couple dépendant constitué d’un arbre t (dans la sorte Set) et d’une preuve de bst t (dans la sorte Prop). Un tel inductif a un constructeur est un record (type enregistrement) :

Coq < Record bst_tree : Set := { 
Coq <   t     :> tree; 
Coq <   bst_t :  bst t 
Coq < }.
Note.

La notation :> introduit une coercion du type bst_tree vers le type tree (la première projection). Ceci permet par exemple d’appliquer directement le prédicat In a une valeur du type bst_tree.

7.3  Modules et foncteurs

L’adéquation de Coq comme formalisme de spécification et de preuve de programmes ML purement fonctionnels s’étend jusqu’au système de modules. En effet, Coq est depuis peu équipé d’un système de modules inspiré de celui d’Objective Caml [Ler00, Chr03a, Chr03b]. De même que les types de fonction Coq peuvent enrichir ceux de ML par des annotations logiques, les modules de Coq peuvent enrichir ceux de ML.

Ainsi, si l’on souhaite écrire notre bibliothèque d’ensembles finis sous la forme d’un foncteur prenant en argument un type quelconque (et non plus Z comme jusqu’à présent) équipé d’un ordre total, on commence par définir une signature pour cet argument. On y met un type t, une égalité eq et une relation d’ordre lt sur ce type :

Coq < Module Type OrderedType.

Coq <   Parameter t : Set.

Coq <   Parameter eq : t -> t -> Prop.

Coq <   Parameter lt : t -> t -> Prop.

ainsi qu’un résultat de décidabilité de lt et eq :

Coq <   Parameter compare : forall x y, {lt x y}+{eq x y}+{lt y x}.

Il faut également fournir quelques propriétés sur eq (relation d’équivalence) et lt (relation d’ordre incompatible avec eq) sans lesquelles les fonctions sur les arbres binaires de recherche ne peuvent être correctes :

Coq <   Axiom eq_refl : forall x, (eq x x).

Coq <   Axiom eq_sym : forall x y, (eq x y) -> (eq y x).

Coq <   Axiom eq_trans : forall x y z, (eq x y) -> (eq y z) -> (eq x z).

Coq <  
Coq <   Axiom lt_trans : forall x y z, (lt x y) -> (lt y z) -> (lt x z).

Coq <   Axiom lt_not_eq : forall x y, (lt x y) -> ~(eq x y).

Enfin, on peut ajouter à la signature des commandes Hint pour la tactique auto —- et elles seront ainsi disponibles automatiquement dans le corps du foncteur :

Coq <   Hint Immediate eq_sym.

Coq <   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.

Coq < End OrderedType.

On peut alors écrire notre bibliothèque d’ensembles sous la forme d’un foncteur prenant un argument X de type OrderedType :

Module ABR (X: OrderedType).

  Inductive tree : Set := 
  | Empty
  | Node : tree -> X.t -> tree -> tree.

  Fixpoint mem (x:X.t) (s:tree) {struct s} : bool := ...

  Inductive In (x:X.t) : tree -> Prop := ...
  Hint Constructors In.

  Inductive bst : tree -> Prop :=
  | bst_empty : (bst Empty)
  | bst_node : 
     forall x (l r : tree),
     bst l -> bst r -> 
     (forall y, In y l -> X.lt y x) ->
     (forall y, In y r -> X.lt x y) -> bst (Node l x r).

  (* etc. *)
Note.

Le langage Objective Caml fournit une bibliothèque d’ensembles finis codés par des arbres binaires de recherche équilibrés (des AVL [AVL62]), sous la forme d’un foncteur prenant en argument un type ordonnée. Cette bibliothèque implante toutes les opérations habituelles sur les ensembles (union, intersection, différence, cardinal, plus petit élément, etc.), des itérateurs (map, fold, iter) et également une fonction d’ordre total sur les ensembles permettant d’obtenir des ensembles d’ensembles par une seconde application du même foncteur (et ainsi de suite). Cette bibliothèque a été certifiée à l’aide de Coq par Pierre Letouzey et Jean-Christophe Filliâtre [FL04]. Cette preuve a permis de découvrir un bug dans le ré-équilibrage des arbres effectué par certaines fonctions ; le code a été corrigé dans la dernière version d’ocaml (3.07).


1
C’est le cas de le dire !

Previous Up Next