Les ordinateurs sont-ils logiques ? 2 : Logique des prédicats

lundi 26 octobre 2015
par  Alain BUSSER

Le logiciel CoqIde ressemble à un environnement de programmation mais son moteur est Coq, un logiciel libre qui permet de faire des déductions dans la logique des prédicats. L’article qui suit ressemble à un tutoriel pour Coqide, tout simplement parce qu’un tel tutoriel n’existe pas !

Le coq et l’outre

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.

Propositions

JPEG - 25.5 ko

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 :

Lemma TE: forall p: Prop, p \/ ~p.
Proof.
    intros p.
    tauto.

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.

Principe

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)

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.

Cas de la double négation

De même, la double négation n’équivaut pas à une affirmation en logique intuitionniste. Sous CoqIde on vérifie avec

Theorem T1: forall p: Prop, p->~~p.

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

Theorem T2: forall p: Prop, ~~p->p.

CoqIde transforme l’hypothèse du « théorème » en \left(p\Rightarrow \bot\right)\Rightarrow \bot et s’arrête sur p à l’étape « Intuition », ce qui confirme que pour CoqIde \neg\neg p \Rightarrow p n’est pas un théorème alors que p \Rightarrow \neg\neg p 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

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 :

Require Import Classical ClassicalFacts.
Lemma TE: forall p: Prop, p \/ ~p.
Proof.
    intros p.
    tauto.
Qed.

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) :

Require Import Classical ClassicalFacts.
Lemma L1: forall p: Prop, forall q: Prop, (p->q)->(~q->~p).
Proof.
    intros.

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

1 subgoals
p : Prop
q : Prop
H : p -> q
H0 : ~ q
______________________________________(1/1)
~ p

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 :

Require Import Classical ClassicalFacts.
Lemma L1: forall p: Prop, forall q: Prop, (p->q)->(~q->~p).
Proof.
    intros p q H nq.
    tauto.
Qed.

Voyons maintenant la réciproque (lemme L2) :

Require Import Classical ClassicalFacts.
Lemma L2: forall p: Prop, forall q: Prop, (~q->~p)->(p->q).
Proof.
    intros.
    tauto.
Qed.

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

1 subgoals
p : Prop
q : Prop
H : ~ q -> ~ p
H0 : p
______________________________________(1/1)
q

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 :

Require Import Classical ClassicalFacts.
Variable Univers: Set.
Variable P: Univers -> Prop.
Lemma E: (forall x: Univers, P x) -> (exists x: Univers, P x).
Proof.
intros.

donne cet affichage

1 subgoals
H : forall x : Univers, P x
______________________________________(1/1)
exists x : Univers, P x

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

Barbara

JPEG -

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

utilitaires

On aura intérêt à charger ce module (préalablement compilé) :

Parameter U: Set.
Definition Prédicat := U->Prop.
Notation "'Tout' sujet 'est' objet" := (forall x:U, sujet(x) -> objet(x)) (at level 50).
Notation "'Aucun' sujet 'n`est' objet" := (forall x:U, sujet(x) -> ~objet(x)) (at level 50).
Notation "'Quelque' sujet 'est' objet" := (exists x:U, sujet(x) /\ objet(x)) (at level 50).
Notation "'Quelque' sujet 'n`est' 'pas' objet" := (exists x:U, sujet(x) /\ ~objet(x)) (at level 50).

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 :

Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
    intros.

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

1 subgoals
x : U
H : frelon x
______________________________________(1/1)
déplaisant x

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 :

Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
    intros x H.
    apply A2.

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

1 subgoals
x : U
H : frelon x
______________________________________(1/1)
agressif x

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

Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
    intros x H.
    apply A2.
    apply A1.

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

1 subgoals
x : U
H : frelon x
______________________________________(1/1)
frelon x

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

Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
    intros x H.
    apply A2.
    apply A1.
    trivial.

La réponse est satisfaisante :

No more subgoals.

On a donc terminé :

Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
    intros x H.
    apply A2.
    apply A1.
    trivial.
Qed.

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.

tactique

Déjà, dans la preuve du théorème, au lieu d’aller à la ligne après chaque tactique, on peut les écrire en une seule ligne, séparées par un point-virgule qui signifie « et ensuite » :

Proof.
    intros x H;  apply A2;  apply A1;  trivial.
Qed.

Alors pourquoi pas donner un mot à cette séquence de 4 tactiques, par exemple « barbara » ?

Ltac barbara P1 P2 := intros x H; apply P2; apply P1; trivial.

