Module L09 · Partie G · Mathématiques de l’informatique

Prouver qu’un programme est juste.

Les tests montrent la présence de bugs, jamais leur absence (Dijkstra). Pour un algorithme de tri, un contrôleur de robot ou un protocole de sécurité, on veut plus : une preuve. Ce module donne les outils — logique propositionnelle, récurrence, invariants de boucle, variants pour la terminaison, triplets de Hoare — et les applique aux algorithmes des modules précédents. C’est le cœur de l’épreuve d’informatique des concours.

Durée : 3 séances · Prérequis : L03-L05. Objectifs : manipuler la logique (tables de vérité, formes normales, quantificateurs), raisonner par récurrence forte et structurelle, écrire et vérifier des invariants, prouver la terminaison par un variant, rédiger une preuve de correction complète, connaître l’existence des assistants de preuve.

Ce que vous saurez faire à la fin

Écrire l’invariant d’une boucle et prouver initialisation, conservation, conclusion.
Exhiber un variant et prouver qu’un algorithme termine.
Prouver la correction de la dichotomie, du tri par insertion, d’Euclide, de BFS.
Traduire un raisonnement en assertions exécutables qui vérifient l’invariant à chaque tour.

Références : programme MP2I (« preuves de programmes »), Software Foundations (Pierce, en Coq), cours de Xavier Leroy, CLRS chapitre 2.

Fiche de cours · Définitions

Logique et preuves : définitions

Définition (proposition, connecteurs). Une proposition est vraie ou fausse. Connecteurs : ¬ (non), ∧ (et), ∨ (ou inclusif), → (implique : p → q est fausse seulement si p vraie et q fausse), ↔ (équivalent). Une tautologie est vraie pour toute valuation ; deux formules sont équivalentes si elles ont la même table de vérité.

Définition (quantificateurs). ∀x P(x) : pour tout x, P(x). ∃x P(x) : il existe x tel que P(x). Négations : ¬∀x P(x) ≡ ∃x ¬P(x) ; ¬∃x P(x) ≡ ∀x ¬P(x). L’ordre compte : ∀x ∃y (y > x) est vrai sur ℕ, ∃y ∀x (y > x) est faux.

Définition (implication, réciproque, contraposée). Réciproque de p → q : q → p (pas équivalente). Contraposée : ¬q → ¬p (équivalente). Condition nécessaire (q est nécessaire à p si p → q), suffisante (p est suffisante pour q si p → q).

Définition (types de preuve). Directe : hypothèses → conclusion par étapes. Par contraposée : prouver ¬q → ¬p. Par l’absurde : supposer ¬conclusion, dériver une contradiction. Par récurrence : P(0) et ∀n (P(n) → P(n+1)) donnent ∀n P(n) ; récurrence forte : (∀k < n, P(k)) → P(n). Par cas : couvrir toutes les possibilités. Par contre-exemple : réfuter un ∀.

Définition (triplet de Hoare). {P} S {Q} : si P est vraie avant l’exécution de S et que S termine, Q est vraie après. Correction partielle (sans terminaison) vs totale (avec variant).

Fiche de cours · Formules

Équivalences et règles à connaître

Nom	Équivalence	Usage
De Morgan	¬(p ∧ q) ≡ ¬p ∨ ¬q ; ¬(p ∨ q) ≡ ¬p ∧ ¬q	Nier une condition composée dans un `if`
Implication	p → q ≡ ¬p ∨ q ≡ ¬q → ¬p	Contraposée ; `not p or q`
Distributivité	p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r) ; p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)	Forme normale conjonctive (SAT)
Absorption	p ∨ (p ∧ q) ≡ p	Simplifier
Tiers exclu, non-contradiction	p ∨ ¬p ≡ ⊤ ; p ∧ ¬p ≡ ⊥	Preuve par cas ; par l’absurde
Modus ponens / tollens	p, p → q ⊢ q ; ¬q, p → q ⊢ ¬p	Règles de déduction
Négation des quantificateurs	¬∀x P ≡ ∃x ¬P ; ¬∃x P ≡ ∀x ¬P	Écrire un contre-exemple

Règles de Hoare — affectation : {Q[x := e]} x := e {Q} ; séquence : {P} S₁ {R}, {R} S₂ {Q} ⊢ {P} S₁; S₂ {Q} ; boucle : {I ∧ c} S {I} ⊢ {I} while c do S {I ∧ ¬c}

Σ_k=1ⁿ k = n(n+1)/2 ; Σ k² = n(n+1)(2n+1)/6 ; Σ_k=0ⁿ q^k = (qⁿ⁺¹ − 1)/(q − 1) les trois identités classiques à prouver par récurrence

Fiche de cours · Théorèmes et démonstrations

Démonstrations à savoir refaire (1/2)

Théorème 1 (√2 est irrationnel).

Par l’absurde : supposons √2 = p/q avec p, q entiers premiers entre eux (fraction irréductible). Alors p² = 2q², donc p² est pair, donc p est pair (contraposée de « p impair ⇒ p² impair » : (2k+1)² = 4k² + 4k + 1). Écrivons p = 2k : 4k² = 2q², q² = 2k², donc q est pair. p et q pairs contredit l’irréductibilité.

Théorème 2 (Euclide : il y a une infinité de nombres premiers).

Par l’absurde : soit p₁, …, p_n la liste finie de tous les premiers. N = p₁·p₂·…·p_n + 1 est > 1, donc a un diviseur premier p (tout entier > 1 en a un : récurrence forte, le plus petit diviseur > 1 est premier). Ce p est l’un des p_i, donc divise le produit, donc divise N − produit = 1 : impossible.

