Comme dans l’article précédent, CoqIde permet aussi de faire du calcul propositionnel. Par exemple, si on veut savoir si une proposition peut être à la fois vraie et fausse, on peut demander à CoqIde de le démontrer sous la forme d’un théorème que l’on va appeler Th1, et dont l’énoncé sera que pour toute proposition , on ait  :

Les deux doubles-points ont des sens différents, le premier sépare le nom du théorème de son énoncé, et le deuxième signifie « de type » ; ainsi est de type c’est-à-dire que c’est une proposition. En effet le plus gênant pour l’utilisation de Coq dans l’enseignement secondaire est que celui-ci est basé sur la théorie des types... On constate la coloration syntaxique.

Pour essayer de faire démontrer le théorème Th1, on clique sur la flèche bleue qui va vers le bas, ce qui produit l’effet suivant :

On voit que la ligne courante est coloriée en vert, et que à droite CoqIde commence à élaborer une stratégie de démonstration (choisir entre le raisonnement par cas, la démonstration par récurrence etc.). Il énumère les sous-buts, ici il n’y en a qu’un. Pour choisir une stratégie de démonstration, on peut cliquer sur l’entrée « tactics » du menu mais il y en a des dizaines dont toutes ne sont pas forcément adéquates (par exemple, la théorie des anneaux semble peu appropriée ici). Alors une liste de stratégies de démonstrations par défaut est proposée par CoqIde (dans l’ordre, CoqIde cherche si le théorème à démontrer est trivial, puis si c’est une tautologie, puis essaye de démontrer par recherche automatique de stratégie, puis par une tactique nommée Omega, puis par une tactique récursive, et à défaut par la logique intuitionniste). Le meilleur moyen de tester tout ça est de cliquer sur l’icône représentant une lampe, ce qui produit cet effet :

Le mot « Intuition » écrit par CoqIde montre que celui-ci a testé toutes ses stratégies de démonstration : La première par exemple a échoué. La réponse apparaît dans le cadre de droite : est faux.

Si maintenant on cherche à regarder ce que CoqIde pense du principe du tiers exclu, on constate qu’il échoue même avec la stratégie « tauto » :

Tout ce qu’il a réussi à faire, c’est remplacer par et c’est tout. Ceci ne signifie pas que CoqIde est bogué mais que la logique intuitionniste refuse le tiers exclu. De même, la double négation n’équivaut pas à une affirmation en logique intuitionniste. Sous CoqIde on vérifie avec

CoqIde répond dès la stratégie Tauto par l’affirmative (démonstration complétée) alors qu’avec

CoqIde transforme l’hypothèse du « théorème » en et s’arrête sur à l’étape « Intuition », ce qui confirme que pour CoqIde n’est pas un théorème alors que est un axiome...

Ceci est bien sûr très gênant parce que, avec un tel choix, la logique intuitionniste s’interdit le raisonnement par l’absurde ; on verra dans le prochain onglet que le raisonnement par contraposition est également inaccessible à CoqIde. Le problème est ancien : Déjà à l’époque de Prolog, on pratiquait la négation par l’échec... Une solution serait de rajouter la double négation comme axiome (la contraposition en découlera alors) avec un Axiom DoubleNeg : forall p q : Prop, ~~p->p

Les autres exemples de l’article sur la logique propositionnelle peuvent être traités sous CoqIde à titre d’exercice, ne serait-ce que pour voir lesquels sont traités à l’identique en logique intuitionniste, et lesquels ne le sont pas...

Pour tester CoqIde sur un problème faisant intervenir la logique des prédicats, on va utiliser un exemple extrait du cours de Logique sans peine de Lewis Carroll :

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 que posait Lewis Carroll était « Que peut-on en déduire ? ».

On imagine l’ensemble des humains, et les propriétés , , et définies sur avec les significations suivantes :

• signifiant que est un bébé ;
• signifiant que est logique ;
• signifiant que est méprisé (on évite les accents par prudence) ;
• signifiant que peut venir à bout d’un crocodile.

L’énoncé de Lewis Carroll se traduit alors par

La transitivité de l’implication permet alors, à partir des affirmations 1 et 3, d’obtenir (on a déjà démontré que les bébés sont méprisés !). Mais la deuxième hypothèse de l’énoncé donne par contraposition (si quelqu’un est méprisé, c’est qu’il ne peut venir à bout d’un crocodile). Récapitulons :

On en déduit alors  : Aucun bébé ne peut venir à bout d’un crocodile.

Sous CoqIde, on doit d’abord déclarer la variable de type ensemble, par Variable X : Set ; puis les prédicats etc. sont définis comme des fonctions de dans l’ensemble des propositions ; en effet pour tout humain , ou bien est un bébé, ou bien n’est pas un bébé : On associe bien une proposition à chaque humain. Ensuite les trois phrases de l’énoncé sont écrites comme des axiomes , et . Enfin la phrase prend le statut de théorème à démontrer :

Las ! Non seulement CoqIde n’arrive pas à le démontrer, mais en plus il déclare la phrase comme fausse ! (voir l’onglet précédent pour une explication de ce phénomène)

Pour ne pas terminer cet onglet sur un échec, on va voir ce que dit CoqIde sur la propriété suivante :

En notant par le fait que alors on veut démontrer que (certes, il y a des manières plus simples de démontrer que 4 est positif...). Dans CoqIde, l’ensemble des entiers naturels est noté nat :

Parfait : CoqIde considère la propriété comme triviale.

En notation abrégée,

Cet extrait du livre Coq’Art montre que CoqIde sait montrer la propriété ci-dessus mais avec Intuition la démonstration n’aboutit pas ; et trouver manuellement la suite de tactiques menant à la démonstration n’est pas facile (il faut pas mal d’expérience en Coq pour penser à ça !).

Du coup, la simple démonstration de propriétés comme

devient un exercice intéressant mais difficile ; et l’analyse de cette propriété en classe risque d’être riche en surprises !

Idem pour

ou sa réciproque...

Un autre grand classique : La différence qu’il y a entre et ...

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 et , arithmétique de premier terme 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 est une fonction dont la variable est entière, dont l’ensemble d’arrivée est et par laquelle l’image de est . Alternativement, on aurait pu déclarer comme une fonction de dans par Definition u := fun (n: nat) => 2*n+3..

Après pour calculer 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 qui est récurrente, c’est un peu plus compliqué :

La notation désigne (le « successeur » de ). On voit avec le « query » que mais ceci ne prouve pas que pour tout . Mais CoqIde est un outil de preuve alors autant essayer de prouver cette égalité avec quantificateur : . Le théorème s’appellera  :

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

On voit maintenant que l’hypothèse de récurrence s’appelle et que c’est (en haut à droite). On voit aussi qu’il reste à démontrer que (en effet 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 alors

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...