La tactique « barbara » (qui n’existe pas dans la version officielle de Coq) s’applique à deux prémisses notées P1 et P2, et consiste à appliquer à l’hypothèse H introduite, la seconde prémisse P2, puis, au résultat, la première prémisse P1. La définition ci-dessus peut être placée dans le fichier des utilitaires proposé en fin d’article, et la résolution du syllogisme des frelons se fait maintenant plus facilement :

Load carroll.
Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
        barbara A1 A2.
Qed.

Maintenant, il subsiste un problème : Ainsi définie, l’opération barbara n’est pas commutative : En essayant

Load carroll.
Parameter frelon agressif déplaisant: Prédicat.
Axiom A1: Tout frelon est agressif.
Axiom A2: Tout agressif est déplaisant.
Theorem T1: Tout frelon est déplaisant.
Proof.
    barbara A2 A1.
Qed.

on a un message d’erreur :

In nested Ltac calls to "barbara" and "apply A2" (expanded to "apply A1"),
last call failed.
Error: Impossible to unify "agressif ?201" with "déplaisant x".

Il faut vraiment appliquer les prémisses dans l’ordre. Ou alors, redéfinir la tactique (c’est le principe de Coq : Changer de tactique en cas d’échec, exactement comme dans les jeux vidéo). Dans la suite, on gardera la non commutativité de barbara.

De la guêpe à l’outre

Voici le fichier Otter de ce syllogisme :

formulas(assumptions).
all x (frelon(x) -> agressif(x)).
all x (agressif(x) -> deplaisant(x)).
end_of_list.
formulas(goals).
all x (frelon(x) -> deplaisant(x)).
end_of_list.

La preuve obtenue est celle-ci :

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.08) seconds.
% Length of proof is 10.
% Level of proof is 4.
% Maximum clause weight is 0.
% Given clauses 0.

1 (all x (frelon(x) -> agressif(x))) # label(non_clause).  [assumption].
2 (all x (agressif(x) -> deplaisant(x))) # label(non_clause).  [assumption].
3 (all x (frelon(x) -> deplaisant(x))) # label(non_clause) # label(goal).  [goal].
4 frelon(c1).  [deny(3)].
5 -frelon(x) | agressif(x).  [clausify(1)].
6 agressif(c1).  [resolve(4,a,5,a)].
7 -agressif(x) | deplaisant(x).  [clausify(2)].
8 deplaisant(c1).  [resolve(6,a,7,a)].
9 -deplaisant(c1).  [deny(3)].
10 $F.  [resolve(8,a,9,a)].

============================== end of proof ==========================

Les lignes 1 et 2 sont les hypothèses, la ligne 3 est le but à prouver. Pour le prouver, on va raisonner par l’absurde : On suppose que c1 est un frelon (ligne 4) et qu’il n’est pas déplaisant (ligne 9) et on en déduit une antilogie (ligne 10).

La ligne 5 est une réécriture de la ligne 1 : « Tout frelon est agressif » peut s’écrire « ou bien x n’est pas un frelon, ou alors il est agressif ». Il s’agit de la réécriture d’une implication sous forme de clause de Horn (disjonction). Maintenant, en comparant les lignes 4 (c1 est un frelon) et 5 (c1 n’est pas un frelon ou alors c1 est agressif) on a la conclusion de la ligne 6 : c1 est agressif. C’est la version booléenne du modus ponens.

Les lignes 7 et 8 sont similaires : On réécrit sous forme de disjonction l’implication 2 et en comparant avec la ligne 6 on conclut que le frelon c1 est déplaisant. C’est maintenant qu’on peut appliquer le raisonnement par l’absurde : On avait supposé (ligne 9) que c1 est sympa comme tout, et en comparant avec la ligne 8 (où on avait prouvé le contraire), on obtient une contradiction ligne 10 (F veut dire « faux »).

Celarent

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é.
JPEG - 518.4 ko

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) :

Require Import ClassicalFacts.
Require Import Classical.
Parameter U: Set.
Definition Prédicat := U->Prop.
Notation "'Tout' sujet 'est' objet" := (forall x:U, sujet(x) -> objet(x)) (at level 50).
Notation "'Aucun' sujet 'n`est' objet" := (forall x:U, sujet(x) -> ~objet(x)) (at level 50).
Notation "'Quelque' sujet 'est' objet" := (exists x:U, sujet(x) /\ objet(x)) (at level 50).
Notation "'Quelque' sujet 'n`est' 'pas' objet" := (exists x:U, sujet(x) /\ ~objet(x)) (at level 50).
Axiom contraposition: forall sujet objet: Prédicat, (Aucun sujet n`est objet) -> (Aucun objet n`est sujet).
Axiom doubleneg: forall p: Prop, ~~p->p.

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

