Implications et équivalences, conjonctions et disjonctions

L'implication

Le premier connecteur logique est l'implication. Étant donnés deux énoncés $P$ et $Q$, on peut construire l'énoncé $P ⇒ Q$ qui affirme « Si $P$ est vrai alors $Q$ est vrai ». On le lit « $P$ implique $Q$ ».

Il est crucial de bien comprendre que le symbole $⇒$ n'est pas l'abréviation du mot « donc ». La déduction d'information à l'aide d'une implication repose sur la véracité de deux énoncés et l'utilisation d'une règle de logique : sachant que $P$ est vrai et que $P$ implique $Q$ (c'est à dire que $P ⇒ Q$ est vrai), on en déduit que $Q$ est vrai, par application de la règle dite du modus ponens. La véracité de $P ⇒ Q$ ne suffit pas à elle seule à conclure quoique ce soit sur $Q$.

De façon peut-être encore plus surprenante, l'énoncé $P ⇒ Q$ est toujours vrai si $P$ est faux. Nous reviendrons sur ce point délicat dans un chapitre ultérieur. Mais il est déjà possible d'y penser du point de vue suivant : on peut voir les démonstrations de $P ⇒ Q$ comme des machines qui transforment toute démonstration de $P$ en démonstration de $Q$. Une telle machine existe toujours lorsqu'aucune démonstration de $P$ n'existe : la machine ne faisant rien convient ! Cette interprétation comme transformation de démonstration explique aussi pourquoi Lean note l'énoncé $P ⇒ Q$ par P → Q, une notation usuellement rencontrée dans le contexte des fonctions.

Utilisation d'une implication

On peut donc utiliser une hypothèse $h$ affirmant $P ⇒ Q$ pour démontrer $Q$ à condition d'avoir une démonstration de $P$. Ce mécanisme est indiqué par une phrase du type « Montrons que $Q$ est vrai. Puisque $P$ implique $Q$, il suffit de démontrer $P$ » ou bien « Puisque $P$ est vrai et que $P$ implique $Q$, $Q$ est vrai », selon qu'on dispose déjà d'une démonstration de $P$ ou non. Le premier cas de figure est appelé raisonnement déductif vers l'arrière, ou raisonnement par condition suffisante, tandis que le second est un raisonnement déductif vers l'avant. La commande Lean initiant une déduction vers l'arrière en utilisant l'implication h est apply h. Pour raisonner vers l'avant en utilisant h et une hypothèse hP affirmant que $P$ est vrai, on écrit exact h hP. Cette dernière notation peut être vue comme une simple liste (ordonnée) d'hypothèses à utiliser, mais on peut aussi la comprendre en voyant les implications comme transformations : l'hypothèse h transforme l'hypothèse hP en démonstration de $Q$.

example (P Q : Prop) (hP : P) (h : P → Q) : Q :=

  exact h hP,

P Q : Prop,
hP : P,
h : P → Q
⊢ Q

no goals

example (P Q : Prop) (hP : P) (h : P → Q) : Q :=

  apply h,

P Q : Prop,
hP : P,
h : P → Q
⊢ Q

P Q : Prop,
hP : P,
h : P → Q
⊢ P

  exact hP,

P Q : Prop,
hP : P,
h : P → Q
⊢ P

no goals

Il faut noter que le raisonnement vers l'arrière n'est pertinent que si la prémisse n'est pas encore démontrée (ni supposée). Si l'objectif est de démontrer $Q$ qui est impliqué par $P$, il est particulièrement maladroit de rédiger une démonstration de $P$ puis d'écrire « Ainsi on a $P$. Comme $P$ implique $Q$ et qu'on veut démontrer $Q$, il suffit de démontrer $P$. Or on a démontré $P$. » (ou des variantes encore plus alambiquées et répétitives). Bien qu'il n'y ait pas d'erreur dans cette rédaction, elle n'est vraiment pas facile à lire. Il est bien préférable d'écrire « Ainsi on a $P$. Comme $P$ implique $Q$, on en déduit $Q$. »

Il faut avouer que Lean encourage un peu le raisonnement vers l'arrière à outrance, en raison de la tentation suivante : face à l'objectif $Q$, on parcourt le contexte à la chercher d'une hypothèse mentionnant Q, on trouve hPQ : P → Q et on tape apply hPQ avant d'avoir eu le temps de se demander si le contexte ne contient pas aussi une hypothèse hP : P, qui permettrait d'écrire directement exact hPQ hP. Il faut donc faire un effort de nettoyage des démonstrations Lean avant de passer à la rédaction sur papier, en gardant à l'esprit ce risque en particulier.

