Ficha de revisão: Introduction aux règles de déduction logique

📋 Plan du Cours

1. Démonstration et utilisation des connecteurs
2. Notation H ⊢ P et état de la preuve
3. Implication : modus ponens et récurrence
4. Conjonction : introduction et éliminations
5. Disjonction : introduction et raisonnement par cas
6. Équivalence : double implication
7. Négation : introduction, double négation et absurde
8. Quantificateur universel : démonstration et condition
9. Quantificateur existentiel : introduction et utilisation
10. Règles Lean : tactiques et correspondances
11. Implication en Lean : intro, apply et specialize
12. Conjonction en Lean : constructor et And.left

📖 1. Démonstration et utilisation des connecteurs

🔑 Notions clés & Définitions

• Déduction naturelle : Méthode de preuve qui organise les raisonnements en règles d’introduction et d’élimination des connecteurs logiques.
• Règles de démonstration : En déduction naturelle, règles qui permettent d’établir un nouveau fait dont le connecteur principal est introduit.
• Règles d’utilisation : En déduction naturelle, règles qui permettent d’exploiter une hypothèse ou un théorème dont le connecteur principal est déjà présent.
• Introduction et élimination : Terminologie alternative en déduction naturelle où « introduction » remplace « démonstration » et « élimination » remplace « utilisation ».
• Turnstile : Symbole logique ` utilisé pour séparer les hypothèses courantes de l’énoncé à démontrer dans une notation de preuve.

📝 Points essentiels

• En mathématiques, un raisonnement alterne deux tâches : démontrer un résultat puis l’utiliser pour avancer.
• Les connecteurs et quantificateurs ont des règles d’utilisation et de démonstration qui correspondent à leurs définitions logiques.
• En Lean, on emploie souvent « introduction » pour les règles de démonstration et « élimination » pour les règles d’utilisation.
• La notation H \` P signifie que, sous les hypothèses $H$, on peut tenter de démontrer $P$ (ce qui peut être vrai ou non).
• Le symbole \` (turnstile) sert aussi en Lean à séparer la liste des hypothèses/objets courants de la formule à prouver.
• Les règles sont classées par connecteur principal : certaines construisent un énoncé avec ce connecteur, d’autres le décomposent pour l’exploiter.

💡 Astuce mémo

Démonstration = je fabrique (introduction), Utilisation = j’exploite (élimination) ; H \` P = « avec $H$, je vise $P$.

📖 2. Notation H ⊢ P et état de la preuve

🔑 Notions clés & Définitions

• Turnstile : Le turnstile est le symbole ` utilisé pour séparer le contexte d’hypothèses et le but dans une écriture de déduction.
• Contexte H : Le contexte H désigne la liste des hypothèses disponibles pour raisonner dans une preuve formelle.
• But P : Le but P est l’énoncé que l’on cherche à établir comme conséquence des hypothèses du contexte H.
• État de la preuve : Un état de la preuve est le couple H ` P, qui exprime que P est démontrissable à partir de H (ce qui peut être vrai ou non).

📝 Points essentiels

• La notation H ` P signifie que, sous les hypothèses H, on peut démontrer l’assertion P.
• Le symbole ` (turnstile) sert aussi en Lean à séparer les objets/hypothèses courants de l’énoncé à prouver.
• Dans H ` P, H correspond aux prémisses disponibles et P au but initial.
• Une preuve formelle consiste à combiner des états H ` P via des règles jusqu’à obtenir l’état correspondant au but.
• La règle Ax clôt une démonstration quand P apparaît déjà dans le contexte : Ax H ∪ {P} ` P.
• La règle d’affaiblissement permet de conserver une déduction quand on ajoute des hypothèses : si H Q alors H ∪ {P} Q.

💡 Astuce mémo