On va donc coder le syllogisme ainsi :

Parameter égoïste populaire serviable: Prédicat.
Axiom A1: Aucun égoïste n`est populaire.
Axiom A2: Tout serviable est populaire.
Theorem T1: Aucun égoïste n`est serviable.

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 :

1 subgoals
x : U
H : égoïste x
______________________________________(1/1)
~ serviable x

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 :

Parameter égoïste populaire serviable: Prédicat.
Axiom A1: Aucun égoïste n`est populaire.
Axiom A2: Tout serviable est populaire.
Theorem T1: Aucun égoïste n`est serviable.
Proof.
    intros.
    apply A1 in H.

Et oui, ça fonctionne :

1 subgoals
x : U
H : ~ populaire x
______________________________________(1/1)
~ serviable x

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 :

Parameter égoïste populaire serviable: Prédicat.
Axiom A1: Aucun égoïste n`est populaire.
Axiom A2: Tout serviable est populaire.
Theorem T1: Aucun égoïste n`est serviable.
Proof.
    intros.
    apply A1 in H.
    contradict H.

On a alors un modus tollens à appliquer :

1 subgoals
x : U
H : serviable x
______________________________________(1/1)
populaire x

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 :

Parameter égoïste populaire serviable: Prédicat.
Axiom A1: Aucun égoïste n`est populaire.
Axiom A2: Tout serviable est populaire.
Theorem T1: Aucun égoïste n`est serviable.
Proof.
    intros.
    apply A1 in H.
    contradict H.
    apply A2.

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

Parameter égoïste populaire serviable: Prédicat.
Axiom A1: Aucun égoïste n`est populaire.
Axiom A2: Tout serviable est populaire.
Theorem T1: Aucun égoïste n`est serviable.
Proof.
    intros.
    apply A1 in H.
    contradict H.
    apply A2.
    tauto.
Qed.

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

Tactique

La tactique celarent peut donc se définir ainsi :

Ltac celarent P1 P2 := intros x H; apply P1 in H; contradict H; apply P2; tauto.

La résolution du syllogisme ci-dessus devient alors

Load carroll.
Parameter égoïste populaire serviable: Prédicat.
Axiom A1: Aucun égoïste n`est populaire.
Axiom A2: Tout serviable est populaire.
Theorem T1: Aucun égoïste n`est serviable.
Proof.
    celarent A1 A2.
Qed.

Passons outre avec Otter

Voici le script Otter (ou Prover9) :

formulas(assumptions).
all x (egoiste(x) -> -populaire(x)).
all x (serviable(x) -> populaire(x)).
end_of_list.
formulas(goals).
all x (egoiste(x) -> -serviable(x)).
end_of_list.

Otter fournit alors la preuve suivante :

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 10.
% Level of proof is 3.
% Maximum clause weight is 0.
% Given clauses 0.

1 (all x (egoiste(x) -> -populaire(x))) # label(non_clause).  [assumption].
2 (all x (serviable(x) -> populaire(x))) # label(non_clause).  [assumption].
3 (all x (egoiste(x) -> -serviable(x))) # label(non_clause) # label(goal).  [goal].
4 egoiste(c1).  [deny(3)].
5 -egoiste(x) | -populaire(x).  [clausify(1)].
6 serviable(c1).  [deny(3)].
7 -serviable(x) | populaire(x).  [clausify(2)].
8 populaire(c1).  [resolve(6,a,7,a)].
9 -populaire(c1).  [resolve(4,a,5,a)].
10 $F.  [resolve(8,a,9,a)].

============================== end of proof ==========================

Les lignes 1 et 2 sont les hypothèses, la ligne 3, la conclusion à prouver. Là encore, Otter va prouver par l’absurde que c1, supposé égoïste (ligne 4) est impopulaire (ligne 9). La ligne 5 réécrit l’implication de la ligne 1 sous forme de disjonction. Par comparaison avec la ligne 4 (où x=c1) on trouve alors à la ligne 9 que c1 est impopulaire.

La ligne 6 est l’hypothèse par l’absurde : c1 étant égoïste quelconque, on suppose qu’il est serviable quand même. La ligne 7 réécrit la seconde implication sous forme de disjonction et par comparaison avec la ligne 6, la ligne 8 conclut que c1 est populaire.