Démonstration d'une implication

Pour montrer que $P$ implique $Q$, on suppose que $P$ est vrai, et on démontre $Q$ sous cette hypothèse. Cela suffit puisque si $P$ est faux alors l'implication $P ⇒ Q$ est toujours vraie, quelle que soit la véracité de $Q$. La rédaction pourra ainsi débuter par : « Montrons que $P$ implique $Q$. Supposons $P$, ...» les points de suspensions étant à remplacer par la démonstration (peut-être très longue !) de $Q$ sous l'hypothèse $P$, en plus des autres hypothèses courantes. Dans un contexte touffu, on peut nommer l'hypothèse ainsi introduite, en écrivant par exemple « Faisons l'hypothèse $hₚ$ que $P$ est vrai ».

Bien sûr on peut imaginer des démonstrations indirectes de $P ⇒ Q$, comme on le verra dans des chapitres ultérieurs. Le paragraphe précédent n'explique que la méthode directe.

Dans Lean, lorsque le but courant est de la forme P → Q, la commande pour dire « Supposons que $P$ est vrai » est intro. Lean va alors choisir lui-même un nom pour l'hypothèse ainsi introduite. Mais il est préférable de toujours fournir ce nom, ne serait-ce que pour s'imposer des conventions de nomenclature qui faciliteront l'organisation des démonstrations complexes. On emploiera alors intro hₚ pour choisir le nom hₚ.

example (P : Prop) : P → P :=

  intro hₚ,

P : Prop
⊢ P → P

P : Prop,
hₚ : P
⊢ P

  exact hₚ,

P : Prop,
hₚ : P
⊢ P

no goals

Chaînes d'implications

Comme l'égalité, la relation d'implication est transitive, c'est à dire que si les énoncés $P ⇒ Q$ et $Q ⇒ R$ sont vrais alors $P ⇒ R$ est vrai. Cette observation est souvent combinée avec l'abus de rédaction consistant à voir le symbole $⇒$ comme abréviation du mot « donc » en comprimant « $P$ et $P ⇒ Q$ sont vrais donc $Q$ est vrai » en « $P ⇒ Q$ ». On obtient alors une succession d'énoncés entrecoupés de symboles $⇒$, et parfois de sauts de lignes. Cette succession est supposée indiquer le dernier énoncé est conséquence du premier. La concision d'une telle écriture est séduisante, mais le risque de confusion est grand. En effet l'énoncé $P ⇒ Q ⇒ R$ est énoncé qui a un sens une fois précisée la convention de regroupement implicite qui l'interprète comme $P ⇒ (Q ⇒ R)$ plutôt que $(P ⇒ Q) ⇒ R$. Mais aucune de ces deux possibilités n'est logiquement équivalente à $P ⇒ R$. La première est équivalente à « Si $P$ et $Q$ sont vrais alors $R$ est vrai » tandis que la deuxième affirme que si l'implication $P ⇒ Q$ est vraie alors $R$ est vrai.

Pour cette raison, nous n'écrirons jamais de chaînes de symboles d'implications dans ce cours. L'utilisation de mots comme « donc », « or » et « ainsi » remplace avantageusement ces chaînes.

L'équivalence

On peut construire à partir de l'implication le connecteur logique d'équivalence. Étant donné deux énoncés $P$ et $Q$, l'équivalence de $P$ et $Q$ est l'énoncé qui affirme que $P$ est vrai si et seulement si $Q$ est vrai. On le note usuellement $P ⇔ Q$ mais Lean le note P ↔ Q, en cohérence avec sa notation pour l'implication. Dans les deux cas on le lit « $P$ équivaut à $Q$ » ou, de façon plus symétrique « $P$ et $Q$ sont équivalents ».

Bien que ce connecteur logique soit redondant au sens où il peut être exprimé à l'aide de deux implications (et d'une conjonction décrite plus bas), il joue un rôle privilégié via le mécanisme de remplacement. Sachant que $P$ équivaut à $Q$, on peut remplacer $P$ par $Q$ ou $Q$ par $P$ dans n'importe quel autre énoncé.

