Coq permet, on le verra ci-dessous, de guider l’utilisateur dans la construction de la preuve ; Par exemple, si on pense des choses comme « et si j’utilisais l’axiome A1, est-ce que je peux y arriver ? », Coq permet de faire rapidement le test et de voir ce qu’il reste alors à faire.

Mais Coq ne permet pas d’avoir automatiquement la preuve, celle-ci reste de la responsabilité de son utilisateur. Otter est une sorte de logiciel de calcul formel dans une algèbre de Boole et peut, lui, fournir automatiquement la preuve d’un théorème qu’on lui soumet. Intéressant, si au bout d’un certain temps, la preuve ne vient pas, on peut essayer son côté sombre Mace qui, lui, cherche un contre-exemple. Otter n’est plus développé, mais il lui succède Prover9 qu’on peut installer ou tester en ligne.

Ci-dessous on va montrer comment Coq aide à démontrer des syllogismes et à chaque fois, on va comparer avec la version Otter prover9. Toutefois, Prolog quand à lui, est capable de trouver tout seul une démonstration.

CoqIde permettant aussi de faire du calcul propositionnel, on peut y revoir les exemples de l’article précédent. Par exemple, le tiers exclu :

Le lemme dit que pour toute proposition $p$ (p est déclarée de « type » $Prop$) on a $p \vee \neg p$.

Une première difficulté pour l’utilisation de Coq dans l’enseignement secondaire est que celui-ci est basé sur la théorie des types.

Une autre est que même en supposant p vraie, la « tactique » $tauto$ échoue :

Error: tauto failed.

Peut-être la tactique tauto après avoir momentanément supposé $p$ vraie, n’était pas la bonne. CoqIde a un outil permettant de tester des tactiques automatiquement, l’une après l’autre. C’est le bouton tout à droite :

Mais ça ne marche toujours pas, il échoue toujours arrivé à la stratégie « tauto » :

Tout ce qu’il a réussi à faire, c’est remplacer $\neg p$ par $p \Rightarrow \bot$ et c’est tout. Ceci ne signifie pas que CoqIde est bogué mais que la logique intuitionniste refuse le tiers exclu.

La solution semble dater de Kurt Gödel (1933) : Ajouter des axiomes comme celui du tiers exclu pour permettre à CoqIde de faire de la logique classique.

Le tiers exclu est maintenant une tautologie, en chargeant les modules de logique classique :

La résolution de syllogismes avec négations (type « celarent ») utilise l’équivalence entre une implication et sa contraposée.

Voyons si $p\Rightarrow q$ implique bien $\neg q \Rightarrow \neg p$ (lemme L1) :

Les introductions suggérées par CoqIde sont les suivantes :

On introduit les hypothèses $p \Rightarrow q$ et $\neg q$ et à partir de ces hypothèses, on essaye de démontrer $\neg p$. C’est ce que propose Coq pour démontrer le lemme. On peut même choisir le nom des hypothèses, par exemple « nq » au lieu de H0 :

Voyons maintenant la réciproque (lemme L2) :

En coloriant en vert les lignes jusqu’à autos, Coq dit que

On suppose que p et q sont de type « Prop », et par hypothèse, que $\neg q \Rightarrow \neg p$. En supposant p, on doit alors montrer q : C’est une tautologie.

Pour résoudre certains syllogismes, on a besoin de cet axiome de Lewis Carroll :

$\forall x \in U, P(x) \Rightarrow \exists x \in U, P(x)$

(si tout élément de l’univers a la propriété P, alors il existe au moins un élément de l’univers ayant la propriété P)

Cet axiome n’est pas un théorème prouvable avec le module classical :

donne cet affichage

Autrement dit, on fait provisoirement l’hypothèse que pour tout x de l’univers, x a la propriété P, et on cherche, à partir de là, à prouver l’existence d’un élément x de l’univers ayant la propriété P. CoqIde n’y arrive pas, toutes les tactiques, et en particulier tauto, échouent.