Contexte H = « ce que j’ai », But P = « ce que je veux » ; le tourniquet ` relie les deux.

📖 3. Implication : modus ponens et récurrence

🔑 Notions clés & Définitions

• Modus ponens : Règle d’inférence qui permet de déduire Q quand on a P ⇒ Q et P dans le même contexte.
• Récurrence : Méthode de preuve fondée sur une implication Q(n) ⇒ Q(n+1) pour établir Q(n) pour tous les entiers.
• Principe de récurrence : Schéma logique qui transforme l’hypothèse (∀n∈N, Q(n) ⇒ Q(n+1)) en la conclusion (∀n∈N, Q(n)).
• Proposition universelle : Énoncé de la forme ∀n∈N Q(n) qui demande de prouver Q(n) pour tout entier n.

📝 Points essentiels

• Si H ⊢ P ⇒ Q et H ⊢ P, alors on peut conclure H ⊢ Q par modus ponens.
• La preuve par récurrence vise un énoncé universel ∀n∈N Q(n) portant sur les entiers.
• Le principe de récurrence s’écrit sous forme d’implication : (∀n∈N, Q(n) ⇒ Q(n+1)) ⇒ ∀n∈N Q(n).
• Pour obtenir ∀n∈N Q(n), il suffit de démontrer la partie gauche : ∀n∈N (Q(n) ⇒ Q(n+1)).
• L’idée centrale est que l’implication Q(n) ⇒ Q(n+1) sert de “chaînage” logique pour propager la propriété à tous les n.
• La récurrence est une application directe du raisonnement par implication : on prouve une condition qui entraîne la conclusion pour tous les entiers.

💡 Astuce mémo

Implication + preuve de l’antécédent → preuve du conséquent : P⇒Q et P donnent Q ; en récurrence, Q(n)⇒Q(n+1) “fait avancer” la propriété de n à n+1.

📖 4. Conjonction : introduction et éliminations

🔑 Notions clés & Définitions

• Équivalence propositionnelle ⇔ : L’équivalence ⇔ relie deux propositions en exigeant qu’elles soient vraies ensemble via deux implications dans les deux sens.
• Double implication : La double implication est une preuve qui établit séparément l’implication directe et l’implication réciproque pour conclure une équivalence.
• Négation ¬ : La négation ¬P exprime que l’énoncé P ne peut pas être maintenu sans provoquer une contradiction dans le contexte.
• Double négation ¬¬ : La double négation ¬¬P signifie que P ne peut pas être faux, et elle se relie à P par une règle d’élimination.

📝 Points essentiels

• Raisonnement par disjonction des cas : pour ∀x∈E P(x) avec E=E1∪E2, il suffit de prouver P(x) séparément sur E1 puis sur E2.
• Élimination du ∨ : si x∈E1 alors P(x) et si x∈E2 alors P(x), alors on conclut P(x) pour x∈E1∪E2.
• Exemple d’entiers : pour n(n+1)/2, on sépare n pair (n/2 entier) et n impair (n+1 pair, donc (n+1)/2 entier) pour conclure que n(n+1)/2 est entier.
• Définition de ⇔ : P ⇔ Q signifie (P ⇒ Q) ∧ (Q ⇒ P).
• Règle dérivée ⇔i : pour prouver P ⇔ Q, on doit démontrer P ⇒ Q et Q ⇒ P séparément.
• Règle dérivée ⇔ed : pour utiliser une équivalence P ⇔ Q, on peut en déduire l’implication directe P ⇒ Q puis l’implication réciproque Q ⇒ P via les règles d’utilisation correspondantes.

💡 Astuce mémo

⇔ = (⇒) + (⇒) : deux flèches, une dans chaque sens ; ¬P se prouve en faisant tomber une contradiction, ¬¬P se prouve en montrant P.

📖 5. Disjonction : introduction et raisonnement par cas

🔑 Notions clés & Définitions

• Double négation : La double négation est la formule $\\neg\\neg P$, qui permet de récupérer $P$ via une règle d’élimination spécifique en logique classique.
• Raisonnement par l’absurde : Le raisonnement par l’absurde est une méthode où l’on suppose $\\neg P$ puis on obtient une contradiction pour conclure $P$.
• Règle d’introduction de la double négation : La règle d’introduction de la double négation permet de déduire $\\neg\\neg P$ à partir d’une contradiction obtenue sous l’hypothèse $\\neg P$.
• Règle d’utilisation de la double négation : La règle d’utilisation de la double négation permet de conclure $P$ à partir de $\\neg\\neg P$.
• Logique intuitionniste : La logique intuitionniste est un cadre où certaines règles classiques sur la négation, comme l’élimination de $\\neg$, ne sont pas valides.

📝 Points essentiels

• Pour prouver $P$, on peut supposer temporairement $\\neg P$ et chercher une contradiction dans ce contexte.
• Si sous l’hypothèse $\\neg P$ on obtient une contradiction, on déduit $\\neg\\neg P$ par la règle d’introduction de la double négation.
• À partir de $\\neg\\neg P$, on conclut $P$ par la règle d’utilisation de la double négation.
• Le raisonnement par l’absurde correspond aussi à un raisonnement par contradiction (terminologie anglaise).
• En logique intuitionniste, l’élimination de $\\neg$ et le raisonnement par l’absurde ne sont pas valides, contrairement au cadre classique.

💡 Astuce mémo

Contradiction sous $\\neg P$ → $\\neg\\neg P$ → $P$ (classique) ; en intuitionniste, la dernière étape ne marche pas.

📖 6. Équivalence : double implication

🔑 Notions clés & Définitions

• Double implication : La double implication est un énoncé où deux implications sont combinées pour exprimer que deux propositions sont équivalentes.
• Équivalence logique : L’équivalence logique signifie que deux propositions ont exactement le même contenu de vérité, via une double implication.
• Implication $\\Rightarrow$ : Une implication $H \\cup {P} \\vdash Q$ formalise le fait que $Q$ se déduit de $H$ en supposant $P$.
• Quantificateur existentiel $\\exists$ : Le quantificateur existentiel $\\exists x,P(x)$ affirme qu’il existe au moins un élément du domaine rendant $P$ vraie.

📝 Points essentiels

• Pour utiliser une propriété existentielle $\\exists x,P(x)$, on peut introduire un témoin $a$ et remplacer par $P(a)$, à condition que $a$ ne soit pas une variable libre du contexte $H$.
• La règle d’élimination de l’existentiel s’écrit : de $H \\cup {\\exists x,P(x)}$ on obtient $Q$ dès qu’on sait déduire $Q$ de $H \\cup {P(a)}$ pour un $a$ quelconque du domaine.
• Le témoin $a$ doit être choisi comme élément arbitraire du domaine : on ne doit pas le lier à une information particulière du contexte.
• Attention à la réutilisation des lettres : ne pas confondre la variable muette $x$ du quantificateur avec une variable déjà utilisée comme témoin dans une preuve.
• En rédaction française, on peut expliciter le témoin par une phrase du type « il existe un élément $a$ tel que $P(a)$ » pour éviter les erreurs de variables.
• En Lean, l’implication $p \\to q$ se prouve typiquement en introduisant une hypothèse $h : p$ (tactique intro), ce qui transforme le but en $q$ ; c’est l’analogue de la règle d’introduction de $\\Rightarrow$.

💡 Astuce mémo

Existentiel = témoin : $\\exists x,P(x)$ donne un $a$ tel que $P(a)$, mais $a$ doit être « frais » (pas libre dans $H$).

📖 7. Négation : introduction, double négation et absurde

🔑 Notions clés & Définitions

• Négation logique : La négation logique exprime qu’une proposition n’est pas vraie, notée généralement par $\\neg p$.
• Double négation : La double négation est l’expression $\\neg\\neg p$, qui nie la négation de $p$.
• Principe d’absurde : Le raisonnement par l’absurde consiste à déduire une contradiction puis à conclure la proposition visée.
• Négation en Lean : En Lean, la négation se manipule via des tactiques qui transforment un but $\\neg p$ en une forme exploitable pour produire une contradiction.

📝 Points essentiels

• En Lean, pour transformer un but $q$ en un but $p$ quand on a une implication $h : p \\to q$, on utilise la tactique $apply\\ h$ (traduction du modus ponens).
• Si on a une hypothèse $hp : p$, on peut spécialiser $h : p \\to q$ avec $specialize\\ h\\ hp$ pour obtenir directement une preuve de $q$.
• Pour construire une conjonction $p \\land q$, la tactique $apply\\ And.intro$ ou $exact\\ And.intro$ génère deux sous-buts, un pour $p$ et un pour $q$.
• Pour extraire $p$ depuis $p \\land q$, on utilise $And.left$ (ou $exact\\ h.left$ si $h : p \\land q$ est déjà en contexte).
• Pour raisonner par cas sur une disjonction, on utilise $cases\\ h$ (ou $left/right$ via $Or.inl/Or.inr$) afin de créer des états séparés selon le cas retenu.

💡 Astuce mémo

Absurd→contradiction : pour $\\neg p$, vise une contradiction à partir de $p$ ; pour $\\neg\\neg p$, transforme $\\neg\\neg p$ en “si $\\neg p$ alors contradiction”, puis conclue $p$.

📖 8. Quantificateur universel : démonstration et condition

🔑 Notions clés & Définitions

• Quantificateur universel : Le quantificateur universel exprime que la propriété est vraie pour tout élément $x$ d’un type donné.
• Tactique cases : La tactique cases découpe une hypothèse inductive ou une équivalence en cas, en générant des sous-buts à prouver.
• Tactique constructor : La tactique constructor construit une preuve d’une conjonction ou d’une équivalence en générant les sous-buts nécessaires.
• Tactique rewrite : La tactique rewrite remplace un terme dans le but courant en utilisant une égalité ou une équivalence fournie.

📝 Points essentiels

• Pour une équivalence $p \\leftrightarrow q$, le symbole s’écrit $\\iff$ en Lean et la tactique la plus simple est constructor.
• Si le but est de la forme $p \\to q$, appliquer constructor génère deux sous-buts : $p \\to q$ et $q \\land p$.
• Si le contexte contient $h : p \\leftrightarrow q$, on peut obtenir une preuve de $p \\to q$ via $exact\\ h.mp$ (ou $exact\\ Iff.mp\\ h$).
• Si le contexte contient $h : p \\leftrightarrow q$, on peut obtenir une preuve de $q \\to p$ via $exact\\ h.mpr$.
• Si le contexte contient $h : \\forall x,\\ p\\ x \\leftrightarrow q\\ x$ et que le but est $p\\ a$, on peut le remplacer par $q\\ a$ avec rewrite\\ \[h\] (et inversement avec la flèche vers la gauche).
• Si le contexte contient $h : p \\land q \\leftrightarrow r$ (ou plus généralement une hypothèse de type équivalence), on peut la « découper » en deux implications $p \\to q$ et $q \\to p$ avec $rcases\ h\ with\ \langle hp, h

💡 Astuce mémo

mp = « modus ponens » (aller de $p$ vers $q$) ; mpr = « réciproque » (aller de $q$ vers $p$).

📖 9. Quantificateur existentiel : introduction et utilisation

🔑 Notions clés & Définitions

• Quantificateur existentiel : Quantificateur qui exprime qu’il existe au moins un élément satisfaisant une propriété, souvent noté $\\exists x, P(x)$.
• Tactique intro : Tactique Lean qui introduit une hypothèse dans le contexte quand le but a la forme attendue (implication ou quantification).
• Tactique apply : Tactique Lean qui transforme un but en utilisant une hypothèse déjà disponible, en instanciant si nécessaire.
• False : Proposition spéciale de Lean pour laquelle il ne peut pas exister de preuve, utilisée comme cible pour fermer un raisonnement par contradiction.

📝 Points essentiels

• En Lean, la négation $\\neg p$ se réécrit comme une implication $p \\to False$, ce qui relie la gestion de $\\neg$ à celle de $\\to$.
• Pour un but de type $\\neg p$, on peut utiliser $\\texttt{intro h}$ : la tactique ajoute $h : p$ au contexte et transforme le but en $False$.
• Réciproquement, si le but est $False$ et qu’on a une hypothèse $h : \\neg p$, alors $\\texttt{apply h}$ change le but en $p$.
• Pour clore un but de type $False$, les options sont : une hypothèse $h : False$ (fermeture directe), une hypothèse $h : \\neg q$ (réduction du but à $q$), ou une contradiction dans le contexte (ex. $q$ et $\\neg q$, ou une
• hypothèse impossible
• ex. $0 = 1$) via $\\texttt{contradiction}$.

💡 Astuce mémo

Négation = implication vers False : $\\neg p$ se traite comme $p \\to False$, donc $\\texttt{intro}$ donne $p$ et $\\texttt{apply}$ remonte depuis $\\neg p$ vers le but.

📖 10. Règles Lean : tactiques et correspondances

🔑 Notions clés & Définitions

• Instanciation d’une hypothèse universelle : Une instanciation universelle consiste à remplacer une hypothèse de la forme $h: \\forall x, e$ par $h,a$ en substituant $a$ à $x$ dans $e$.
• Tactique apply : La tactique apply utilise une hypothèse ou un théorème pour transformer le but courant en un sous-but correspondant à l’instance attendue.
• Spécialisation d’une hypothèse : La spécialisation remplace une hypothèse universelle $h: \\forall x, e$ par $h: e'$ où $e'$ est obtenu en substituant $a$ à $x$.
• Tactique exists : La tactique exists introduit un témoin $a$ pour un but de la forme $\\forall x, e$ en remplaçant $x$ par $a$ dans $e$.
• Tactique obtain : La tactique obtain extrait un objet $a$ et une hypothèse $h a: e'$ à partir d’une hypothèse universelle $h: \\forall x, e$.

📝 Points essentiels

• Pour une hypothèse $h: \\forall x, e$ avec $x$ variable libre dans $e$, instancier revient à substituer $a$ à $x$ dans $e$ pour obtenir une expression $e'$ de type $e'$.
• Si le but courant est une instance $e'$, la tactique apply peut clore le but en utilisant l’hypothèse $h$ correspondante.
• Lean infère souvent automatiquement l’expression à utiliser pour $a$ lors d’un apply, sans que l’utilisateur fournisse explicitement l’instance.
• On peut instancier une hypothèse universelle du contexte via specialize $h,a$ ou replace $h := h,a$, ce qui remplace $h: \\forall x, e$ par $h: e'$ dans le contexte.
• La tactique exists est la plus courante pour démontrer un but de la forme $\\forall x, e$ en remplaçant le but par $e'$ obtenu par substitution de $a$ à $x$.
• Dans des cas simples, le but $e'$ peut devenir clos automatiquement, par exemple si l’égalité obtenue est triviale (selon le contexte).

💡 Astuce mémo

Universel = substitution : $h: \\forall x, e$ devient $h,a$ en remplaçant $x$ par $a$ ; apply ferme quand le but est déjà l’instance attendue.

📖 11. Implication en Lean : intro, apply et specialize

🔑 Notions clés & Définitions

• Implication comme type fonctionnel : Une implication $p \\to q$ est traitée comme un type de fonction, et une preuve de $p \\to q$ comme une fonction qui transforme une preuve de $p$ en preuve de $q$.
• Tactique apply : La tactique apply utilise une hypothèse de type $p \\to q$ pour réduire un but $q$ en un nouveau but $p$.
• Tactique intro : La tactique intro introduit une hypothèse correspondant à une prémisse, typiquement pour passer d’un but $p \\to q$ à un but $q$ sous l’hypothèse $p$.
• Tactique specialize : La tactique specialize instancie un quantificateur universel en remplaçant la variable par un terme $a$, pour obtenir un but avec $P,a$.

📝 Points essentiels

• apply ne correspond pas toujours exactement aux règles de déduction naturelle : c’est une analogie qui peut changer le contexte plutôt que le but.
• Si vous avez $e : p$ et $h : p \\to q$, vous pouvez fermer un but $q$ en appliquant $h$ à $e$ (écriture du type exact h e).
• apply h transforme un but $q$ en un but $p$ lorsque $h : p \\to q$ est disponible.
• apply h sur un but False avec $h : ¬p$ permet de produire False à partir de $p$ (enchaînement via la forme logique de l’implication/contradiction).
• specialize h a transforme $h : \\forall x, P,x \\vdash q$ en une hypothèse $h : P,a \\vdash q$ en instanciant $x$ par $a$.
• Comparaison : apply vs règles de déduction naturelle — apply vise un but en utilisant une hypothèse, alors que les règles naturelles décrivent une transformation formelle du contexte et du but, sans coïncider terme à ter

💡 Astuce mémo

apply = « $p\\to q$ donne $q$ si je fournis $p$ » ; specialize = « $\\forall x$ devient $P,a$ »

📖 12. Conjonction en Lean : constructor et And.left

🔑 Notions clés & Définitions

• intro : Tactique qui introduit une hypothèse ou un quantificateur dans le contexte et réduit le but correspondant.
• apply : Tactique qui transforme le but en un nouveau but en utilisant une implication disponible, pour faire correspondre la conclusion attendue.
• contradiction : Tactique qui clôt une preuve dès qu’on a une contradiction dans le contexte, typiquement $False$ obtenu à partir de $p$ et $¬p$.
• Classical.not_not : Théorème prédéfini du module Classical donnant l’équivalence entre $¬¬q$ et $¬q → False$ via une forme de double négation.
• And.left : Fonction/projection qui extrait la partie gauche d’une conjonction $A ∧ B$.

📝 Points essentiels

• Dans une preuve par implications, on utilise souvent plusieurs $intro$ pour passer successivement de $(p → q) → (¬q → ¬p)$ à des buts plus simples.
• Pour montrer $¬q → ¬p$, on suppose $¬q$ puis on doit produire $¬p$, ce qui revient à prouver $p → False$.
• À partir de $p → q$ et de $p$, on déduit $q$ (modus ponens) puis on combine avec $¬q$ pour obtenir $False$.
• Dans la preuve de $(¬q → ¬p) → (p → q)$, après avoir introduit $hnqnp : ¬q → ¬p$, on suppose $p$ et il reste à prouver $q$.
• Quand on est bloqué pour obtenir $q$, on applique la double négation via $Classical.not_not.mp$ pour transformer le but en $¬¬q$ (équivalent à $¬q → False$).
• Une fois $¬q$ supposé, on obtient $¬p$ par modus ponens avec $hnqnp$, puis $p$ et $¬p$ donnent $False$ et la preuve se termine par $contradiction$.

💡 Astuce mémo

intro = « j’entre l’hypothèse », apply = « je réduis le but avec une implication », contradiction = « p et ¬p → False ».

⚠️ Pièges & confusions fréquents

1. Confondre règle de démonstration et règle d’utilisation : en ⇒i on ajoute P temporairement au contexte, alors qu’en ⇒e (modus ponens) on utilise P et P⇒Q pour obtenir Q.
2. Croire que H ` P signifie que P est vrai : c’est seulement “P est démontrissable à partir de H” (ce qui peut être vrai ou non).
3. En récurrence, oublier que le principe s’écrit comme une implication : il faut prouver ∀n∈N (Q(n) ⇒ Q(n+1)) pour obtenir ∀n∈N Q(n).
4. Pour ∀e, ne pas respecter la condition “x non libre dans H” lors de ∀i : sinon la règle ne s’applique pas telle quelle et il faut changer de variable.
5. Pour ∃e, réutiliser la mauvaise variable : le témoin a doit être “quelconque” (pas lié au contexte), et ne pas confondre la variable muette x du quantificateur avec une variable déjà utilisée.
6. En logique intuitionniste, croire que l’élimination de ¬ ou le raisonnement par l’absurde sont valides : le cours précise que ces règles ne marchent pas en intuitionniste.
7. En Lean, confondre apply et intro : intro correspond à une introduction (ajouter une hypothèse / entrer dans une implication), tandis que apply transforme le but en un sous-but via une hypothèse disponible.

