Logique et démonstrations assistées par ordinateur

Les mathématiques se préoccupent de nombreux types d'objets : des nombres, des figures géométriques, des fonctions, des opérations etc... Initialement, la plupart de ces objets proviennent de notre expérience du monde qui nous entoure, mais tous ont fait l'objet d'un processus d'idéalisation et de tri de l'information. Ainsi le nombre 3 est l'objet mathématique abstrait extrait d'une multitude de collections de trois choses, c'est le point commun entre une collection de trois élèves, trois chaises ou trois idées. Cette extraction d'un concept mathématique débute donc dès la maternelle. Plus tard on rencontre la notion de figure géométrique, la notion de point n'ayant ni largeur ni longueur ni épaisseur, la notion de rectangle dont les côtés n'ont aucune épaisseur et dont les angles mesurent exactement un quart de tour.

Le premier intérêt de ce processus est la simplification qui en résulte : le nombre trois oublie toute la complexité des objets de la collection dont on parle, un rectangle est bien plus simple qu'un livre de forme approximativement rectangulaire. Cette simplification permet de se concentrer sur les aspects d'un objet qui sont pertinents pour la discussion en cours. Le processus d'abstraction permet aussi d'affirmer en une seule phrase quelque chose à propos d'un ensemble d'objets. Ainsi l'affirmation « les diagonales d'un rectangle se coupent en leurs milieux » porte sur tous les rectangles. On en déduit une propriété (approximative) de tous les objets du monde réel qui sont (approximativement) des rectangles. Cette possibilité repose sur un autre bénéfice du processus d'abstraction : au contraire des autres sciences et de la vie quotidienne, les mathématiques profitent de l'existence d'affirmations qui sont vraies ou fausses, sans aucune négociation ni nuance. Ces affirmations sont appelées énoncés ou propositions mathématiques. Par exemple « 2 est pair » et « 1 + 1 = 3 » sont des énoncés. Le premier est vrai, tandis que le second est faux.

L'abstraction permet et nécessite le raisonnement logique rigoureux. Elle le permet car les objets manipulés sont suffisamment idéalisés pour que les énoncés deviennent vrais de façon définitive et non ambiguë. Elle le nécessite car elle éloigne de l'intuition immédiate. On peut même dire que ce qui distingue essentiellement les énoncés vrais est qu'on peut les démontrer. Une démonstration est un enchaînement de raisonnements logiques élémentaires permettant de combiner des énoncés vrais à l'aide d'un petit nombre de règles pour obtenir de nouveaux énoncés vrais. L'objectif de ce cours est d'expliciter ces règles et de pratiquer la démonstration et la rédaction de démonstration.

Bien sûr la combinaison d'énoncés vrais au moyen de règles logiques ne peut démarrer qu'en s'appuyant sur un certain nombre d'énoncés fondamentaux non démontrés, qu'on appelle des axiomes. La description d'axiomes n'est pas un objectif de ce cours, qui ne remontera jamais aussi loin dans la chaîne des raisonnements mathématiques. En réalité la manipulation des axiomes n'est l'activité quotidienne que d'une minorité infime de mathématiciens, sans parler des utilisateurs de mathématiques qui ne sont pas mathématiciens et peuvent entièrement ignorer ces axiomes durant toute leur vie. Ainsi c'est bien le raisonnement logique déduisant des énoncés nouveaux à partir d'énoncés supposés vrais qui joue le premier rôle plutôt que les axiomes. Cette observation permet d'évacuer au passage l'épineuse question philosophique de la définition du mot « vrai » pour la remplacer par la question bien plus simple de la validité du raisonnement qui, répétons-le, repose sur un petit nombre de règles très bien définies.

