Coq (logiciel)
Pour les articles homonymes, voir Coq (homonymie).
Cet article est une ébauche concernant les mathématiques et un logiciel libre.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
.mw-parser-output .entete.informatique{background-image:url("//upload.wikimedia.org/wikipedia/commons/a/ae/Picto-infoboxinfo.png")}
CoqIde : l'environnement de développement de Coq.
| Développé par | INRIA, Université Paris Diderot, École polytechnique, Université Paris-Sud, École normale supérieure de Lyon |
|---|---|
| Première version | 1984 |
| Dernière version | 8.8.0 (17 avril 2018)[1] |
| Dépôt | scm.gforge.inria.fr/anonscm/git/coq/coq.git |
| Écrit en | OCaml |
| Système d'exploitation | Multiplateforme |
| Environnement | Multiplate-forme |
| Langues | Anglais |
| Type | Assistant de preuve |
| Licence | GNU LGPL 2.1 |
| Site web | The Coq Proof Assistant |
Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 d'Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon).
Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!.
Coq a été récompensé du ACM SIGPLAN Programming Languages Software 2013 Award.
Sommaire
1 Caractéristiques du logiciel
2 Éléments du langage
2.1 Exemple de programme
2.2 Exemple de démonstration (avec Ltac)
3 Notes et références
4 Voir aussi
4.1 Liens externes
Caractéristiques du logiciel |
Coq est fondé sur le calcul des constructions, une théorie des types d'ordre supérieur, et son langage de spécification est une forme de lambda-calcul typé. Le calcul des constructions utilisé dans Coq comprend directement les constructions inductives, d'où son nom de calcul des constructions inductives (CIC).
Coq a été récemment doté de fonctionnalités d'automatisation croissantes. Citons notamment la tactique Omega qui décide l'arithmétique de Presburger[2].
Plus particulièrement, Coq permet :
- de manipuler des assertions du calcul ;
- de vérifier mécaniquement des preuves de ces assertions ;
- d'aider à la recherche de preuves formelles ;
- de synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications.
C'est un logiciel libre distribué selon les termes de la licence GNU LGPL.
Parmi les grands succès de Coq, on peut citer :
théorème des quatre couleurs : la démonstration complètement mécanisée a été terminée en 2004 par Georges Gonthier et Benjamin Werner ;
théorème de Feit-Thompson : la preuve du théorème a été terminée par Georges Gonthier et son équipe en septembre 2012[3] ;
CompCert C un compilateur optimisant le C qui est en grande partie programmé et prouvé en Coq.
Éléments du langage |
Coq utilise la correspondance de Curry-Howard. La preuve d'une proposition est vue comme un programme dont le type est cette proposition.
Pour définir un programme ou une preuve, il faut:
- Soit l'écrire dans le langage Gallina, proche du langage de programmation fonctionnelle OCaml.
- Soit déclarer son type (ou la proposition que l'on veut démontrer). Le langage Ltac permet alors de définir cette preuve/programme par chaînage arrière, de façon interactive. Cette méthode est privilégiée pour les preuves mathématiques car Coq est alors capable de deviner certaines étapes intermédiaires.
Il est aussi possible d'utiliser SSReflect à la place de Ltac. Autrefois développé séparément, il est maintenant inclus par défaut dans Coq.
Exemple de programme |
- La fonction factorielle (avec Gallina):
Require Import Arith List Bool.
Fixpoint factorielle (x : nat) : nat :=
match x with
0 => 1
| S p => x * factorielle( p )
end.
- La fonction factorielle (avec Ltac):
Require Import Arith List Bool.
Definition factorielle: forall n:nat, nat.
(* on nomme l'argument *)
intro n.
(* on fait une définition par récurrence*)
induction n.
* (* si l'argument est 0, on retourne 1*)
apply 1%nat.
* (* si l'argument de la forme (S n), on retourne un produit *)
apply Nat.mul.
- (* 1er terme du produit: valeur de factorielle en n *)
apply IHn.
- (* 2e terme du produit: le successeur de n *)
apply S.
+ apply n.
(*On indique que la définition est terminée et que l'on souhaite pouvoir calculer cette fonction. *)
Defined.
Exemple de démonstration (avec Ltac) |
- Tout entier naturel est soit pair, soit impair.
Require Import Omega.
Lemma odd_or_ind: forall n : nat,
(exists p:nat, n=2*p) / (exists p:nat, n = 1 + 2 * p).
Proof.
induction n.
- (* cas 0 *) left. exists 0. trivial.
- (* cas (n + 1) *)
destruct IHn as [[p Hpair] | [p Himpair]].
+ (* n pair *)
right. exists p. omega.
+ (* n impair *)
left. exists (p + 1). omega.
(* On indique que la preuve est terminée et qu'elle ne sera pas utilisée comme un programme.*)
Qed.
Notes et références |
(en) « Coq 8.8.0 is out | The Coq Proof Assistant » (consulté le 8 mai 2018)
L'arithmétique de Presburger, contrairement à l'arithmétique usuelle due à Peano, est une théorie complète, c'est-à-dire que pour tout énoncé de son langage on peut décider si c'est un théorème de la théorie ou non (sa négation étant alors théorème). Cette arithmétique de Presburger, qui n'a pas d'axiome pour la multiplication, échappe donc à l'incomplétude énoncée par théorème d'incomplétude.
(en) « Feit-Thompson theorem has been totally checked in Coq », Msr-inria.inria.fr, 20 septembre 2012(consulté le 25 septembre 2012).
Voir aussi |
- Démonstration automatique de théorèmes
- Isabelle
- Mizar
- PhoX
- PVS
Liens externes |
(en) Le site du projet Coq
(en) Le Wiki de Coq
(en) Compte-rendu de l'équipe-projet PI.R2 qui développe Coq
(fr) Livre sur coq de Yves Bertot et Pierre Castéran
Portail des logiciels libres 
Portail des mathématiques 
Portail de la logique