Théorème 3 (récurrence : Σ_k=0ⁿ 2^k = 2ⁿ⁺¹ − 1).

P(0) : 2⁰ = 1 = 2¹ − 1. Hérédité : si Σ_k≤n 2^k = 2ⁿ⁺¹ − 1, alors Σ_k≤n+1 2^k = 2ⁿ⁺¹ − 1 + 2ⁿ⁺¹ = 2·2ⁿ⁺¹ − 1 = 2ⁿ⁺² − 1. Conclusion par le principe de récurrence. (Cette identité est celle du coût du tableau dynamique, L01.)

Théorème 4 (Cantor : ℝ n’est pas dénombrable — argument diagonal). Il n’existe pas de suite (x_n) énumérant tous les réels de [0, 1[.

Soit une suite quelconque x₀, x₁, … de réels de [0, 1[, écrits en développement décimal (on choisit celui sans 9 infini). Construisons y dont la n-ième décimale est 5 si la n-ième décimale de x_n ≠ 5, et 6 sinon. y ∈ [0, 1[ et, pour tout n, y diffère de x_n à la n-ième décimale : y n’est dans la suite. Aucune suite n’épuise [0, 1[. Le même argument diagonal prouve l’indécidabilité de l’arrêt (L23) et qu’il y a plus de fonctions ℕ → {0, 1} que de programmes.

Fiche de cours · Théorèmes et démonstrations

Démonstrations à savoir refaire (2/2) : programmes

Théorème 5 (correction de l’exponentiation rapide). def puiss(x, n): r, b, e = 1, x, n ; while e > 0: if e % 2: r *= b ; b *= b ; e //= 2 ; return r renvoie xⁿ en O(log n) multiplications.

Invariant I : r · b^e = xⁿ. Initialisation : 1 · xⁿ. Conservation : si e est impair, e = 2e′ + 1 : r·b^e = (r·b)·(b²)^e′, et après le tour r ← r·b, b ← b², e ← e′ : invariant conservé ; si e pair, e = 2e′ : r·b^e = r·(b²)^e′. Variant : e (entier ≥ 0, strictement décroissant car e ≥ 1 ⇒ e//2 < e). Sortie : e = 0 donc r · b⁰ = r = xⁿ. Nombre de tours : ⌊log₂ n⌋ + 1, chacun ≤ 2 multiplications.

Théorème 6 (correction de l’algorithme d’Euclide). while b: a, b = b, a % b ; return a renvoie pgcd(a₀, b₀).

Invariant : pgcd(a, b) = pgcd(a₀, b₀). Il tient car pgcd(a, b) = pgcd(b, a mod b) : tout diviseur commun de a et b divise a − qb = a mod b, et réciproquement tout diviseur commun de b et a mod b divise a = qb + (a mod b). Variant : b (a mod b < b). Sortie : b = 0, pgcd(a, 0) = a. Terminaison en O(log min(a₀, b₀)) tours (Lamé : le pire cas est deux Fibonacci consécutifs).

Théorème 7 (tri par insertion : correction partielle). Invariant externe : après i itérations, L[0..i] est trié et est une permutation des éléments initiaux de L[0..i].

Initialisation : L[0..1] (un élément) est trié. Conservation : l’itération i insère L[i] dans L[0..i] trié en décalant vers la droite les éléments > L[i] (invariant interne : L[0..j] ∪ L[j+1..i+1] est trié et contient les mêmes éléments, avec un « trou » en j où l’on écrira L[i]) ; à la fin L[0..i+1] est trié. Variant interne : j ; externe : n − i. Sortie : L[0..n] trié, permutation de l’entrée.

Fiche de cours · Méthodes

Méthodes de rédaction et pièges

Méthode — rédiger une preuve. Annoncer la méthode (« par récurrence sur n », « par l’absurde »). Écrire précisément la propriété P(n). Traiter le cas de base explicitement. Dans l’hérédité, dire où l’hypothèse est utilisée. Conclure. Une preuve est un texte lu par quelqu’un d’autre : chaque « donc » doit être justifiable.

Méthode — choisir le type de preuve. « Pour tout n » avec une structure récursive → récurrence. « Il n’existe pas » / « est irrationnel » / « infini » → absurde. « Si … alors » où la négation de la conclusion est plus maniable → contraposée. Un ∀ à réfuter → un contre-exemple concret. Une propriété d’un programme → invariant + variant.

Méthode — trouver l’invariant d’une boucle. Exécuter à la main deux ou trois tours en notant les variables ; chercher la relation qui reste vraie (souvent : « ce qui est calculé = la formule appliquée à la partie déjà traitée », ou une égalité entre l’état et la cible comme r·b^e = xⁿ). Vérifier au tout premier état et au dernier.

Pièges : confondre p → q et sa réciproque ; « prouver » P(n+1) sans utiliser P(n) (ce n’est alors pas une récurrence, ou l’hérédité est fausse) ; oublier le cas de base (la « preuve » que tous les chevaux ont la même couleur échoue en n = 2) ; un exemple n’est pas une preuve ; ∀x ∃y ≠ ∃y ∀x.

Fiche de cours · Exercices corrigés

Exercices corrigés

Exercice 1. Montrer que pour tout entier n ≥ 1, un tableau binaire à n feuilles distinctes a une hauteur ≥ ⌈log₂ n⌉.

Correction. Lemme par récurrence sur h : un arbre binaire de hauteur h a au plus 2^h feuilles. h = 0 : une feuille = 2⁰. Hérédité : un arbre de hauteur h+1 a deux sous-arbres de hauteur ≤ h, donc ≤ 2^h + 2^h = 2^h+1 feuilles. Donc n ≤ 2^h, soit h ≥ log₂ n, et h entier donne h ≥ ⌈log₂ n⌉. (C’est le cœur de la borne inférieure des tris, L04.)

Exercice 2. Nier formellement « tout robot qui détecte un obstacle s’arrête en moins d’une seconde », puis écrire le test qui cherche un contre-exemple.

Correction. Formule : ∀r ∀t (detecte(r, t) → ∃t′ ∈ ]t, t+1], arrete(r, t′)). Négation : ∃r ∃t (detecte(r, t) ∧ ∀t′ ∈ ]t, t+1], ¬arrete(r, t′)) — « il existe un robot et un instant de détection tels que, pendant toute la seconde suivante, le robot ne s’arrête pas ». Test : générer des scénarios (robots, instants de détection), simuler, et échouer dès qu’un (r, t) vérifie la négation : c’est exactement un test par propriétés (hypothesis), dont l’échec fournit le contre-exemple.

Exercice 3. Prouver la correction et la terminaison de def somme_chiffres(n): s = 0 ; while n > 0: s += n % 10 ; n //= 10 ; return s pour n ≥ 0.

Correction. Notons n₀ la valeur initiale et sc(n) la somme des chiffres de n (sc(0) = 0). Invariant : s + sc(n) = sc(n₀). Initialisation : 0 + sc(n₀). Conservation : n = 10·q + c avec c = n % 10, q = n // 10 : sc(n) = c + sc(q) ; après le tour, s′ + sc(n′) = (s + c) + sc(q) = s + sc(n) = sc(n₀). Variant : n (entier ≥ 0, et n // 10 < n pour n ≥ 1). Sortie : n = 0, donc s = sc(n₀). Nombre de tours : nombre de chiffres, ⌊log₁₀ n₀⌋ + 1.

01 / Logique

Propositions, connecteurs, tables de vérité

from itertools import product

def table(formule, variables):
    print(" ".join(variables), "| f")
    for valeurs in product([False, True], repeat=len(variables)):
        env = dict(zip(variables, valeurs))
        print(" ".join("1" if v else "0" for v in valeurs), "|", int(formule(**env)))

implique = lambda a, b: (not a) or b          # a → b est faux seulement si a vrai et b faux
table(lambda p, q: implique(p, q), "pq")
print()
# Équivalences à connaître : vérifiées sur toutes les valuations
lois = {
    "De Morgan ¬(p∧q) = ¬p∨¬q": lambda p, q: (not (p and q)) == ((not p) or (not q)),
    "Contraposée (p→q) = (¬q→¬p)": lambda p, q: implique(p, q) == implique(not q, not p),
    "Distributivité p∧(q∨r) = (p∧q)∨(p∧r)": lambda p, q, r: (p and (q or r)) == ((p and q) or (p and r)),
    "Réciproque (p→q) = (q→p) ?": lambda p, q: implique(p, q) == implique(q, p),
}
for nom, f in lois.items():
    n = f.__code__.co_argcount
    ok = all(f(*v) for v in product([False, True], repeat=n))
    print(("tautologie " if ok else "FAUX      "), nom)

Vocabulaire

Une tautologie est vraie pour toute valuation ; une formule satisfiable l’est pour au moins une ; une contradiction pour aucune. Deux formules sont équivalentes si elles ont la même table. Toute formule s’écrit en forme normale conjonctive (ET de OU de littéraux) — c’est l’entrée du problème SAT (module L17). Piège classique : confondre l’implication et sa réciproque. « S’il pleut, le sol est mouillé » n’implique pas « si le sol est mouillé, il pleut ».

01 / Logique

Quantificateurs et négation : ce que dit exactement un énoncé

Savoir écrire « la liste est triée », « x est le maximum », « le tableau ne contient pas de doublon », « le chemin est valide » avec des quantificateurs est la première étape de toute preuve — et de tout test par propriétés (module L01).

02 / Récurrence

Récurrence simple, forte, structurelle

# Récurrence simple : P(0) et P(n) ⇒ P(n+1). Exemple : 1 + 2 + … + n = n(n+1)/2
def somme(n): return 0 if n == 0 else somme(n - 1) + n
assert all(somme(n) == n * (n + 1) // 2 for n in range(50))
# La preuve : P(0) : 0 = 0. Si somme(n) = n(n+1)/2, alors somme(n+1) = n(n+1)/2 + (n+1) = (n+1)(n+2)/2. ∎

# Récurrence forte : P(k) pour tout k < n ⇒ P(n). Exemple : tout n ≥ 2 a un diviseur premier.
def diviseur_premier(n):
    for d in range(2, n + 1):
        if n % d == 0: return d          # le plus petit diviseur ≥ 2 est premier
# Preuve : soit d le plus petit diviseur ≥ 2 de n. Si d n'était pas premier, il aurait un diviseur
# 1 < e < d, qui diviserait aussi n : contradiction avec la minimalité de d. ∎

# Récurrence structurelle : sur la forme des données (liste vide / x :: reste ; feuille / nœud)
def hauteur(a):     # arbre : None ou (gauche, droit)
    return 0 if a is None else 1 + max(hauteur(a[0]), hauteur(a[1]))
def taille(a):
    return 0 if a is None else 1 + taille(a[0]) + taille(a[1])
# Propriété : taille(a) ≤ 2^hauteur(a) − 1.
# Preuve : feuille : 0 ≤ 0. Nœud : taille = 1 + t(g) + t(d) ≤ 1 + (2^h(g) − 1) + (2^h(d) − 1) ≤ 2·2^(h−1) − 1 = 2^h − 1. ∎
import random
def arbre_aleatoire(p=0.6):
    return (arbre_aleatoire(p * 0.8), arbre_aleatoire(p * 0.8)) if random.random() < p else None
random.seed(2)
print(all(taille(a) <= 2 ** hauteur(a) - 1 for a in (arbre_aleatoire() for _ in range(500))))

La récurrence structurelle suit la définition inductive du type (module L07, types algébriques d’OCaml) : un cas par constructeur. C’est la raison profonde pour laquelle la récursion et la preuve vont ensemble.

03 / Invariants

L’invariant de boucle : la propriété qui survit à chaque tour

Les trois étapes d’une preuve par invariant

Initialisation : l’invariant est vrai avant le premier tour. Pour maximum : i = 1, m = t[0] = max(t[:1]). ✓
Conservation : s’il est vrai avant un tour, il l’est après. Si m = max(t[:i]) et qu’on fait if t[i] > m: m = t[i], alors m = max(t[:i+1]). ✓
Conclusion : à la sortie, l’invariant plus la négation de la condition donnent la postcondition. i = len(t) ⇒ m = max(t). ✓

C’est exactement la récurrence sur le numéro du tour. L’invariant se trouve en se demandant « qu’est-ce que la boucle a construit jusqu’ici ? ». Les assert dans le code sont des invariants exécutables : en développement, ils attrapent la boucle qui déraille au tour précis où ça arrive.

03 / Invariants

Cas d’école : dichotomie et tri par insertion

def dichotomie(t, x):
    """Pré : t trié. Post : renvoie i avec t[i] == x, ou -1 si x ∉ t."""
    bas, haut = 0, len(t)
    # INVARIANT : (x ∈ t) ⇒ (x ∈ t[bas..haut[)   et   0 ≤ bas ≤ haut ≤ len(t)
    # VARIANT : haut − bas (entier ≥ 0, strictement décroissant)
    while bas < haut:
        assert 0 <= bas <= haut <= len(t) and (x not in t or x in t[bas:haut])
        m = (bas + haut) // 2
        if t[m] < x: bas = m + 1        # t trié ⇒ x ∉ t[bas..m] ⇒ invariant conservé
        elif t[m] > x: haut = m         # t trié ⇒ x ∉ t[m..haut[
        else: return m                  # postcondition directe
    return -1                           # bas == haut : t[bas..haut[ vide ⇒ x ∉ t par l'invariant

print(dichotomie([1, 3, 4, 8, 12, 15], 8), dichotomie([1, 3, 4, 8, 12, 15], 5))

def tri_insertion(t):
    t = list(t)
    # INVARIANT externe : t[0..i[ est trié ET est une permutation des i premiers éléments d'origine
    for i in range(1, len(t)):
        assert all(t[k] <= t[k + 1] for k in range(i - 1))
        x, j = t[i], i - 1
        # INVARIANT interne : t[j+1..i] > x  et  t[0..j] ∪ t[j+2..i] = anciens t[0..i[ ; VARIANT : j + 1
        while j >= 0 and t[j] > x:
            t[j + 1] = t[j]; j -= 1
        t[j + 1] = x
    return t
print(tri_insertion([5, 2, 4, 6, 1, 3]))

Notez le lien entre invariant et correction (la bonne réponse) d’une part, variant et terminaison d’autre part. La correction sans terminaison est une « correction partielle » : « si ça s’arrête, c’est juste ». La correction totale exige les deux.

04 / Terminaison

Le variant : une quantité entière positive qui décroît strictement

def pgcd(a, b):
    """Pré : a, b ≥ 0. VARIANT : b (entier ≥ 0, strictement décroissant car a mod b < b)."""
    trace = []
    while b:
        trace.append(b)
        a, b = b, a % b
    return a, trace
print(pgcd(1071, 462))

def collatz(n):
    """Personne ne connaît de variant : la terminaison est une CONJECTURE (ouverte depuis 1937)."""
    etapes = 0
    while n != 1:
        n = n // 2 if n % 2 == 0 else 3 * n + 1; etapes += 1
    return etapes
print(max(collatz(n) for n in range(1, 10_000)))

def ackermann(m, n):
    """Termine, mais le variant est le couple (m, n) en ordre lexicographique, pas un entier simple."""
    if m == 0: return n + 1
    if n == 0: return ackermann(m - 1, 1)
    return ackermann(m - 1, ackermann(m, n - 1))
print([ackermann(m, n) for m in range(3) for n in range(4)], ackermann(3, 3))

# Une boucle qui ne termine pas toujours : où est l'erreur de variant ?
def recherche_bug(t, x):
    i = 0
    while t[i] != x:      # si x ∉ t : IndexError (ou boucle infinie en C !). Le variant len(t) − i
        i += 1            # ne garantit pas que la condition devienne fausse AVANT de sortir du tableau.
    return i
print(recherche_bug([4, 7, 9], 9))

Ordres bien fondés

Un variant est une fonction de l’état vers un ensemble bien fondé (sans suite infinie strictement décroissante) : les entiers naturels, les couples d’entiers en ordre lexicographique (Ackermann), la taille d’une structure (récursion structurelle). Pour la fonction 91 de McCarthy ou Collatz, on ne connaît pas de variant simple : la terminaison est prouvée autrement (McCarthy) ou pas du tout (Collatz). Le problème de l’arrêt (module L23) dit qu’aucun programme ne peut décider dans tous les cas si un autre programme termine — c’est pour cela qu’on doit fournir le variant soi-même.

05 / Hoare

Triplets de Hoare : {P} programme {Q}

# {P} C {Q} : si P est vraie avant C et que C termine, alors Q est vraie après.
# Règles :
#   affectation   {Q[x := e]} x = e {Q}          (« Q avec x remplacé par e » doit être vraie avant)
#   séquence      {P} C1 {R}  et  {R} C2 {Q}  ⇒  {P} C1; C2 {Q}
#   condition     {P ∧ b} C1 {Q}  et  {P ∧ ¬b} C2 {Q}  ⇒  {P} if b: C1 else: C2 {Q}
#   boucle        {I ∧ b} C {I}  ⇒  {I} while b: C {I ∧ ¬b}        (I = invariant)
#   conséquence   P ⇒ P', {P'} C {Q'}, Q' ⇒ Q  ⇒  {P} C {Q}

def echange(a, b):
    # {a = A ∧ b = B}
    t = a        # {t = A ∧ b = B}
    a = b        # {t = A ∧ a = B}
    b = t        # {b = A ∧ a = B}  ✓ postcondition : les valeurs sont échangées
    return a, b

def division(a, b):
    """{a ≥ 0 ∧ b > 0}  q, r = division(a, b)  {a = q·b + r ∧ 0 ≤ r < b}"""
    q, r = 0, a
    # I : a = q·b + r ∧ r ≥ 0        (vrai : a = 0·b + a)
    while r >= b:                     # {I ∧ r ≥ b}
        q, r = q + 1, r - b           # a = (q+1)·b + (r−b), et r − b ≥ 0 : {I}  ; variant r
    # {I ∧ r < b} = postcondition ✓
    return q, r

import random
for _ in range(1000):
    a, b = random.randint(0, 500), random.randint(1, 30)
    q, r = division(a, b)
    assert a == q * b + r and 0 <= r < b
print("division : 1000 postconditions vérifiées ; et la preuve dit : toutes.")

Ce que les assistants de preuve automatisent

Coq, Isabelle, Lean, Why3, Dafny, F* : on écrit le programme, ses spécifications (pré/post/invariants) et l’outil vérifie mécaniquement chaque étape ou génère les obligations de preuve à démontrer. Le compilateur C CompCert (Xavier Leroy, Inria) est prouvé en Coq : il ne peut pas produire de code faux. Le noyau seL4 est prouvé sans bug. Ces outils sont utilisés pour l’avionique, les cartes bancaires, la cryptographie et de plus en plus pour les systèmes embarqués critiques. Lean est aujourd’hui aussi utilisé par des mathématiciens pour formaliser des théorèmes récents — un sujet de recherche très actif.

05 / Hoare

Rédiger une preuve complète : BFS trouve le plus court chemin

La rédaction attendue en concours

Terminaison. Chaque sommet est ajouté à la file au plus une fois (on l’ajoute seulement s’il n’est pas dans dist, et on l’y met aussitôt). Le nombre d’extractions est donc ≤ |S| : la boucle termine.

Correction. Montrons par récurrence sur les extractions que (I1) tient. Initialement dist = {s: 0} : vrai. Supposons (I1)-(I3) avant l’extraction de u, de distance k. Pour un voisin v non encore vu : d(s, v) ≤ k + 1 via u. Si d(s, v) ≤ k, alors par (I3) v serait déjà dans dist : contradiction. Donc d(s, v) = k + 1 = dist[v]. (I2) reste vrai car on n’ajoute que des sommets de distance k + 1 en queue. À la fin, tout sommet accessible a été atteint (sinon considérer le premier sommet non atteint d’un plus court chemin : son prédécesseur a été extrait et l’aurait ajouté). ∎

Cette structure — invariants, variant, récurrence, argument « premier élément qui échoue » — est celle de toutes les preuves d’algorithmes de graphes (Dijkstra : « le sommet extrait a sa distance définitive »).

Cours

Cours 1 — Rédiger une preuve : structure, vocabulaire, erreurs classiques

Type de preuve	Schéma	Quand l’utiliser
Directe	Hypothèses ⇒ … ⇒ conclusion	Par défaut
Par contraposée	Pour montrer P ⇒ Q, montrer ¬Q ⇒ ¬P	Quand ¬Q donne plus de prise (« si n² est pair alors n est pair »)
Par l’absurde	Supposer ¬conclusion, dériver une contradiction	Existence, unicité, impossibilité (arrêt, √2)
Par récurrence (simple, forte, structurelle)	Base + hérédité	Propriétés indexées par un entier ou une structure
Par disjonction de cas	Cas 1, cas 2, …, exhaustifs	Quand une condition sépare les situations (filtrage OCaml)
Par invariant / variant	Initialisation, conservation, conclusion ; décroissance	Boucles et algorithmes itératifs
Par argument d’échange	Transformer une solution optimale sans perte	Gloutons (L04)
Par « premier élément qui échoue »	Considérer le plus petit contre-exemple	Parcours de graphes (L05), minimalité

Les mots qui comptent. « Soit x » (on prend un élément quelconque : prouve un ∀) ; « il existe » (on exhibe ou on construit) ; « supposons » (hypothèse de récurrence ou d’absurde : à refermer explicitement) ; « donc », « car », « d’où » (chaque étape justifiée par une hypothèse, une définition, un résultat antérieur). Une preuve se termine par la phrase de conclusion et ∎.

Erreurs qui coûtent tous les points. Prouver la réciproque au lieu de l’énoncé ; utiliser la conclusion dans la preuve (circularité) ; oublier le cas de base ; hérédité qui ne marche pas pour n = 0 ou 1 (la fameuse preuve que « tous les chevaux ont la même couleur ») ; « c’est évident » à l’endroit précis où ça ne l’est pas ; confondre « pour tout x, il existe y » et « il existe y, pour tout x ».

Cours

Cours 2 — Exemple travaillé : prouver l’exponentiation rapide de A à Z

def puissance(x, n):            # précondition : n entier ≥ 0
    r, b, e = 1, x, n
    while e > 0:
        if e % 2 == 1:
            r = r * b
        b = b * b
        e = e // 2
    return r                    # postcondition : r = x^n

Invariant I : r · b^e = xⁿ et e ≥ 0.

Initialisation. Avant le premier tour : r = 1, b = x, e = n, donc r · b^e = xⁿ. ✓

Conservation. Supposons I vrai en début de tour avec e > 0. Notons r′, b′, e′ les valeurs en fin de tour. Deux cas. e pair : r′ = r, b′ = b², e′ = e/2, donc r′ · b′^e′ = r · b^2·e/2 = r · b^e = xⁿ. e impair : r′ = r·b, b′ = b², e′ = (e−1)/2, donc r′ · b′^e′ = r · b · b^e−1 = r · b^e = xⁿ. Dans les deux cas e′ ≥ 0. ✓

Terminaison. Variant e : entier ≥ 0, et e′ = ⌊e/2⌋ < e dès que e > 0. ✓

Conclusion. À la sortie, e = 0 et I donne r · b⁰ = r = xⁿ. ∎

Complexité. e est divisé par 2 à chaque tour : au plus ⌊log₂ n⌋ + 1 tours, chacun avec au plus 2 multiplications : O(log n) multiplications. (Sur de grands entiers, chaque multiplication coûte elle-même — module L04.)

Cours

Cours 3 — Spécifier avant de prouver : contrats, et ce qu’un outil peut vérifier

Le contrat d’une fonction (Meyer, « design by contract ») : pré (ce que l’appelant garantit), post (ce que la fonction garantit), invariants de classe (toujours vrais entre deux appels de méthode). Violer la pré est un bug de l’appelant ; violer la post un bug de la fonction. En Python, les assert en entrée et sortie matérialisent le contrat ; en Ada/SPARK, Eiffel, Dafny, ils font partie du langage et sont vérifiés statiquement.

// Dafny : le vérificateur prouve automatiquement (ou demande des indices)
method Dichotomie(t: array<int>, x: int) returns (i: int)
  requires forall a, b :: 0 <= a < b < t.Length ==> t[a] <= t[b]      // pré : trié
  ensures 0 <= i < t.Length ==> t[i] == x                              // post : si trouvé, c'est x
  ensures i == -1 ==> forall k :: 0 <= k < t.Length ==> t[k] != x       // post : si -1, x absent
{
  var bas, haut := 0, t.Length;
  while bas < haut
    invariant 0 <= bas <= haut <= t.Length
    invariant forall k :: 0 <= k < t.Length && t[k] == x ==> bas <= k < haut
    decreases haut - bas
  {
    var m := (bas + haut) / 2;
    if t[m] < x { bas := m + 1; } else if t[m] > x { haut := m; } else { return m; }
  }
  return -1;
}

Le vérificateur (Z3 derrière) prouve initialisation, conservation, terminaison et postcondition ; si vous vous trompez dans l’invariant, il refuse et montre l’étape qui coince. Essayez en ligne (dafny.org, « Try Dafny ») : c’est la version exécutable du module L09, et un excellent moyen de tester vos invariants avant de les rédiger.

Outil	Ce qu’il vérifie	Effort
Types (mypy, OCaml)	Cohérence des types	Nul à faible
Analyse statique (ruff, Frama-C pour C)	Bugs de forme, débordements (Frama-C/Eva)	Faible
Tests par propriétés (Hypothesis)	Invariants sur des entrées aléatoires	Faible
Vérification déductive (Dafny, Why3, SPARK)	Contrats prouvés pour toutes les entrées	Moyen à élevé
Assistants de preuve (Coq, Lean, Isabelle)	Tout, y compris les mathématiques	Élevé
Vérification de modèles (TLA+, SPIN)	Protocoles, concurrence, machines à états	Moyen

TP guidé

TP — Prouver avec un outil : Dafny, puis Lean (sur PC, 2 h 30)

Dafny en ligne. Ouvrez « Try Dafny » (ou VS Code + extension Dafny). Copiez la dichotomie du cours 3 ; vérifiez qu’elle passe (coche verte). Supprimez l’invariant sur bas ≤ k < haut : lisez l’erreur (« postcondition might not hold »). Remettez-le, puis remplacez bas := m + 1 par bas := m : Dafny signale la non-terminaison (« decreases might not decrease »). Notez les trois messages.
Prouver vos algorithmes. Écrivez en Dafny avec contrats et invariants : Maximum (postcondition : ≥ tous les éléments et présent), SommePrefixe, Puissance (cours 2), TriInsertion (postcondition : trié et permutation — utilisez multiset(t[..]) == multiset(old(t[..]))). Chaque preuve acceptée est un invariant que vous avez trouvé vous-même.
Lean, les nombres. Faites les 3 premiers mondes du « Natural Number Game » (adam.math.hhu.de) : addition, multiplication, récurrence. Vous prouvez 0 + n = n, la commutativité, etc., avec les tactiques induction, rw, simp. C’est la récurrence du cours, vérifiée par la machine.
Lean sur PC (optionnel). Installer via elan + VS Code « Lean 4 » ; créer un projet ; prouver theorem somme_pairs (n : ℕ) : 2 ∣ n * (n + 1) et un lemme sur les listes (List.length (l ++ m) = l.length + m.length) par induction structurelle.
Retour au Python. Pour chaque fonction prouvée en Dafny, réécrivez-la en Python avec les invariants en assert et un test Hypothesis. Comparez : ce que Dafny garantit pour toutes les entrées, Hypothesis ne fait que l’échantillonner.
Livrable. Les fichiers .dfy vérifiés (captures des coches vertes), les captures du Natural Number Game, et une page : « ce que j’ai dû ajouter comme invariant pour que la machine accepte, et pourquoi ».

Exercices

Exercices auto-corrigés — logique et quantificateurs

Exercice 1 — Vérifier des équivalences par table de vérité

Écrivez equivalentes(f, g, n) qui teste si deux formules booléennes à n variables sont équivalentes sur les 2ⁿ valuations, puis tautologie(f, n). Ensuite complétez le dictionnaire verdicts (True = équivalence valide).

Correction

def equivalentes(f, g, n): return all(f(*v) == g(*v) for v in product([False, True], repeat=n))
def tautologie(f, n): return all(f(*v) for v in product([False, True], repeat=n))
# True, True, False, True, True (la dernière est la loi de Peirce, valide en logique classique)

Exercice 2 — Écrire des propriétés avec des quantificateurs

Implémentez chaque propriété comme une fonction booléenne sur une liste, avec all/any exactement comme la formule le dit.

Correction

def strictement_croissante(t): return all(t[i] < t[i + 1] for i in range(len(t) - 1))
def a_un_doublon(t): return any(t[i] == t[j] for i in range(len(t)) for j in range(i + 1, len(t)))
def est_permutation_de(t, u): return all(t.count(x) == u.count(x) for x in set(t) | set(u))
def chaque_element_a_un_plus_grand(t): return all(any(t[j] > t[i] for j in range(len(t))) for i in range(len(t)))
def existe_un_majorant(t): return any(all(t[j] >= t[i] for i in range(len(t))) for j in range(len(t)))

Exercices

Exercices auto-corrigés — invariants et variants

Exercice 3 — Trouver l’invariant qui rend le test vert

Chaque fonction a un trou INV = … : une expression booléenne, évaluée avant chaque tour, qui doit être vraie à tous les tours et suffisante pour prouver la postcondition (elle est vérifiée en sortie combinée à la négation de la condition). Écrivez-la avec les variables du programme.

Correction

INV = r * r <= n                 # et à la sortie : (r+1)² > n, d'où la postcondition
INV2 = gcd(a, b) == gcd(a0, b0)  # invariant d'Euclide : le PGCD est conservé ; à la sortie b = 0 donc gcd(a, 0) = a

Exercice 4 — Variant et terminaison

Pour chaque boucle, donnez un variant (expression entière ≥ 0 strictement décroissante) sous forme de fonction des variables ; la cellule vérifie qu’il décroît strictement et reste ≥ 0 sur des exécutions.

def variant_binaire(bas, haut): return ...          # boucle « while bas < haut: m = (bas+haut)//2 ; bas = m+1 ou haut = m »
def variant_collatz_borne(n, k): return ...         # boucle « while n != 1 and k < 1000: n = …; k += 1 » (variant simple grâce à la borne)
def variant_deux_indices(i, j): return ...          # boucle « while i < j: i += 1 ; j -= 1 »
# à vous

import random
def verifier(variant, etats):
    v = [variant(*e) for e in etats]
    assert all(x >= 0 for x in v) and all(a > b for a, b in zip(v, v[1:])), v
for _ in range(50):
    bas, haut, etats = 0, random.randint(1, 100), []
    x = random.randint(0, 100)
    while bas < haut:
        etats.append((bas, haut)); m = (bas + haut) // 2
        if m < x: bas = m + 1
        else: haut = m
    verifier(variant_binaire, etats)
n, k, etats = 27, 0, []
while n != 1 and k < 1000: etats.append((n, k)); n = n // 2 if n % 2 == 0 else 3 * n + 1; k += 1
verifier(variant_collatz_borne, etats)
i, j, etats = 0, 15, []
while i < j: etats.append((i, j)); i += 1; j -= 1
verifier(variant_deux_indices, etats)
print("✔ exercice 4 réussi")

Correction

def variant_binaire(bas, haut): return haut - bas
def variant_collatz_borne(n, k): return 1000 - k
def variant_deux_indices(i, j): return j - i

06 / Défis

Défi ★ — Invariants à compléter

Consigne

Pour chacune de ces fonctions, écrivez l’invariant de boucle en commentaire, ajoutez l’assert correspondant, identifiez le variant, puis rédigez les trois étapes de la preuve. 1) inverser(t) qui inverse une liste en place avec deux indices ; 2) puissance(x, n) par multiplications successives ; 3) compter(t, x).

Correction

# inverser : soit T la liste d'origine.
# INVARIANT : t[:i] == T[len−i:][::-1]  et  t[j+1:] == T[:len−j−1][::-1]  et  t[i:j+1] == T[i:j+1]
#             (les extrémités déjà échangées, le milieu intact)
# VARIANT : j − i. Conclusion : i ≥ j ⇒ tout est échangé (le milieu a ≤ 1 élément).
# puissance :
# INVARIANT : r == x ** k  et  0 ≤ k ≤ n. Init : 1 == x**0. Conservation : r·x == x**(k+1).
# Conclusion : k == n ⇒ r == x**n. VARIANT : n − k.

06 / Défis

Défi ★★ — Trouver le bug par l’invariant

Consigne

Cette fonction est censée partitionner une liste autour d’un pivot (tri rapide) : à la fin, tous les éléments < pivot sont avant l’indice renvoyé, les ≥ après. Écrivez l’invariant attendu (« t[lo..i[ < pivot, t[i..j[ ≥ pivot, t[j..hi[ pas encore vus »), ajoutez-le en assert, trouvez le tour où il casse, corrigez, puis écrivez le tri rapide complet avec preuve de terminaison (variant : hi − lo, et il faut que chaque sous-appel soit strictement plus petit — attention aux listes d’éléments tous égaux !).

Correction

def partition(t, lo, hi):
    pivot = t[hi - 1]; i = lo
    for j in range(lo, hi - 1):
        # INVARIANT : ∀k∈[lo,i[ t[k] < pivot ; ∀k∈[i,j[ t[k] ≥ pivot
        assert all(t[k] < pivot for k in range(lo, i)) and all(t[k] >= pivot for k in range(i, j))
        if t[j] < pivot:
            t[i], t[j] = t[j], t[i]; i += 1          # i += 1 SEULEMENT après un échange
    t[i], t[hi - 1] = t[hi - 1], t[i]                # placer le pivot
    return i

def tri_rapide(t, lo=0, hi=None):
    if hi is None: hi = len(t)
    if hi - lo > 1:
        p = partition(t, lo, hi)      # p ∈ [lo, hi[ : les deux sous-intervalles sont strictement plus petits
        tri_rapide(t, lo, p); tri_rapide(t, p + 1, hi)
    return t
import random
for _ in range(300):
    l = [random.randint(0, 5) for _ in range(random.randint(0, 20))]
    assert tri_rapide(list(l)) == sorted(l)
print("OK")

Le bug : i += 1 inconditionnel. L’invariant casse dès le premier élément ≥ pivot. Terminaison : après partition, le pivot est à sa place définitive en p ; les appels portent sur [lo, p[ et [p+1, hi[, de taille < hi − lo. Sans le placement du pivot hors des sous-appels, une liste de valeurs égales donnerait p = lo et une récursion infinie.

06 / Défis

Défi ★★★ — Esprit prépa : preuve de Dijkstra et exponentiation rapide

Consigne

1) Pour l’exponentiation rapide itérative du module L04 (while n: if n & 1: r = r·x ; x = x·x ; n >>= 1), trouvez l’invariant qui lie r, x, n à la valeur cherchée x₀^n₀, écrivez-le en assert, prouvez. 2) Pour Dijkstra, énoncez précisément l’invariant « pour tout sommet extrait u, dist[u] = d(s, u) », et rédigez la preuve par l’absurde (considérer un plus court chemin vers u et le premier sommet de ce chemin non encore extrait). 3) Montrez par un contre-exemple que l’invariant est faux avec un poids négatif, et dites quelle étape de la preuve utilise la positivité.

Correction

# 1) INVARIANT : r · x**n == x0**n0   (et n ≥ 0). VARIANT : n.
#    Init : 1 · x0**n0. Si n pair : r · (x²)**(n/2) = r · x**n. Si n impair : (r·x) · (x²)**((n−1)/2) = r · x**n. ✓
#    Sortie : n = 0 ⇒ r = x0**n0. ✓
# 2) Dijkstra. INVARIANT : (a) pour tout u extrait, dist[u] = d(s,u) ; (b) pour tout v non extrait,
#    dist[v] = longueur du plus court chemin de s à v n'utilisant que des sommets extraits comme intermédiaires.
#    Soit u le sommet extrait (dist minimal parmi les non extraits). Supposons d(s,u) < dist[u]. Sur un plus court
#    chemin s → … → u, soit y le premier sommet non extrait, x son prédécesseur (extrait). Par (b), dist[y] ≤
#    dist[x] + w(x,y) = d(s,y) ≤ d(s,u) < dist[u] (poids ≥ 0 pour la 2e inégalité). Donc dist[y] < dist[u] :
#    contradiction avec le choix de u comme minimum. ∎
# 3) A→B (5), A→C (2), C→B (−4) : Dijkstra extrait C (2) puis B (5) alors que d(A,B) = −2.
#    L'étape « d(s,y) ≤ d(s,u) » suppose que le reste du chemin (y → u) est de longueur ≥ 0.

07 / Vérification

Qu’est-ce qu’un variant de boucle ?

Deux questions supplémentaires

1. Pourquoi les tests ne remplacent-ils pas une preuve ? Ils couvrent un nombre fini d’entrées ; la preuve couvre toutes les entrées vérifiant la précondition.

2. Quelle est la négation de « tous les capteurs répondent en moins de 10 ms » ? « Il existe un capteur qui répond en 10 ms ou plus ».

Référence

Les mots à retenir

Mot	Définition
Tautologie	Formule vraie pour toute valuation.
Contraposée	(p → q) ≡ (¬q → ¬p) ; ne pas confondre avec la réciproque.
Récurrence forte	Supposer P(k) pour tous k < n.
Récurrence structurelle	Récurrence sur la construction d’une donnée (liste, arbre).
Précondition / postcondition	Ce qu’on suppose en entrée / ce qu’on garantit en sortie.
Invariant	Propriété vraie avant chaque tour de boucle (correction).
Variant	Quantité bien fondée strictement décroissante (terminaison).
Correction partielle / totale	Juste si ça termine / juste et termine.
Triplet de Hoare	{P} C {Q}.
Assistant de preuve	Coq, Lean, Isabelle… : vérification mécanique des preuves.

Pour continuer

Vous prouvez ce que vous codez

Module suivant : l’algèbre linéaire numérique — vecteurs, matrices, systèmes linéaires, moindres carrés, valeurs propres — avec NumPy, pour la robotique et l’IA.

À faire chez soi

Prouver la correction et la terminaison du tri fusion, du tri par tas et de Kruskal.
Faire les 3 premiers chapitres de Software Foundations (Coq) ou le tutoriel « Natural Number Game » (Lean).
Prendre un sujet MP2I de preuve de programme et le rédiger entièrement.

← L08 Sommaire L10 : Algèbre linéaire numérique →