Lean 3 - Propositions et Preuves

Navigation : ← Lean-02-Dependent-Types-Lean | Index | Lean-04-Quantifiers-Lean →

Introduction

Ce notebook explore la caractéristique la plus puissante de Lean : sa capacite a representer des propositions mathematiques comme des types et des preuves comme des termes. Cette correspondance, connue sous le nom d’isomorphisme de Curry-Howard, est le fondement de la vérification formelle.

Objectifs d’apprentissage

  1. Comprendre le type special Prop pour les propositions
  2. Maitriser l’isomorphisme de Curry-Howard (propositions = types, preuves = termes)
  3. Manipuler les connecteurs logiques : ->, And, Or, Not, Iff
  4. Construire des preuves par manipulation de termes
  5. Utiliser l’égalité et les preuves calculatoires avec calc
  6. Distinguer logique constructive et logique classique

Prerequis

  • Avoir complète les notebooks Lean-01-Setup-Lean-Python et Lean-02-Dependent-Types-Lean
  • Notions de base en logique propositionnelle

Duree estimée : 45-50 minutes

Plan de ce Notebook

L’isomorphisme de Curry-Howard

Le principe fondamental

Haskell Curry et William Howard ont independamment decouvert une correspondance profonde entre logique et programmation :

Logique Programmation (types)
Proposition Type
Preuve Terme (valeur) du type
Implication P -> Q Type fonction P -> Q
Conjonction P et Q Type produit P x Q
Disjonction P ou Q Type somme P + Q
Vrai Type Unit (un seul habitant)
Faux Type Empty (aucun habitant)

Consequence : Prouver une proposition revient a construire un terme du type correspondant. Si le type est habite (il existe un terme), la proposition est vraie.

## 1. Le Type Prop

1.1 Introduction a Prop

En Lean, Prop est un univers special qui contient les propositions - des enonces qui peuvent etre vrais ou faux. Contrairement a Type, les propositions ont une sémantique logique : ce qui compte n’est pas la forme de la preuve, mais son existence.

Pourquoi un univers Prop séparé de Type ?

Avant Lean, la plupart des langages ne distinguent pas valeur et proposition : un booléen est une valeur, une proposition est True/False. En Lean, la distinction est dans le type lui-même. Prop est l’univers des types habités par une preuve : True : Prop (habité par True.intro), p ∧ q : Prop (habité par ⟨hp, hq⟩), n < m : Prop (habité par un constructeur de preuve). Un objet de type Prop n’est pas une valeur qu’on calcule, c’est un objet mathématique dont on exhibe la preuve.

Cette séparation a trois conséquences pédagogiques que vous ressentirez dans tout le reste de la série Lean :

  1. Preuve = objet de première classe. Une preuve h : P est une valeur comme une autre : on peut la passer en argument, la stocker dans une let, la retourner. C’est l’isomorphisme de Curry-Howard en acte. Vous retrouverez cette idée dans Lean-12 (preuve de la formule de sensibilité de Huang, où la preuve de S(f, n, k) = 0 est un objet construit pas-à-pas) et dans Lean-14 (les (value, proof) paires sont des paires Nat × (n < m)).
  2. Réduction de preuves. Quand vous écrivez #reduce sur un Prop, le noyau calcule la preuve comme n’importe quel terme : True.intro ▸ True se réduit en True. C’est ce qui permet à #check de normaliser et à #rfl de trancher a = a. Lean-5 (tactiques rfl/decide/simp) automatise cette bêta-réduction.
  3. Extractionnalité : deux preuves du même Prop sont considérées égales par le noyau (propext), même si elles sont construites différemment. C’est pourquoi rfl tranche : il n’a pas besoin de comparer les arbres de syntaxe, juste de savoir qu’ils normalisent au même terme.

Le pont vers la partie haute : Prop est le véhicule de toutes les preuves de la série Lean. Lean-3 introduit la machinerie (intro/elim/constructeurs) ; Lean-4 ajoute les quantificateurs ∀/∃ ; Lean-5 fournit les tactiques qui automatisent ; Lean-12 (Huang) met tout en pratique sur une preuve. Si la notion de « preuve = objet de type Prop » est floue, relisez cette cellule avant d’aborder Lean-4.

-- Prop est l'univers des propositions
#check Prop          -- Prop : Type

-- Quelques propositions de base
#check True          -- True : Prop (proposition toujours vraie)
#check False         -- False : Prop (proposition toujours fausse)

-- Declarer des variables propositionnelles
-- Note: certaines variables peuvent etre non utilisees dans cette cellule
-- mais seront disponibles dans les cellules suivantes (chainage REPL)
variable (p q r : Prop)

#check p             -- p : Prop
#check p -> q        -- p -> q : Prop (implication)
-- Prop est l'univers des propositions
 Prop : Type
-- Quelques propositions de base
 True : Prop
 False : Prop
-- Declarer des variables propositionnelles
-- Note: certaines variables peuvent etre non utilisees dans cette cellule
-- mais seront disponibles dans les cellules suivantes (chainage REPL)
variable (p q r : Prop)
 p : Prop
 p → q : Prop
--% env 0
Raw input {"cmd": "-- Prop est l'univers des propositions\n#check Prop -- Prop : Type\n\n-- Quelques propositions de base\n#check True -- True : Prop (proposition toujours vraie)\n#check False -- False : Prop (proposition toujours fausse)\n\n-- Declarer des variables propositionnelles\n-- Note: certaines variables peuvent etre non utilisees dans cette cellule\n-- mais seront disponibles dans les cellules suivantes (chainage REPL)\nvariable (p q r : Prop)\n\n#check p -- p : Prop\n#check p -> q -- p -> q : Prop (implication)"}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Prop : Type"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "True : Prop"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "False : Prop"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 6}, "data": "p : Prop"}, {"severity": "info", "pos": {"line": 14, "column": 0}, "endPos": {"line": 14, "column": 6}, "data": "p → q : Prop"}], "env": 0}

1.2 Propositions vs Types

Aspect Prop Type
Sémantique Verite/Faussete Données/Calcul
Proof irrelevance Oui (toutes les preuves sont egales) Non
Usage Raisonnement logique Programmation
Extraction Effacee a la compilation Conservee

Prop vs Type — trois différences opérationnelles

Le tableau du notebook résume la séparation, mais trois points méritent d’être soulignés parce qu’ils déterminent ce que vous pouvez écrire :

  1. Habitants. Un Type est habité par des valeurs : Nat par 0, 1, 2, … ; Bool par true, false. Un Prop est habité par des preuves : True par True.intro, False par rien (preuve = Empty-élimination). Une fonction f : P → Q n’est pas un programme qui transforme une valeur P en une valeur Q ; c’est un objet qui, étant donné une preuve de P, construit une preuve de Q. C’est Curry-Howard, encore.
  2. Élimination. Une valeur de Nat peut être éliminée par rfl, #reduce, #norm_num, omega. Une preuve de Prop peut être éliminée par rfl (pour True/Iff/Eq), cases (pour And/Or/Exists), intro/apply/exact (pour les flèches). Tactiques spécifiques à Prop dans Lean-5 : assumption, trivial, contradiction, tauto.
  3. Réduction. Le noyau réduit les valeurs de Type (par bêta-réduction), les preuves de Prop (par les mêmes règles), et rien d’autre (les univers Sort u ne se réduisent pas). C’est pour ça que #reduce (1 + 2) donne 3 mais #reduce Type ne donne rien.

Le pont : la séparation Prop/Type devient cruciale dans Lean-12 (preuve de la formule de sensibilité), où l’on manipule simultanément des Nat (indices de sommes), des Fin (n+1) (types dépendants des indices), et des Prop (les bornes à prouver). Mélanger les niveaux = erreur de type.

-- True a une preuve triviale
#check True.intro    -- True.intro : True

-- False n'a pas de preuve (type vide)
-- False.elim permet d'en deduire n'importe quoi (ex falso quodlibet)
#check @False.elim   -- False.elim : {C : Sort u} -> False -> C

-- Exemple de theorem trivial
theorem trivial_true : True := True.intro
-- True a une preuve triviale
 True.intro : True
-- False n'a pas de preuve (type vide)
-- False.elim permet d'en deduire n'importe quoi (ex falso quodlibet)
 @False.elim : {C : Sort u_1} → False → C
-- Exemple de theorem trivial
theorem trivial_true : True := True.intro
--% env 1
Raw input {"cmd": "-- True a une preuve triviale\n#check True.intro -- True.intro : True\n\n-- False n'a pas de preuve (type vide)\n-- False.elim permet d'en deduire n'importe quoi (ex falso quodlibet)\n#check @False.elim -- False.elim : {C : Sort u} -> False -> C\n\n-- Exemple de theorem trivial\ntheorem trivial_true : True := True.intro", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "True.intro : True"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "@False.elim : {C : Sort u_1} → False → C"}], "env": 1}

## 2. L’Implication : Preuves comme Fonctions

2.1 L’implication P -> Q

En Lean, l’implication P -> Q est representee par le type fonction. Une preuve de P -> Q est une fonction qui transforme toute preuve de P en preuve de Q.

C’est l’essence de Curry-Howard : prouver une implication = programmer une fonction.

L’implication comme type flèche

La cellule de droite construit impl_refl : p → p par theorem ... := fun h => h. Trois choses à comprendre :

  1. Notation fun h => h. C’est la lambda-abstraction de Lean-2 (fun x => corps) appliquée à une preuve. La fonction prend une preuve h : p et retourne la même preuve comme preuve de p. C’est la fonction identité sur les preuves de p, et c’est la preuve la plus simple qu’une proposition s'implique elle-même.
  2. Pourquoi c’est une preuve valide. Le type p → p est (h : p) → p. Construire un terme de ce type = exhiber une fonction qui, pour toute preuve h : p, retourne une preuve de p. Ici on retourne h directement — trivialement correct.
  3. Variantes syntaxiques. Vous verrez d’autres formes dans le notebook : assume h, exact h (tactic-style) ; id (la fonction identité de Prelude) ; fun h => h (lambda-style, ce qu’on utilise ici). Les trois sont interchangeables pour le noyau.

Piège classique : croire que fun h => h est une démonstration « circulaire » et refuser de l’écrire. C’est valide parce que h est une hypothèse fournie, pas une conclusion à prouver — la preuve est h elle-même.

Le pont vers la partie haute : p → q est omniprésent. Lean-12 l’utilise 100+ fois dans la preuve de la formule de sensibilité ; Lean-14 l’utilise pour typer les prédicats (n : Nat) → (h : n > 0) → ... ; Lean-16b l’utilise pour typer les transitions du Game of Life. Maîtriser fun h => h est la brique de base.

-- Variables propositionnelles
variable (p q : Prop)

-- Théorème : p implique p (reflexivite)
-- La preuve est la fonction identite!
theorem impl_refl : p -> p :=
  fun hp : p => hp

#check impl_refl     -- impl_refl : p -> p

-- Théorème : p implique (q implique p)
-- C'est la fonction constante!
theorem impl_intro : p -> q -> p :=
  fun hp : p =>
    fun _hq : q => hp

#check impl_intro    -- impl_intro : p -> q -> p
-- Variables propositionnelles
variable (p q : Prop)
-- Theoreme : p implique p (reflexivite)
-- La preuve est la fonction identite!
theorem impl_refl : p -> p :=
  fun hp : p => hp
 impl_refl (p : Prop) : p → p
-- Theoreme : p implique (q implique p)
-- C'est la fonction constante!
theorem impl_intro : p -> q -> p :=
  fun hp : p =>
    fun _hq : q => hp
 impl_intro (p q : Prop) : p → q → p