Ce mécanisme donne hélas lieu à la tentation d'utiliser le symbole $⇔$ comme abréviation dans une phrase. Le résultat est au mieux une faute de goût, mais le plus souvent aboutit à un sens complètement différent de l'intention de l'auteur. Un piège typique de ce genre est d'abréger la phrase « Montrons $P$, ce qui revient à montrer $Q$ » (dans un contexte où $P$ et $Q$ sont connus comme étant équivalents) par « Montrons $P ⇔ Q$ », qui semble annoncer une démonstration de l'équivalence de $P$ et $Q$. Une alternative qui met mieux en valeur l'équivalence, tout en évitant l'ambiguïté, est par exemple « Montrons $P$, qui équivaut à $Q$ ».

La discussion des chaînes d'implications à la fin de la section précédente s'applique aussi aux équivalence. L'équivalence est transitive, c'est à dire que si $P ⇔ Q$ et $Q ⇔ R$ alors $P ⇔ R$ mais nous n'écrirons pas $P ⇔ Q ⇔ R$, même si cet abus est parfois commode, par exemple dans le contexte d'une résolution d'équation.

Utilisation d'une équivalence

Pour utiliser une équivalence « $P ⇔ Q$ », on peut la décomposer en deux implications et utiliser l'une d'entre elle. On écrira par exemple « Puisque $P$ et $Q$ sont équivalents, $P$ implique $Q$ ». Dans Lean, si h est une hypothèse affirmant P ↔ Q, on peut la scinder à l'aide de la commande cases h with hPQ hQP pour obtenir hPQ : P → Q et hQP : Q → P. On peut aussi accéder à la première implication (de la gauche vers la droite) sous le nom h.1 et à la seconde sous le nom h.2.

example (P Q R : Prop) (h : P ↔ Q) (hQR : Q → R) : P → R :=

  intro hP,

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R
⊢ P → R

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R,
hP : P
⊢ R

  apply hQR,

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R,
hP : P
⊢ R

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R,
hP : P
⊢ Q

  cases h with hPQ hQP,

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R,
hP : P
⊢ Q

P Q R : Prop,
hQR : Q → R,
hP : P,
hPQ : P → Q,
hQP : Q → P
⊢ Q

  exact hPQ hP,

P Q R : Prop,
hQR : Q → R,
hP : P,
hPQ : P → Q,
hQP : Q → P
⊢ Q

no goals

Dans la démonstration précédente, on peut aussi accéder à l'implication $P ⇒ Q$ comme h.1, et utiliser la possibilité de former une démonstration en appliquant comme une fonction une hypothèse d'implication à une hypothèse assurant sa prémisse. On obtient la démonstration très concise suivante.

example (P Q R : Prop) (h : P ↔ Q) (hQR : Q → R) : P → R :=

  intro hP,

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R
⊢ P → R

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R,
hP : P
⊢ R

  exact hQR (h.1 hP),

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R,
hP : P
⊢ R

no goals

On peut aussi utiliser utiliser l'équivalence de $P$ et $Q$ pour remplacer $P$ par $Q$ (ou $Q$ par $P$) dans une hypothèse ou dans le but. Dans Lean sous l'hypothèse h : P ↔ Q, on peut remplacer P par Q dans le but à l'aide la commande rw h (ce rw est l'abréviation de rewrite). Pour remplacer de la droite vers la gauche, c'est à dire ici remplacer Q par P, on utilise rw ← h. Pour opérer ces remplacements dans une autre hypothèse h', on écrit rw h at h', ou dans l'autre sens rw ← h at h'.

example (P Q R : Prop) (h : P ↔ Q) (hQR : Q → R) : P → R :=

  rw ← h at hQR,

P Q R : Prop,
h : P ↔ Q,
hQR : Q → R
⊢ P → R

P Q R : Prop,
h : P ↔ Q,
hQR : P → R
⊢ P → R

  exact hQR

P Q R : Prop,
h : P ↔ Q,
hQR : P → R
⊢ P → R

P Q R : Prop,
h : P ↔ Q,
hQR : P → R
⊢ P → R

La conjonction

Étant donnés deux énoncés $P$ et $Q$, on peut construire la conjonction de $P$ et $Q$, il s'agit de l'énoncé qui affirme « $P$ et $Q$ sont vrais ». Le langage mathématique usuel n'emploie pas de notation pour la conjonction, le mot « et » étant bien assez court. Cependant les cours de logique et Lean utilisent la notation $P ∧ Q$.

Utilisation d'une conjonction

