peut égal ement effectuer des ca lcul s,
numé1iques ou symboliques. L'un des plus
uti I isés est le logiciel Coq , déve loppé
par des chercheurs d ' In ria depui s 1984.
L ' utili sa teur intera git avec Coq pour
introduire des définition s. énoncer des
th éorèmes et construire des preuves. L e
sys tème vérifie alors la va lidité de ces
divers éléments.
L e log iciel Coq a été utili sé pour vérifier des démonstrations de grande ampleur.
A in si on peut citer la preuve du théorème fondamental de ! 'a lgè bre ( tout
po lynôme non constant à coefficients
dans C admet au moins une rac ine) en
2000 par une équipe de chercheurs de
Nimègue (Pays- Bas) ou encore la preuve
du th éorème des quatre cou leurs (toute
carte planaire peut être co loriée avec
seulement quatre cou leurs sans que deux
pays ayant une frontière commune soient
de la même couleur) en 2005 par deux
cherc heurs de Microsoft Resea rch et
lnri a (Georges Gonthier et Benjamin
Werner) . Il ex iste d 'a utres d ' assistants
de preuve , développés dans des laboratoires de recherche du monde entier :
PYS (SRL Cali fornie) , HOL-Light (Intel ,
Oregon), Isabell e (TUM , Muni ch) ...
la démonstration automatique
Deuxième outil : le démonstrateur automatique . C'est un progra mme qui prend
en entrée un énoncé mathématique et
tente d 'en étab lir une preuve automati -
quement. En cas de succès, on a la garantie que ! 'énoncé est vrai . En cas d'échec ,
en revanche, il se peut que l ' énoncé so it
tout de même vra i mais que le logiciel
n·a pas su en trouver une preuve.
On a montré qu ' il n' es t pas possible
d ' éc rire un progra mme qui prend en
entrée un énoncé math ématique et qui
déten11ine, en un temps fini, si cet énoncé
es t vra i ou fa ux. En quelque sorte, c'est
là une assurance anti-chômage pour les
POUR LES MATHS
Coq en action
Voici un exemple d'utilisation de Coq. On commence par
définir la propriété« être un multiple de 5 » pour un entier
relatif x.
Definition mult5 (x: Z) : = exists k: Z, x = 5 * k.
Ici le symbole Z dénote l'ensemble des entiers relatifs, fourni
par la bibliothèque de Coq. La syntaxe (x: Z) peut se lire comme
« x est un entier relatif ». On peut ensuite énoncer un théorème stipulant que si deux entiers a et b sont multiples de
5, alors leur somme l'est également.
Theorem thmt: forall ab: Z,
mult5 a f\ mult5 b ! mult5 (a+ b).
Ici « thm1 » est le nom que l'on a choisi de donner à ce
théorème, par exemple pour y faire référence plus tard.
Pour procéder à la preuve de ce théorème, on commence
par la commande « intros » qui permet de séparer les hypothèses (a et b sont des entiers multiples de 5) et la conclusion à prouver (a + b est multiple de 5). On poursuit la
preuve avec la commande « exists » qui nous permet de
donner l'entier kjustifiant que a+ b est multiple de 5, c'està-dire tel que a+b est égal à 5* k.
On peut terminer la preuve automatiquement avec la commande « ring », car il ne reste que du calcul.
a + b • 5 • ( k 1 + k2)
La figure montre l'interface graphique du logiciel Coq, avec
notamment les commandes saisies par l'utilisateur dans la
partie gauche et le but à prouver dans la partie droite.
mathématiciens. Il n' y a pas de contradiction pour autant à chercher à développer
des démonstrateurs automatiques. Il faut
seul ement être consc ient du fa it qu ' un
démon strateur automatique pourra tou -
jours ne pas terminer ou répondre « j e
ne sa is pas », y co mpri s sur des énoncés vra is.
Hors-série n ° 52. Mathématiques & informatique Tangente
77
numé1iques ou symboliques. L'un des plus
uti I isés est le logiciel Coq , déve loppé
par des chercheurs d ' In ria depui s 1984.
L ' utili sa teur intera git avec Coq pour
introduire des définition s. énoncer des
th éorèmes et construire des preuves. L e
sys tème vérifie alors la va lidité de ces
divers éléments.
L e log iciel Coq a été utili sé pour vérifier des démonstrations de grande ampleur.
A in si on peut citer la preuve du théorème fondamental de ! 'a lgè bre ( tout
po lynôme non constant à coefficients
dans C admet au moins une rac ine) en
2000 par une équipe de chercheurs de
Nimègue (Pays- Bas) ou encore la preuve
du th éorème des quatre cou leurs (toute
carte planaire peut être co loriée avec
seulement quatre cou leurs sans que deux
pays ayant une frontière commune soient
de la même couleur) en 2005 par deux
cherc heurs de Microsoft Resea rch et
lnri a (Georges Gonthier et Benjamin
Werner) . Il ex iste d 'a utres d ' assistants
de preuve , développés dans des laboratoires de recherche du monde entier :
PYS (SRL Cali fornie) , HOL-Light (Intel ,
Oregon), Isabell e (TUM , Muni ch) ...
la démonstration automatique
Deuxième outil : le démonstrateur automatique . C'est un progra mme qui prend
en entrée un énoncé mathématique et
tente d 'en étab lir une preuve automati -
quement. En cas de succès, on a la garantie que ! 'énoncé est vrai . En cas d'échec ,
en revanche, il se peut que l ' énoncé so it
tout de même vra i mais que le logiciel
n·a pas su en trouver une preuve.
On a montré qu ' il n' es t pas possible
d ' éc rire un progra mme qui prend en
entrée un énoncé math ématique et qui
déten11ine, en un temps fini, si cet énoncé
es t vra i ou fa ux. En quelque sorte, c'est
là une assurance anti-chômage pour les
POUR LES MATHS
Coq en action
Voici un exemple d'utilisation de Coq. On commence par
définir la propriété« être un multiple de 5 » pour un entier
relatif x.
Definition mult5 (x: Z) : = exists k: Z, x = 5 * k.
Ici le symbole Z dénote l'ensemble des entiers relatifs, fourni
par la bibliothèque de Coq. La syntaxe (x: Z) peut se lire comme
« x est un entier relatif ». On peut ensuite énoncer un théorème stipulant que si deux entiers a et b sont multiples de
5, alors leur somme l'est également.
Theorem thmt: forall ab: Z,
mult5 a f\ mult5 b ! mult5 (a+ b).
Ici « thm1 » est le nom que l'on a choisi de donner à ce
théorème, par exemple pour y faire référence plus tard.
Pour procéder à la preuve de ce théorème, on commence
par la commande « intros » qui permet de séparer les hypothèses (a et b sont des entiers multiples de 5) et la conclusion à prouver (a + b est multiple de 5). On poursuit la
preuve avec la commande « exists » qui nous permet de
donner l'entier kjustifiant que a+ b est multiple de 5, c'està-dire tel que a+b est égal à 5* k.
On peut terminer la preuve automatiquement avec la commande « ring », car il ne reste que du calcul.
a + b • 5 • ( k 1 + k2)
La figure montre l'interface graphique du logiciel Coq, avec
notamment les commandes saisies par l'utilisateur dans la
partie gauche et le but à prouver dans la partie droite.
mathématiciens. Il n' y a pas de contradiction pour autant à chercher à développer
des démonstrateurs automatiques. Il faut
seul ement être consc ient du fa it qu ' un
démon strateur automatique pourra tou -
jours ne pas terminer ou répondre « j e
ne sa is pas », y co mpri s sur des énoncés vra is.
Hors-série n ° 52. Mathématiques & informatique Tangente
77