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

Exemple

Soit $P$ et $Q$ deux énoncés. Sous l'hypothèse que $P$ et $P ⇒ Q$ sont vrais, on peut déduire que $Q$ est vrai.

example (P Q : Prop) (hP : P) (h : P  Q) : Q :=
Démonstration
Puisque $P$ est vrai et que $P$ implique $Q$, $Q$ est vrai.
  exact h hP,
P Q : Prop,
hP : P,
h : P  Q
 Q
no goals
QED.
Exemple

Redémontrons l'exemple précédant en faisant un raisonnement vers l'arrière (même si ce n'est pas très percutant ici).

example (P Q : Prop) (hP : P) (h : P  Q) : Q :=
Démonstration
Puisque l'hypothèse h garantit que $P$ implique $Q$, il suffit de démontrer $P$.
  apply h,
P Q : Prop,
hP : P,
h : P  Q
 Q
P Q : Prop,
hP : P,
h : P  Q
 P
Or l'hypothèse $hP$ affirme que $P$ est vrai.
  exact hP,
P Q : Prop,
hP : P,
h : P  Q
 P
no goals
QED.

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

Exemple

À ce stade, nous manquons d'autres connecteurs logiques pour démontrer une implication intéressante (même un tout petit peu). Démontrons donc que $P$ implique $P$.

example (P : Prop) : P  P :=
Démonstration
Supposons $P$. Il s'agit alors de montrer $P$.
  intro hₚ,
P : Prop
 P  P
P : Prop,
hₚ : P
 P
C'est exactement ce qu'on vient de supposer !
  exact hₚ,
P : Prop,
hₚ : P
 P
no goals
QED.

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.

Exemple

Soit $P$, $Q$ et $R$ trois énoncés tels que $P$ équivaut à $Q$ et $Q$ implique $R$. $P$ implique $R$.

example (P Q R : Prop) (h : P  Q) (hQR : Q  R) : P  R :=
Démonstration
Supposons que $P$ est vrai, et montrons $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
Comme $Q$ implique $R$, il suffit de montrer $Q$.
  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
Comme $P$ et $Q$ sont équivalents, $P$ implique $Q$ (et $Q$ implique $P$).
  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
En particulier on peut déduire $Q$ de notre hypothèse $P$.
  exact hPQ hP,
P Q R : Prop,
hQR : Q  R,
hP : P,
hPQ : P  Q,
hQP : Q  P
 Q
no goals
QED.

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.

Exemple

Soit $P$, $Q$ et $R$ trois énoncés tels que $P$ équivaut à $Q$ et $Q$ implique $R$. $P$ implique $R$.

example (P Q R : Prop) (h : P  Q) (hQR : Q  R) : P  R :=
Démonstration
Supposons que $P$ est vrai.
  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
Comme $P$ équivaut à $Q$, donc implique $Q$, et que $Q$ implique $R$, on obtient $R$.
  exact hQR (h.1 hP),
P Q R : Prop,
h : P  Q,
hQR : Q  R,
hP : P
 R
no goals
QED.

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

Exemple

On reprends l'exemple précédent en effectuant un remplacement.

example (P Q R : Prop) (h : P  Q) (hQR : Q  R) : P  R :=
Démonstration
Comme $P$ et $Q$ sont équivalents, on peut remplacer $Q$ par $P$ dans l'hypothèse que $Q$ implique $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
Cette hypothèse devient alors exactement l'implication à démontrer.
  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
QED.

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.

Exemple

Montrons que l'hypothèse que $P$ et $Q$ sont vrais entraîne que $P$ est vrai.

example (P Q : Prop) : P  Q  P :=
Démonstration
Supposons que $P$ et $Q$ sont vrais.
  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
En particulier $P$ est vrai.
  exact hP,
P Q : Prop,
hP : P,
hQ : Q
 P
no goals
QED.

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.

Exemple

Montrons que si $P$ est vrai et $P$ implique $Q$ alors $P$ et $Q$.

example (P Q : Prop) (hP : P) (hPQ : P  Q) : P  Q :=
Démonstration
Montrons que $P$ et $Q$ sont vrais.
  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
$P$ est vrai par hypothèse.
    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
$Q$ est vrai car, par hypothèse, $P$ et $P$ implique $Q$ sont vrais.
    exact hPQ hP,
P Q : Prop,
hP : P,
hPQ : P  Q
 Q
no goals
QED.

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.

Exemple

Soit $P$, $Q$ et $R$ trois énoncés tels que $P$ implique $R$ et $Q$ implique $R$. Si $P$ ou $Q$ alors $R$.

example (P Q R : Prop) (hPR : P  R) (hQR : Q  R) : P  Q  R :=
Démonstration
Supposons que $P$ ou $Q$ est vrai.
  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
De deux choses l'une,
  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
ou bien $P$ est vrai, et on obtient $R$ car $P$ implique $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
ou bien $Q$ est vrai, et on obtient $R$ car $Q$ implique $R$.
   exact hQR hQ,
case or.inr
P Q R : Prop,
hPR : P  R,
hQR : Q  R,
hQ : Q
 R
no goals
QED.

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.

Exemple
example (P Q R : Prop) (h : P  R) : P  Q  R :=
Démonstration
Supposons $P$.
  intro hP,
P Q R : Prop,
h : P  R
 P  Q  R
P Q R : Prop,
h : P  R,
hP : P
 Q  R
Pour montrer que $Q$ ou $R$ est vrai, montrons $R$.
  right,
P Q R : Prop,
h : P  R,
hP : P
 Q  R
P Q R : Prop,
h : P  R,
hP : P
 R
Cet énoncé découle de l'hypothèse que $P$ est vrai car $P$ implique $R$.
  exact h hP,
P Q R : Prop,
h : P  R,
hP : P
 R
no goals
QED.

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

Exemple

Soit $P$, $Q$, $R$ et $S$ quatre énoncés tels que $P$ ou $Q$ implique $R$ et que $S$ implique $P$. Montrons que $S$ implique $R$.

example (P Q R S : Prop) (hPQR : P  Q  R) (hSP : S  P) : S  R :=
Démonstration
Supposons $S$.
  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
Alors on peut affirmer que $P$ ou $Q$ est vrai
  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
En effet $P$ est vrai
    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
car nous avons supposé que $S$ implique $P$ et que $S$ est vrai.
    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
Puisque $P$ ou $Q$ implique $R$, on déduit $R$ de cette affirmation.
  exact hPQR hPQ,
P Q R S : Prop,
hPQR : P  Q  R,
hSP : S  P,
hS : S,
hPQ : P  Q
 R
no goals
QED.
Exemple

On peut démontrer le même énoncé sans énoncé intermédiaire, en utilisant une déduction vers l'arrière, et comparer la lisibilité obtenue. Dans un exemple aussi simple, on peut considérer que cette seconde démonstration est plus percutante tout en restant lisible, mais il n'en sera pas toujours ainsi.

example (P Q R S : Prop) (hPQR : P  Q  R) (hSP : S  P) : S  R :=
Démonstration
Supposons $S$ et montrons $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
Par hypothèse, il suffit de montrer que $P$ ou $Q$ est vrai.
  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
Or $P$ est vrai,
  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
car nous avons supposé que $S$ implique $P$ et que $S$ est vrai.
  exact hSP hS,
P Q R S : Prop,
hPQR : P  Q  R,
hSP : S  P,
hS : S
 P
no goals
QED.

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.