En comparant les lignes 8 et 9, on aboutit à une antilogie.

Darii

JPEG - 6.7 ko

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 :

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.

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 » :

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.

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

1 subgoals
x : U
H : victorieux x /\ méritant x
______________________________________(1/1)
Quelque méritant est brave

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 :

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.
    destruct H as [a b].

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

1 subgoals
x : U
a : victorieux x
b : méritant x
______________________________________(1/1)
Quelque méritant est brave

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

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.
    destruct H as [a b].
    apply 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 :

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.
    destruct H as [a b].
    pattern A2.

La réponse obtenue est celle-ci :

1 subgoals
x : U
a : victorieux x
b : méritant x
______________________________________(1/1)
(fun _ : Tout victorieux est brave => Quelque méritant est brave) A2

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 :

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.
    destruct H as [a b].
    apply A2 in a.

Cela donne alors

1 subgoals
x : U
a : brave x
b : méritant x
______________________________________(1/1)
Quelque méritant est brave

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 :

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.
    destruct H as [a b].
    apply A2 in a.
    exists x.

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

1 subgoals
x : U
a : brave x
b : méritant x
______________________________________(1/1)
méritant x /\ brave x

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

Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
    destruct A1.
    destruct H as [a b].
    apply A2 in a.
    exists x.
    tauto.
Qed.

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

tactique

Pour définir la tactique darii :

Ltac darii P1 P2 := destruct P1 as [x H]; destruct H as [a b]; apply P2 in a; exists x; tauto.

Une fois cette tactique ajoutée à l’utilitaire carroll, le syllogisme se résout ainsi :

Load carroll.
Parameter victorieux méritant brave: Prédicat.
Axiom A1: Quelque victorieux est méritant.
Axiom A2: Tout victorieux est brave.
Theorem T1: Quelque méritant est brave.
Proof.
        darii A1 A2.
Qed.

l’outre victorieuse

Le fichier Otter peut être ouvert avec Prover9 :

formulas(assumptions).
exists x (victorieux(x) & meritant(x)).
all x (victorieux(x) -> brave(x)).
end_of_list.
formulas(goals).
exists x (brave(x)&meritant(x)).
end_of_list.

Soumis à Otter ou Prover9, il donne la preuve suivante :

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.01) seconds.
% Length of proof is 10.
% Level of proof is 3.
% Maximum clause weight is 0.
% Given clauses 0.

1 (exists x (victorieux(x) & meritant(x))) # label(non_clause).  [assumption].
2 (all x (victorieux(x) -> brave(x))) # label(non_clause).  [assumption].
3 (exists x (brave(x) & meritant(x))) # label(non_clause) # label(goal).  [goal].
4 -victorieux(x) | brave(x).  [clausify(2)].
5 victorieux(c1).  [clausify(1)].
6 -brave(x) | -meritant(x).  [deny(3)].
7 meritant(c1).  [clausify(1)].
8 -brave(c1).  [resolve(6,b,7,a)].
9 brave(c1).  [resolve(4,a,5,a)].
10 $F.  [resolve(8,a,9,a)].

============================== end of proof ==========================

Les lignes 1 et 2 sont les hypothèses, la ligne 3 est le but à prouver. La ligne 4 est une réécriture de la ligne 2 sous forme de disjonction. L’hypothèse ligne 1 peut s’écrire sous la forme de deux hypothèses sur c1 : Lignes 5 et 7.

Ligne 6 on fait une hypothèse par l’absurde : c1 n’est pas brave ou alors il n’est pas méritant. Mais ligne 7 on se rappelle qu’il est méritant. Par conséquent il n’est pas brave (ligne 8). En comparant les lignes 4 et 5 (modus ponens) on apprend qu’en fait si, il est brave (ligne 9). Donc il est brave et pas brave en même temps (ligne 10) ce qui achève la preuve par l’absurde.

Ferio

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.
JPEG - 23 ko

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 :

Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.

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

Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.
Proof.
    destruct A2.

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

1 subgoals
x : U
H : fanfaron x /\ lâche x
______________________________________(1/1)
Quelque fanfaron n`est pas méritant

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 :

Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.
Proof.
    destruct A2.
    destruct H as [a b].

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

1 subgoals
x : U
a : fanfaron x
b : lâche x
______________________________________(1/1)
Quelque fanfaron n`est pas méritant

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

Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.
Proof.
    destruct A2.
    destruct H as [a b].
    apply A1 in b.

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