✅ Checklist Examen

1. Savoir interpréter la notation H P : contexte H, but P, et rôle du turnstile en déduction naturelle et en Lean.
2. Distinguer pour chaque connecteur les règles “démonstration/introduction” vs “utilisation/élimination”, et relier cette distinction aux noms i/e (ou intro/elim en Lean).
3. Appliquer la règle Ax : fermer une preuve quand P apparaît déjà dans le contexte (aucune prémisse au-dessus de la barre).
4. Utiliser l’affaiblissement : de H Q déduire H ∪ {P} Q.
5. Pour ⇒ : démontrer P ⇒ Q via ⇒i (ajouter P au contexte), puis utiliser ⇒e (modus ponens) pour passer de P⇒Q et P à Q.
6. Pour la récurrence : écrire correctement le principe (∀n∈N, Q(n) ⇒ Q(n+1)) ⇒ ∀n∈N Q(n) et expliquer pourquoi il suffit de prouver la partie gauche.
7. Pour ∧ : démontrer P ∧ Q en séparant les preuves de P et de Q avec les mêmes hypothèses, puis utiliser ∧eg/∧ed (And.left/And.right) pour extraire.
8. Pour ∨ : démontrer P ∨ Q en choisissant P ou Q (∨ig/∨id), puis utiliser ∨e pour un raisonnement par cas (P⇒R et Q⇒R).
9. Pour ⇔ : démontrer P ⇔ Q en prouvant séparément P⇒Q et Q⇒P, puis utiliser ⇔ed/⇔er (Iff.mp/Iff.mpr) pour obtenir l’implication voulue.
10. Pour ¬ : démontrer ¬P en montrant que H ∪ {P} permet d’obtenir une contradiction (¬i), puis utiliser ¬e pour passer de ¬¬P à P (double négation).
11. Pour ∀ : démontrer ∀x P(x) avec ∀i sous la condition “x non libre dans H”, puis utiliser ∀e pour instancier à un élément a.
12. Pour ∃ : démontrer ∃x P(x) via un témoin a (∃i), puis utiliser ∃e en introduisant un a arbitraire et en prouvant le but Q à partir de P(a) (sans lier a au contexte).
13. En Lean : maîtriser intro/apply/specialize/exists/obtain/rcases/rewrite/contradiction et savoir associer chaque tactique à l’analogue de la règle de déduction naturelle correspondante.