--% env 2
Raw input {"cmd": "-- Variables propositionnelles\nvariable (p q : Prop)\n\n-- Theoreme : p implique p (reflexivite)\n-- La preuve est la fonction identite!\ntheorem impl_refl : p -> p :=\n fun hp : p => hp\n\n#check impl_refl -- impl_refl : p -> p\n\n-- Theoreme : p implique (q implique p)\n-- C'est la fonction constante!\ntheorem impl_intro : p -> q -> p :=\n fun hp : p =>\n fun _hq : q => hp\n\n#check impl_intro -- impl_intro : p -> q -> p", "env": 1}
Raw output {"messages": [{"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "impl_refl (p : Prop) : p → p"}, {"severity": "info", "pos": {"line": 17, "column": 0}, "endPos": {"line": 17, "column": 6}, "data": "impl_intro (p q : Prop) : p → q → p"}], "env": 2}

2.2 Transitivite de l’implication

Si P -> Q et Q -> R, alors P -> R. C’est la composition de fonctions!

Transitivité = composition de fonctions

impl_trans : (p → q) → (q → r) → p → r se prouve par fun hpq hqr hp => hqr (hpq hp). Décortiquons :

  • On prend trois arguments : hpq : p → q, hqr : q → r, et hp : p.
  • On applique hpq à hp → on obtient hpq hp : q (par bêta-réduction, on substitue hp dans le corps de hpq).
  • On applique hqr au résultat → on obtient hqr (hpq hp) : r.

C’est exactement la composition de fonctions (hqr ∘ hpq) hp. Mathématiquement : (p ⇒ q) ∧ (q ⇒ r) ⊢ (p ⇒ r) est la transitivité de l’implication. En Lean : c’est une fonction à trois arguments curryfiés.

L’isomorphisme de Curry-Howard en embuscade : « transitivité de l’implication » et « composition de fonctions » sont le même objet dans deux habillages différents. La curryfication rend les deux indistinguables syntaxiquement : impl_trans est (p → q) → (q → r) → p → r, et la composition de fonctions est ∀ {α β γ}, (β → γ) → (α → β) → (α → γ) avec α := p, β := q, γ := r.

Le pont : cette preuve est la base de toutes les chaînes d’implications dans la partie haute. Lean-12 (sensibilité) enchaine 5+ implications en cascade ; Lean-14 (Finiteness) utilise la transitivité pour borner des dérivées successives ; Lean-16b (Game of Life) utilise la transitivité pour prouver l’invariance de motifs. Le pattern f (g x) est universel.

Lire un théorème avant de le prouver

Avant de plonger dans la preuve de impl_trans, exerçons-nous à lire son statement. C’est un réflexe qui s’applique à tous les théorèmes Lean : statement d’abord, preuve ensuite.

Le statement : impl_trans : (p → q) → (q → r) → p → r

Décortiquons en 4 temps :

  1. Les paramètres implicites (entre {}) : aucun ici — toutes les propositions p, q, r ont été déclarées via variable (p q r : Prop) plus haut dans le notebook (cellule 6).
  2. Les paramètres explicites (entre ()) : hpq : p → q et hqr : q → r. Ce sont les hypothèses que la preuve peut utiliser.
  3. Le type de retour (après le : final) : p → r. C’est la conclusion — ce qu’on doit démontrer.
  4. Le nom du théorème : impl_trans est mnémonique — implication transitivity. Le nom EST la spécification (cf. Lean-6, où cette convention est centrale dans le catalogue Mathlib).

Reformulation en français : « Étant donné une preuve de p → q et une preuve de q → r, on doit construire une preuve de p → r ». La preuve est donc une fonction qui prend deux arguments et retourne la conclusion curryfiée.

Vérification de plausibilité : ce théorème est évident mathématiquement (transitivité de l’implication). Lean ne demande pas qu’on découvre la preuve, mais qu’on construise un terme du bon type. La curryfication → rend la construction entièrement mécanique ici : il suffit de composer les deux fonctions.

Cette grille de lecture — paramètres implicites, paramètres explicites, conclusion, nom — s’applique à tout théorème Lean 4. Les notebooks Lean-5 (tactiques) et Lean-6 (Mathlib) la réutilisent implicitement à chaque apply? / exact?.

variable (p q r : Prop)

-- Transitivite = composition de fonctions
theorem impl_trans (hpq : p -> q) (hqr : q -> r) : p -> r :=
  fun hp : p =>
    hqr (hpq hp)     -- Appliquer hpq a hp, puis hqr au résultat

-- Version avec application de fonction explicite
theorem impl_trans' (hpq : p -> q) (hqr : q -> r) : p -> r :=
  fun hp : p =>
    let hq : q := hpq hp    -- Obtenir preuve de q
    let hr : r := hqr hq    -- Obtenir preuve de r
    hr

#check @impl_trans   -- impl_trans : (p -> q) -> (q -> r) -> p -> r
variable (p q r : Prop)
-- Transitivite = composition de fonctions
theorem impl_trans (hpq : p -> q) (hqr : q -> r) : p -> r :=
  fun hp : p =>
    hqr (hpq hp)     -- Appliquer hpq a hp, puis hqr au resultat
-- Version avec application de fonction explicite
theorem impl_trans' (hpq : p -> q) (hqr : q -> r) : p -> r :=
  fun hp : p =>
    let hq : q := hpq hp    -- Obtenir preuve de q
    let hr : r := hqr hq    -- Obtenir preuve de r
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 impl_trans : ∀ (p q r : Prop), (p → q) → (q → r) → p → r
--% env 3
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Transitivite = composition de fonctions\ntheorem impl_trans (hpq : p -> q) (hqr : q -> r) : p -> r :=\n fun hp : p =>\n hqr (hpq hp) -- Appliquer hpq a hp, puis hqr au resultat\n\n-- Version avec application de fonction explicite\ntheorem impl_trans' (hpq : p -> q) (hqr : q -> r) : p -> r :=\n fun hp : p =>\n let hq : q := hpq hp -- Obtenir preuve de q\n let hr : r := hqr hq -- Obtenir preuve de r\n hr\n\n#check @impl_trans -- impl_trans : (p -> q) -> (q -> r) -> p -> r", "env": 2}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 13, "column": 5}, "endPos": {"line": 13, "column": 6}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 15, "column": 0}, "endPos": {"line": 15, "column": 6}, "data": "impl_trans : ∀ (p q r : Prop), (p → q) → (q → r) → p → r"}], "env": 3}

## 3. La Conjonction : And (et logique)

3.1 Définition de And

La conjonction P And Q (ou P /\ Q) est vraie si et seulement si P et Q sont toutes deux vraies. C’est un type produit : une preuve de P /\ Q contient a la fois une preuve de P et une preuve de Q.

Pourquoi And est un type produit pour les propositions

La cellule de droite fait #check And et #check @And.intro. Trois choses à retenir :

  1. And p q est p ∧ q. Notation Unicode : ∧ (U+2227). C’est le type des paires de preuves (hₚ : p, h_q : q). Le constructeur est And.intro : p → q → p ∧ q. Les projections sont And.left : p ∧ q → p et And.right : p ∧ q → q. Symétriquement, p × q (Prod de Lean-2) est habité par des valeurs ; p ∧ q (And) est habité par des preuves. Même forme, contenu différent.
  2. Curryfication. And p q : Prop, pas (p, q) → Prop. Cela permet de raisonner sur p ∧ q comme un type unique qu’on peut eliminer par cases h with | intro hp hq => ... (qui donne hp : p et hq : q comme hypothèses).
  3. Pourquoi theorem and_comm ... := And.intro (And.right h) (And.left h). Pour prouver q ∧ p depuis h : p ∧ q, on prend la droite (qui est : q) et on en fait la gauche de la nouvelle conjonction, et symétriquement. C’est la commutativité du Prod de Lean-2, transposée aux preuves.

Le pont vers la partie haute : And est utilisé partout. Lean-12 (Huang) accumule des conjonctions de conditions sur les sommes partielles ; Lean-14 (Finiteness) les utilise pour borner les dérivées partielles conjointes ; Lean-16b (Game of Life) les utilise pour spécifier des conditions de bordure. La preuve de commutativité que vous voyez ici est la brique de ces raisonnements.

variable (p q : Prop)

-- And est un type produit pour les propositions
#check And           -- And : Prop -> Prop -> Prop
#check p /\ q        -- p /\ q : Prop (notation pour And p q)

-- Constructeur : And.intro combine deux preuves
#check @And.intro    -- And.intro : p -> q -> p /\ q

-- Destructeurs : And.left et And.right extraient les composantes
#check @And.left     -- And.left : p /\ q -> p
#check @And.right    -- And.right : p /\ q -> q
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- And est un type produit pour les propositions
 And (a b : Prop) : Prop
 p ∧ q : Prop
-- Constructeur : And.intro combine deux preuves
 @And.intro : ∀ {a b : Prop}, a → b → a ∧ b
-- Destructeurs : And.left et And.right extraient les composantes
 @And.left : ∀ {a b : Prop}, a ∧ b → a
 @And.right : ∀ {a b : Prop}, a ∧ b → b
--% env 4
Raw input {"cmd": "variable (p q : Prop)\n\n-- And est un type produit pour les propositions\n#check And -- And : Prop -> Prop -> Prop\n#check p /\\ q -- p /\\ q : Prop (notation pour And p q)\n\n-- Constructeur : And.intro combine deux preuves\n#check @And.intro -- And.intro : p -> q -> p /\\ q\n\n-- Destructeurs : And.left et And.right extraient les composantes\n#check @And.left -- And.left : p /\\ q -> p\n#check @And.right -- And.right : p /\\ q -> q", "env": 3}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "And (a b : Prop) : Prop"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "p ∧ q : Prop"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "@And.intro : ∀ {a b : Prop}, a → b → a ∧ b"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "@And.left : ∀ {a b : Prop}, a ∧ b → a"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "@And.right : ∀ {a b : Prop}, a ∧ b → b"}], "env": 4}

3.2 Preuves avec la conjonction

Pour prouver une conjonction P /\ Q, on doit fournir des preuves des deux parties separement. Pour l’utiliser, on peut extraire chaque partie avec .left et .right.

Pattern d’introduction : And.intro hp hq ou ⟨hp, hq⟩ Pattern d’élimination : h.left et h.right

And.intro et And.elim — symétrie introduction/élimination

La cellule de droite montre deux formes de preuve : - theorem and_intro_example (hp : p) (hq : q) : p ∧ q := And.intro hp hq — on fournit les deux preuves, And.intro les combine. - L’élimination se fait par cases h with | intro hp hq => ... (Lean-4 tactic-style) qui produit deux hypothèses hp : p et hq : q.

Pourquoi deux noms pour And et ∧ : ∧ est la notation infixe (Unicode U+2227) pour And. Lean supporte les deux interchangeablement — vous pouvez écrire p ∧ q ou And p q au choix. Dans le code des proofs Mathlib, ∧ est préféré pour la lisibilité. Dans les .lean compilés, c’est And partout.

Variantes utiles : - ⟨hp, hq⟩ est la notation anonyme pour And.intro hp hq (sugar syntaxique). - h.left et h.right projettent comme pour Prod, mais attention : h.left est une preuve, pas une valeur. - cases h with | intro hp hq => ... est la forme tactic-style (Lean-5 introduit les tactiques).

Le pont : And est la conjonction dans Lean-3 ; Lean-4 l’étend avec les quantificateurs (∀ x, P x ∧ Q x) ; Lean-12 (Huang) l’utilise intensivement dans les sommes partielles. Le pattern cases h with | intro hp hq => ... (Lean-4 tactic-style) est universel — vous l’utiliserez sur chaque conjonction.

variable (p q : Prop)

-- Introduction de la conjonction
theorem and_intro_example (hp : p) (hq : q) : p /\ q :=
  And.intro hp hq

-- Syntaxe avec chevrons (angle brackets)
theorem and_intro_example' (hp : p) (hq : q) : p /\ q :=
  ⟨hp, hq⟩           -- Equivalent a And.intro

-- Élimination : extraire les composantes
theorem and_left_example (hpq : p /\ q) : p :=
  hpq.left           -- Equivalent a And.left hpq

theorem and_right_example (hpq : p /\ q) : q :=
  hpq.right

-- Commutativite de And (notre propre version pour eviter conflit de nom)
theorem and_comm_demo : p /\ q -> q /\ p :=
  fun hpq => ⟨hpq.right, hpq.left⟩
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- Introduction de la conjonction
theorem and_intro_example (hp : p) (hq : q) : p /\ q :=
  And.intro hp hq
-- Syntaxe avec chevrons (angle brackets)
theorem and_intro_example' (hp : p) (hq : q) : p /\ q :=
  ⟨hp, hq⟩           -- Equivalent a And.intro
-- Elimination : extraire les composantes
theorem and_left_example (hpq : p /\ q) : p :=
  hpq.left           -- Equivalent a And.left hpq
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  hpq.right
-- Commutativite de And (notre propre version pour eviter conflit de nom)
theorem and_comm_demo : p /\ q -> q /\ p :=
  fun hpq => ⟨hpq.right, hpq.left⟩
--% env 5
Raw input {"cmd": "variable (p q : Prop)\n\n-- Introduction de la conjonction\ntheorem and_intro_example (hp : p) (hq : q) : p /\\ q :=\n And.intro hp hq\n\n-- Syntaxe avec chevrons (angle brackets)\ntheorem and_intro_example' (hp : p) (hq : q) : p /\\ q :=\n \u27e8hp, hq\u27e9 -- Equivalent a And.intro\n\n-- Elimination : extraire les composantes\ntheorem and_left_example (hpq : p /\\ q) : p :=\n hpq.left -- Equivalent a And.left hpq\n\ntheorem and_right_example (hpq : p /\\ q) : q :=\n hpq.right\n\n-- Commutativite de And (notre propre version pour eviter conflit de nom)\ntheorem and_comm_demo : p /\\ q -> q /\\ p :=\n fun hpq => \u27e8hpq.right, hpq.left\u27e9", "env": 4}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 15, "column": 19}, "endPos": {"line": 15, "column": 20}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 15, "column": 21}, "endPos": {"line": 15, "column": 22}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 15, "column": 23}, "endPos": {"line": 15, "column": 24}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 5}

3.3 Propriétés de la conjonction

La conjonction possede des propriétés algébriques importantes qui se prouvent en manipulant les composantes :

  • Commutativite : p /\ q <-> q /\ p
  • Associativite : (p /\ q) /\ r <-> p /\ (q /\ r)
  • Idempotence : p /\ p <-> p
  • Absorption : p /\ True <-> p

Propriétés algébriques de la conjonction

La cellule de droite prouve l’associativité de And : (p ∧ q) ∧ r ↔︎ p ∧ (q ∧ r). Décortiquons :

  • Sens direct (→) : on a h : (p ∧ q) ∧ r. On doit construire p ∧ (q ∧ r). Par And.intro : (And.left (And.left h)) pour le côté gauche (p), et And.intro (And.right (And.left h)) (And.right h) pour le côté droit (q ∧ r). C’est une réorganisation structurelle de paires imbriquées.
  • Sens réciproque (←) : symétrique.

Pourquoi cette preuve est instructive : elle illustre le pattern « reconstruction explicite par And.intro ». C’est verbeux mais mécaniquement correct. Lean-5 fournit tauto qui prouve ce genre de chose automatiquement (tauto tranche toutes les tautologies propositionnelles en logique intuitionniste). Apprendre à écrire ces preuves à la main vous donne l’intuition de ce que tauto fait pour vous.

Associativité + commutativité + élément neutre (True.intro : True ∧ p ↔︎ p) font de ∧ un monoïde commutatif sur les propositions. Mathlib capitalise dessus : And.semigroup, And.comm_monoid, etc.

Le pont vers la partie haute : associativité et commutativité sont utilisées dans Lean-14 (Finiteness) pour réarranger les dérivées partielles d’ordre multiple ; Lean-16b (Game of Life) les utilise pour raisonner sur les invariants spatiaux ; Lean-12 (Huang) les utilise pour réorganiser les sommes partielles. Ces preuves « scolaires » sont les briques des preuves sérieuses.

variable (p q r : Prop)

-- Associativite (version demo, la bibliotheque standard définit deja and_assoc)
theorem and_assoc_demo : (p /\ q) /\ r <-> p /\ (q /\ r) :=
  ⟨fun h => ⟨h.left.left, ⟨h.left.right, h.right⟩⟩,
   fun h => ⟨⟨h.left, h.right.left⟩, h.right.right⟩⟩