C’est que pour Lewis Carroll, l’univers du discours est supposé non vide, alors que pour montrer $\exists x \in U, P(x)$ il faut déjà $\exists x \in U$...

Voici un syllogisme de type Barbara (source : Lewis Carroll) :

• tout frelon est agressif.
• or tout être agressif est déplaisant.
• donc tout frelon est déplaisant.

(Lewis Carroll parlait de guêpes, pour éviter les accents et l’accord de « toute » on parlera ici de frelon).

On entre le syllogisme en

• déclarant les prédicats frelon, agressif, déplaisant de type Prédicat (fonction de l’univers du discours vers les propositions) ;
• traduisant les deux prémisses en langage Coq (avec le module adapté), comme axiomes ;
• écrivant la conclusion comme théorème T1 : Tout frelon est déplaisant.

Ensuite on attaque la preuve du théorème, avec intros :

Coq propose d’introduire l’hypothèse H selon laquelle x est un frelon :

Sous cette hypothèse, il reste alors à démontrer que x (le frelon) est déplaisant. Pour cela, on constate que l’axiome A2 termine par « est déplaisant ». Ce qui donne envie d’appliquer cet axiome :

On obtient alors un nouveau sous-but : Montrer que x est agressif :

Du coup ça vaut la peine d’essayer d’appliquer l’axiome A1 :

Il reste alors à prouver que tout frelon x est un frelon :

On est en droit d’estimer que c’est trivial :

La réponse est satisfaisante :

No more subgoals.

On a donc terminé :

après exécution de ce script, le théorème T1 est défini et peut être utilisé par la suite.

La preuve ci-dessus utilise successivement 4 tactiques :

• introduire les notations x et H ;
• appliquer l’axiome A2 ;
• appliquer (au résultat) l’axiome A1 ;
• finir par « trivial » pour « démontrer » que x=x

On peut considérer ces tactiques comme des instructions d’un langage de programmation spécialisé dans la description des algorithmes de preuve. Ce langage s’appelle Ltac (« langage de tactiques ») et permet notamment de définir une instruction unique pour résumer cette séquence de tactiques. Cette instruction est elle-même une tactique.

Encore un exemple de Lewis Carroll :

• Tous les gens égoïstes sont impopulaires ;
• or Tous les gens serviables sont populaires ;
• donc Tous les gens égoïstes sont dépourvus de serviabilité.

Les « e » de « celarent » désignent des phrases négatives, par exemple la première prémisse « aucun égoïste n’est populaire », qui se traduit en Coq par « forall x : U, égoïste x -> populaire x ».

La gestion de la négation va rendre un peu plus longue la résolution de ce syllogisme. Là encore, on va créer des utilitaires gérant les phrases négatives et la traduction du langage presque naturel en Coq (et en passant on définit l’univers U une fois pour toutes) :

On ne recopiera pas ce préliminaire pas la suite, il est implicite.

On va donc coder le syllogisme ainsi :