1 subgoals
x : U
a : fanfaron x
b : ~ méritant x
______________________________________(1/1)
Quelque fanfaron n`est pas méritant

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

Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.
Proof.
    destruct A2.
    destruct H as [a b].
    apply A1 in b.
    exists x.

La conjonction de a et b convient maintenant :

1 subgoals
x : U
a : fanfaron x
b : ~ méritant x
______________________________________(1/1)
fanfaron x /\ ~ méritant x

Encore une fois, la fin est tauto-matique :

Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.
Proof.
    destruct A2.
    destruct H as [a b].
    apply A1 in b.
    exists x.
    tauto.
Qed.

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

tactique

La tactique ferio se définit ainsi :

Ltac ferio P1 P2 := destruct P2 as [x H]; destruct H as [a b]; apply P1 in b; exists x; tauto.

Le syllogisme ci-dessus, avec cette tactique, se résout ainsi :

Load carroll.
Parameter lâche fanfaron méritant: Prédicat.
Axiom A1: Aucun lâche n`est méritant.
Axiom A2: Quelque fanfaron est lâche.
Theorem T1: Quelque fanfaron n`est pas méritant.
Proof.
    ferio A1 A2.
Qed.

L’outre sans outrage

La version Otter (ou Prover9) est similaire aux précédentes :

formulas(assumptions).
all x (lache(x)-> -meritant(x)).
exists x (fanfaron(x)& lache(x)).
end_of_list.
formulas(goals).
exists x (fanfaron(x)& -meritant(x)).
end_of_list.

Ce fichier, une fois digéré par l’outre, donne cette preuve :

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.03) seconds.
% Length of proof is 10.
% Level of proof is 3.
% Maximum clause weight is 0.
% Given clauses 0.

1 (all x (lache(x) -> -meritant(x))) # label(non_clause).  [assumption].
2 (exists x (fanfaron(x) & lache(x))) # label(non_clause).  [assumption].
3 (exists x (fanfaron(x) & -meritant(x))) # label(non_clause) # label(goal).  [goal].
4 lache(c1).  [clausify(2)].
5 -lache(x) | -meritant(x).  [clausify(1)].
6 -fanfaron(x) | meritant(x).  [deny(3)].
7 fanfaron(c1).  [clausify(2)].
8 meritant(c1).  [resolve(6,a,7,a)].
9 -meritant(c1).  [resolve(4,a,5,a)].
10 $F.  [resolve(8,a,9,a)].

============================== end of proof ==========================

En voici le résumé en langue naturelle :

Les lignes 1 et 2 sont les hypothèses, la ligne 3 le but à prouver. La ligne 2 suppose qu’il existe un individu que nous appellerons c1 par souci d’anonymat, qui est à la fois lâche et fanfaron. Ces deux hypothèses sur c1 sont séparées lignes 4 et 7.

La ligne 5 est une réécriture de la ligne sous forme de disjonction. Appliquée à c1, cela dit que ou bien c1 n’est pas lâche (ce qui n’est pas le cas à cause de la ligne 4) ou il n’est pas méritant. On en déduit (par modus ponens) que c1 n’est pas méritant (ligne 9).

On suppose par l’absurde ligne 6, que, ou bien c1 n’est pas fanfaron, ou bien il est méritant. Dans ce cas, comme on sait (ligne 7) qu’il est fanfaron, c’est que forcément il est méritant (ligne 8). Mais on a vu (ligne 9) que non. Par conséquent (ligne 10) l’hypothèse que c1 est méritant ou pas fanfaron est absurde : Il existe quelqu’un (c1 pour ne pas le nommer) qui est à la fois fanfaron et sans mérite.

Crocos

JPEG - 40.8 ko

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.

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.

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

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    intros.

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) :

1 subgoals
x : U
H : bébé x
______________________________________(1/1)
~ champion x

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

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    intros.
    apply A1 in H.

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

1 subgoals
x : U
H : illogique x
______________________________________(1/1)
~ champion x

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

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    intros.
    apply A1 in H.
    apply A3 in H.

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

1 subgoals
x : U
H : méprisé x
______________________________________(1/1)
~ champion x

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 :

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    intros.
    apply A1 in H.
    apply A3 in H.
    contradict H.

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

1 subgoals
x : U
H : champion x
______________________________________(1/1)
~ méprisé x

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 :

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    intros.
    apply A1 in H.
    apply A3 in H.
    contradict H.
    apply A2 in H.

Le problème devient tautologique :

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    intros.
    apply A1 in H.
    apply A3 in H.
    contradict H.
    apply A2 in H.
    tauto.
Qed.

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

1 subgoals
x : U
H : ~ méprisé x
______________________________________(1/1)
~ méprisé x

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

Version courte

Avec un peu d’expérience des syllogismes, on peut voir que les axiomes A1 et A3 permettent de démontrer, par la tactique barbara, que tout bébé est méprisé. Le problème, c’est que ce n’est pas ce que l’on voulait démontrer. Alors on en fait une sorte de théorème provisoire dans la démonstration principale, c’est-à-dire un lemme (mathématiques) :

Parameter bébé illogique méprisé champion: Prédicat.
Axiom A1: Tout bébé est illogique.
Axiom A2: Aucun champion n`est méprisé.
Axiom A3: Tout illogique est méprisé.
Theorem T1: Aucun bébé n`est champion.
Proof.
    Lemma L1: Tout bébé est méprisé.
        Proof.
            barbara A1 A3.
        Qed.
    celarent L1 A2.
Qed.

On peut traduire cette démonstration ainsi :

  • On applique barbara aux axiomes A1 et A3 ; on obtient ainsi le lemme L1 ;
  • On applique celarent à ce lemme et à l’axiome A2.

Le crocodile et l’outre

La version Otter (ou Prover9) de ce problème s’écrit comme ceci :

formulas(assumptions).
all x (bebe(x) -> -logique(x)).
all x (champion(x) -> -meprise(x)).
all x (-logique(x) -> meprise(x)).
end_of_list.
formulas(goals).
all x (bebe(x) -> meprise(x)).
end_of_list.

Soumis à Otter, on a la preuve suivante :

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.03) seconds.
% Length of proof is 10.
% Level of proof is 4.
% Maximum clause weight is 0.
% Given clauses 0.

1 (all x (bebe(x) -> -logique(x))) # label(non_clause).  [assumption].
3 (all x (-logique(x) -> meprise(x))) # label(non_clause).  [assumption].
4 (all x (bebe(x) -> meprise(x))) # label(non_clause) # label(goal).  [goal].
5 bebe(c1).  [deny(4)].
6 -bebe(x) | -logique(x).  [clausify(1)].
7 -logique(c1).  [resolve(5,a,6,a)].
8 logique(x) | meprise(x).  [clausify(3)].
9 meprise(c1).  [resolve(7,a,8,a)].
10 -meprise(c1).  [deny(4)].
11 $F.  [resolve(9,a,10,a)].

============================== end of proof ==========================

Les lignes 1 à 3 rappellent les hypothèses et la ligne 4 rappelle la conclusion. Otter prouve la ligne 4 par l’absurde : On suppose (ligne 5) qu’il existe un bébé (lrépondant au doux nom de c1) qui n’est pas méprisé (ligne 10). Et on va à partir de cette hypothèse, prouver qu’en fait il est méprisé quand même (ligne 9) ce qui à partir de la ligne 10, signifiera qu’il est à la fois méprisé et pas méprisé (ligne 11).

La ligne 6 est une réécriture de l’implication ligne 1 sous forme d’une disjonction. Par comparaison avec sa prémisse ligne 5, on en déduit que c1 est illogique. Or en réécrivant (ligne 8) la troisième implication (ligne 3) sous forme de disjonction, on en déduit (ligne 9) qu’il est méprisé. Ce qui clôt la preuve.

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

Algorithmique

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}

Conclusion

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 :

Require Import ClassicalFacts.
Require Import Classical.
Parameter Univers: Set.
Definition Prédicat := Univers->Prop.
Notation "'Tout' sujet 'est' objet" := (forall x:Univers, sujet(x) -> objet(x)) (at level 50).
Notation "'Aucun' sujet 'n`est' objet" := (forall x:Univers, sujet(x) -> ~objet(x)) (at level 50).
Notation "'Quelque' sujet 'est' objet" := (exists x:Univers, sujet(x) /\ objet(x)) (at level 50).
Notation "'Quelque' sujet 'n`est' 'pas' objet" := (exists x:Univers, sujet(x) /\ ~objet(x)) (at level 50).
Axiom contraposition: forall sujet objet: Prédicat, (Aucun sujet n`est objet) -> (Aucun objet n`est sujet).
Axiom doubleneg: forall p: Prop, ~~p->p.
Ltac barbara P1 P2 := intros x H; apply P2; apply P1; trivial.
Ltac celarent P1 P2 := intros x H; apply P1 in H; contradict H; apply P2; tauto.
Ltac darii P1 P2 := destruct P1 as [x H]; destruct H as [a b]; apply P2 in a; exists x; tauto.
Ltac ferio P1 P2 := destruct P2 as [x H]; destruct H as [a b]; apply P1 in b; exists x; tauto.

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

