Formation Lean : Assistant de preuve

Programme de notre formation Lean

[Jour 1 – Matin]

Prise en main de Lean et du workflow de preuve

• Installer Lean 4 et l’environnement (VS Code, extension Lean, lake)
• Comprendre la boucle : objectifs, tactiques, messages d’erreur, recherche
• Manipuler les bases : Prop, Type, variables, implicites, notations
• Écrire des preuves simples : by, intro, exact, apply
• Atelier pratique : Configurer un projet Lean et prouver des implications élémentaires.

[Jour 1 – après-midi]

Logique propositionnelle : connecteurs et tactiques essentielles

• Conjonction/disjonction : constructor, cases, left/right
• Négation et contradiction : by_contra, contradiction, exfalso
• Égalité : rfl, simp, réécriture avec rw
• Structurer une preuve : have, let, sous-preuves et lisibilité
• Atelier pratique : Prouver une série de lemmes de logique (de Morgan, contraposée) avec simp et rw.

[Jour 2 – Matin]

Quantificateurs et preuves sur les types de base

• Quantificateurs : ∀ (intro), ∃ (exists), extraction par cases
• Fonctions et lambda : preuves sur des fonctions, extensionalité (funext)
• Raisonnement sur Nat : calcul, inégalités simples, normalisation par simp
• Utiliser la bibliothèque : trouver un lemme, naviguer dans Mathlib, #check, #find
• Atelier pratique : Formaliser des énoncés avec ∀/∃ et prouver des propriétés simples sur Nat.

[Jour 2 – Après-midi]

Induction et preuves structurées

• Induction sur Nat : induction, cas base, hypothèse d’induction
• Récursion et définitions : écrire des fonctions et prouver leurs propriétés
• Chaînage de réécritures : calc, ring (si disponible), simplifications ciblées
• Gestion des objectifs : simp?, aesop (si activé), stratégies de débogage
• Atelier pratique : Prouver par induction des propriétés classiques (somme, double, associativité sur Nat).

[Jour 3 – Matin]

Structures, types inductifs et preuves par cas

• Types inductifs : définition, constructeurs, élimination par cases
• Listes : nil/cons, preuves par induction sur List
• Structures et records : champs, projections, égalité de structures
• Automatisation raisonnable : règles simp, attributs, lemmes auxiliaires
• Atelier pratique : Définir une fonction sur listes et prouver une propriété (longueur, append, map).

[Jour 3 – Après-midi]

Mini-projet : formaliser un énoncé et produire une preuve robuste

• Choisir un énoncé réaliste (logique + induction) et le découper en lemmes
• Écrire une preuve maintenable : noms, sections, commentaires, factorisation
• Stabiliser avec simp/rw : éviter les boucles et les réécritures fragiles
• Revue et amélioration : lisibilité, performance, dépendances minimales
• Atelier pratique : Réaliser un mini-projet complet (spécification, lemmes, preuve finale) et le présenter.