📐 Preuves de logique propositionnelle avec Lean 4 : un guide pratique 🔗

Cet article propose une présentation technique pas à pas des concepts fondamentaux de la logique propositionnelle et de leur implémentation formelle à l’aide du langage de programmation et assistant de preuve Lean 4.

Que vous soyez un mathématicien cherchant à formaliser des preuves ou un programmeur plongeant dans la théorie des types, ce guide reconstruit la logique à partir des premiers principes. Nous commencerons par les constantes logiques de base et explorerons comment Lean 4 modélise élégamment les constructions logiques grâce à l’isomorphisme de Curry-Howard — le principe selon lequel les propositions sont des types et les preuves sont des programmes.

📑 Table des Matières 🔗

⚙️ Le préambule : préparer le terrain 🔗

Avant de définir nos connecteurs logiques, nous devons mettre en place un environnement de base. Dans Lean 4, cela se fait généralement à l’aide de deux commandes spécifiques pour contrôler la portée (scope) et le comportement de calcul.

namespace Basic

noncomputable section

• namespace Basic : Cette commande regroupe nos définitions, évitant ainsi les conflits de noms avec la bibliothèque intégrée de Lean (le Prelude). Elle nous permet de redéfinir des structures fondamentales comme True, False et And à partir de zéro à des fins pédagogiques.
• noncomputable section : Lean 4 est à la fois un assistant de preuve et un langage de programmation fonctionnelle. Par défaut, il essaie de générer du bytecode exécutable pour chaque définition. Marquer une section comme noncomputable indique au compilateur d’ignorer cette étape, ce qui est courant en logique formelle où nous nous intéressons aux propriétés mathématiques plutôt qu’à l’exécution à l’instant T (runtime).

🧩 Les connecteurs logiques fondamentaux 🔗

Dans cette section, nous allons définir les éléments fondamentaux de la logique, en faisant correspondre la notation mathématique standard au code Lean 4.

✅ 1. Vrai / True (⊤) 🔗

La proposition la plus simple est celle qui est universellement valide sur le plan logique. En termes de programmation, $\top$ se comporte comme un type Unité (Unit type) — il possède exactement un état et ne transporte aucune donnée supplémentaire.

Définition :

inductive True : Prop where
  | intro : True

Comme il est défini avec un seul constructeur (intro), la seule façon de « prouver » True est de fournir ce constructeur exact.

Exemples :

-- Proving True unconditionally
example : True := True.intro

-- Any proposition 'a' trivially implies True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. Faux / False (⊥) 🔗

Alors que True est défini par l’existence triviale d’une preuve, False est défini par l’absence totale de preuve. C’est un type Vide (Empty type ou Void type).

Définition :

inductive False : Prop

Comme False n’a aucun constructeur, vous ne pouvez jamais l’instancier à partir de rien. Il représente une contradiction logique.

Le principe d’explosion (Ex Falso Quodlibet) : Si jamais vous vous retrouvez en possession d’une preuve de False, la logique s’effondre et vous pouvez prouver n’importe quoi. Lean gère cela à l’aide du récurseur False.elim.

-- From a falsehood, any proposition 'a' follows (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. Négation (¬) 🔗

Dans Lean 4, la négation n’est pas un concept primitif intégré. Elle est plutôt définie de manière fonctionnelle à l’aide de l’implication et de False. Pour prouver que la proposition $a$ est fausse (notée $\neg a$), vous devez démontrer une fonction dans laquelle supposer $a$ mène directement à une contradiction ($\bot$).

Définition :

def Not (a : Prop) : Prop := a → False

Théorèmes clés :

-- Proving Negation: If assuming 'a' proves False, then Not 'a' is true.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Double Negation Introduction (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' has type (a → False), so passing 'ha' yields False.

-- Modus Tollens: If (a → b) and (¬b), then (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. Implication (→) 🔗

Comme Lean repose sur la théorie des types, l’implication logique ($a \to b$) est traitée littéralement comme une fonction. Pour prouver que $a$ implique $b$, vous devez écrire une fonction qui prend une preuve arbitraire de $a$ et renvoie une preuve de $b$.

Exemple d’implication chaînée : Si vous pouvez transformer $c$ en $a$, et transformer $b$ en $d$, vous pouvez transformer une fonction de $a \to b$ en une fonction de $c \to d$.

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. Conjonction (∧) 🔗

La conjonction logique, qui exige que $a$ et $b$ soient tous deux vrais, est modélisée sous forme de structure. En termes de programmation, il s’agit d’un type Produit (Product type) (une structure ou un tuple) qui contient deux éléments de preuve distincts.

Définition :

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

Schémas de preuve clés :

-- Introduction: Creating an And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Symmetry: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. Disjonction (∨) 🔗

La disjonction logique exige qu’au moins l’une des propositions soit vraie. Contrairement à And, Or est un type Somme (Sum type) inductif (une union étiquetée), car il existe deux manières distinctes et alternatives de construire une preuve.

Définition :

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

Pour prouver $a \lor b$, vous enveloppez une preuve de $a$ dans le constructeur inl (inject-left), ou une preuve de $b$ dans le constructeur inr (inject-right).

Exemple :

-- Symmetry: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. Équivalence logique (↔) 🔗

La bi-implication, ou « si et seulement si » (Iff), signifie que deux propositions sont logiquement équivalentes. Elle est définie comme une structure contenant des implications dans les deux sens.

Définition :

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

Exemple de réflexivité :

-- Every proposition is equivalent to itself (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 Conclusion et points clés à retenir 🔗

En reconstruisant la logique propositionnelle à partir de zéro dans Lean 4, nous révélons la beauté mécanique des systèmes formels :

1. Constructif par défaut : Nous définissons ce que signifie détenir la preuve d’une vérité, plutôt que d’affirmer simplement que quelque chose est vrai.
2. Les propositions comme types : Grâce à la correspondance de Curry-Howard, les connecteurs logiques correspondent directement aux structures de programmation standards : l’implication est une fonction, And est une structure (struct), Or est une énumération (enum), True est le type unité (unit) et False est le type vide (void).
3. Les preuves comme programmes : Écrire une preuve mathématique dans Lean revient exactement à écrire une fonction au typage sûr (type-safe) qui satisfait une signature spécifique.

La maîtrise de ces briques fondamentales fournit le tremplin indispensable pour aborder des théorèmes mathématiques plus complexes, la logique des prédicats et la vérification de systèmes logiciels complexes.