L'utilisation d'un hypothèse affirmant $P$ et $Q$ est quasiment transparente, on poursuit la démonstration en cours en utilisant la véracité de $P$ et celle de $Q$. Dans Lean, on peut explicitement décomposer une telle hypothèse h en deux hypothèses, nommées par exemple hP et hQ, à l'aide de la commande cases h with hP hQ.

example (P Q : Prop) : P ∧ Q → P :=

  intro h,

P Q : Prop
⊢ P ∧ Q → P

P Q : Prop,
h : P ∧ Q
⊢ P

  cases h with hP hQ,

P Q : Prop,
h : P ∧ Q
⊢ P

P Q : Prop,
hP : P,
hQ : Q
⊢ P

  exact hP,

P Q : Prop,
hP : P,
hQ : Q
⊢ P

no goals

On remarque que la démonstration précédente comporte deux commandes Lean pour une seule phrase. On peut éviter ce hiatus en remplaçant ces deux commande par l'unique commande rintro ⟨hP, hQ⟩ (le r étant l'abréviation de « récursif »). Mais l'utilisation de ce raccourci n'est pas encouragée dans un premier temps, à la fois pour bien décomposer les opérations et pour éviter de se surcharger la mémoire du côté technologique. Dans le même ordre d'idée, on peut se contenter d'utiliser intro h au début (sans le faire suivre de cases) mais se référer ensuite au membre de gauche en utilisant exact h.1.

Démonstration d'une conjonction

Pour démontrer (directement) une conjonction « $P$ et $Q$ », il faut fournir deux démonstrations : une démonstration de $P$ et une démonstration de $Q$. Le flot de la démonstration en cours se scinde donc en deux branches. Ces deux branches commencent avec un contexte commun mais des buts distincts. Puis elles progressent indépendamment l'une de l'autre. En particulier les résultats intermédiaires éventuellement démontrés dans une branche n'ont aucune influence sur l'autre. Dans Lean, cet embranchement est provoqué par la commande split. On peut alors focaliser son attention successivement sur les deux branches en entourant d'accolades les deux démonstrations.

example (P Q : Prop) (hP : P) (hPQ : P → Q) : P ∧ Q :=

  split,

P Q : Prop,
hP : P,
hPQ : P → Q
⊢ P ∧ Q

2 goals
P Q : Prop,
hP : P,
hPQ : P → Q
⊢ P

P Q : Prop,
hP : P,
hPQ : P → Q
⊢ Q

    exact hP,

2 goals
P Q : Prop,
hP : P,
hPQ : P → Q
⊢ P

P Q : Prop,
hP : P,
hPQ : P → Q
⊢ Q

P Q : Prop,
hP : P,
hPQ : P → Q
⊢ Q

    exact hPQ hP,

P Q : Prop,
hP : P,
hPQ : P → Q
⊢ Q

no goals

La disjonction

Étant donnés deux énoncés $P$ et $Q$, on peut construire la disjonction de $P$ et $Q$, il s'agit de l'énoncé qui affirme « $P$ ou $Q$ est vrai ». Le langage mathématique usuel n'emploie pas de notation pour la disjonction, le mot « ou » étant bien assez court. Cependant les cours de logique et Lean utilisent la notation $P ∨ Q$.

Il est important de bien noter que le ou de la logique est toujours inclusif. L'affirmation « $P$ ou $Q$ » est vrai n'exclut pas la possibilité que $P$ et $Q$ soient deux énoncés vrais.

Utilisation d'une disjonction

L'utilisation d'une hypothèse affirmant $P$ ou $Q$ scinde la démonstration en deux branches. La première branche suppose que $P$ est vrai tandis que la seconde suppose que $Q$ est vrai. Ces deux branches commencent avec un contexte commun mais une hypothèse différente. Puis elles progressent indépendamment l'une de l'autre. En particulier les résultats intermédiaires éventuellement démontrés dans une branche n'ont aucune influence sur l'autre. Ce phénomène d'embranchement rappelle la démonstration d'une conjonction, sauf que cette fois c'est l'utilisation d'une hypothèse qui provoque l'embranchement. Dans Lean, si h est une hypothèse assurant P ∨ Q, on crée les branches avec des noms d'hypothèses hP dans une branche et hQ dans l'autre à l'aide de la commande cases h with hP hQ. Là encore, on peut focaliser son attention successivement sur les deux branches en les entourant d'accolades.