Require Import carroll.
Parameter cétacé mammifère homéostatique: Prédicat.
Axiom A1: Tout cétacé est mammifère.
Axiom A2: Tout mammifère est homéostatique.
Theorem T1: Tout cétacé est homéostatique.

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

fichier Coq (Load) fichier compilé (Import)
Zip - 548 octets
Zip - 2.7 ko

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) :

• Prendre un nombre
• Lui ajouter 8
• Multiplier le résultat par 3
• Enlever 24
• Enlever le nombre de départ

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 » :

brevet(x):={
  y := x + 8;
  y := y*3;
  y := y-24;
  y := y-x;
  retourne y;
}:;

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

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.

le source html

Voici le contenu du fichier ; c’est dans la ligne 16 qu’on va insérer les définitions de blocs :

<!DOCTYPE html>
<html lang="fr">
<head>
  <meta charset="utf-8">
  <title>Blockly</title>
<script src="https://blockly-demo.appspot.com/static/blockly_compressed.js"></script>
<script src="https://blockly-demo.appspot.com/static/blocks_compressed.js"></script>
<script src="https://blockly-demo.appspot.com/static/javascript_compressed.js"></script>
<script src="https://blockly-demo.appspot.com/static/msg/js/fr.js"></script>
</head>
<body>
  <div id="blocklyDiv" style="height: 320px; width: 480px;"></div>
  <xml id="toolbox" style="display: none">
 
 
  </xml>
 
