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$ ». L'énoncé $P$ est appelé la prémisse de l'implication $P ⇒ 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.

Dans Lean, pour raisonner vers l'avant en utilisant h et une hypothèse hP affirmant que $P$ est vrai, on écrit On conclut par h appliqué à hP ou bien simplement On conclut par 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$ et la notation h hP est une application de transformation.

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

  On conclut par h appliqué à hP,

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

Gagné ! 🎉

La commande Lean initiant une déduction vers l'arrière en utilisant l'implication h est On applique h. Cette commande cherche aussi si la prémisse de h est présente parmi les hypothèses, et l'utilise automatiquement si elle la trouve. En vue de la rédaction sur papier, il est souvent plus clair d'annoncer quel est le nouveau but B en écrivant : Par h il suffit de montrer que B.

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

  Par h il suffit de montrer que P,

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

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

  On conclut par hP,

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

Gagné ! 🎉

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$. » C'est pour cette raison que la commande On applique cherche automatiquement la prémisse parmi les hypothèses.

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 recherche d'une hypothèse mentionnant Q, on trouve hPQ : P → Q et on tape On applique 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 On conlut par hPQ appliqué à 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 Supposons hₚ : P où hₚ est un nom choisit par l'utilisateur pour évoquer une hypothèse affirmant que P est vrai. Ce nom peut être choisi assez librement mais il est commode de suivre la convention de faire débuter par la lettre h les hypothèses. On peut omettre l'indication : P (Lean sait bien ce qu'il y a à supposer) mais cela diminue la lisibilité. S'il y a plusieurs hypothèses successives, on peut les écrire sur la même lignes, séparées par des espaces, à condition de mettre des parenthèses losque le : est précisé, par exemple Supposons (hP : P) (hQ : Q).

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

  Supposons hₚ : P,

P : Prop
⊢ P → P

P : Prop,
hₚ : P
⊢ P

  On conclut par hₚ,

P : Prop,
hₚ : P
⊢ P

Gagné ! 🎉

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 Par h on obtient (hPQ : P → Q) (hQP : Q → P) 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 :=

  Supposons hP : P,

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

  Par hQR il suffit de montrer que Q,

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

  Par h on obtient (hPQ : P → Q) (hQP : Q → P),

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

  On conclut par hPQ appliqué à hP,

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

Gagné ! 🎉

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. Il ne faudra pas abuser de cette possibilité car elle n'aide pas vraiment à passer sur papier (mais le problème se posera nettement moins dans les vrais exercices portant sur les suites ou les fonctions).

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

  Supposons hP : P,

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

  On conclut par hQR (h.1 hP),

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

Gagné ! 🎉

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 On réécrit via h. Pour remplacer de la droite vers la gauche, c'est à dire ici remplacer Q par P, on utilise On réécrit via ← h. Pour opérer ces remplacements dans une autre hypothèse h', on écrit On réécrit via h dans h', ou dans l'autre sens On réécrit via ← h dans h'.

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

  On réécrit via ← h dans 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

  On conclut par hQR,

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

Gagné ! 🎉

Démonstration d'une équivalence

Il y a deux grandes façons de démontrer une équivalence $P ⇔ Q$. La première est de démontrer successivement les deux implications (on parle parfois de « démonstration par double implication »). Dans Lean, on annonce simplement qu'on va montrer la première implication en écrivant Montrons que P → Q. La deuxième façon est d'utiliser des réécritures via des équivalences déjà disponibles jusqu'à arriver à une équivalence déjà connue ou à un énoncé de la forme $P ⇔ P$.

L'exemple suivant montre la transititivé de la notion d'équivalence. On notera qu'il s'agit exactement de la même démonstration par remplacement que pour la transitivité de l'égalité.

