Initiation à la démonstration sur ordinateur et certification de logiciel

Introduction

Coq est un logiciel d'aide à la preuve mathématique développé par les équipes PI.R2 et Marelle d'Inria et l'équipe Systèmes Sûrs du Cnam. La première version a été publiée en 1984 et a été codée sous CAML.

Coq est fondé sur le calcul des constructions, une théorie concurrente à la théorie des ensembles de Zermelo-Fraenkel, et plus particulièrement la correspondance de Curry-Howard dont l'une des caractéristiques est que les propositions sont des types, tandis que les preuves dont des objets.

Parmi les théorèmes issus des mathématiques dont les preuves sont volumineuses et qui ont été démontrées à l'aide de Coq, on peut citer notamment :

• Théorème des quatre couleurs

Le théorème des quatre couleurs indique qu'il est possible en utilisant seulement quatre couleurs différentes de colorier n'importe quelle carte découpée en régions de sorte que deux régions ayant une frontière en commun ne soient pas de la même couleur. Le résultat fut initialement conjecturé en 1852, avec les deux premières preuves étant publiées en 1879 et 1880, celles-ci se révélant cependant fausses. La première preuve utilisant l'outil informatique date de 1976 et fut reprise et simplifiée par la suite. Enfin, en 2005, Georges Gonthier et Benjamin Werner ont réussi à formuler avec Coq une preuve formelle permettant à un ordinateur de complètement vérifier le théorème des quatre couleurs. À ce jour, aucune preuve qui ne fasse pas appel à un ordinateur n'a été découverte.

• Théorème de Feit-Thompson

Le théorème de Feit-Thompson énonce que tout groupe fini d'ordre impair est résoluble, ce qui équivaut à dire que tout groupe simple fini non commutatif est d'ordre pair. Le théorème fut conjecturé en 1911 par William Burnside et démontré en 1963 par Walter Feit et John Griggs Thompson. Une formalisation de la preuve en Coq a été achevée en 2012 par Georges Gonthier et son équipe du laboratoire commun Inria-Microsoft.

Coq sert également à la certification de logiciel. Parmi la multitude d'exemples, on peut mentionner :

• CompCert

CompCert est un projet ayant pour but de réaliser des compilateurs certifiés formellement. Ce projet développe notamment le compilateur CompCert C pour le langage C. Le projet est réalisé notamment en Coq.

• Iris Project

Iris Project utilise la logique de séparation (formalisée en Coq) pour certifier les propriétés de programmes concurrents.

Types, fonctions et preuves basiques

Déclaration de types

Pour définir un type sur Coq, une première méthode est l'induction. Cela consiste à utiliser les différents cas particuliers pour définir le cas général.

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Ici, pour le type day, on énumère les différentes valeurs que peut adopter le type, à savoir les jours de la semaine. Cette méthode permet notamment de définir des types dont l'ensemble de valeurs possibles est fini, comme les booléens ou les bits. Cependant, tenter de représenter les nombres avec cette méthode est contre-indiqué, car il faudrait un temps et une capacité de stockage disproportionnellement élevés.

Pour définir les nombres ou d'autres types dont l'ensemble de valeurs possibles est infini, il est possible de définir un type par récurrence.

Inductive nat : Type:=
  | O
  | S (n : nat).

Dans ce cas-là, par exemple, on définit le type nat (correspondant aux entiers naturels) par un cas initial, ici 0, modélisé par la lettre O, et une hérédité, ici le fait que pour tout n ∈ ℕ, il existe un n' appartenant à ce même intervalle tel que n corresponde à S n'. L'écriture mathématique équivalente de cette définition est : $\forall n>0,\exists n'\geqslant 0,n=n'+1$

Enfin, il est également possible avec Coq de créer un type utilisant un autre type pour sa définition. Ainsi, si l'on définit comme suit les teintes RGB d'une couleur :

Inductive rgb : Type :=
  | red
  | green
  | blue.

Il est possible de définir les composantes d'une couleur en utilisant le type rgb préalablement créé :

Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

Ainsi, color possède trois composantes, à savoir black, white et primary, cette dernière ayant elle-même trois composantes, red, green et blue.

Fonctions

Il y a plusieurs manières de définir une fonction dans Coq. La première est d'utiliser la commande Definition et de spécifier au cas par cas quel résultat la fonction retourne selon la valeur de la variable d'entrée.
Ainsi, en reprenant le type day, on peut définir la fonction next_weekday comme suit :