-- Distributivite sur l'implication
theorem and_impl_distrib : (p /\ q -> r) <-> (p -> q -> r) :=
  ⟨fun h hp hq => h ⟨hp, hq⟩,
   fun h hpq => h hpq.left hpq.right⟩
variable (p q r : Prop)
-- Associativite (version demo, la bibliotheque standard definit deja and_assoc)
theorem and_assoc_demo : (p /\ q) /\ r <-> p /\ (q /\ r) :=
  ⟨fun h => ⟨h.left.left, ⟨h.left.right, h.right⟩⟩,
   fun h => ⟨⟨h.left, h.right.left⟩, h.right.right⟩⟩
-- Distributivite sur l'implication
theorem and_impl_distrib : (p /\ q -> r) <-> (p -> q -> r) :=
  ⟨fun h hp hq => h ⟨hp, hq⟩,
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
--% env 6
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Associativite (version demo, la bibliotheque standard definit deja and_assoc)\ntheorem and_assoc_demo : (p /\\ q) /\\ r <-> p /\\ (q /\\ r) :=\n \u27e8fun h => \u27e8h.left.left, \u27e8h.left.right, h.right\u27e9\u27e9,\n fun h => \u27e8\u27e8h.left, h.right.left\u27e9, h.right.right\u27e9\u27e9\n\n-- Distributivite sur l'implication\ntheorem and_impl_distrib : (p /\\ q -> r) <-> (p -> q -> r) :=\n \u27e8fun h hp hq => h \u27e8hp, hq\u27e9,\n fun h hpq => h hpq.left hpq.right\u27e9", "env": 5}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 11, "column": 16}, "endPos": {"line": 11, "column": 17}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 11, "column": 18}, "endPos": {"line": 11, "column": 19}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 11, "column": 20}, "endPos": {"line": 11, "column": 21}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 6}

## 4. La Disjonction : Or (ou logique)

4.1 Définition de Or

La disjonction P Or Q (ou P \/ Q) est vraie si au moins l’une des deux propositions est vraie. C’est un type somme : une preuve de P \/ Q est soit une preuve de P, soit une preuve de Q.

Or comme somme pour les propositions

La cellule de droite fait #check Or et #check @Or.inl. Trois choses à retenir :

  1. Or p q est p ∨ q. Notation Unicode : ∨ (U+2228). C’est le type des témoins : soit Or.inl hp : p ∨ q (témoin à gauche = on a une preuve de p), soit Or.inr hq : p ∨ q (témoin à droite = on a une preuve de q). Notez la symétrie avec Sum de Lean-2 (somme de valeurs) : Or est la somme de preuves.
  2. Élimination par cases. Pour utiliser une preuve h : p ∨ q, on fait cases h with | inl hp => ... | inr hq => .... Le motif force à considérer les deux cas : soit on est dans le cas gauche (avec hp : p comme nouvelle hypothèse), soit dans le cas droit (avec hq : q). C’est l’analyse par cas sur les Or.
  3. Constructeurs inl/inr. Or.inl : p → p ∨ q (témoin gauche) et Or.inr : q → p ∨ q (témoin droit). Notation sugar : ⟨Or.inl, hp⟩ ou Or.inl hp.

Pourquoi deux constructeurs : on ne peut pas prouver p ∨ q sans savoir laquelle des deux est vraie. Or.inl exige une preuve de p ; Or.inr exige une preuve de q. On ne peut pas écrire Or.intro car il n’y a pas de « tierce voie » en logique intuitionniste.

Le pont vers la partie haute : Or est crucial dans Lean-14 (Finiteness) où les dérivées partielles se ramifient ; Lean-16b (Game of Life) où l’état suivant est une disjonction de configurations possibles ; Lean-3 (De Morgan classique, section 9) où la disjonction devient ¬¬p → p via Classical.em. Le pattern cases h with | inl | inr => ... est universel.

variable (p q : Prop)

#check Or            -- Or : Prop -> Prop -> Prop
#check p \/ q        -- p \/ q : Prop

-- Deux constructeurs : Or.inl et Or.inr (left et right)
#check @Or.inl       -- Or.inl : p -> p \/ q
#check @Or.inr       -- Or.inr : q -> p \/ q

-- Élimination : Or.elim (analyse par cas)
#check @Or.elim      -- Or.elim : p \/ q -> (p -> r) -> (q -> r) -> r
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 Or (a b : Prop) : Prop
 p ∨ q : Prop
-- Deux constructeurs : Or.inl et Or.inr (left et right)
 @Or.inl : ∀ {a b : Prop}, a → a ∨ b
 @Or.inr : ∀ {a b : Prop}, b → a ∨ b
-- Elimination : Or.elim (analyse par cas)
 @Or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
--% env 7
Raw input {"cmd": "variable (p q : Prop)\n\n#check Or -- Or : Prop -> Prop -> Prop\n#check p \\/ q -- p \\/ q : Prop\n\n-- Deux constructeurs : Or.inl et Or.inr (left et right)\n#check @Or.inl -- Or.inl : p -> p \\/ q\n#check @Or.inr -- Or.inr : q -> p \\/ q\n\n-- Elimination : Or.elim (analyse par cas)\n#check @Or.elim -- Or.elim : p \\/ q -> (p -> r) -> (q -> r) -> r", "env": 6}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Or (a b : Prop) : Prop"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "p ∨ q : Prop"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "@Or.inl : ∀ {a b : Prop}, a → a ∨ b"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "@Or.inr : ∀ {a b : Prop}, b → a ∨ b"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "@Or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c"}], "env": 7}

4.2 Preuves avec la disjonction

Pour prouver une disjonction P \/ Q, il suffit de prouver l’une des deux parties. Pour l’utiliser, on doit traiter les deux cas possibles (analyse par cas).

Pattern d’introduction : Or.inl hp (gauche) ou Or.inr hq (droite) Pattern d’élimination : match h with | Or.inl hp => ... | Or.inr hq => ...

Or.inl, Or.inr et l’élimination par cas

La cellule de droite prouve plusieurs propriétés : - or_intro_left : p → p ∨ q (témoin gauche). - or_intro_right : q → p ∨ q (témoin droit). - L’élimination se fait par cases h with | inl hp => ... | inr hq => ... (Lean-4 tactic-style) qui force l’analyse par cas.

Symétrie introduction/élimination : - Introduction : Or.inl hp / Or.inr hq — on choisit le côté en exhibant une preuve. - Élimination : cases h with | inl hp => ... | inr hq => ... — le contexte force à traiter les deux cas.

Pourquoi Or.intro n’existe pas : parce qu’il n’y a pas de « tierce voie ». Si on veut prouver p ∨ q, on doit prouver p (alors Or.inl hp) OU prouver q (alors Or.inr hq). C’est la différence majeure avec And où And.intro combine deux preuves existantes.

Notation pratique : cases h with | inl hp => ... | inr hq => ... est la forme tactic-style (Lean-4). En lambda-style, on peut écrire Or.elim h : (p → r) → (q → r) → p ∨ q → r — une fonction à trois arguments qui traite les deux cas.

Le pont : cette asymétrie introduction/élimination est la même que dans Lean-3 (De Morgan, section 9) : prouver p ∨ ¬p (le tiers exclu, LEM) n’est pas possible en logique intuitionniste — il faut savoir lequel des deux cas est vrai, ce que la logique intuitionniste refuse. En classique, p ∨ ¬p se prouve trivialement par Classical.em p. À l’inverse, ¬¬(p ∨ ¬p) est prouvable intuitionnistiquement (LEM-stability) : si ¬(p ∨ ¬p), alors ¬p ∧ ¬¬p, absurde. Lean-12 (Huang) ne raisonne pas sur les disjonctions directement (ses preuves sont des sommes de conjonctions), mais Lean-14 (Finiteness) les utilise abondamment.

variable (p q r : Prop)

-- Introduction a gauche
theorem or_intro_left (hp : p) : p \/ q :=
  Or.inl hp

-- Introduction a droite
theorem or_intro_right (hq : q) : p \/ q :=
  Or.inr hq

-- Élimination : analyser les deux cas
theorem or_elim_example (hpq : p \/ q) (hpr : p -> r) (hqr : q -> r) : r :=
  Or.elim hpq hpr hqr

-- Version avec match (plus lisible)
theorem or_elim_match (hpq : p \/ q) (hpr : p -> r) (hqr : q -> r) : r :=
  match hpq with
  | Or.inl hp => hpr hp
  | Or.inr hq => hqr hq

-- Commutativite de Or (version demo)
theorem or_comm_demo : p \/ q -> q \/ p :=
  fun hpq => match hpq with
    | Or.inl hp => Or.inr hp
    | Or.inr hq => Or.inl hq
variable (p q r : Prop)
-- Introduction a gauche
theorem or_intro_left (hp : p) : p \/ q :=
  Or.inl hp
-- Introduction a droite
theorem or_intro_right (hq : q) : p \/ q :=
  Or.inr hq
-- Elimination : analyser les deux cas
theorem or_elim_example (hpq : p \/ q) (hpr : p -> r) (hqr : q -> r) : r :=
  Or.elim hpq hpr hqr
-- Version avec match (plus lisible)
theorem or_elim_match (hpq : p \/ q) (hpr : p -> r) (hqr : q -> r) : r :=
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  | Or.inl hp => hpr hp
  | Or.inr hq => hqr hq
-- Commutativite de Or (version demo)
theorem or_comm_demo : p \/ q -> q \/ p :=
  fun hpq => match hpq with
    | Or.inl hp => Or.inr hp
    | Or.inr hq => Or.inl hq
--% env 8
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Introduction a gauche\ntheorem or_intro_left (hp : p) : p \\/ q :=\n Or.inl hp\n\n-- Introduction a droite\ntheorem or_intro_right (hq : q) : p \\/ q :=\n Or.inr hq\n\n-- Elimination : analyser les deux cas\ntheorem or_elim_example (hpq : p \\/ q) (hpr : p -> r) (hqr : q -> r) : r :=\n Or.elim hpq hpr hqr\n\n-- Version avec match (plus lisible)\ntheorem or_elim_match (hpq : p \\/ q) (hpr : p -> r) (hqr : q -> r) : r :=\n match hpq with\n | Or.inl hp => hpr hp\n | Or.inr hq => hqr hq\n\n-- Commutativite de Or (version demo)\ntheorem or_comm_demo : p \\/ q -> q \\/ p :=\n fun hpq => match hpq with\n | Or.inl hp => Or.inr hp\n | Or.inr hq => Or.inl hq", "env": 7}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 17, "column": 5}, "endPos": {"line": 17, "column": 6}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 17, "column": 9}, "endPos": {"line": 17, "column": 10}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 8}

## 5. La Negation : Not

5.1 Définition de Not

La negation Not P (ou \neg P) est définie comme P -> False. Intuitivement : si on suppose P, on arrive a une contradiction.

Négation = implication vers False

Not p est défini comme p → False. C’est-à-dire : « p est faux » = « de p on peut dériver une contradiction ». Trois choses à comprendre :

  1. Notation ¬p. C’est du sugar pour Not p. Le caractère ¬ est U+00AC. Notez la différence avec ~p (qui n’existe pas comme notation Lean — c’est une erreur courante des débutants qui mélangent Coq et Lean).
  2. Pourquoi cette définition. False est le Prop qui n’a aucun habitant (pas de constructeur, pas de preuve possible). Donc p → False est le type des fonctions qui, étant donné une preuve de p, dérivent une preuve de False. Une telle fonction exhibe le fait que p est contradictoire. C’est Curry-Howard encore : la négation est une fonction, pas une valeur.
  3. Variante Unicode ¬ vs ASCII. Vous verrez Not p, ¬p, (p → False) interchangeablement. Lean accepte les trois. Mathlib préfère ¬p.

Piège classique : croire que ¬p est « la valeur booléenne false ». Non : ¬p est un type (de preuves de l’absurdité). Il n’a pas de valeur « false » comme Bool ; il a pour habitants les fonctions qui dérivent False.

Le pont : la négation est cruciale dans Lean-14 (Finiteness, où les dérivées partielles sont strictement positives) ; Lean-16b (Game of Life, où la non-périodicité est une négation) ; Lean-12 (Huang, où les conditions de non-trivialité sont des négations). Le pattern assume h : p, ... False.elim ... est universel — c’est la preuve par l’absurde.

variable (p : Prop)

#check Not           -- Not : Prop -> Prop
#check ¬p            -- ¬p : Prop (equivalent a p -> False)

-- Définition de Not
#print Not           -- def Not (a : Prop) : Prop := a -> False

-- Prouver une negation = construire une fonction vers False
theorem not_false_demo : ¬False :=
  fun h : False => h   -- La preuve de False est elle-meme

-- Ex falso quodlibet : de False on deduit tout
theorem false_elim_example (h : False) : p :=
  False.elim h
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 Not (a : Prop) : Prop
 ¬p : Prop
-- Definition de Not
 def Not : Prop → Prop :=
fun a => a → False
-- Prouver une negation = construire une fonction vers False
theorem not_false_demo : ¬False :=
  fun h : False => h   -- La preuve de False est elle-meme
-- Ex falso quodlibet : de False on deduit tout
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  False.elim h
--% env 9
Raw input {"cmd": "variable (p : Prop)\n\n#check Not -- Not : Prop -> Prop\n#check \u00acp -- \u00acp : Prop (equivalent a p -> False)\n\n-- Definition de Not\n#print Not -- def Not (a : Prop) : Prop := a -> False\n\n-- Prouver une negation = construire une fonction vers False\ntheorem not_false_demo : \u00acFalse :=\n fun h : False => h -- La preuve de False est elle-meme\n\n-- Ex falso quodlibet : de False on deduit tout\ntheorem false_elim_example (h : False) : p :=\n False.elim h", "env": 8}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 12}, "endPos": {"line": 1, "column": 13}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Not (a : Prop) : Prop"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "¬p : Prop"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "def Not : Prop → Prop :=\nfun a => a → False"}, {"severity": "warning", "pos": {"line": 14, "column": 24}, "endPos": {"line": 14, "column": 25}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 9}