<script>
    var workspace = Blockly.inject('blocklyDiv',
        {media: 'media/',
         toolbox: document.getElementById('toolbox')});
</script>
 
</body>
</html>

La seule fonction en JavaScript qui existe là-dedans, se contente de créer une variable « workspace » dans laquelle sont injectés les outils de 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 :

Blockly.Blocks['axiome1'] = {
  init: function() {
    this.appendDummyInput()
        .appendField("Les bébés sont illogiques");
    this.setPreviousStatement(true, "bébé");
    this.setNextStatement(true, "illogique");
    this.setColour(330);
    this.setTooltip('axiome 1');
  }
};

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)

Nouveau fichier html

On obtient alors ce fichier html :

<!DOCTYPE html>
<html lang="fr">
<head>
  <meta charset="utf-8">
  <title>Blockly</title>
<script src="https://blockly-demo.appspot.com/static/blockly_compressed.js"></script>
<script src="https://blockly-demo.appspot.com/static/blocks_compressed.js"></script>
<script src="https://blockly-demo.appspot.com/static/javascript_compressed.js"></script>
<script src="https://blockly-demo.appspot.com/static/msg/js/fr.js"></script>
<script>
Blockly.Blocks['axiome1'] = {
  init: function() {
    this.appendDummyInput()
        .appendField("Les bébés sont illogiques");
    this.setPreviousStatement(true, "bébé");
    this.setNextStatement(true, "illogique");
    this.setColour(330);
    this.setTooltip('axiome 1');
  }
};
Blockly.Blocks['axiome2'] = {
  init: function() {
    this.appendDummyInput()
        .appendField("Si on vient à bout d'un croco on n'est pas méprisé");
    this.setPreviousStatement(true, "méprisé");
    this.setNextStatement(true, "crocodile");
    this.setColour(90);
    this.setTooltip('axiome 2');
  }
};
Blockly.Blocks['axiome3'] = {
  init: function() {
    this.appendDummyInput()
        .appendField("Les gens illogiques sont méprisés");
    this.setPreviousStatement(true, "illogique");
    this.setNextStatement(true, "méprisé");
    this.setColour(195);
    this.setTooltip('axiome 3');
  }
};
</script>
</head>
<body>
  <div id="blocklyDiv" style="height: 320px; width: 640px;"></div>
  <xml id="toolbox" style="display: none">
  <category name="axiomes">
  <block type="axiome1"></block>
  <block type="axiome2"></block>
  <block type="axiome3"></block>
  </category>
  </xml>
 
