Ce cours traite de la preuve formelle, comme discipline de l’informatique. Il prolonge donc le cours de tronc commun « Fondements des systèmes de preuves », mais en mettant l’accent sur la construction effective de preuves formelles et de leur vérification sur ordinateur.
Si la logique mathématique, c’est-à-dire la formalisation complète du raisonnement est une discipline déjà relativement ancienne, elle a été relativement bouleversée par l’arrivée de l’ordinateur: la capacité de la machine à manipuler rapidement de grosses expressions symboliques permet de formaliser entièrement des raisonnements non-triviaux. La question que se pose le logicien n’est alors plus tant « existe-t-il une formalisation de tel raisonnement ? » que de construire et d’exhiber cette formalisation.
C’est avec cette observation à l’esprit que nous chercherons à traiter des points suivants:
Le choix du formalisme est important pour la pratique des mathématiques formelles. Non seulement il doit être capable d’exprimer la preuve conçue par le mathématicien, mais il doit permettre de le faire de la manière la plus facile et la plus intuitive possible. De fait, les évolutions récentes du Calcul des Constructions Inductives ont presque toujours été motivées par la pratique et sont donc postérieures aux premières implémentations de CoC puis Coq.
Plus encore qu’en mathématiques usuelles, savoir bien énoncer les propositions que l’on espère prouver est essentiel si l’on veut ultimement aboutir à une preuve formelle. Si l’on fait l’analogie entre les activités de prouver et programmer, alors le choix de la modélisation correspond à celui de la structure de représentation des données, avec les conséquences immédiates et évidentes sur l’architecture du logiciel obtenu.
Plus généralement, il nous semble que les analogies entre les activités de preuves et de programmation sont nombreuses, et s’il existe un « art » de la bonne programmation, il en va de même pour les preuves formelles. De plus, à chaque couple formalisme/problème, correspond un, ou plusieurs, style de bonne preuve, tout comme il existe de bons styles de programmation pour un problème et un langage de programmation donné.
Nous nous attacherons particulièrement à la modélisation et la formalisation de problèmes informatiques où la sûreté est importante, et à la preuve de correction de programmes.
Enfin nous chercherons à décrire les grands principes d’un logiciel d’assistant à la démonstration. Poursuivant encore l’analogie avec la programmation, ceci correspondrait à la description d’un compilateur. Nous nous intéresserons principalement au système de preuves Coq.
Aujourd’hui, on désigne généralement par « théorie des types » un formalisme logique dont les objets sont des λ-termes typés. Il existe plusieurs formalismes rentrant dans cette catégorie, et ils se distinguent essentiellement par le système de types plus ou moins riche des objets, ainsi que par la logique pour parler de ces objets. On peut citer en particulier la logique d’ordre supérieur de Church, la Théorie des Types de Martin-Löf, la logique du système PVS et le Calcul des Constructions Inductives (CCI) dont les variantes implantées par Coq seront l’objet et le support premier de ce cours.
Les objets de la logique d’ordre supérieur de Church sont les λ-termes simplement typés. Les trois autres formalismes utilisent essentiellement des variantes (ou plutôt des fragments) du langage de programmation ML. Ils se distinguent par leur logique:
Sur tous ces points, nous renvoyons bien sûr au cours de tronc commun. La plupart seront par ailleurs illustrés tout au long du cours.
Un point commun essentiel de CCI et de la théorie de Martin-Löf est bien sûr qu’ils sont construits sur la correspondance de Curry-Howard. Rappelons que cela signifie que:
En simplifiant, on peut dire que les avantages informatiques de cette approche sont:
Le système Coq est un système de traitement de preuves pour une version prédicative du Calcul des Constructions Inductives. Les composantes essentielles du système Coq sont:
Le formalisme implanté par Coq sera donc couramment appelé CCI. Il s’agit pour l’essentiel d’une extension du Calcul de Constructions (CC) traité en tronc commun. Il nous faut dès maintenant signaler quelques différences de notations avec la syntaxe employée jusqu’ici.
Tout d’abord, Coq est conçu pour pouvoir être utilisé par une interface en mode texte (ASCII ou Unicode). Les notations de Coq pour λ x:A.t et Π x:A.B sont:
Par ailleurs, essentiellement pour des raisons historiques, les sortes portent d’autres noms en Coq que dans le cours de tronc commun. Rappelons que les sortes sont des constantes particulières, qui sont les types des types. Dans le cours de tronc commun, on utilisait une sorte Type qui est le type des types, et une sorte Kind qui était le type de Type. Cette dernière servant essentiellement à énoncer les règles correspondant au polymorphisme.
Dans les versions de Coq antérieures à la version 8.0, Type est remplacée par deux sortes « jumelles », Prop et Set. Intuitivement, Set contient les types de données (objets « calculatoires » qui sont pris en compte par le processus d’extraction de programmes de Coq – cf le chapitre consacré) et Prop les énoncés « logiques » (qui sont « oubliés » par le processus d’extraction).
Depuis la version 8.0 de Coq, Prop garde le rôle joué par Type dans le Calcul des Constructions traité dans le cours de tronc commun. Il reste une sorte nommée Set mais qui est une version prédicative de Type. Typiquement, le type forall A:Set, A->A ne peut pas s’appliquer à lui-même en Coq version 8.0.
Pour ne rien arranger, la sorte Kind se trouve renommée Type dans Coq. Au lecteur qui serait tenté de voir là une source de confusion, rappelons simplement que l’informatique est sans doute la science de la bureaucratie et d’une vision un peu tyrannique de l’ordre et particulièrement du renommage…
A partir de là, nous pouvons taper nos premières commandes pour utiliser le vérificateur de type. En syntaxe Coq, l’identité polymorphe est donc notée fun (A:Type) (a:A) => a. On demande au système de vérifier la bonne-formation d’un objet par la commande Check; les commandes Coq étant toujours terminées par un point, cela donne:
Toutes les opérations de typage de Coq ont lieu dans un environnement global. Cet environnement correspond au contexte Γ des jugements de typage Γ ⊢ t:T. Il est donc possible de pousser de nouvelles variables dans l’environnement:
De plus, l’environnement de Coq peut également contenir des constantes, ou abréviations. Pour cela, on associe un terme à un nom; de plus, l’environnement mémorise aussi un des types du corps de la constante1.
Construire une preuve revient, dans notre formalisme, à exhiber un λ-terme du type attendu. L’utilisateur dispose pour cela d’un mode de preuve interactif. Les commandes de ce mode interactif sont appelées tactiques de preuve. Voici une illustration sommaire de leur principe, sur un exemple simple; on se donne trois variables propositionnelles A, B et C, puis l’on cherche à prouver la tautologie suivante:
On a alors le lemme comme seul but courant, sous la double barre. On peut commencer à construire la preuve:
On voit que (A->B)->C et B ont été poussées comme hypothèses dans le contexte local, au-dessus de la double barre. Elles ont été nommées comme demandé.
Du point de vue de la construction de la preuve, cette tactique correspond à la λ-abstraction comme on peut le voir en affichant la preuve partielle construite.
Une preuve partielle peut comporter plusieurs points d’interrogations, c’est-à-dire que l’on peut avoir plusieurs sous-buts simultanément, chacun avec son contexte local.
La tactique apply correspond à l’application:
On est alors passé au terme de preuve partiel
fun (c:(A->B)->C) (b:B) => c ?1
où le but courant est maintenant A->C. On finit donc la preuve
par
La commande Qed (ou Save) permet alors d’ajouter à l’environnement global le terme exemp1 ainsi crée:
Rassurons enfin le lecteur: une preuve aussi simple peut, heureusement, également être trouvée automatiquement par les tactiques de preuve plus évoluées dont dispose le système. Plus généralement, ce document n’est d’ailleurs pas un manuel d’utilisateur, ni un cours de Coq. Nous renvoyons pour cela à la documentation standard de Coq [Coq07].
Le type des entiers naturels est le plus petit type contenant 0 et clos par le successeur S; une telle définition par plus petit point fixe est appelée une définition inductive.
La syntaxe en Coq d’une telle définition est:
Cette commande ajoute à l’environnement du système les objets suivants:
nat : Set
O : nat et S : nat -> nat appelés constructeurs de nat.
En général, cette définition (ainsi que la plupart de celles qui suivent) sont déjà présentes dans l’environnement du système au lancement.
Remarque
Informellemment, le plus petit type ainsi défini est celui dont les
habitants sont O, (S O), (S (S O)), etc. On a
donc bien une
représentation de la notion mathématique d’entier naturel.
Remarque
La vision informatique est que cette définition est la version Coq du
type concret ML bien connu:
# type nat = O | S of nat;;
On peut remarquer au passage, qu’en Coq le constructeur S est
fonctionnel et peut donc exister sans son argument. Il s’agit là d’un
point syntaxique, d’importance marginale.
Remarque
D’un point de vue ensembliste, les entiers naturels sont le plus petit
point fixe de l’opérateur suivant:
| F(X) ≡ {0}⋃{(S x),x∈ X}. |
Cet opérateur est monotone, et admet donc un plus petit point fixe. En effet, l’univers des ensembles est un treillis complet par rapport à l’ordre d’inclusion.
Cette possibilité de voir la définition comme un plus petit point fixe sera commune à toutes les définitions inductives. Par ailleurs on verra plus tard, comment ces points fixes apparaissent également dans la sémantique de la théorie.
Dans ce chapitre, nous n’expliciterons pas les règles de typage qui sous-tendent les définitions inductives. Elles seront explicitées en partie lors du cours 3.
Par défaut, les entiers de nat sont représentés en Coq via la
notation standard en base 10. Par exemple, la notation 3 désigne
l’entier naturel (S(S(S O))). Qu’il soit clair que ces deux
écritures désignent le même terme et sont représentées de manière
identique dans le système.
On verra plus loin que les symboles infixes +, *, <=, ... désignent aussi par défaut en Coq les opérations arithmétiques sur nat. À tout moment lors d’une session Coq, on peut désactiver les notations évoluées telles que 3, +, <=, ... en utilisant la commande Set Printing All.
Les entiers sont l’archétype du type de données récursif. Tout comme en ML, l’on calcule sur ces entiers grâce à des fonctions définies par deux mécanismes fondamentaux:
Le premier exemple d’une telle fonction est en général l’addition. Voici sa définition en ML:
let rec plus n m = match n with O -> m | (S p) -> S(plus p m);;
et l’équivalent en syntaxe Coq:
Et voici, de même, une définition de la multiplication:
On comprend bien que la construction Fixpoint correspond à la définition d’une fonction récursive, au même titre que le let rec de ML. On note en revanche que le premier des deux arguments de chacune des deux fonctions est syntaxiquement distingué par l’emploi du mot-clé struct. La raison en est simple: lorsque la théorie des types, comme ici, est utilisée en tant que formalisme logique, la cohérence du formalisme est essentiellement assurée par la propriété de normalisation, c’est-à-dire de la terminaison des calculs. Une sommaire justification informelle pourrait être donnée ainsi: supposons qu’il soit possible de définir la fonction suivante.
Il est alors clair que l’objet (non_sens O) ne correspond
mathématiquement pas à un entier naturel, et ne saurait être accepté
dans le formalisme.
On reviendra par la suite à l’étude de la propriété de normalisation, et renverra, pour l’instant, au cours de tronc commun. Retenons pour l’instant que:
Toutes les fonctions récursives acceptées par le système doivent terminer.
Pour pouvoir définir des règles de typage, il importe donc d’isoler une classe de fonctions récursives terminantes. Pour ce faire, on généralise la classe des fonctions définissables dans le système T de Gödel:
nat de la forme
(S n). Sont considérés comme structurellement plus petit que
(S n) les termes suivants:
Une fonction est structurellement récursive si l’on peut distinguer l’un de ses arguments, qui décroit structurellement à chaque appel récursif.
En Coq, seules des fonctions structurellement récursives peuvent être définies par Fixpoint.
Les fonctions plus et mult définies ci-dessus sont structurellement récursives par rapport à leur premier argument. Bien sûr, la fonction non_sens est rejetée par le système.
Voici une définition alternative de l’addition, qui décroit par rapport à son second argument.
Dans le système T, seul n est considéré comme structurellement plus petit que (S n). La définition ci-dessus est plus souple, par exemple voici une définition possible en Coq du quotient de la division entière par deux:
Il faut noter que cette fonction pourrait également être définie dans le système T, mais de manière un peu plus lourde. Il s’agit donc là d’un aménagement du formalisme qui n’étend pas l’expressivité du formalisme, mais juste son confort d’utilisation.
Dans un registre différent, le mécanisme de récursion structurelle permet la définition de fonctions logiquement complexes, c’est-à-dire qui croissent très vite. L’exemple le plus connu est la fonction due à Ackermann, dont voici la définition ML:
let rec ack = function O,m -> S(m) | S(n),O -> ack(n,(S(O))) | S(n),S(m) -> ack(n,ack(S(n),m));;
La terminaison de cette définition est assurée par une décroissance de la paire d’arguments vis-à-vis de l’ordre lexicographique. En terme de récursion structurelle, ceci est codé par l’utilisation de deux récursions emboîtées. En Coq, la syntaxe est alors un peu plus complexe; la commande fix jouant le rôle d’un let rec…in:
Donnons un exemple simple (et classique) d’utilisation de la règle de conversion; il s’agit de prouver 2+2=4 où + est la notation infixe de Coq pour plus et 2 et 4 les représentations de S (S O) et S (S (S (S O))). Ici, cette proposition s’énonce:
Il suffit d’observer que le terme correspondant à 2+2 se réduit effectivement vers 4, et donc que la proposition est logiquement identifiée à 4=4:
Remarquons que la tactique simpl, qui procède donc à la β-normalisation du but courant, ne construit pas de terme-preuve. Cela est dû à la forme de la règle de conversion qui, rappelons-le est:
|
On voit bien que les termes-preuves de la conclusion et de la prémisse principale sont identiques.
En conséquence, l’on pourrait dans l’exemple précédent, se passer complètement de simpl et utiliser juste reflexivity, qui construit la preuve correspondant à la réflexivité de l’égalité. La définition exacte du prédicat d’égalité sera détaillée plus tard.
Le fait que nat est bien le plus petit type clos par ses deux constructeurs est exprimé par le schéma de récurrence. Il s’agit d’une propriété logique qui s’énonce ainsi: soit P un prédicat sur les entiers; pour que la proposition P(n) soit vraie pour tout entier n, il suffit que les deux conditions suffisantes soient vérifiées:
Dans une logique d’ordre supérieur, ce schéma peut être exprimé comme une proposition. En syntaxe Coq:
forall (P: nat -> Prop),
(P O) ->
(forall (m:nat), (P m)->(P (S m)))->
forall (n:nat), (P n)
De fait, la définition d’un type inductif génère automatiquement une preuve du schéma de récurrence correspondant. Si le type inductif est nommé I, la preuve du schéma de récurrence s’appellera I_ind; par exemple:
L’utilisation du schéma de récurrence en Coq se fait grâce aux tactiques elim et induction.
Voici un autre exemple simple, combinant le calcul et le raisonnement par récurrence. Il s’agit de prouver une première étape vers la commutativité de l’addition, à savoir:
Cette preuve se fait bien sûr par récurrence sur n; le cas de base est trivial:
Pour le cas par récurrence, on peut procéder à une étape de réduction:
Il suffit alors d’utiliser l’hypothèse de récurrence pour remplacer dans le but courant, p+0 par p; cela peut se faire par:
Comme en ML, le principe de définitions inductives permet la construction de types de données plus complexes que les entiers. Suivent quelques exemples courants.
Il est sans doute inutile de rappeler la structure des listes, avec leurs deux constructeurs nil et cons. La commande définissant les listes d’entiers naturels est bien sûr:
Une première remarque, marginale, est que contrairement à ML, les constructeurs peuvent avoir plusieurs arguments: ici cons est curryfié.
Il est préférable de remplacer la définition précédente par une autre où le type des éléments des listes est un paramètre. La bonne définition des listes est:
Il s’agit de la même définition, mais paramétrée par le type A. Cette abstraction est possible grâce aux types fonctionnels:
A titre d’exemple, on écrira ainsi l’équivalent de l’objet ML [1;2;3]:
À condition de recourir à la définition définie dans le module List de la bibliothèque standard de Coq, on peut aussi utiliser la notation suivante:
Le schéma de récurrence structurelle sur les listes est:
On reconnaît la même structure que pour les entiers, avec toutefois l’argument supplémentaire de cons et la paramétrisation par rapport à A.
Un exemple courant de type paramétré est le type somme:
Son schéma d’élimination est plus simple, puisque le type est non récursif; il s’agit juste d’exprimer que tout élément de (sum A B) ne peut être construit qu’à partir de l’un des deux constructeurs:
Dans tous les exemples de types récursifs vus jusqu’ici, l’ordre correspondant à la récursion (et la récurrence) structurelle se confondait avec la relation de sous-terme. Le mécanisme des types inductifs autorise toutefois des constructions plus générales.
La définition qui suit est souvent appelé « type des ordinaux » par abus de langage. Il s’agit en fait d’une notation ordinale, qui ne permet que la représentation d’un fragment des ordinaux constructible dans CCI. Il s’agit d’une copie du type des entiers naturels, étendue par un nouveau constructeur correspondant à la limite ordinale:
On remarque que le constructeur lim est récursif, mais que son argument est une suite entière d’ordinaux.
L’ordre de la récursion structurelle est alors généralisé de la manière suivante: quel que soit les termes n de type nat et f de type nat→ord, (f n) est structurellement plus petit que (limit f).
Voici une définition légale de fonction sur ce type des ordinaux:
Cette vision de la récursion structurelle est également reflétée dans l’énoncé du schéma de récurrence du type:
C’est-à-dire que pour appliquer le schéma spécialisé à un prédicat P, il faut vérifier que si:
alors (lim f) vérifie également P.
On peut utiliser l’idée précédente pour définir un type d’arbre très général: en utilisant le polymorphisme on s’autorise à indexer les fils de chaque nœud par un type arbitraire.
Ce type est très peu intuitif. Il utilise et combine toutes les ressources du formalismes et permet ainsi la construction de très nombreux éléments. De fait, le logicien anglais Peter Aczel a prouvé qu’il était possible d’encoder les éléments de la théorie des ensembles dans ce type.
Nous avons vu comment construire des objets concrets. Le mécanisme de définitions inductives permet également la définition d’objets plus logiques, et en particulier de prédicats. En particulier, ce sera en général la manière la plus commode d’isoler une partie des éléments d’un type inductif.
En théorie des ensembles, une définition possible de l’ensemble des entiers pairs est de dire que c’est le plus petit ensemble tel que:
La même définition est possible dans CCI. Le prédicat even, « être pair », étant un objet de type nat→Prop. Les deux clauses de la définition ci-dessus correspondant aux deux constructeurs du prédicat inductif. En Coq:
On voit bien que la structure d’une preuve de parité est récursive, à l’image de la structure d’un terme de type nat. Ceci est reflété dans le schéma de récurrence qui permet de prouver des propriétés d’entiers pairs:
Un exemple essentiel est l’ordre sur les entiers:
Son principe de récurrence:
Exercice Prouver:
forall (n m:nat), (le n m)->(le (S n) (S m)) forall (n:nat), (le O n) forall (n m:nat), (le n m)->(le m p)->(le n p)
Voici un exemple pour illustrer les subtilités propres aux mathématiques formelles. On peut proposer une définition alternative à le:
Or cette définition, qui semble raisonnable et est mathématiquement saine, est peu praticable telle quelle. En particulier la preuve de la transitivité est très pénible; on peut utiliser cette définition, mais pour certaines propriétés, il vaut mieux commencer par prouver d’abord l’équivalence avec la définition précédente. L’on risque sinon de s’ensabler rapidement.