5.2 Contradiction et absurdite

La contradiction est l’outil principal pour prouver des negations. Si on peut deduire False d’une hypothese, cette hypothese est fausse.

Principe cle : absurd hp hnp - de p et ¬p on deduit n’importe quoi (ex falso quodlibet) Modus tollens : de p -> q et ¬q, on deduit ¬p

Modus tollens et preuve par l’absurde

La cellule de droite prouve deux résultats emblématiques : - modus_tollens : (p → q) → ¬q → ¬p — contraposée sous forme curryfiée. - absurdity : p → ¬p → False — une preuve et sa négation mènent à False.

Décortiquons modus_tollens : on a hpq : p → q et hnq : ¬q. On doit construire ¬p = p → False. On prend h : p et on compose : hnq (hpq h) : False. C’est la contraposée : p ⇒ q et ¬q implique ¬p.

Décortiquons absurdity : on a hp : p et hnp : ¬p. Par application : hnp hp : False. C’est la forme la plus simple de preuve par l’absurde : si on a p et ¬p, on a False.

Pourquoi False est spécial. False.elim : False → C (pour tout C) — de False on peut tout dériver (ex falso quodlibet). C’est la base de toutes les preuves par l’absurde : on dérive False, puis on False.elim pour obtenir la conclusion.

Le pont : modus_tollens est la base de toutes les preuves par contraposée. Lean-14 (Finiteness) l’utilise pour borner les dérivées ; Lean-16b (Game of Life) l’utilise pour prouver des invariants par négation. Le pattern False.elim (h ...) est universel.

variable (p q : Prop)

-- Modus tollens : (p -> q) -> ¬q -> ¬p
theorem modus_tollens (hpq : p -> q) (hnq : ¬q) : ¬p :=
  fun hp : p =>
    let hq : q := hpq hp   -- On obtient q
    hnq hq                  -- Contradiction avec ¬q

-- Non-contradiction : ¬(p /\ ¬p)
theorem non_contradiction : ¬(p /\ ¬p) :=
  fun h : p /\ ¬p =>
    h.right h.left   -- ¬p applique a p donne False

-- absurd : de p et ¬p on deduit tout
#check @absurd       -- absurd : {a : Prop} -> {b : Sort v} -> a -> ¬a -> b

theorem absurd_example (hp : p) (hnp : ¬p) : q :=
  absurd hp hnp
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- Modus tollens : (p -> q) -> ¬q -> ¬p
theorem modus_tollens (hpq : p -> q) (hnq : ¬q) : ¬p :=
  fun hp : p =>
    let hq : q := hpq hp   -- On obtient q
    hnq hq                  -- Contradiction avec ¬q
-- Non-contradiction : ¬(p /\ ¬p)
theorem non_contradiction : ¬(p /\ ¬p) :=
  fun h : p /\ ¬p =>
    h.right h.left   -- ¬p applique a p donne False
-- absurd : de p et ¬p on deduit tout
 @absurd : {a : Prop} → {b : Sort u_1} → a → ¬a → b
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
theorem absurd_example (hp : p) (hnp : ¬p) : q :=
  absurd hp hnp
--% env 10
Raw input {"cmd": "variable (p q : Prop)\n\n-- Modus tollens : (p -> q) -> \u00acq -> \u00acp\ntheorem modus_tollens (hpq : p -> q) (hnq : \u00acq) : \u00acp :=\n fun hp : p =>\n let hq : q := hpq hp -- On obtient q\n hnq hq -- Contradiction avec \u00acq\n\n-- Non-contradiction : \u00ac(p /\\ \u00acp)\ntheorem non_contradiction : \u00ac(p /\\ \u00acp) :=\n fun h : p /\\ \u00acp =>\n h.right h.left -- \u00acp applique a p donne False\n\n-- absurd : de p et \u00acp on deduit tout\n#check @absurd -- absurd : {a : Prop} -> {b : Sort v} -> a -> \u00aca -> b\n\ntheorem absurd_example (hp : p) (hnp : \u00acp) : q :=\n absurd hp hnp", "env": 9}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 15, "column": 0}, "endPos": {"line": 15, "column": 6}, "data": "@absurd : {a : Prop} → {b : Sort u_1} → a → ¬a → b"}, {"severity": "warning", "pos": {"line": 15, "column": 10}, "endPos": {"line": 15, "column": 11}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 15, "column": 12}, "endPos": {"line": 15, "column": 13}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 10}

Exercice intermediaire : De Morgan (direction constructive)

Avant de passer aux exercices finaux, voici un exercice pour vérifier votre comprehension de la negation et de la disjonction.

Objectif : Prouver la direction constructive de la première loi de De Morgan : ¬(p \/ q) -> ¬p /\ ¬q

Indices : 1. Rappelez-vous que ¬P est défini comme P -> False 2. Pour prouver une conjonction ¬p /\ ¬q, utilisez la syntaxe ⟨_, _⟩ 3. Pour chaque composante (¬p puis ¬q), construisez p \/ q avec Or.inl ou Or.inr et appliquez l’hypothese ¬(p \/ q)

Exercice intermédiaire : De Morgan (direction constructive)

Avant de plonger dans la logique classique (section 9), cet exercice vous demande de prouver une seule direction de De Morgan en logique constructive pure :

¬(p ∨ q) → ¬p ∧ ¬q  -- constructif

Pourquoi c’est faisable et sans piège. Vous avez hnpq : ¬(p ∨ q) et vous devez construire ¬p ∧ ¬q. Vous prouvez ¬p directement (supposez p, on a Or.inl p : p ∨ q, contredisant hnpq). Symétriquement pour ¬q. Pas besoin de Classical — la preuve est constructive.

Indice : utilisez hnpq : ¬(p ∨ q) directement. Pour prouver ¬p, supposez hp : p, exhibez Or.inl hp : p ∨ q, appliquez hnpq pour obtenir False. Pareil pour ¬q avec Or.inr. Aucune hypothèse classique requise.

Ancrage Mathlib : la loi ¬(p ∨ q) ↔︎ ¬p ∧ ¬q que vous prouverez ici s’appelle not_or dans Mathlib (constructive, sans hypothèse). Sa sœur ¬(p ∧ q) ↔︎ ¬p ∨ ¬q s’appelle not_and_or et exige Decidable / Classical.em — c’est le contenu de la cellule 43. La distinction est non symétrique en intuitionniste : c’est précisément ce que la cellule 45 démontre.

Le pont : cet exercice est la frontière entre logique constructive et classique. Lean-3 (section 9) l’aborde avec Classical.em ; Lean-12 (Huang) l’utilise dans certaines étapes mais jamais de façon centrale ; Lean-14 (Finiteness) reste en constructif strict. Maîtriser la distinction = comprendre pourquoi Lean vous force parfois à Classical.

variable (p q : Prop)

-- Exercice intermediaire : De Morgan (direction constructive)
-- TODO étudiant : prouver ¬(p \/ q) -> ¬p /\ ¬q
-- Indice 1 : ¬P est defini comme P -> False
-- Indice 2 : utiliser ⟨_, _⟩ pour la conjonction
-- Indice 3 : construire p \/ q avec Or.inl ou Or.inr pour obtenir False
theorem de_morgan_constructive : ¬(p \/ q) -> ¬p /\ ¬q :=
  sorry
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- Exercice intermediaire : De Morgan (direction constructive)
-- TODO etudiant : prouver ¬(p \/ q) -> ¬p /\ ¬q
-- Indice 1 : ¬P est defini comme P -> False
-- Indice 2 : utiliser ⟨_, _⟩ pour la conjonction
-- Indice 3 : construire p \/ q avec Or.inl ou Or.inr pour obtenir False
🟨 declaration uses `sorry`
  sorry