<script>
    var workspace = Blockly.inject('blocklyDiv',
        {media: 'media/',
         toolbox: document.getElementById('toolbox')});
</script>
 
</body>
</html>

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


[1extrait de logique sans peine.


Documents joints

HTML - 1.8 ko
HTML - 1.8 ko
HTML - 2.3 ko
HTML - 2.3 ko

Portfolio

JPEG - 21.7 ko

Commentaires

Annonces

Prochains rendez-vous de l’IREM

Séminaire EDIM-IREM

- Mercredi 22 novembre 2017, 14h-18h, campus du Tampon, amphi 120 D
- Mercredi 7 février 2018, PTU, Saint-Denis, salle S23.6
- Mercredi 7 mars 2018, 14h-18h, campus du Tampon
- Mercredi 4 avril 2018, PTU, Saint-Denis, salle S23.6
- Mercredi 2 mai, 14h-18h, campus du Tampon
- Mardi 5 juin 2018, PTU, Saint-Denis, salle S23.6
- Mercredi 6 juin, 14h-18h, campus du Tampon

Fête de la science

Campus du Moufia, 16 et 17 novembre 2017.
Thème : « La recherche à l’heure du numérique »

Semaine des mathématiques

Du 26 au 31 mars 2018.
Thème : « Mathématiques et mouvement »


Brèves

Décès de Raymond Smullyan

mercredi 15 mars

Le logicien Raymon Smullyan est décédé en février 2017, à l’âge respectable de 97 ans : Il avait eu Alonzo Church comme professeur ! Pour en savoir plus, voir cet article

Travailler à plusieurs

lundi 19 décembre 2016

Les enseignements d’exploration au lycée imposent aux enseignants de travailler ensemble. Chantal Tuffery-Rochdi a analysé dans sa thèse les pratiques des enseignants de MPS (méthodes et pratiques scientifiques). Elle répond aux questions des Cahiers pédagogiques.

Un document sur Eduscol

mardi 19 mai 2015

Un document clarifiant bien la façon dont les mêmes concepts vivent en mathématiques et dans les sciences « exactes » les utilisant, publié par Eduscol en octobre 2014. Citons-les :
« Le document proposé ci-dessous s’adresse aux professeurs de mathématiques, physique-chimie et sciences de l’ingénieur intervenant dans le segment [Bac-3 ; Bac+3]. Il vise à les informer des différences de présentation et d’interprétation qui sont faites de certains concepts mathématiques dans les autres disciplines. Ces éclaircissements peuvent contribuer à harmoniser et à clarifier l’utilisation de ces notions auprès des élèves. »

Histoire de la comptabilité

vendredi 28 décembre 2012

Sur ce site (en anglais) dédié à la comptabilité, on trouve des informations intéressantes sur l’histoire et les pratiques de ce domaine, qui peuvent être utiles aux professeurs enseignant des mathématiques financières (et aussi aux autres...).

La CGE et la réforme des lycées

lundi 16 janvier 2012

La Conférence des Grandes Écoles publie 19 préconisations pour la réforme du lycée.

Sur le Web : Les 19 préconisations

Pratique des mathématiques en série STD2A

lundi 16 janvier 2012

Le site de l’IGEN offre des recommandations et des ressources pour enseigner les mathématiques en série STD2A. Les thèmes abordés (couleurs et nuances de gris, arcs et architecture, jeux vidéos, photo et tableur, perspectives parallèles...) sont de nature à donner aussi des idées d’activités aux enseignants des autres séries !

En cheminant avec Kakeya

lundi 16 janvier 2012

Un livre (à télécharger) de Vincent Borelli et Jean-Luc Rullière qui présente le calcul intégral et la dérivation en s’appuyant sur la question de Kakeya. Pour les lycéens, les étudiants et tous les esprits curieux qui souhaitent voir les mathématiques sous un jour différent.

Sur le Web : Livre à télécharger

Bicentenaire Galois

lundi 12 septembre 2011

À l’occasion du bicentenaire de la naissance d’Évariste Galois (1811-2011), l’Institut Henri Poincaré et la Société mathématique de France organisent un ensemble de manifestations et proposent un site contenant diverses ressources documentaires susceptibles d’intéresser les enseignants.

Statistiques

Dernière mise à jour

dimanche 10 décembre 2017

Publication

775 Articles
Aucun album photo
134 Brèves
11 Sites Web
132 Auteurs

Visites

405 aujourd'hui
1013 hier
2196658 depuis le début
35 visiteurs actuellement connectés