Attention à l’apostrophe, qu’il faut mettre à l’envers (enfin à l`envers) pour éviter la confusion avec les guillemets simples.

Comme précédemment, on peut essayer de démarrer la preuve avec intros, ce qui donne ces nouvelles hypothèses :

Autrement dit, la stratégie proposée par Coq consiste à supposer que x est égoïste, et à démontrer, à partir de cette hypothèse, que x n’est pas serviable (comme ça on va porter plainte contre x, ça lui apprendra à être égoïste). Comme l’axiome A1 parle d’égoïsme, on va voir si on peut l’appliquer à l’hypothèse H :

Et oui, ça fonctionne :

Puisqu’on a supposé (H) que x est égoïste, l’axiome A1 permet effectivement de dire que x est impopulaire, et on peut donc remplacer H par «  populaire x ».

Tel quel, on ne peut pas appliquer A2 (« unable to unify »), alors on contrapose H :

On a alors un modus tollens à appliquer :

L’hypothèse H a été transformée en la négation de l’ancienne conclusion et vice-versa : On suppose maintenant que x est serviable mais du coup on doit prouver que x est populaire (ce n’est donc plus le même x qu’avant). Maintenant on peut appliquer A2 comme dans l’onglet précédent :

Il reste ensuite, toujours sous l’hypothèse selon laquelle x est serviable, à prouver qu’il l’est. C’est une tautologie :

« No more subgoals », gooooooooooaaaaaaaal, on a gagné !

Voici un exemple de syllogisme de type Darii (source : Lewis Carroll) :

• Quelques personnes qui méritent la victoire ont ce qu’elles méritent.
• or Nul autre que le brave ne mérite la victoire.
• donc Quelques braves ont ce qu’ils méritent.

Pour en rendre l’écriture plus naturelle, on va utiliser l’utilitaire décrit dans l’onglet précédent.

Voici comment on peut poser le problème :

Maintenant à cause d’une affirmation existentielle, c’est moins facile à prouver que la syllogisme précédent. Un principe fonctionne cependant : Lorsque l’on parle d’existence, remplacer « apply » par « destruct » :

La destruction de l’axiome A1 a fourni une nouvelle hypothèse à utiliser :

L’hypothèse H est une conjonction : x (le « quelque » de l’axiome A1) est à la fois victorieux et brave. Or pour utiliser l’axiome A2, seul le fait que x est victorieux est utile. On a donc intérêt à « détruire » H aussi, en appelant a et b ses termes :

Ces destructions (le terme « déconstruction » serait peut-être plus approprié) ont pour effet de multiplier les hypothèses :

Maintenant qu’on a l’hypothèse a selon laquelle x est victorieux, on peut appliquer l’axiome A2 :

Mais ça ne marche pas :

Error: Impossible to unify "brave ?200" with "Quelque méritant est brave".

Pour quelque raison mystérieuse, Coq n’arrive pas à unifier le fait que x est brave (x a été renommé  ?200 entre-temps) avec le fait que tout méritant est brave. Une rapide consultation de l’aide en ligne de Coq conseille d’appliquer la tactique pattern alors suivons ce conseil :

La réponse obtenue est celle-ci :

Attention, λ-calcul inside ! On apprend que l’application de A2 est une fonction, envoyant l’affirmation selon laquelle tout victorieux est brave sur l’affirmation selon laquelle quelque méritant est brave, autrement dit, que apply A2 applique A2 au théorème T1. Le résultat (la fonction en question) étant appliqué à A2, devait donner le théorème T1.

Il faut donc appliquer A2 avec l’hypothèse a et non l’hypothèse par défaut :

Cela donne alors

On veut toujours montrer que quelque méritant est brave et on aperçoit que x convient puisqu’il est à la fois méritant (hypothèse b) et brave (hypothèse a). Ah ce brave x, il a bien du mérite ! Mais Coq le voit-il ? On peut le lui dire :

Pas de message d’erreur, c’est bon signe :

Maintenant la tête à tauto suffit à faire en sorte qu’il n’y ait pas de « subgoals » et complète la preuve :

Arrivé là, on est en droit d’estimer qu’il n’y a pas que x qui est à la fois brave et méritant !

Vu que le Celarent est plus difficile parce qu’il comporte une négation, et le Darii encore plus difficile parce qu’il comporte un quantificateur existentiel, le Ferio, qui comporte les deux, fait un peu peur.

En voici un classique, lui aussi dû à Lewis Carroll :

• Seuls les braves méritent la victoire.
• Quelques fanfarons sont des lâches.
• donc Quelques fanfarons ne méritent pas la victoire.

La première prémisse peut aussi s’écrire « aucun lâche ne mérite la victoire ». On n’a donc besoin que de 3 prédicats :

1. lâche x veut diire que x est lâche ;
2. fanfaron x veut dire que x est un fanfaron ;
3. méritant x veut dire que x mérite la victoire.

Voilà comment, avec les utilitaires des onglets précédents, on peut poser le problème :

Dans l’onglet précédent, on a vu que pour un axiome existentiel, une destructuration est utile, alors on va essayer ici aussi :

Là encore ça marche, on gagne une hypothèse H :

L’hypothèse H est une conjonction, et seul son second terme est à utiliser avec l’axiome A1. Alors on destructure H en ses deux termes a et b :

On a maintenant les deux hypothèses a et b séparées :

C’est donc à b seul qu’on va appliquer l’axiome A1 :

Bingo, le nouveau b, avec a, répond à la question :

Il suffit d’aplliquer la tactique exists avec le témoin x :

La conjonction de a et b convient maintenant :

Encore une fois, la fin est tauto-matique :

« no more subgoal » puis Qed clôt le problème. Finalement, il fait rire, le Ferio des jours fériés !

Avec les utilitaires des onglets précédents, on peut maintenant résoudre ce sorite de Lewis Carroll [1] :

• Les bébés sont illogiques ;
• Nul n’est méprisé s’il peut venir à bout d’un crocodile ;
• Les gens illogiques sont méprisés.

La question est de savoir ce qu’on peut déduire de ces trois hypothèses. L’onglet « Blockly » montre une méthode permettant de trouver le théorème à prouver.

On commence la preuve par intros, comme d’habitude :

Cela consiste à supposer que x est un bébé et le but final est de prouver que x est pas un champion (i.e. il ne peut pas venir à bout d’un crocodile) :

L’hypothèse H étant (pour l’instant) que x est un bébé, on peut déjà lui appliquer l’axiome A1 :

Cela a pour effet de remplacer l’hypothèse par « x est illogique », le but final n’ayant pas changé :

On peut alors appliquer A3 à cette nouvelle hypothèse :

Cela change encore l’hypothèse de laquelle on part pour arriver à la conclusion :

L’exercice est devenu celui-ci : On suppose que x est méprisé ; en déduire qu’il n’est pas champion. Mais l’axiome A2 ne le permet pas : C’est la contraposée de H. Alors on peut contraposer H pour lui appliquer A2 :

Le problème à résoudre ressemble alors beaucoup à A2 :

Pour montrer, à partir de l’hypothèse selon laquelle x est méprisé, la conclusion selon laquelle x n’est pas un champion, on peut, en lieu et place, à partir de l’hypothèse selon laquelle x est un champion, prouver la conclusion selon laquelle x n’est pas méprisé : C’est le raisonnement par contraposition ; et on peut évidemment appliquer A2 à H qui n’est jamais qu’une autre manière d’écrire A2 :

Le problème devient tautologique :

Le problème devient « on suppose que x n’est pas méprisé ; en déduire qu’il n’est pas méprisé » :

tauto répond « no more subgoals » et le sorite est résolu.

Ni Coq ni Otter ne savent trouver seuls quelle est la solution, ils ne savent que prouver le théorème une fois qu’on sait quel est le théorème à prouver. Prolog sait résoudre ce genre de sorite.

Remarque : Ce sorite a probablement inspiré à Martin Gardner le paradoxe du crocodile et du bébé :

Une maman veut traverser la rivière avec sa petite Odile, un bébé tout minuscule. Un crocodile, qui sait parler, dit de sa voix caverneuse « Attention à ce que tu vas dire : Si tu dis la vérité, je te laisse passer ; sinon je mange ton bébé ». Alors la maman dit « Tu vas croquer Odile »...

Sous Ubuntu, le lanceur de CoqIde se trouve à côté de ceux d’Eric et de Scratch, c’est parce que c’est un IDE donc a priori fait pour écrire des programmes. Ceci dit les fonctionnalités de CoqIde ne le rendent pas spécialement propice à la programmation en lycée. En effet le logiciel CoqIde est écrit en CamL et est donc un langage fonctionnel basé sur la récursivité (hors programme). Cependant l’excellent livre de Guillaume Connan sur l’algorithmique comprend une foule d’exercices dont la moitié en CamL...

Voyons toutefois comment on peut définir et calculer les deux suites $u_n=2n+3$ et $v_n$, arithmétique de premier terme $v_0=3$ et de raison 2. En Coq, une fonction s’appelle un Fixpoint (l’héritage d’Haskell Curry), alors on écrit Fixpoint u(n:nat) :nat :=2*n+3. pour dire que $u$ est une fonction dont la variable $n$ est entière, dont l’ensemble d’arrivée est $\N$ et par laquelle l’image de $n$ est $2n+3$. Alternativement, on aurait pu déclarer $u$ comme une fonction de $\N$ dans $\N$ par Definition u := fun (n: nat) => 2*n+3..

Après pour calculer $u_3$ on peut écrire Eval compute in u(3) ou cliquer sur « Queries » et là, choisir « eval compute in » puis entrer « u(3) » :

Pour définir la suite $v_n$ qui est récurrente, c’est un peu plus compliqué :

La notation $S(k)$ désigne $k+1$ (le « successeur » de $k$). On voit avec le « query » que $v_3=u_3$ mais ceci ne prouve pas que $u_n=v_n$ pour tout $n$. Mais CoqIde est un outil de preuve alors autant essayer de prouver cette égalité avec quantificateur : $\forall n \in \N, u_n=v_n$. Le théorème s’appellera $suites$ :

En essayant toutes sortes de tactiques (entrée « try tactics » du menu) la seule qui donne quelque chose est induction : La récurrence sur $n$ ; on voit ci-dessus l’étape d’initiation de la récurrence : Le début c’est de prouver que $u_0=v_0$. La tactique trivial donne immédiatement ce résultat ($3=3$) :

On voit maintenant que l’hypothèse de récurrence s’appelle $Hn$ et que c’est $u_n=v_n$ (en haut à droite). On voit aussi qu’il reste à démontrer que $u_{n+1}=v_{n+1}$ (en effet $n+1$ se note Sn comme on l’a vu plus haut).

Hélas pour continuer la récurrence il faut charger d’autres théories (au moins l’arithmétique de Peano) faute de quoi CoqIde ne trouve pas spontanément la démonstration. Alors la voici : Puisque $u_n=v_n$ alors $u_{n+1}=2(n+1)+3=2n+2+3=2n+3+2=u_n+2=v_n+2=v_{n+1}$

Faire des démonstrations avec CoqIde, ça a l’air encore plus compliqué que les faire de tête ; est-ce à dire que son usage n’est pas recommandé au lycée ?

• Oui puisque ce logiciel utilise la logique intuitionniste qui n’est pas au programme du lycée ;
• Mais tout de même, il a déjà servi, notamment en géométrie. Un outil analogue à CoqIde mais en ligne s’appelle Coqweb et se trouve sur le serveur wims. Son intérêt est que chaque fois qu’un élève réussit à démontrer un nouveau théorème avec Coqweb, le théorème est ajouté à une base de données qui par suite va s’agrandir et Coqweb va devenir de plus en plus puissant. C’est par ce processus que le logiciel de théorie des types ScratchPad est devenu le logiciel de calcul formel Axiom...

Pour faire des syllogismes et des sorites avec Coq, on a intérêt à enregistrer les utilitaires que voici :

Une fois enregistrés sous le nom carroll.v, il suffit de précéder une feuille de travail Coq, de la ligne

Load carroll.

Alternative : en double-cliquant sur le fichier carroll.v, on ouvre CoqIde avec ce fichier ; après, on clique dans le menu « Compile », sur « compile buffer » ce qui crée un fichier carroll.vo. Alors en première ligne on peut mettre

Require Import carrol.

Après ça, on peut faire des choses comme

Voici les deux fichiers (le fichier Coq au format v et le fichier compilé) pour personnaliser un peu son CoqIde :

Et au collège ?

OK, la doc de Coq ?

Il est dit dans le coq’art que Coq « est un assistant de preuves », et pas vraiment un solveur logique. Mais aussi, Coq « fait partie d’une longue tradition de systèmes informatiques d’aide à la
démonstration de théorèmes ». Faire de la logique avec Coq n’est donc pas facile et en collège on peut lui préférer jGex au moins pour la géométrie.

Et les programmes ?

Voici un programme de calcul du brevet des collèges (métropole-Réunion-Antilles-Guyane 2015) :

Un exercice intéressant serait de prouver que pour tout nombre x entré initialement, on récupère son double 2x en sortie. Mais il y a deux problèmes si on veut utiliser Coq :

1. Coq est programmé dans un langage fonctionnel et il faut simuler la programmation impérative dans ce langage fonctionnel : Pas facile...
2. Ce genre de preuve ne relève pas de la logique pure, il faut utiliser la tactique ring ce qui rapproche l’exercice d’un exercice de calcul formel.

Voici comment on peut prouver l’affirmation précédente avec Xcas :

On commence par programmer une fonction « brevet » :

On compile cette fonction, puis si on entre

brevet(x)

on a

3*(x+8)-x-24

et si on entre

simplify(brevet(x))

on a

2*x

Blockly peut être vu comme une aide à la résolution de sorites : L’idée est de considérer chaque prémisse comme un être d’un micromonde, et de ne permettre le positionnement d’une prémisse après une autre, que si la conclusion de la première est de même « type » que l’hypothèse de la seconde.

Pour les crocodiles, il s’agit essentiellement de mettre les dans un ordre facilitant la résolution du sorite ; le reste est à faire mentalement.

On commence par préparer un fichier html contenant Blockly.

Ensuite, on crée des blocs, un par prémisse, en n’oubliant pas de leur donner un type restreignant leur usage. La création de blocs est faite avec cet outil. Par exemple, un bloc de type « bébé » sera réservé au texte « Les bébés sont illogiques » (retraduit ici en « tout bébé est illogique »). On lui donne une couleur rose comme un bébé.

On prévoit une entrée en haut et une sortie en bas, mais l’entrée est de type « bébé ». Ce type n’ayant pas été prévu par les concepteurs de Blockly, on choisit « other » :

Puis on entre « bébé » dans le champ texte :

La sortie, celle-ci de type « illogique », permettra à ce bloc de fonctionner :

L’aspect du bloc obtenu est satisfaisant :

Pour l’utiliser, on récupère ce code, depuis la fabrique de blocs :

Ce script est placé dans une balise « script » de l’entête (« head ») du document. Pour voir le bloc, il faut encore le placer dans l’espace de travail de Blockly, avec cette ligne :

<block type="axiome1"></block>

(ci-dessous dans une « category » de nom « axiomes » qui améliore la visibilité de l’espace de travail)

Ensuite, il suffit de créer des blocs similaires :

Un bloc de type « méprisé » n’acceptant que des blocs de type « crocodile » et disant que « les gens méprisés ne viennent pas à bout d’un crocodile », et un bloc de type « illogique » n’acceptant que les blocs de type « méprisé » et disant que « les gens illogiques sont méprisés ». Cela donne le micromonde suivant :

En manipulant le fichier Blockly ci-dessus, on constate qu’il est impossible de brancher l’axiome 2 à la suite de l’axiome 1, mais que par contre l’axiome 3, lui, convient. Et de plus, l’axiome 2 peut être ajouté à la suite des axiomes 1 et 3 ; le sorite se réorganise alors ainsi :

1. Les bébés sont illogiques ;
2. Les gens illogiques sont méprisés ;
3. Les gens méprisés ne peuvent venir à bout d’un crocodile ;

On peut maintenant remplacer les deux (nouveaux) premiers par « les bébés sont méprisés » et obtenir

1. Les bébés sont méprisés ;
2. Les gens méprisés ne peuvent venir à bout d’un crocodile.

Ce qui mène à la conclusion, et permet de savoir ce que Coq doit démontrer.

Voici un autre exemple de Lewis Carroll, montrant que son chien ne peut être satisfait :

C’est en cherchant à représenter ainsi une démonstration qu’Hao Wang a inventé ses pavages calculateurs (Wang était avant tout un logicien).