--% env 11
--% prove 0
Raw input {"cmd": "variable (p q : Prop)\n\n-- Exercice intermediaire : De Morgan (direction constructive)\n-- TODO etudiant : prouver \u00ac(p \\/ q) -> \u00acp /\\ \u00acq\n-- Indice 1 : \u00acP est defini comme P -> False\n-- Indice 2 : utiliser \u27e8_, _\u27e9 pour la conjonction\n-- Indice 3 : construire p \\/ q avec Or.inl ou Or.inr pour obtenir False\ntheorem de_morgan_constructive : \u00ac(p \\/ q) -> \u00acp /\\ \u00acq :=\n sorry", "env": 10}
Raw output {"sorries": [{"proofState": 0, "pos": {"line": 9, "column": 2}, "goal": "p q : Prop\n⊢ ¬(p ∨ q) → ¬p ∧ ¬q", "endPos": {"line": 9, "column": 7}}], "messages": [{"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 8, "column": 8}, "endPos": {"line": 8, "column": 30}, "data": "declaration uses `sorry`"}], "env": 11}

## 6. L’Equivalence : Iff

6.1 Définition de Iff

L’equivalence P <-> Q (“P si et seulement si Q”) signifie que P -> Q et Q -> P. C’est une conjonction de deux implications.

Iff : l’équivalence logique

La cellule de droite fait #check Iff. Trois choses à retenir :

  1. Iff p q est p ↔︎ q. Notation Unicode : ↔︎ (U+2194). C’est le type des paires de preuves : (Iff.intro : (p → q) → (q → p) → (p ↔︎ q)). Les projections sont Iff.mp : p ↔︎ q → p → q et Iff.mpr : p ↔︎ q → q → p. Symétriquement à And qui porte deux preuves en parallèle, Iff porte deux implications.
  2. Constructeur unique. Contrairement à Or (deux constructeurs inl/inr), Iff n’a qu’un constructeur : Iff.intro qui prend les deux directions. C’est parce que les deux directions sont symétriques : on a p ↔︎ q ssi on a p → q ET q → p.
  3. Notation sugar. ⟨hmp, hmpr⟩ ou Iff.intro hmp hmpr sont équivalents.

Pourquoi Iff plutôt que ↔︎. Les deux notations sont interchangeables dans le code utilisateur. Mathlib utilise ↔︎ par défaut pour les déclarations (lisibilité) et Iff dans les preuves tactiques (clarté syntaxique).

Le pont : Iff est omniprésent dans la partie haute. Lean-12 (Huang) prouve des équivalences entre formulations ; Lean-14 (Finiteness) prouve des équivalences entre dérivées partielles ; Lean-16b (Game of Life) prouve des bijections entre états. Le pattern Iff.intro (fun hp => ...) (fun hq => ...) est universel.

variable (p q : Prop)

#check Iff           -- Iff : Prop -> Prop -> Prop
#check p <-> q       -- p <-> q : Prop

-- Structure de Iff
#check @Iff.intro    -- Iff.intro : (p -> q) -> (q -> p) -> (p <-> q)
#check @Iff.mp       -- Iff.mp : (p <-> q) -> p -> q (modus ponens)
#check @Iff.mpr      -- Iff.mpr : (p <-> q) -> q -> p (modus ponens reverse)

-- Reflexivite de l'equivalence
theorem iff_refl : p <-> p :=
  ⟨fun hp => hp, fun hp => hp⟩
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 Iff (a b : Prop) : Prop
 p ↔ q : Prop
-- Structure de Iff
 @Iff.intro : ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
 @Iff.mp : ∀ {a b : Prop}, (a ↔ b) → a → b
 @Iff.mpr : ∀ {a b : Prop}, (a ↔ b) → b → a
-- Reflexivite de l'equivalence
theorem iff_refl : p <-> p :=
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
--% env 12
Raw input {"cmd": "variable (p q : Prop)\n\n#check Iff -- Iff : Prop -> Prop -> Prop\n#check p <-> q -- p <-> q : Prop\n\n-- Structure de Iff\n#check @Iff.intro -- Iff.intro : (p -> q) -> (q -> p) -> (p <-> q)\n#check @Iff.mp -- Iff.mp : (p <-> q) -> p -> q (modus ponens)\n#check @Iff.mpr -- Iff.mpr : (p <-> q) -> q -> p (modus ponens reverse)\n\n-- Reflexivite de l'equivalence\ntheorem iff_refl : p <-> p :=\n \u27e8fun hp => hp, fun hp => hp\u27e9", "env": 11}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Iff (a b : Prop) : Prop"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "p ↔ q : Prop"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "@Iff.intro : ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "@Iff.mp : ∀ {a b : Prop}, (a ↔ b) → a → b"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "@Iff.mpr : ∀ {a b : Prop}, (a ↔ b) → b → a"}, {"severity": "warning", "pos": {"line": 13, "column": 28}, "endPos": {"line": 13, "column": 29}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 13, "column": 30}, "endPos": {"line": 13, "column": 30}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 12}

6.2 Preuves d’equivalence

Symétrie introduction/élimination pour Iff

L’introduction se fait par Iff.intro : (p → q) → (q → p) → (p ↔︎ q) — on fournit les deux directions. L’élimination se fait par Iff.mp (forward) ou Iff.mpr (backward) :

  • h.mp : étant donné h : p ↔︎ q et hp : p, on a h.mp hp : q.
  • h.mpr : étant donné h : p ↔︎ q et hq : q, on a h.mpr hq : p.
  • rfl : étant donné h : p ↔︎ q, on a h.mp h.mpr : (q → q) (preuve triviale par la transitivité de l’identité).

Notation sugar en Lean 4 : h ▸ e (sugar pour h ▸ e = « substitute e modulo h ») — équivalent à Eq.subst h e mais concis. Vous le reverrez en Lean-3 (cellule 33).

Le pont : Iff est l’outil de base pour les reformulations. Lean-12 (Huang) utilise Iff pour passer de la définition combinatoire de la sensibilité à la formule close. Lean-14 (Finiteness) utilise Iff pour relier différentes notions de dérivée. Lean-16b (Game of Life) utilise Iff pour les bijections entre grilles.

variable (p q r : Prop)

-- Commutativite de And (version iff)
theorem and_comm_iff : p /\ q <-> q /\ p :=
  ⟨fun h => ⟨h.right, h.left⟩,
   fun h => ⟨h.right, h.left⟩⟩

-- Commutativite de Or (version iff)
theorem or_comm_iff : p \/ q <-> q \/ p :=
  ⟨fun h => h.elim Or.inr Or.inl,
   fun h => h.elim Or.inr Or.inl⟩

-- Transitivite de l'equivalence
theorem iff_trans (hpq : p <-> q) (hqr : q <-> r) : p <-> r :=
  ⟨fun hp => hqr.mp (hpq.mp hp),
   fun hr => hpq.mpr (hqr.mpr hr)⟩

-- Utilisation de l'equivalence pour reecrire
theorem use_iff (hpq : p <-> q) (hq : q) : p :=
  hpq.mpr hq
variable (p q r : Prop)
-- Commutativite de And (version iff)
theorem and_comm_iff : p /\ q <-> q /\ p :=
  ⟨fun h => ⟨h.right, h.left⟩,
   fun h => ⟨h.right, h.left⟩⟩
-- Commutativite de Or (version iff)
theorem or_comm_iff : p \/ q <-> q \/ p :=
  ⟨fun h => h.elim Or.inr Or.inl,
   fun h => h.elim Or.inr Or.inl⟩
-- Transitivite de l'equivalence
theorem iff_trans (hpq : p <-> q) (hqr : q <-> r) : p <-> r :=
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
   fun hr => hpq.mpr (hqr.mpr hr)⟩
-- Utilisation de l'equivalence pour reecrire
theorem use_iff (hpq : p <-> q) (hq : q) : p :=
  hpq.mpr hq
--% env 13
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Commutativite de And (version iff)\ntheorem and_comm_iff : p /\\ q <-> q /\\ p :=\n \u27e8fun h => \u27e8h.right, h.left\u27e9,\n fun h => \u27e8h.right, h.left\u27e9\u27e9\n\n-- Commutativite de Or (version iff)\ntheorem or_comm_iff : p \\/ q <-> q \\/ p :=\n \u27e8fun h => h.elim Or.inr Or.inl,\n fun h => h.elim Or.inr Or.inl\u27e9\n\n-- Transitivite de l'equivalence\ntheorem iff_trans (hpq : p <-> q) (hqr : q <-> r) : p <-> r :=\n \u27e8fun hp => hqr.mp (hpq.mp hp),\n fun hr => hpq.mpr (hqr.mpr hr)\u27e9\n\n-- Utilisation de l'equivalence pour reecrire\ntheorem use_iff (hpq : p <-> q) (hq : q) : p :=\n hpq.mpr hq", "env": 12}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 15, "column": 11}, "endPos": {"line": 15, "column": 12}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 15, "column": 13}, "endPos": {"line": 15, "column": 14}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 13}

Une equivalence P <-> Q se prouve en fournissant deux implications : P -> Q (sens direct) et Q -> P (sens reciproque). Le constructeur <forward, backward> (sucre pour Iff.intro) attend ces deux preuves. Ici, la commutativite de And : chaque direction echange les composantes (<h.right, h.left>). C’est le patron universel des preuves d’equivalence – toujours deux sens, jamais un seul.

Iff et Eq — relations complémentaires

Une équivalence P ↔︎ Q se prouve en fournissant deux implications : P → Q et Q → P. Une égalité a = b se prouve en exhibant une preuve que a et b se réduisent au même terme (le plus souvent par rfl). Les deux relations sont proches mais différentes :

  • Iff lie des propositions. Deux propositions sont équivalentes ssi elles sont prouvablement identiques au sens du noyau.
  • Eq lie des valeurs. Deux valeurs sont égales ssi elles se réduisent au même terme normal (bêta-réduction + delta pour Nat.add/Nat.mul).

Pourquoi Iff est constructif et Eq est définitionnel. Iff est un type avec constructeur explicite (Iff.intro) — vous devez écrire la preuve. Eq est définitionnellement vrai quand le noyau réduit les deux côtés au même terme : rfl : (1 + 2 = 3) parce que 1 + 2 se réduit en 3. Cette automaticité rend Eq beaucoup plus facile à manipuler dans les preuves.

Piège classique : croire que Iff est plus « faible » que Eq. Faux : Iff.refl : (P ↔︎ P) et Eq.refl : (a = a) sont tous deux triviaux, mais pour des raisons différentes (Iff.refl = Iff.intro id id ; Eq.refl = rfl).

Le pont : la distinction Iff/Eq est cruciale dans Lean-12 (Huang) où l’on manipule simultanément Eq (sur les sommes) et Iff (sur les formulations). Lean-14 (Finiteness) utilise les deux en parallèle. Le pattern h.mp / h.mpr / rfl est universel.

## 7. Égalité et Substitution

7.1 Le type Eq (égalité)

L’égalité a = b est une proposition fondamentale. Elle est reflexive (rfl), symetrique et transitive.

Le type Eq : égalité propositionnelle

#check Eq affiche Eq : {a : Sort u} → a → a → Prop. Trois choses à comprendre :

  1. Polymorphisme. Eq est polymorphe en univers (u) et en type (a). C’est la seule relation d’égalité — pas de EqNat, EqBool, etc. Quand vous écrivez 1 = 1, Lean infère Eq Nat.
  2. Constructeur unique. Eq.refl : (a : α) → a = a (par bêta-réduction, rfl se réduit en lui-même). Pas d’autre constructeur : deux valeurs sont égales ssi le noyau peut les réduire au même terme.
  3. Notation rfl. rfl : a = a est la seule preuve définitionnelle. C’est aussi une tactique (Lean-5) : rfl tranche toute égalité que le noyau peut calculer.

Pourquoi Eq est Prop. L’égalité est une proposition : « a = b » est une assertion qu’on prouve ou qu’on réfute. Si on peut exhiber rfl ou une chaîne de bêta-réductions, la proposition est vraie. Sinon, elle est fausse (ou non-prouvée).

Piège classique : croire que 1 = 2 est faux. Non : 1 = 2 est une proposition que le noyau peut réduire (les deux côtés sont des Nat distincts après normalisation, donc non-égaux). decide ou omega peut trancher ; rfl ne le peut pas.

Le pont : Eq est omniprésent. Lean-12 (Huang) utilise l’égalité pour réécrire les sommes partielles. Lean-14 (Finiteness) utilise Eq pour identifier des dérivées à des indices différents. Lean-16b (Game of Life) utilise Eq pour prouver l’invariance de configuration. Le pattern rfl / h.symm / h.trans est universel.

#check Eq            -- Eq : {a : Sort u} -> a -> a -> Prop
#check (1 = 1)       -- 1 = 1 : Prop
#check (1 = 2)       -- 1 = 2 : Prop (mais non prouvable!)

-- Reflexivite : rfl
#check @rfl          -- rfl : a = a

-- Exemples
theorem one_eq_one : 1 = 1 := rfl
theorem two_plus_two : 2 + 2 = 4 := rfl   -- Lean calcule!

-- Symetrie et transitivite
#check @Eq.symm      -- Eq.symm : a = b -> b = a
#check @Eq.trans     -- Eq.trans : a = b -> b = c -> a = c
 Eq.{u_1} {α : Sort u_1} : α → α → Prop
 1 = 1 : Prop
 1 = 2 : Prop
-- Reflexivite : rfl
 @rfl : ∀ {α : Sort u_1} {a : α}, a = a
-- Exemples
theorem one_eq_one : 1 = 1 := rfl
theorem two_plus_two : 2 + 2 = 4 := rfl   -- Lean calcule!
-- Symetrie et transitivite
 @Eq.symm : ∀ {α : Sort u_1} {a b : α}, a = b → b = a
 @Eq.trans : ∀ {α : Sort u_1} {a b c : α}, a = b → b = c → a = c
--% env 14
Raw input {"cmd": "#check Eq -- Eq : {a : Sort u} -> a -> a -> Prop\n#check (1 = 1) -- 1 = 1 : Prop\n#check (1 = 2) -- 1 = 2 : Prop (mais non prouvable!)\n\n-- Reflexivite : rfl\n#check @rfl -- rfl : a = a\n\n-- Exemples\ntheorem one_eq_one : 1 = 1 := rfl\ntheorem two_plus_two : 2 + 2 = 4 := rfl -- Lean calcule!\n\n-- Symetrie et transitivite\n#check @Eq.symm -- Eq.symm : a = b -> b = a\n#check @Eq.trans -- Eq.trans : a = b -> b = c -> a = c", "env": 13}
Raw output {"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Eq.{u_1} {α : Sort u_1} : α → α → Prop"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "1 = 1 : Prop"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "1 = 2 : Prop"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "@rfl : ∀ {α : Sort u_1} {a : α}, a = a"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 6}, "data": "@Eq.symm : ∀ {α : Sort u_1} {a b : α}, a = b → b = a"}, {"severity": "info", "pos": {"line": 14, "column": 0}, "endPos": {"line": 14, "column": 6}, "data": "@Eq.trans : ∀ {α : Sort u_1} {a b c : α}, a = b → b = c → a = c"}], "env": 14}

7.2 Substitution

Le principe de substitution : si a = b, alors on peut remplacer a par b dans n’importe quel contexte.

Note importante sur variable en Lean 4 : Les declarations variable n’ajoutent automatiquement les variables a une définition que si elles apparaissent dans le type de cette définition. Si une variable n’apparait que dans le corps (la preuve), elle doit etre passee explicitement comme paramètre.

Substitution : Eq.mp, Eq.subst, ▸

Le principe de substitution : si a = b, alors on peut remplacer a par b dans n’importe quel contexte qui en dépend. En Lean, c’est Eq.subst : a = b → P a → P b (et sa réciproque Eq.symm).

Notation sugar ▸. La cellule de droite utilise h ▸ e : étant donné h : a = b et e : P b, on obtient h ▸ e : P a (substitution de b vers a). C’est l’inversion de la direction de la substitution — ▸ pointe dans le sens de la substitution.

Pourquoi ▸ est pratique : il évite d’écrire Eq.subst h.symm e (qui est exactement h ▸ e). En Lean-5, la tactique subst h fait la même chose automatiquement : elle substitue b par a dans le goal.

Trois usages courants : 1. Réécriture : Eq.subst h : P a → P b (remplacer a par b dans P). 2. Symétrie : Eq.symm : a = b → b = a (inverser la direction). 3. Transitivité : Eq.trans : a = b → b = c → a = c (chaîner les égalités).

Le pont : la substitution est la base de toutes les preuves « calculatoires » (Lean-3 cellule 33 + Lean-5 tactique simp). Lean-12 (Huang) utilise h ▸ e pour réécrire les sommes partielles ; Lean-14 (Finiteness) utilise la transitivité pour chaîner les dérivées ; Lean-16b (Game of Life) utilise la symétrie pour basculer entre l’état actuel et l’état suivant.

-- Substitution avec le triangle : h ▸ e remplace a par b dans e

-- De P a et a = b, deduire P b
-- Note: les paramètres sont explicites car `variable` n'ajoute pas
-- automatiquement les variables qui n'apparaissent pas dans le TYPE
theorem subst_example (a b : Nat) (P : Nat -> Prop)
    (h : a = b) (hp : P a) : P b := h ▸ hp

-- Congruence : si a = b alors f a = f b
#check @congrArg     -- congrArg : (f : a -> b) -> x = y -> f x = f y

theorem congr_example (a b : Nat) (f : Nat -> Nat) (h : a = b) : f a = f b :=
  congrArg f h

-- Exemple concret
theorem add_congr (a b c : Nat) (h : a = b) : a + c = b + c :=
  congrArg (· + c) h
-- Substitution avec le triangle : h ▸ e remplace a par b dans e
-- De P a et a = b, deduire P b
-- Note: les parametres sont explicites car `variable` n'ajoute pas
-- automatiquement les variables qui n'apparaissent pas dans le TYPE
theorem subst_example (a b : Nat) (P : Nat -> Prop)
    (h : a = b) (hp : P a) : P b := h ▸ hp
-- Congruence : si a = b alors f a = f b
 @congrArg : ∀ {α : Sort u_1} {β : Sort u_2} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
theorem congr_example (a b : Nat) (f : Nat -> Nat) (h : a = b) : f a = f b :=
  congrArg f h
-- Exemple concret
theorem add_congr (a b c : Nat) (h : a = b) : a + c = b + c :=
  congrArg (· + c) h