example (P Q R : Prop) (hPR : P → R) (hQR : Q → R) : P ∨ Q → R :=

  intro h,

P Q R : Prop,
hPR : P → R,
hQR : Q → R
⊢ P ∨ Q → R

P Q R : Prop,
hPR : P → R,
hQR : Q → R,
h : P ∨ Q
⊢ R

  cases h with hP hQ,

P Q R : Prop,
hPR : P → R,
hQR : Q → R,
h : P ∨ Q
⊢ R

2 goals
case or.inl
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hP : P
⊢ R

case or.inr
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hQ : Q
⊢ R

   exact hPR hP,

2 goals
case or.inl
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hP : P
⊢ R

case or.inr
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hQ : Q
⊢ R

case or.inr
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hQ : Q
⊢ R

   exact hQR hQ,

case or.inr
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hQ : Q
⊢ R

no goals

Ici aussi, on peut regretter qu'il faille deux lignes pour introduire l'hypothèse h puis provoquer l'embranchement. L'utilisateur expert peut écrire plutôt rintro (hP | hQ), mais il n'est pas nécessaire de retenir cette syntaxe pour faire les exercices.

Démonstration d'une disjonction

Pour démontrer (directement) la disjonction « $P$ ou $Q$ », il faut, au choix, démontrer $P$ ou démontrer $Q$. Il n'y a qu'une seule branche, mais l'auteur de la démonstration doit choisir (en général une seule des deux possibilités permet de conclure). Face à un but de la forme P ∨ Q, la commande Lean permettant de choisir de démontrer P est left tandis que celle choisissant Q est right.

example (P Q R : Prop) (h : P → R) : P → Q ∨ R :=

  intro hP,

P Q R : Prop,
h : P → R
⊢ P → Q ∨ R

P Q R : Prop,
h : P → R,
hP : P
⊢ Q ∨ R

  right,

P Q R : Prop,
h : P → R,
hP : P
⊢ Q ∨ R

P Q R : Prop,
h : P → R,
hP : P
⊢ R

  exact h hP,

P Q R : Prop,
h : P → R,
hP : P
⊢ R

no goals

L'affirmation intermédiaire

Les démonstrations des sections précédentes ne rendent évidemment pas compte de la complexité usuelle d'une démonstration mathématique, même en première année d'université. Il est très souvent nécessaire d'introduire des énoncés intermédiaires dans la démonstration. Un tel énoncé interrompt le flot principal de la démonstration en créant un nouveau but : démontrer l'énoncé intermédiaire. Une fois ce but atteint, on peut reprendre la démonstration principale là où elle s'était arrêtée, mais muni d'une nouvelle hypothèse affirmant la véracité de l'énoncé intermédiaire.

En plus de limiter la complexité locale de la démonstration, le recours à un énoncé intermédiaire permet d'éviter d'avoir trop souvent recours aux déductions vers l'arrière, qui peuvent parfois rendre la lecture plus difficile.

Dans Lean, la commande introduisant un énoncé intermédiaire qui sera utilisable sous le nom h est have h : ..., les points de suspension étant à remplacer par l'énoncé.

example (P Q R S : Prop) (hPQR : P ∨ Q → R) (hSP : S → P) : S → R :=

  intro hS,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P
⊢ S → R

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ R

  have hPQ : P ∨ Q,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ R

2 goals
P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P ∨ Q

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S,
hPQ : P ∨ Q
⊢ R

    left,

2 goals
P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P ∨ Q

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S,
hPQ : P ∨ Q
⊢ R

2 goals
P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S,
hPQ : P ∨ Q
⊢ R

    exact hSP hS,

2 goals
P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S,
hPQ : P ∨ Q
⊢ R

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S,
hPQ : P ∨ Q
⊢ R

  exact hPQR hPQ,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S,
hPQ : P ∨ Q
⊢ R

no goals

example (P Q R S : Prop) (hPQR : P ∨ Q → R) (hSP : S → P) : S → R :=

  intro hS,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P
⊢ S → R

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ R

  apply hPQR,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ R

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P ∨ Q

  left,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P ∨ Q

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P

  exact hSP hS,

P Q R S : Prop,
hPQR : P ∨ Q → R,
hSP : S → P,
hS : S
⊢ P

no goals

Les fichier Lean correspondant à ce chapitre sauf la disjonction sont ici. Les exercices concernant la disjonction sont dans la feuille suivante.

Le cours continue avec le chapitre 3.