example (P Q R : Prop) (h : P ↔ Q) (h' : Q ↔ R) : P ↔ R :=

  On réécrit via ← h',

P Q R : Prop,
h : P ↔ Q,
h' : Q ↔ R
⊢ P ↔ R

P Q R : Prop,
h : P ↔ Q,
h' : Q ↔ R
⊢ P ↔ Q

  On conclut par h,

P Q R : Prop,
h : P ↔ Q,
h' : Q ↔ R
⊢ P ↔ Q

Gagné ! 🎉

On peut aussi montrer le même énoncé, moins efficacement, par double implication après avoir séparé chaque hypothèse d'équivalence en deux implications. Les lignes de conclusions dans chaque cas utilisent la syntaxe concise d'application d'une implication à un fait. Plus loin on expliquera comment créer une affirmation intermédiaire pour rendre cela plus clair.

example (P Q R : Prop) (h : P ↔ Q) (h' : Q ↔ R) : P ↔ R :=

  Par h on obtient (hPQ : P → Q) (hQP : Q → P),

P Q R : Prop,
h : P ↔ Q,
h' : Q ↔ R
⊢ P ↔ R

P Q R : Prop,
h' : Q ↔ R,
hPQ : P → Q,
hQP : Q → P
⊢ P ↔ R

  Par h' on obtient (hQR : Q → R) (hRQ : R → Q),

P Q R : Prop,
h' : Q ↔ R,
hPQ : P → Q,
hQP : Q → P
⊢ P ↔ R

P Q R : Prop,
hPQ : P → Q,
hQP : Q → P,
hQR : Q → R,
hRQ : R → Q
⊢ P ↔ R

  Montrons que P → R,

P Q R : Prop,
hPQ : P → Q,
hQP : Q → P,
hQR : Q → R,
hRQ : R → Q
⊢ P ↔ R

2 goals
P Q R : Prop,
hPQ : P → Q,
hQP : Q → P,
hQR : Q → R,
hRQ : R → Q
⊢ P → R

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

  Supposons hP : P,

2 goals
P Q R : Prop,
hPQ : P → Q,
hQP : Q → P,
hQR : Q → R,
hRQ : R → Q
⊢ P → R

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

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

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

  On conclut par hQR (hPQ hP),

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

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

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

  Montrons que R → P,

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

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

  Supposons hR : R,

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

P Q R : Prop,
hPQ : P → Q,
hQP : Q → P,
hQR : Q → R,
hRQ : R → Q,
hR : R
⊢ P

  On conclut par hQP (hRQ hR),

P Q R : Prop,
hPQ : P → Q,
hQP : Q → P,
hQR : Q → R,
hRQ : R → Q,
hR : R
⊢ P

Gagné ! 🎉

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 Par h on obtient hP hQ. Comme d'habitude, il peut être plus clair de préciser ce que disent hP et hQ, comme dans l'exemple suivant.

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

  Supposons h : P ∧ Q,

P Q : Prop
⊢ P ∧ Q → P

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

  Par h on obtient (hP : P) (hQ : Q),

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

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

  On conclut par hP,

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

Gagné ! 🎉

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é en annonçant la démonstration du premier énoncé par la commande Montrons que P (ou Montrons P qui sonne un peu mieux ici).

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

  Montrons P,

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

    On conclut par 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

    On conclut par hPQ appliqué à hP,

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

Gagné ! 🎉

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 font 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 à l'aide de la commande On discute en utilisant h.

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

  Supposons h : P ∨ Q,

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

  On discute en utilisant h,

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

2 goals
P Q R : Prop,
hPR : P → R,
hQR : Q → R
⊢ P → R

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

   Supposons hP : P,

2 goals
P Q R : Prop,
hPR : P → R,
hQR : Q → R
⊢ P → R

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

2 goals
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hP : P
⊢ R

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

   On conclut par hPR appliqué à  hP,

2 goals
P Q R : Prop,
hPR : P → R,
hQR : Q → R,
hP : P
⊢ R

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

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

   Supposons hQ : Q,

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

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

   On conclut par hQR appliqué à hQ,

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

Gagné ! 🎉

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, on annonce à Lean quel côté va être démontré en utilisant la commande Montrons que.

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

  Supposons hP,

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

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

  Montrons que R,

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

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

  On conclut par h appliqué à hP,

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

Gagné ! 🎉

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 Fait 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 :=

  Supposons hS : S,

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

  Fait 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

    Montrons P,

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

    On conclut par 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

  On conclut par hPQR appliqué à hPQ,

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

Gagné ! 🎉

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

  Supposons hS : S,

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

  Par hPQR il suffit de montrer que P ∨ Q,

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

  Montrons P,

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

  On conclut par hSP appliqué à hS,

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

Gagné ! 🎉

Le cours continue avec le chapitre 3.