--% env 15
Raw input {"cmd": "-- Substitution avec le triangle : h \u25b8 e remplace a par b dans e\n\n-- De P a et a = b, deduire P b\n-- Note: les parametres sont explicites car `variable` n'ajoute pas\n-- automatiquement les variables qui n'apparaissent pas dans le TYPE\ntheorem subst_example (a b : Nat) (P : Nat -> Prop)\n (h : a = b) (hp : P a) : P b := h \u25b8 hp\n\n-- Congruence : si a = b alors f a = f b\n#check @congrArg -- congrArg : (f : a -> b) -> x = y -> f x = f y\n\ntheorem congr_example (a b : Nat) (f : Nat -> Nat) (h : a = b) : f a = f b :=\n congrArg f h\n\n-- Exemple concret\ntheorem add_congr (a b c : Nat) (h : a = b) : a + c = b + c :=\n congrArg (\u00b7 + c) h", "env": 14}
Raw output {"messages": [{"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "@congrArg : ∀ {α : Sort u_1} {β : Sort u_2} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂"}], "env": 15}

## 8. Preuves Calculatoires avec calc

8.1 La construction calc

Pour les chaînes d’égalités ou d’inégalités, calc permet d’ecrire des preuves lisibles étape par étape.

calc : preuves calculatoires pas-à-pas

calc est un mode de preuve qui permet d’enchaîner des étapes de raisonnement, chacune justifiée par une relation (=, <=, <, ↔︎, etc.). Décortiquons la cellule de droite :

calc_example : a = b := calc a = c := h1; c = b := h2.symm

Structure : calc sépare les étapes par ;. Chaque étape est de la forme lhs RELATION rhs := preuve. La relation doit être cohérente : = c = b := h2.symm exige que la RHS de l’étape précédente (c) soit égale à la LHS de celle-ci (c). La dernière étape n’a pas de ; final.

Pourquoi calc est utile. Sans calc, la preuve serait Eq.trans h1 h2.symm. Avec calc, c’est lisible : on voit le chemin (a → c → b) plutôt que l’opération (trans). C’est l’équivalent mathématique de transitivity.refl mais en syntaxe déclarative.

Le pont : calc est intensivement utilisé dans Lean-12 (Huang) pour les preuves d’égalité des sommes partielles ; Lean-14 (Finiteness) pour les bornes de dérivées ; Lean-16b (Game of Life) pour les calculs d’invariants. Le pattern calc lhs = mid1 := ...; mid1 = mid2 := ...; ... = rhs := ... est universel.

-- Exemple simple avec calc
theorem calc_example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c :=
  calc a = b := h1
       _ = c := h2

-- Calcul arithmetique
theorem arith_calc : (2 + 3) * 4 = 20 :=
  calc (2 + 3) * 4
       = 5 * 4 := rfl
     _ = 20    := rfl

-- Preuve algébrique
-- Note: Cette preuve utilise des lemmes de la bibliotheque standard
-- La tactique `ring` (Mathlib) simplifierait cette preuve, mais nous
-- utilisons ici les tactiques de base disponibles dans Lean de base.
theorem double_sum (n : Nat) : n + n = 2 * n :=
  calc n + n
       = 1 * n + 1 * n := by rw [Nat.one_mul]
     _ = (1 + 1) * n   := by rw [Nat.add_mul]
     _ = 2 * n         := rfl
-- Exemple simple avec calc
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  calc a = b := h1
       _ = c := h2
-- Calcul arithmetique
theorem arith_calc : (2 + 3) * 4 = 20 :=
  calc (2 + 3) * 4
       = 5 * 4 := rfl
     _ = 20    := rfl
-- Preuve algebrique
-- Note: Cette preuve utilise des lemmes de la bibliotheque standard
-- La tactique `ring` (Mathlib) simplifierait cette preuve, mais nous
-- utilisons ici les tactiques de base disponibles dans Lean de base.
theorem double_sum (n : Nat) : n + n = 2 * n :=
  calc n + n
       = 1 * n + 1 * n := by rw [Nat.one_mul]
     _ = (1 + 1) * n   := by rw [Nat.add_mul]
     _ = 2 * n         := rfl
--% env 16
Raw input {"cmd": "-- Exemple simple avec calc\ntheorem calc_example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c :=\n calc a = b := h1\n _ = c := h2\n\n-- Calcul arithmetique\ntheorem arith_calc : (2 + 3) * 4 = 20 :=\n calc (2 + 3) * 4\n = 5 * 4 := rfl\n _ = 20 := rfl\n\n-- Preuve algebrique\n-- Note: Cette preuve utilise des lemmes de la bibliotheque standard\n-- La tactique `ring` (Mathlib) simplifierait cette preuve, mais nous\n-- utilisons ici les tactiques de base disponibles dans Lean de base.\ntheorem double_sum (n : Nat) : n + n = 2 * n :=\n calc n + n\n = 1 * n + 1 * n := by rw [Nat.one_mul]\n _ = (1 + 1) * n := by rw [Nat.add_mul]\n _ = 2 * n := rfl", "env": 15}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 13}, "endPos": {"line": 2, "column": 14}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 15}, "endPos": {"line": 2, "column": 16}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 16}

8.2 calc avec plusieurs relations

calc avec relations mixtes

calc n’est pas limité à = : on peut mélanger les relations tant qu’elles sont transitives compatibles. Exemples : - calc a = b := h1; b < c := h2; c = d := h3.symm — on enchaîne =, <, = (la transitivité passe par <). - calc a ≤ b := h1; b < c := h2; c = d := h3 — la transitivité </≤ permet < = ≤.

La règle cachée : Lean vérifie que la dernière colonne de chaque étape et la première colonne de l’étape suivante sont compatibles. Si ce n’est pas le cas, calc échoue avec un message « type mismatch ».

Pourquoi cette rigidité est utile. Elle force à déclarer les intermédiaires. Sans calc, une preuve par transitivité est facile à écrire mais difficile à lire : le_trans (lt_trans h1 h2) h3 est opaque sans la lecture des arguments. Avec calc, le chemin est explicite.

Le pont : calc mixte est utilisé dans Lean-14 (Finiteness) pour borner les dérivées : calc d²f/dxdy ≤ ... = ... ≤ ... ; Lean-16b (Game of Life) pour raisonner sur les invariants spatiaux ; Lean-12 (Huang) pour les comparaisons entre formulations. Le pattern calc a ≤ b := ...; b < c := ... est universel.

-- calc peut melanger = et <= etc.
theorem mixed_calc (a b c : Nat) (h1 : a = b) (h2 : b <= c) : a <= c :=
  calc a = b  := h1
       _ <= c := h2

-- Preuve plus complexe
theorem calc_complex (a b c d : Nat)
  (h1 : a = b) (h2 : c = d) (h3 : b + c = 10) : a + d = 10 :=
  calc a + d
       = b + d := congrArg (· + d) h1
     _ = b + c := congrArg (b + ·) h2.symm
     _ = 10    := h3
-- calc peut melanger = et <= etc.
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  calc a = b  := h1
       _ <= c := h2
-- Preuve plus complexe
theorem calc_complex (a b c d : Nat)
  (h1 : a = b) (h2 : c = d) (h3 : b + c = 10) : a + d = 10 :=
  calc a + d
       = b + d := congrArg (· + d) h1
     _ = b + c := congrArg (b + ·) h2.symm
     _ = 10    := h3
--% env 17
Raw input {"cmd": "-- calc peut melanger = et <= etc.\ntheorem mixed_calc (a b c : Nat) (h1 : a = b) (h2 : b <= c) : a <= c :=\n calc a = b := h1\n _ <= c := h2\n\n-- Preuve plus complexe\ntheorem calc_complex (a b c d : Nat)\n (h1 : a = b) (h2 : c = d) (h3 : b + c = 10) : a + d = 10 :=\n calc a + d\n = b + d := congrArg (\u00b7 + d) h1\n _ = b + c := congrArg (b + \u00b7) h2.symm\n _ = 10 := h3", "env": 16}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 6}, "endPos": {"line": 2, "column": 7}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 8}, "endPos": {"line": 2, "column": 9}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 17}

calc n’est pas limite a l’égalité : il enchaine toute relation munie d’une règle de transitivite (=, <=, <, ~, …). Ici, on melange = puis <= ; Lean deduit le résultat composite a <= c en composant les transitivites. C’est ce qui fait la puissance de calc : la lisibilite d’une chaîne de calcul, pour tout preorder – pas seulement l’égalité.

calc est polymorphe en relation

calc accepte toute relation munie d’une instance de Trans (transitivité). Lean dispose automatiquement de : - Trans Eq Eq Eq (transitivité de l’égalité). - Trans LE LE LE (transitivité de ≤). - Trans LT LT LT (transitivité de <). - Trans Eq LE LE (passage de = à ≤). - … et bien d’autres.

Pourquoi cette automaticité. Les typeclasses de Lean (Lean-3 cellule 19, Lean-6 tactique linarith) résolvent les instances à la volée. Vous écrivez calc a = b := h1; b ≤ c := h2 et Lean trouve Trans Eq LE LE tout seul.

Variante Relations vs Calc. Mathlib définit calc comme un mode syntaxique qui se réduit à Eq.trans (pour =) ou LE.trans (pour ≤). Sous le capot, c’est du sucre syntaxique. Mais la lecture est incomparable : un mathématicien préfère calc à trans pour des chaînes non-triviales.

Le pont : le polymorphisme de calc (relations multiples) est utilisé dans Lean-12 (Huang) où les preuves combinent = (sur les sommes), <= (sur les sommes partielles), et ↔︎ (sur les formulations). Lean-14 (Finiteness) utilise calc avec ≤ pour borner les dérivées. Le pattern « calc polymorphe » est universel dans les preuves sérieuses.

## 9. Logique Classique vs Constructive

9.1 La logique constructive par defaut

Par defaut, Lean utilise une logique constructive (ou intuitionniste). Cela signifie que certaines “lois” de la logique classique ne sont pas admises sans justification :

  • Tiers exclu : P \/ ¬P n’est pas prouvable en général
  • Double negation : ¬¬P -> P n’est pas prouvable en général
  • Preuve par contradiction : pour prouver P, on ne peut pas juste supposer ¬P et deriver False

Pourquoi ? En logique constructive, prouver P \/ Q necessite de savoir lequel est vrai. Pour les propositions non decidables, ce n’est pas toujours possible.

Constructivisme vs classicisme : la frontière

La cellule de droite montre qu’en logique constructive pure, certains énoncés intuitionnistes vrais ne sont pas prouvables : - p ∨ ¬p (tiers exclu) — non prouvable constructivement. - ¬¬p → p (double négation) — non prouvable constructivement. - ¬(p ∧ q) ↔︎ ¬p ∨ ¬q (De Morgan non symétrique) — la direction ¬p ∨ ¬q → ¬(p ∧ q) est constructive (trivial) ; la direction ¬(p ∧ q) → ¬p ∨ ¬q exige Classical.em (équivalente au tiers exclu faible).

Pourquoi. En constructif, prouver p ∨ q exige de savoir laquelle des deux est vraie. Le tiers exclu p ∨ ¬p dirait « p est vraie OU p est fausse » — c’est ce qu’on appelle le principe du tiers exclu (LEM), que les intuitionnistes rejettent (il suppose que toute proposition est décidable).

Les mathématiciens classiques acceptent LEM. La quasi-totalité des mathématiques publiées depuis Aristote suppose le tiers exclu. Lean par défaut est constructif (lean-4 ajoutera la logique classique à la demande). Pour utiliser le classique, on fait open Classical (Lean-3 section 9.2) ou on importe Classical.

Trois conséquences pédagogiques : 1. Vous rencontrerez Classical dans la partie haute — Lean-12 (Huang) ne l’utilise pas (la preuve est intuitionniste), Lean-14 (Finiteness) l’utilise pour certaines bornes, Lean-16b (Game of Life) ne l’utilise pas. Connaître la distinction = lire le contexte. 2. Les preuves classiques sont plus courtes mais moins informatives. Classical.em p : p ∨ ¬p ne vous dit pas lequel est vrai ; il vous dit juste qu’il y en a un. Parfois c’est suffisant (vous éliminez le Or par cas), parfois non (vous avez besoin de savoir). 3. L’intuitionnisme est plus expressif pour la logique. La double négation ¬¬p est plus faible que p en intuitionniste (prouver ¬¬p ne prouve pas p). C’est ce qui permet des distinctions fines (cf. cellule 23 sur De Morgan).

Le pont : Lean-3 section 9.2 active le classique ; Lean-12 (Huang) reste constructif ; Lean-14 (Finiteness) utilise Classical.em pour certaines bornes de dérivées. La distinction est cruciale pour lire les preuves sérieuses.

variable (p : Prop)

-- En logique constructive, ces théorèmes NE SONT PAS prouvables sans hypothese :
-- theorem em_attempt : p \/ ¬p := sorry  -- Impossible sans Classical
-- theorem dne_attempt : ¬¬p -> p := sorry  -- Impossible sans Classical

-- Ce qui EST prouvable constructivement :

-- Introduction de la double negation
theorem dne_intro : p -> ¬¬p :=
  fun hp hnp => hnp hp

-- Triple negation = simple negation
theorem triple_neg : ¬¬¬p -> ¬p :=
  fun h hp => h (fun hnp => hnp hp)
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- En logique constructive, ces theoremes NE SONT PAS prouvables sans hypothese :
-- theorem em_attempt : p \/ ¬p := sorry  -- Impossible sans Classical
-- theorem dne_attempt : ¬¬p -> p := sorry  -- Impossible sans Classical
-- Ce qui EST prouvable constructivement :
-- Introduction de la double negation
theorem dne_intro : p -> ¬¬p :=
  fun hp hnp => hnp hp
-- Triple negation = simple negation
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  fun h hp => h (fun hnp => hnp hp)
--% env 18
Raw input {"cmd": "variable (p : Prop)\n\n-- En logique constructive, ces theoremes NE SONT PAS prouvables sans hypothese :\n-- theorem em_attempt : p \\/ \u00acp := sorry -- Impossible sans Classical\n-- theorem dne_attempt : \u00ac\u00acp -> p := sorry -- Impossible sans Classical\n\n-- Ce qui EST prouvable constructivement :\n\n-- Introduction de la double negation\ntheorem dne_intro : p -> \u00ac\u00acp :=\n fun hp hnp => hnp hp\n\n-- Triple negation = simple negation\ntheorem triple_neg : \u00ac\u00ac\u00acp -> \u00acp :=\n fun h hp => h (fun hnp => hnp hp)", "env": 17}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 12}, "endPos": {"line": 1, "column": 13}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 1, "column": 14}, "endPos": {"line": 1, "column": 15}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 14, "column": 14}, "endPos": {"line": 14, "column": 15}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 14, "column": 16}, "endPos": {"line": 14, "column": 17}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 18}

9.2 Activer la logique classique

Pour utiliser le tiers exclu et les autres principes classiques, on importe Classical ou on utilise open Classical.

open Classical : activer la logique classique

La cellule de droite utilise open Classical puis vérifie que Classical.em : ∀ p, p ∨ ¬p est disponible. Trois choses à comprendre :

  1. open Classical importe les axiomes. Il rend disponibles : Classical.em : ∀ p, p ∨ ¬p ; Classical.byContradiction : (¬p → False) → p (équivalent à ¬¬p → p) ; Classical.choose (axiome du choix dépendant).
  2. Coût : on perd la garantie constructive. Toute preuve qui utilise Classical est non-constructive : elle peut prouver p ∨ q sans exhiber de preuve de p ou de q. Pour les preuves numériques (Lean-12, Lean-14), c’est acceptable. Pour les preuves algorithmiques (extraction de code), c’est rédhibitoire.
  3. Alternative Mathlib. Au lieu de open Classical, on peut utiliser Classical.em directement (have hem := Classical.em p; cases hem with | inl hp => ... | inr hnp => ...). Plus verbeux mais plus clair sur où le classique est utilisé.