Definition next_weekday (d:day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday
  | sunday    => monday
  end.

Dans cet exemple, on introduit le nom de la fonction, on indique le nom utilisé en son sein pour désigner la variable ainsi que son type, puis le type du résultat.
L'instruction match d with sert à analyser la valeur de la variable d. La liste qui suit signifie que pour telle valeur de d (par exemple wednesday), on retourne le résultat indiqué par la flèche (ici thursday). Enfin, la commande end permet de délimiter la fin de la fonction.

Cependant, il est également possible de ne retenir que certains cas et de retourner une même réponse pour tous les cas non vérifiés, dans la même veine qu'un else dans d'autres langages.
Par exemple, en supposant que l'on a défini précédemment un type bool qui ne peut prendre que true et false comme valeurs, on peut établir la fonction suivante :

Definition isred (c : color) : bool :=
  match c with
  | black => false
  | white => false
  | primary red => true
  | primary _ => false
  end.

Ici, si l'on voulait écrire la fonction en Python, on aurait :

def isred(c) :
    if c == black :
        return False
    elif c == white :
        return False :
    elif c == primary[red] :
        return True
    else :
        return False

On remarque donc que le caractère _ signifie "dans tous les autres cas possibles", ce qui permet de ne retenir que les situations particulières et de généraliser le reste.

Une autre manière d'écrire une fonction est d'utiliser la commande Fixpoint. La différence majeure entre Fixpoint et Definition est la possibilité d'appeler la fonction récursivement avec Fixpoint.

Par exemple, une fonction pour définir si un entier naturel est pair s'écrit :

Fixpoint evenb(n:nat) : bool :=
  match n with
  | 0 => true
  | S 0 => false
  | S (S n') => evenb n'

Cela signifie que pour tout entier n, trois cas de figure se présentent :

1. $n=0\rightarrow n\ pair$
2. $n=1\rightarrow n\ non\ pair$
3. $\exists n',n=n'+2$

Dans le troisième cas, on réitère l'étude, mais avec n'.

Enfin, une troisième méthode pour définir une fonction est la commande Theorem qui permet, comme son nom l'indique, de définir un théorème, généralement sous la forme d'une égalité ou d'une implication. S'il s'agit d'une implication A -> B, A peut être utilisé comme hypothèse lors de la preuve.

Preuves simples

Structure générale

Dans Coq, la structure d'une preuve suit toujours la même structure :

Proof. (* On indique le début de la preuve... *)
(* On insère ici toutes les instructions nécessaires... *)
Qed. (* Quod erat demonstrandum, équivalent latin de C.Q.F.D., signifie que la preuve est finie *)

Tactiques

Les tactiques sont des instructions pour aider Coq à résoudre une preuve.

• simpl.

simpl. permet, comme son nom l'indique, de simplifier une formule.

• reflexivity.

reflexivity. permet de vérifier si une égalité est du type a = a. Si la réflexivité de l'égalité est prouvée, alors la proposition est vraie. Cette instruction permet généralement d'achever une preuve.

• intros n.

intros. s'utilise en début de preuve pour introduire les variables présentes dans un théorème ou une hypothèse. S'il y a plusieurs variables à introduire, il faut les séparer par des espaces

• unfold f.

unfold f. permet de développer l'expression à étudier selon la fonction f.

• rewrite <- / -> H.

Permet de réécrire l'expression en fonction de l'hypothèse H. La flèche <- indique que l'on souhaite passer du membre de droite à celui de gauche et inversement pour ->. Coq va ensuite essayer de trouver un membre de l'expression qui correspond au terme de départ et va le remplacer par le terme d'arrivée.

• destruct n as [n1 | n2 | ...] eqn:E.

destruct permet de décomposer une variable en plusieurs cas de figure qui sont traités séparément. destruct fonctionne différemment selon le type de la variable utilisée. Avec les booléens ou d'autres types binaires, on peut se passer du as [...] car il n'y a par définition que deux valeurs que peut prendre la variable. Avec les entiers, on va généralement décomposer sous la forme as [| n'], autrement dit, on établit une pseudo-récurrence en vérifiant pour n = 0 et ensuite pour tout n' tel que n = n' + 1. Il ne s'agit cependant pas d'une vraie récurrence car il n'y a pas de lien entre n et n'.

Séparation des cas

Dans Coq, certaines commandes comme destruct occasionnent une séparation de l'expression en plusieurs cas. Pour identifier ces cas, il y a deux méthodes.

1. Commencer chaque cas par une puce (-, + et * dans cet ordre)
2. Délimiter un cas par des astérisque {}, ce qui permet de réinitialiser la hiérarchie des puces

Preuve par récurrence, preuves à l'intérieur de preuves, preuves formelles et informelles

Preuve par récurrence

Bien que les tactiques mentionnées dans la partie précédente permettent de résoudre une grande partie des preuves, certains cas requièrent une attention plus particulière. Si la situation s'y prête, on peut notamment utiliser la récurrence avec la syntaxe suivante :

Proof.
  intros n. induction n as [| n' IHn']. (* On décompose n en un cas initial, généralement 0, et on introduit l'hypothèse que la proposition est vérifiée pour un palier arbitraire n'. *)
  - (* Initialisation. On met ici toutes les tactiques nécessaires pour prouver que la proposition est vérifiée pour le cas initial. *)
  - (* Hérédité. On met ici toutes les tactiques nécessaires pour prouver que la proposition est vérifiée à un niveau n' + 1 si elle est vérifiée pour n'. *)
Qed.

Ben que la récurrence soit une tactique puissante, il vaut mieux la réserver aux situations qui le nécessitent. Il est également nécessaire d'utiliser à un moment l'hypothèse d'hérédité avec rewrite. S'il est possible de compléter la preuve sans l'utiliser, une autre tactique aurait été probablement plus appropriée.

Preuves à l'intérieur de preuves

Parfois, il n'est pas possible de démontrer une équation telle quelle. Il faut passer par un lemme qui est introduit en Coq par l'instruction assert. Par exemple, la preuve servant à démontrer que $\forall n,m\in \mathbb {R} ,(0+n)*m=n*m$ se structure comme tel :

Proof.
  intros n m.            (* On introduit les deux variables n et m *)
  assert (H: 0 + n = n). (* On définit le lemme H qui dit que 0 + n = n *)
    { reflexivity. }     (* On vérifie que H est vrai *)
  rewrite -> H.          (* On reformule l'équation initiale en remplaçant 0 + n par n, maintenant que l'on sait que les deux sont égaux *)
  reflexivity.           (* Les deux membres de l'équation sont alors identiques, la preuve est achevée *)
Qed.

Preuves formelles et informelles

Le principe d'une preuve est de convaincre le lecteur de sa véracité. Cependant, tous les lecteurs n'ont pas la même capacité de compréhension.

Par exemple, en langage mathématique, le théorème de Taylor à l'ordre n en a pourrait s'écrire :

$f(x)=\sum _{k=0}^{n}{{\frac {f^{(k)}(a)}{k!}}{x-a}^{k}}+R_{n}(x),\lim _{x\to a}R_{n}(x)=0$

Cette écriture peut être lue aisément par un humain, mais pas par une machine. Cependant, si l'on écrit :

f(x) = \sum_{k=0}^{n}{\frac{f^{(k)}(a)}{k!}{x - a}^{k}} + R_{n}(x), \lim_{x \to a} R_{n}(x)= 0

Un humain aurait du mal à lire cette ligne de code, mais si un interpréteur LaTeX la lit, il affiche l'équation précédente. Il existe donc plusieurs façons de présenter la même information en fonction du lecteur visé. Il en est de même pour les preuves sur Coq.

• Preuves formelles

Les preuves formelles sont celles que Coq peut comprendre facilement et qui n'est pas prévue pour être facilement comprise par un humain. Par exemple, la preuve formelle de l'associativité de l'addition est structurée comme suit :

Proof. intros n m p. induction n as [| n' IHn']. reflexivity. simpl. rewrite -> IHn'. reflexivity.  Qed.

Le code est réduit à l'essentiel, mais la clarté pour le lecteur humain est moindre.

• Preuves informelles

Les preuves informelles sont celles que Coq accepte et qu'un humain peut comprendre facilement. Par exemple, la preuve informelle de l'associativité de l'addition est structurée comme tel :

Proof.
  intros n m p. induction n as [| n' IHn'].
  - (* n = 0 *)
    reflexivity.
  - (* n = S n' *)
    simpl. rewrite -> IHn'. reflexivity.
Qed.

Ici, on a éclaté le code pour notamment séparer les deux cas étudiés lors de la récurrence et on a ajouté des commentaires. Coq interprète toujours le code, mais un lecteur humain peut davantage comprendre ce qui se passe.

Listes, sacs de nombres et opérations sur ces types

Listes de nombres

Dans Coq, on peut définir une liste de nombres sous le type natlist de façon récursive. Une liste est composée soit de l'élément vide, soit de la concaténation d'un entier naturel et d'une autre liste. Parmi les différentes opérations que l'on peut exécuter sur les listes, on peut évoquer :

• Créer une liste de longueur déterminée composée d'un seul élément

Fixpoint repeat (n count : nat) : natlist :=
  match count with                     (* Si count vaut... *)
  | O => nil                           (* ... 0, on ferme la liste avec l'élément nul *)
  | S count' => n :: (repeat n count') (* ... count' + 1, on concatène le nombre avec la liste de longueur count' répétant ce nombre *)
  end.

• Calculer la longueur d'une liste

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil => O               (* Cas 1, la liste n'est composée que de l'élément nul, sa longueur est donc nulle *)
  | h :: t => S (length t) (* Cas 2, la liste est composée de la concaténation d'un entier et d'une liste, sa longueur vaut donc 1 + la longueur de cette deuxième liste *)
  end.

• Joindre deux listes

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil    => l2              (* Si la première liste est vide, le résultat de la jonction est donc la seule deuxième liste *)
  | h :: t => h :: (app t l2) (* Si la première liste est composée d'un entier et d'une liste, on concatène cet entier avec la jonction de la liste et de la deuxième liste *)
  end.

• Définir la tête et la queue d'une liste

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil => default (* Si la liste est vide, on retourne le nombre défini par défaut, l'élément vide n'ayant pas de premier élément *)
  | h :: t => h    (* Si la liste est composée d'un entier et d'une liste, on retourne l'entier, celui-ci étant le premier élément *)
  end.

Definition tl (l:natlist) : natlist :=
  match l with
  | nil => nil  (* Si la liste est vide, on retourne l'ensemble vide *)
  | h :: t => t (* Si la liste est composée d'un entier et d'une liste, on retourne la liste *)
  end.

Sacs de nombres

Un sac de nombres ressemble à une liste, à l'exception prêt qu'un même élément peut apparaître plusieurs fois. Mis à part ce détail, le type bag est défini comme une liste de nombres. Parmi les opérations possibles sur ce type, on peut citer :

• Compter le nombre d'occurrence d'un nombre au sein d'un sac

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0                          (* Si la liste est vide, l'élément recherché ne peut pas apparaître *)
  | h :: t => match h =? v with       (* Si la liste est composée d'un entier et d'une liste, on compare l'entier avec l'élément recherché *)
              | true => S (count v t) (* S'ils sont égaux, on continue la recherche sur le reste de la liste en ajoutant 1 au nombre d'occurrences *)
              | false => count v t    (* S'ils ne sont pas égaux, on continue la recherche sur le reste de la liste *)
              end
  end.

• Vérifier qu'un nombre appartient à un sac

Fixpoint member (v:nat) (s:bag) : bool :=
  match s with
  | nil => false
  | h :: t => match h =? v with
              | true => true
              | false => member v t
              end
  end.

• Retirer un ou toutes les occurrences d'un nombre dans un sac

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
  | nil => nil                               (* Si la liste est vide, on n'a plus rien à enlever *)
  | h :: t => match h =? v with              (* Similairement à count, si la liste est composée d'un entier et d'une liste, on compare l'entier à l'élément recherché *)
              | true => t                    (* S'ils sont égaux, on retourne le reste de la liste, car on a enlevé la première occurrence d'un élément *)
              | false => h :: remove_one v t (* S'ils ne sont pas égaux, on concatène l'entier avec le résultat de la recherche au sein de la liste restante *)
              end
  end.

remove_all et remove_one fonctionne exactement de la même manière, excepté que remove_all continue la recherche dans tous les cas.

Fixpoint remove_all (v:nat) (s:bag) : bag :=
  match s with
  | nil => nil
  | h :: t => match h =? v with
              | true => remove_all v t
              | false => h :: remove_all v t
              end
  end.

• Vérifier qu'un sac est inclus dans un deuxième sac

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | nil => true                                    (* Si le sac de référence est vide, il est forcément inclus dans le deuxième sac *)
  | h :: t => match (member h s2) with             (* Si le sac de référence est composée d'un entier et d'une liste, on regarde si cet entier est présent dans le deuxième sac *)
              | true => subset t (remove_one h s2) (* S'il est présent, on continue la recherche avec le reste du sac de référence est en retirant une occurrence de l'élément dans le deuxième sac *)
              | false => false                     (* S'il n'est pas présent, alors le sac de référence n'est pas inclus dans le deuxième sac *)
              end
  end.

Sources et annexes

Sources

• Software Foundations volume 1 [1]

• Page Wikipédia de Coq [2]

Annexe

• Théorème des quatre couleurs [3]

• Théorème de Feit-Thompson [4]

• Compcert [5]

• Iris Project [6]

• Software Foundations [7]

• Verified Software Toolchain [8]

• FSCQ [9]

• Bedrock [10]

• CFML [11]