À ce stade il est important de ne pas perdre de vue l'objectif initial de manipulation et de compréhension des objets mathématiques. Le mécanisme du raisonnement logique est indispensable à la pratique mathématique, mais ce n'en est pas l'objet (sauf dans la branche spécialisée de la théorie de la démonstration). De même que la musique ne se réduit ni au solfège ni à la lutherie, et de même que la littérature ne se réduit pas à la grammaire ou à la syntaxe, les mathématiques ne se réduisent pas à la logique. Cependant, de même qu'il est impossible de faire de la musique sans un minimum de solfège ou d'écrire sans grammaire, on ne peut faire de mathématique sans logique ni démonstration. Et il ne suffit pas d'avoir rencontré les règles de logique, il est nécessaire d'avoir des automatismes, des réflexes.

De même qu'on ne peut pas faire de sport en réfléchissant à la succession des muscles à contracter, on ne peut pas faire de mathématiques sans un certain nombre de réflexes de manipulation formelle des énoncés et objets, complètement indépendamment de leur signification. L'activité mathématique est faite d'oscillations incessantes entre l'intuition et la rigueur logique, entre la créativité et la manipulation formelle de symboles.

Ce cours utilise l'assistant de démonstration Lean, un logiciel dédié à la vérification de démonstrations développé principalement par Leonardo de Moura au sein de Microsoft Research. L'objectif le plus visible de cette utilisation est de vérifier l'application stricte des règles logiques. Mais son objectif principal est de fournir en temps réel le contexte local et le but de chaque étape de raisonnement. Le contexte local est la collection des objets mathématiques introduits par l'énoncé à démontrer et par les étapes antérieures de la démonstration. Il s'ajoute au contexte global constitué des définitions, lemmes et théorèmes intervenant dans un exercice (et qui est trop vaste pour être affiché). Le but est simplement l'énoncé à démontrer mais il varie d'une ligne à l'autre suivant la progression de la démonstration. Certaines étapes peuvent entraîner la création de nouveaux buts, par exemple lors de la démonstration d'une équivalence par double implication ou lors de l'introduction d'un but intermédiaire.

Dans Lean, le mot énoncé est noté Prop. Pour exprimer que « 1 + 1 = 3 » est un énoncé, on écrit 1 + 1 = 3 : Prop. Pour tout énoncé $P$, une hypothèse $h$ affirmant que $P$ est vrai s'écrit h : P. On peut aussi lire cela comme « $h$ est une démonstration de $P$ ».

Le cours alternera entre les exercices de logique abstraite et les démonstrations reprises du cours d'analyse du premier semestre. Voici un exemple de démonstration typique de ce dernier cas. Bien sûr toutes les commandes seront discutées dans la suite. L'objectif immédiat est simplement d'avoir une idée de comment le logiciel se présente.

Dans cet exemple, comme dans tous les autres, on affiche en alternance le texte mathématique usuel et les commandes Lean correspondantes. Chaque ligne de code Lean commence et finit par une zone cliquable grise qui déclenche l'affichage du contexte local, listant objets mathématiques et hypothèses, et du but courant précédé du symbole ⊢. Dans une démonstration sans embranchement logique, le contexte au début d'une ligne est évidemment le même qu'à la fin de la ligne précédente. Bien sûr ce contexte dynamique n'est pas affiché à l'impression sur papier.