Le pont : Classical.em est utilisé dans Lean-14 (Finiteness) pour les bornes de dérivées ; Lean-16b (Game of Life) ne l’utilise pas (preuve directe) ; Lean-12 (Huang) ne l’utilise pas (preuve purement intuitionniste). La règle informelle : « si vous voyez Classical.em, demandez-vous si la preuve peut être rendue constructive ».

open Classical

variable (p q : Prop)

-- Le tiers exclu est maintenant disponible
#check em p          -- em p : p \/ ¬p

-- Élimination de la double negation (notre version pedagogique)
theorem dne_demo : ¬¬p -> p :=
  fun hnnp =>
    Or.elim (em p)
      (fun hp => hp)           -- Cas p vrai
      (fun hnp => absurd hnp hnnp)  -- Cas ¬p (contradiction)

-- Preuve par contradiction
-- On utilise Classical.byContradiction (disponible avec open Classical)
theorem by_contradiction_demo (h : ¬p -> False) : p :=
  Classical.byContradiction (fun hnp => h hnp)
open Classical
variable (p q : Prop)
-- Le tiers exclu est maintenant disponible
 em p : p ∨ ¬p
-- Elimination de la double negation (notre version pedagogique)
theorem dne_demo : ¬¬p -> p :=
  fun hnnp =>
    Or.elim (em p)
      (fun hp => hp)           -- Cas p vrai
      (fun hnp => absurd hnp hnnp)  -- Cas ¬p (contradiction)
-- Preuve par contradiction
-- On utilise Classical.byContradiction (disponible avec open Classical)
theorem by_contradiction_demo (h : ¬p -> False) : p :=
  Classical.byContradiction (fun hnp => h hnp)
--% env 19
Raw input {"cmd": "open Classical\n\nvariable (p q : Prop)\n\n-- Le tiers exclu est maintenant disponible\n#check em p -- em p : p \\/ \u00acp\n\n-- Elimination de la double negation (notre version pedagogique)\ntheorem dne_demo : \u00ac\u00acp -> p :=\n fun hnnp =>\n Or.elim (em p)\n (fun hp => hp) -- Cas p vrai\n (fun hnp => absurd hnp hnnp) -- Cas \u00acp (contradiction)\n\n-- Preuve par contradiction\n-- On utilise Classical.byContradiction (disponible avec open Classical)\ntheorem by_contradiction_demo (h : \u00acp -> False) : p :=\n Classical.byContradiction (fun hnp => h hnp)", "env": 18}
Raw output {"messages": [{"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "em p : p ∨ ¬p"}], "env": 19}

9.3 Lois de De Morgan

De Morgan en logique classique

En activant Classical, les deux directions de De Morgan deviennent prouvables : - ¬(p ∧ q) ↔︎ ¬p ∨ ¬q : maintenant les deux directions sont prouvables (la direction ¬p ∨ ¬q → ¬(p ∧ q) reste constructive — trivial —, la direction ¬(p ∧ q) → ¬p ∨ ¬q utilise Classical.em). - ¬(p ∨ q) ↔︎ ¬p ∧ ¬q : les deux directions sont constructives (comme avant).

Pourquoi Classical.em aide ¬(p ∧ q) → ¬p ∨ ¬q. La preuve directe utilise Classical.em p pour basculer entre les deux cas :

theorem dem_and_classical (p q : Prop) (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
  Classical.em p.elim
    (fun hp : p => Or.inr (fun hq : q => h ⟨hp, hq⟩))
    (fun hnp : ¬p => Or.inl hnp)

Décomposons : Classical.em p donne p ∨ ¬p. Cas p : on a h : ¬(p ∧ q). Si on suppose q, alors p ∧ q (par And.intro) contredit h. Donc ¬q (par introduction de ¬), et on conclut Or.inr ‹¬q›. Cas ¬p : on a directement ¬p, donc Or.inl ‹¬p›. C’est la magie du classique : Classical.em p case-sur p et nous permet de choisir le bon Or.inl/Or.inr sans connaître p à l’avance.

Asymétrie restante : même en classique, ¬¬p → p ne donne pas informations : savoir ¬¬p ne dit pas pourquoi p est vraie. C’est pour ça que les preuves classiques sont plus courtes mais moins informatives que les constructives.

Le pont : la frontière constructif/classique est cruciale dans Lean-14 (Finiteness) où les bornes de dérivées peuvent être prouvées de deux façons (directe ou via Classical.em). Lean-12 (Huang) prouve sans Classical (la formule est intuitionniste). Lean-16b (Game of Life) ne l’utilise pas. La question « pourquoi cette preuve est-elle classique ? » est légitime.

open Classical

variable (p q : Prop)

-- De Morgan 1 : ¬(p \/ q) <-> ¬p /\ ¬q (constructif)
theorem de_morgan_1 : ¬(p \/ q) <-> ¬p /\ ¬q :=
  ⟨fun h => ⟨fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)⟩,
   fun h hpq => hpq.elim h.left h.right⟩

-- De Morgan 2 : ¬(p /\ q) <-> ¬p \/ ¬q (necessite Classical!)
theorem de_morgan_2 : ¬(p /\ q) <-> ¬p \/ ¬q :=
  ⟨fun h => Or.elim (em p)
    (fun hp => Or.inr (fun hq => h ⟨hp, hq⟩))
    (fun hnp => Or.inl hnp),
   fun h hpq => h.elim (fun hnp => hnp hpq.left) (fun hnq => hnq hpq.right)⟩
open Classical
variable (p q : Prop)
-- De Morgan 1 : ¬(p \/ q) <-> ¬p /\ ¬q (constructif)
theorem de_morgan_1 : ¬(p \/ q) <-> ¬p /\ ¬q :=
  ⟨fun h => ⟨fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)⟩,
   fun h hpq => hpq.elim h.left h.right⟩
-- De Morgan 2 : ¬(p /\ q) <-> ¬p \/ ¬q (necessite Classical!)
theorem de_morgan_2 : ¬(p /\ q) <-> ¬p \/ ¬q :=
  ⟨fun h => Or.elim (em p)
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
    (fun hnp => Or.inl hnp),
   fun h hpq => h.elim (fun hnp => hnp hpq.left) (fun hnq => hnq hpq.right)⟩
--% env 20
Raw input {"cmd": "open Classical\n\nvariable (p q : Prop)\n\n-- De Morgan 1 : \u00ac(p \\/ q) <-> \u00acp /\\ \u00acq (constructif)\ntheorem de_morgan_1 : \u00ac(p \\/ q) <-> \u00acp /\\ \u00acq :=\n \u27e8fun h => \u27e8fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)\u27e9,\n fun h hpq => hpq.elim h.left h.right\u27e9\n\n-- De Morgan 2 : \u00ac(p /\\ q) <-> \u00acp \\/ \u00acq (necessite Classical!)\ntheorem de_morgan_2 : \u00ac(p /\\ q) <-> \u00acp \\/ \u00acq :=\n \u27e8fun h => Or.elim (em p)\n (fun hp => Or.inr (fun hq => h \u27e8hp, hq\u27e9))\n (fun hnp => Or.inl hnp),\n fun h hpq => h.elim (fun hnp => hnp hpq.left) (fun hnq => hnq hpq.right)\u27e9", "env": 19}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 13, "column": 35}, "endPos": {"line": 13, "column": 151}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 13, "column": 151}, "endPos": {"line": 13, "column": 36}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 13, "column": 37}, "endPos": {"line": 13, "column": 38}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 20}

Subtilite importante : les deux sens de ¬(p ∨ q) <-> ¬p ∧ ¬q sont constructifs (pas besoin de logique classique). En revanche, l’autre loi ¬(p ∧ q) <-> ¬p ∨ ¬q n’est constructive que dans un sens : la direction ¬p ∨ ¬q → ¬(p ∧ q) (trivial) ; la direction ¬(p ∧ q) → ¬p ∨ ¬q exige le tiers exclu. C’est pourquoi cette cellule ouvre Classical : pour le sens qui en depend. Cette distinction constructif/classique est l’un des points pedagogiques cles de Lean.

Asymétrie subtile de De Morgan

La cellule note que ¬(p ∨ q) → ¬p ∧ ¬q est constructif (les deux directions) tandis que la biconditionnelle ¬(p ∧ q) ↔︎ ¬p ∨ ¬q n’est pas entièrement constructive (seule la direction ¬p ∨ ¬q → ¬(p ∧ q) l’est ; la direction opposée exige le tiers exclu). Décortiquons pourquoi :

¬(p ∨ q) → ¬p ∧ ¬q (constructif) : - On a hnpq : ¬(p ∨ q) et on doit prouver ¬p ∧ ¬q. - ¬p : on suppose hp : p, on a Or.inl hp : p ∨ q, contredisant hnpq. Donc ¬p. - ¬q : symétrique.

C’est constructif parce qu’on construit explicitement ¬p et ¬q à partir de hnpq.

¬(p ∧ q) → ¬p ∨ ¬q (NON constructif) : - On a hnpq : ¬(p ∧ q) et on doit prouver ¬p ∨ ¬q. - En classique (Classical.em), on prouve p ∨ ¬p. Cas gauche p : alors ¬q est prouvable (supposez q, on a (p, q) : p ∧ q, contredisant hnpq). Cas droit ¬p : directement ¬p. - En constructif, on ne peut pas prouver p ∨ ¬p, donc on est bloqué.

La subtilité : dans le cas constructif, on utilise l’hypothèse hnpq pour dériver directement ¬p (en exhibant un witness de contradiction). Dans le cas classique, on bifurque sur p ∨ ¬p et on utilise hnpq dans un seul des deux cas.

Le pont : cette asymétrie est la raison pour laquelle Lean-12 (Huang) peut être prouve en intuitionniste (les formules sont « positives » dans le bon sens) tandis que Lean-14 (Finiteness) a besoin de Classical.em pour certaines étapes (les bornes sont « existentielles » dans le mauvais sens). Comprendre l’asymétrie De Morgan = comprendre quand vous avez besoin du classique.

10. Exemples guides et Exercices

Exemple guide 1 : Associativite de Or

Preuve complète de l’associativite de la disjonction.

Exemples guides vs exercices

Cette cellule introduit des exemples résolus (associativité de Or, distributivité de And sur Or, contraposée classique) qui démontrent les patterns de preuve vus dans les sections 1-9. Suivez-les activement :

  1. Associativité de Or : Or.assoc : (p ∨ q) ∨ r ↔︎ p ∨ (q ∨ r). La preuve est purement constructive (les deux directions utilisent cases).
  2. Distributivité de And sur Or : p ∧ (q ∨ r) ↔︎ (p ∧ q) ∨ (p ∧ r). La preuve utilise cases h with | intro hp hor => ... puis reconstruction par Or.inl/Or.inr.
  3. Contraposée classique : (p → q) ↔︎ (¬q → ¬p) (utilise Classical.em pour l’une des directions).

Pourquoi plusieurs exemples et pas un seul. Chaque exemple illustre un pattern distinct : - (1) montre la réorganisation structurelle des Or (équivalent à la curryfication de Lean-2 pour Sum). - (2) montre la distribution d’un connecteur sur un autre (pattern fréquent dans la partie haute). - (3) montre l’usage du classique (vs constructif).

Le pont : ces patterns sont la base des preuves sérieuses. Lean-12 (Huang) utilise massivement la réorganisation structurelle et la distribution ; Lean-14 (Finiteness) utilise la contraposée classique ; Lean-16b (Game of Life) utilise la réorganisation. Les exemples guident le passage du pédagogique à l’appliqué.

variable (p q r : Prop)

-- Exemple guide 1 : Solution complète
-- Associativite de la disjonction
theorem or_assoc_sol : (p \/ q) \/ r <-> p \/ (q \/ r) :=
  ⟨fun left_or => left_or.elim
    (fun left_left_or => left_left_or.elim (Or.inl) (fun left_q => Or.inr (Or.inl left_q)))
    (fun left_r => Or.inr (Or.inr left_r)),
   fun right_or => right_or.elim
    (fun right_p => Or.inl (Or.inl right_p))
    (fun right_right_or => right_right_or.elim (fun right_q => Or.inl (Or.inr right_q)) Or.inr)⟩
variable (p q r : Prop)
-- Exemple guide 1 : Solution complete
-- Associativite de la disjonction
theorem or_assoc_sol : (p \/ q) \/ r <-> p \/ (q \/ r) :=
  ⟨fun left_or => left_or.elim
    (fun left_left_or => left_left_or.elim (Or.inl) (fun left_q => Or.inr (Or.inl left_q)))
    (fun left_r => Or.inr (Or.inr left_r)),
   fun right_or => right_or.elim
    (fun right_p => Or.inl (Or.inl right_p))
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
--% env 21
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Exemple guide 1 : Solution complete\n-- Associativite de la disjonction\ntheorem or_assoc_sol : (p \\/ q) \\/ r <-> p \\/ (q \\/ r) :=\n \u27e8fun left_or => left_or.elim\n (fun left_left_or => left_left_or.elim (Or.inl) (fun left_q => Or.inr (Or.inl left_q)))\n (fun left_r => Or.inr (Or.inr left_r)),\n fun right_or => right_or.elim\n (fun right_p => Or.inl (Or.inl right_p))\n (fun right_right_or => right_right_or.elim (fun right_q => Or.inl (Or.inr right_q)) Or.inr)\u27e9", "env": 20}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 11, "column": 38}, "endPos": {"line": 11, "column": 39}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 11, "column": 40}, "endPos": {"line": 11, "column": 41}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 11, "column": 42}, "endPos": {"line": 11, "column": 43}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 21}

Exemple guide 2 : Distributivite de And sur Or

Preuve complète de la distributivite de la conjonction sur la disjonction.

Exemple guide 2 : distributivité de And sur Or

La distributivité p ∧ (q ∨ r) ↔︎ (p ∧ q) ∨ (p ∧ r) est un cas d’école qui combine plusieurs patterns : - Élimination d’un Or par cases h with | inl hq => ... | inr hr => ... (Lean-4 tactic-style). - Reconstruction par Or.inl / Or.inr. - Élimination d’un And par cases hpq with | intro hp hq => ... (pour extraire hp : p et hq : q).

Direction → : on a h : p ∧ (q ∨ r). Par cases h with | intro hp hor => ..., on a hp : p et hor : q ∨ r. Par cases hor with | inl hq => ... | inr hr => ... (Lean-4 tactic-style). Cas gauche : hp ∧ hq puis Or.inl ⟨hp, hq⟩. Cas droit : hp ∧ hr puis Or.inr ⟨hp, hr⟩.

Direction ← : on a h : (p ∧ q) ∨ (p ∧ r). Par cases h with | inl hpq => ... | inr hpr => ... (Lean-4 tactic-style). Dans chaque cas, on extrait hp et on reconstruit p ∧ (q ∨ r) par And.intro hp (Or.inl hq) ou And.intro hp (Or.inr hr).

Pourquoi cette preuve est intéressante : elle illustre la double élimination (cases sur And, puis cases sur Or à l’intérieur, toujours en Lean-4 tactic-style cases h with | ...) et la double reconstruction (And.intro pour reconstruire le And, Or.inl/Or.inr pour reconstruire le Or). C’est le pattern « zig-zag » des preuves propositionnelles.

Le pont : ce pattern « zig-zag » est utilisé dans Lean-12 (Huang) pour réorganiser les sommes partielles. Lean-14 (Finiteness) l’utilise pour distribuer les dérivées sur les cas. Lean-16b (Game of Life) l’utilise pour raisonner sur les configurations spatiales. Maîtriser le zig-zag = pouvoir lire les preuves sérieuses.

variable (p q r : Prop)

-- Exemple guide 2 : Solution complète
-- Distributivite : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r)
theorem and_or_distrib_sol : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r) :=
  ⟨fun left_and => left_and.right.elim
    (fun left_q => Or.inl ⟨left_and.left, left_q⟩)
    (fun left_r => Or.inr ⟨left_and.left, left_r⟩),
   fun right_or => right_or.elim
    (fun right_left_and => ⟨right_left_and.left, Or.inl right_left_and.right⟩)
    (fun right_right_and => ⟨right_right_and.left, Or.inr right_right_and.right⟩)⟩
variable (p q r : Prop)
-- Exemple guide 2 : Solution complete
-- Distributivite : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r)
theorem and_or_distrib_sol : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r) :=
  ⟨fun left_and => left_and.right.elim
    (fun left_q => Or.inl ⟨left_and.left, left_q⟩)
    (fun left_r => Or.inr ⟨left_and.left, left_r⟩),
   fun right_or => right_or.elim
🟨 unused variable `p`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
    (fun right_right_and => ⟨right_right_and.left, Or.inr right_right_and.right⟩)⟩
--% env 22
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Exemple guide 2 : Solution complete\n-- Distributivite : p /\\ (q \\/ r) <-> (p /\\ q) \\/ (p /\\ r)\ntheorem and_or_distrib_sol : p /\\ (q \\/ r) <-> (p /\\ q) \\/ (p /\\ r) :=\n \u27e8fun left_and => left_and.right.elim\n (fun left_q => Or.inl \u27e8left_and.left, left_q\u27e9)\n (fun left_r => Or.inr \u27e8left_and.left, left_r\u27e9),\n fun right_or => right_or.elim\n (fun right_left_and => \u27e8right_left_and.left, Or.inl right_left_and.right\u27e9)\n (fun right_right_and => \u27e8right_right_and.left, Or.inr right_right_and.right\u27e9)\u27e9", "env": 21}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 10, "column": 61}, "endPos": {"line": 10, "column": 62}, "data": "unused variable `p`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 10, "column": 63}, "endPos": {"line": 10, "column": 64}, "data": "unused variable `q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 10, "column": 65}, "endPos": {"line": 10, "column": 66}, "data": "unused variable `r`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 22}

Exemple guide 3 : Contraposee (classique)

Preuve complète de la contraposee en logique classique.

Exemple guide 3 : contraposée (classique)

La contraposée classique (p → q) ↔︎ (¬q → ¬p) combine implication et négation, et utilise Classical.em pour l’une des directions. C’est l’archétype de la preuve où le classique « collapse » ¬¬p → p.

Direction → (constructif) : on a hpq : p → q et on doit prouver ¬q → ¬p. On prend hnq : ¬q et hp : p, on compose hnq (hpq hp) : False. Donc ¬q → ¬p. Pas de Classical requis.

Direction ← (classique) : on a hnqh : ¬q → ¬p et on doit prouver p → q. En classique : Classical.em q : q ∨ ¬q. Cas gauche hq : q : trivial fun _ => hq. Cas droit hnq : ¬q : par hnqh hnq : ¬p, donc ¬¬p, donc p (par Classical.byContradiction ou Classical.em), donc q (mais on n’a pas besoin : on a déjà hnq qui contredit hq… attention, on raisonne mal).

Reprenons : on veut p → q. On prend hp : p. On veut q. Par Classical.em q : q ∨ ¬q. Cas gauche hq : q : terminé. Cas droit hnq : ¬q : par hnqh hnq : ¬p, contradiction avec hp. Donc on a False.elim dans le cas droit, ce qui nous donne q (par False.elim : False → q). Donc dans les deux cas on a q. Donc p → q.

Pourquoi c’est instructif : la preuve utilise deux fois le classique (Classical.em q puis False.elim pour conclure depuis ¬p ∧ p). Le mécanisme « collapse ¬¬p → p » est central.

Le pont : la contraposée classique est la base des preuves par l’absurde dans Lean-14 (Finiteness). Lean-12 (Huang) ne l’utilise pas (preuve directe). Lean-16b (Game of Life) l’utilise pour certains invariants. Comprendre le collapse ¬¬p → p = comprendre quand la logique classique est nécessaire.

open Classical
variable (p q : Prop)

-- Exemple guide 3 : Solution complète
-- Contraposee : (p -> q) <-> (¬q -> ¬p)
theorem contrapositive_sol : (p -> q) <-> (¬q -> ¬p) :=
  ⟨fun h hnq hp => hnq (h hp),
   fun h hp => Or.elim (em q) id (fun hnq => absurd hp (h hnq))⟩
open Classical
variable (p q : Prop)
-- Exemple guide 3 : Solution complete
-- Contraposee : (p -> q) <-> (¬q -> ¬p)
theorem contrapositive_sol : (p -> q) <-> (¬q -> ¬p) :=
  ⟨fun h hnq hp => hnq (h hp),
   fun h hp => Or.elim (em q) id (fun hnq => absurd hp (h hnq))⟩
--% env 23
Raw input {"cmd": "open Classical\nvariable (p q : Prop)\n\n-- Exemple guide 3 : Solution complete\n-- Contraposee : (p -> q) <-> (\u00acq -> \u00acp)\ntheorem contrapositive_sol : (p -> q) <-> (\u00acq -> \u00acp) :=\n \u27e8fun h hnq hp => hnq (h hp),\n fun h hp => Or.elim (em q) id (fun hnq => absurd hp (h hnq))\u27e9", "env": 22}
Raw output {"env": 23}

Exercices a completer

Prouvez les théorèmes suivants. Remplacez sorry par votre preuve.

Exercices à compléter — niveaux progressifs

Cette cellule introduit les exercices du notebook. Lisez-les comme un tout : ils couvrent les patterns de preuve des sections 1-9 et vous préparent aux notebooks appliqués.

Stratégie : commencez par l’exercice 1 (associativité de Or — c’est l’exemple guide 1 transposé), puis l’exercice 2 (distributivité de And sur Or — c’est l’exemple guide 2), puis l’exercice 3 (contraposée classique — c’est l’exemple guide 3). Pour chacun : 1. Écrivez la preuve sans regarder l’exemple résolu (essayez 5 min). 2. Comparez avec l’exemple résolu (identifiez le pattern commun). 3. Reformulez votre preuve en suivant le pattern de l’exemple.

Erreurs classiques à éviter : - Oublier cases sur un Or ou un And : Lean rejette la preuve avec « goal is not an Or/matching constructor ». - Confondre Or.inl et And.intro : Or.inl hp (pas Or.inl hp hq — c’est And.intro). - Mal nommer les hypothèses : cases h with | inl hp => ... doit utiliser hp (pas h', pas _). Le nom doit correspondre à l’utilisation en aval. - Oublier Classical quand nécessaire : pour les exercices qui demandent Classical.em, ajoutez open Classical en tête.

Le pont : les exercices valident les patterns utilisés dans Lean-12 (Huang), Lean-14 (Finiteness), et Lean-16b (Game of Life). Si vous bloquez sur un exercice, relisez la section correspondante du notebook (les cellules 5-50). Si vous bloquez sur tous, revenez à Lean-2 (types dépendants) — la maîtrise des types est un prérequis.

variable (p q r : Prop)

-- Exercice 1 : Associativite de la disjonction
-- TODO étudiant : prouver (p \/ q) \/ r <-> p \/ (q \/ r)
-- Indice : utiliser Or.elim sur les deux disjonctions
theorem or_assoc_exercise : (p \/ q) \/ r <-> p \/ (q \/ r) :=
  sorry

-- Exercice 2 : Distribution conjunction/disjonction
-- TODO étudiant : prouver p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r)
-- Indice : decomposer avec .elim sur la disjonction
theorem and_or_distrib_exercise : p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r) :=
  sorry

-- Exercice 3 : Contraposition
-- TODO étudiant : prouver (p -> q) <-> (¬q -> ¬p)
-- Indice : utiliser open Classical et Or.elim (em q)
open Classical in
theorem contrapositive_exercise : (p -> q) <-> (¬q -> ¬p) :=
  sorry
variable (p q r : Prop)
-- Exercice 1 : Associativite de la disjonction
-- TODO etudiant : prouver (p \/ q) \/ r <-> p \/ (q \/ r)
-- Indice : utiliser Or.elim sur les deux disjonctions
🟨 declaration uses `sorry`
  sorry
-- Exercice 2 : Distribution conjunction/disjonction
-- TODO etudiant : prouver p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r)
-- Indice : decomposer avec .elim sur la disjonction
🟨 declaration uses `sorry`
  sorry
-- Exercice 3 : Contraposition
-- TODO etudiant : prouver (p -> q) <-> (¬q -> ¬p)
-- Indice : utiliser open Classical et Or.elim (em q)
open Classical in
🟨 declaration uses `sorry`
  sorry
--% env 24
--% prove 3
Raw input {"cmd": "variable (p q r : Prop)\n\n-- Exercice 1 : Associativite de la disjonction\n-- TODO etudiant : prouver (p \\/ q) \\/ r <-> p \\/ (q \\/ r)\n-- Indice : utiliser Or.elim sur les deux disjonctions\ntheorem or_assoc_exercise : (p \\/ q) \\/ r <-> p \\/ (q \\/ r) :=\n sorry\n\n-- Exercice 2 : Distribution conjunction/disjonction\n-- TODO etudiant : prouver p /\\ (q \\/ r) <-> (p /\\ q) \\/ (p /\\ r)\n-- Indice : decomposer avec .elim sur la disjonction\ntheorem and_or_distrib_exercise : p /\\ (q \\/ r) <-> (p /\\ q) \\/ (p /\\ r) :=\n sorry\n\n-- Exercice 3 : Contraposition\n-- TODO etudiant : prouver (p -> q) <-> (\u00acq -> \u00acp)\n-- Indice : utiliser open Classical et Or.elim (em q)\nopen Classical in\ntheorem contrapositive_exercise : (p -> q) <-> (\u00acq -> \u00acp) :=\n sorry", "env": 23}
Raw output {"sorries": [{"proofState": 1, "pos": {"line": 7, "column": 2}, "goal": "p q r : Prop\n⊢ (p ∨ q) ∨ r ↔ p ∨ q ∨ r", "endPos": {"line": 7, "column": 7}}, {"proofState": 2, "pos": {"line": 13, "column": 2}, "goal": "p q r : Prop\n⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r", "endPos": {"line": 13, "column": 7}}, {"proofState": 3, "pos": {"line": 20, "column": 2}, "goal": "p q : Prop\n⊢ p → q ↔ ¬q → ¬p", "endPos": {"line": 20, "column": 7}}], "messages": [{"severity": "warning", "pos": {"line": 6, "column": 8}, "endPos": {"line": 6, "column": 25}, "data": "declaration uses `sorry`"}, {"severity": "warning", "pos": {"line": 12, "column": 8}, "endPos": {"line": 12, "column": 31}, "data": "declaration uses `sorry`"}, {"severity": "warning", "pos": {"line": 19, "column": 8}, "endPos": {"line": 19, "column": 31}, "data": "declaration uses `sorry`"}], "env": 24}

Resume

Concept Description Construction
Prop Univers des propositions Prop : Type
Implication P -> Q fun hp => ...
Conjonction P /\ Q ⟨hp, hq⟩ ou And.intro
Disjonction P \/ Q Or.inl hp ou Or.inr hq
Negation ¬P = P -> False fun hp => contradiction
Equivalence P <-> Q ⟨fun hp => ..., fun hq => ...⟩
Égalité a = b rfl (reflexivite)
calc Chaînes de preuves calc a = b := ... _ = c := ...
Classique Tiers exclu open Classical + em p

Prochaine étape

Dans le notebook Lean-04-Quantifiers-Lean, nous etendrons ces concepts aux quantificateurs (pour tout, il existe), permettant de raisonner sur des ensembles infinis d’objets.

Notebook base sur “TP - Z3 - Tweety - Lean.pdf” Section VI.B.2 et adapte pour Lean 4

Navigation : ← Lean-02-Dependent-Types-Lean | Index | Lean-04-Quantifiers-Lean →

Retour au sommet