Définition
Soit $f$ une fonction de $ℝ$ dans $ℝ$, et soit $x_0$ un nombre réel. On dit que $f$ est continue en $x_0$ si $ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x_0| ≤ δ ⇒ |f(x) - f(x_0)| ≤ ε$ 
def continue_en (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
Définition
Une suite $u$ de nombres réels tend vers un réel $x_0$ si $∀ ε > 0, ∃ N, ∀ n ≥ N, |u_n - l| ≤ ε$. 
def limite_suite (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
Exemple

Si une suite $u$ tend vers $x_0$ et si une fonction $f$ est continue en $x_0$ alors la suite $f ∘ u$ (de terme général $f(u_n)$) tend vers $f(x_0)$.

example (f : ℝ → ℝ)  (u : ℕ → ℝ)  (x₀ : ℝ) (hu : limite_suite u x₀)
  (hf : continue_en f x₀) : limite_suite (f ∘ u) (f x₀) :=
Démonstration
Notre but est de montrer que, pour tout $ε$ strictement positif, il existe un entier $N$ tel que, pour tout entier $n$ supérieur à $N$, $|f(u_n) - f(x_0)|$ est inférieur à $ε$. 
  Montrons que ∀ ε > 0, ∃ N, ∀ n ≥ N, |(f ∘ u) n - f x₀| ≤ ε,

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀
⊢ limite_suite (f ∘ u) (f x₀)

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀
⊢ ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε)
Soit $ε$ un réel strictement positif. 
  Soit ε > 0,

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀
⊢ ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε)

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε
Par hypothèse de limite sur $f$, appliquée à cet $ε$ strictement positif, il existe un réel $δ$ strictement positif tel que :
Pour tout $x$ réel, si $|x - x_0| ≤ δ$ alors $|f(x) - y_0| ≤ ε$ (1).
On fixe un tel $δ$. 
  Par hf appliqué à [ε, ε_pos] on obtient (δ : ℝ) tel que 

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

    (δ_pos : δ > 0) (hδf : ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε),

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε
Par l'hypothèse de limite sur $u$, appliquée au réel $δ$ strictement positif que nous venons de fixer, il existe un entier $N$ tel que :
Pour tout entier $n$, si $n ≥ N$ alors $|u_n - x_0| ≤ δ$ (2).
On fixe un tel N. 
  Par hu appliqué à [δ, δ_pos] on obtient (N : ℕ) tel que

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

    (hNu : ∀ n ≥ N, |u n - x₀| ≤ δ),

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε
Montrons que N convient à notre objectif. 
  Montrons que N convient : ∀ n ≥ N, |(f ∘ u) n - f x₀| ≤ ε,

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ
⊢ ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε
Soit $n$ un entier supérieur à $N$. 
  Soit n ≥ N,

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ
⊢ ∀ (n : ℕ), n ≥ N → |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ,
n : ℕ,
n_ge : n ≥ N
⊢ |(f ∘ u) n - f x₀| ≤ ε
Vu la propriété (1), il suffit de montrer que $|u_n - x_0| ≤ δ$. 
  Par hδf il suffit de montrer que |u n - x₀| ≤ δ,

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ,
n : ℕ,
n_ge : n ≥ N
⊢ |(f ∘ u) n - f x₀| ≤ ε

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ,
n : ℕ,
n_ge : n ≥ N
⊢ |u n - x₀| ≤ δ
Cela découle immédiatement de la propriété (2) et de notre hypothèse sur $n$. 
  On conclut par hNu appliqué à [n, n_ge],

f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀,
ε : ℝ,
ε_pos : ε > 0,
δ : ℝ,
δ_pos : δ > 0,
hδf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε,
N : ℕ,
hNu : ∀ (n : ℕ), n ≥ N → |u n - x₀| ≤ δ,
n : ℕ,
n_ge : n ≥ N
⊢ |u n - x₀| ≤ δ

Gagné ! 🎉
QED.

Le logiciel Lean est installé en salle informatique du bâtiment 307. Pour l'utiliser ailleurs dans le cadre de ce cours, le plus simple est de télécharger une archive zip pour linux, MacOS ou Windows. Chacune de ces archives contient un répertoire mdd154 comprenant Lean et sa bibliothèque mathématique, Visual Studio Code et son extension faisant l'interface avec Lean ainsi que les premiers exercices du cours et un exécutable mdd154 à lancer.

Pour utiliser Lean dans un contexte plus large, on peut se référer à la documentation et au forum de discussion des utilisateurs de Lean (mais bien sûr les commandes en français que nous utilisons ne sont pas très répandues, elles ont été écrites spécialement pour ce cours).

Plan du cours