Lean 5 - Mode Tactique

Navigation : ← Lean-04-Quantifiers-Lean | Index | Lean-06-Mathlib-Essentials-Lean →

---

Introduction

Jusqu’ici, nous avons construit des preuves en ecrivant directement des termes de preuve. Cette approche, bien que fondamentale, peut devenir fastidieuse pour des preuves complexes.

Le mode tactique offre une approche alternative : au lieu de construire le terme de preuve directement, on manipule des buts (goals) de maniere interactive jusqu’a ce que la preuve soit complète.

Objectifs d’apprentissage

1. Comprendre le mode tactique et la notion de but
2. Maitriser les tactiques de base : apply, exact, intro, rfl
3. Gerer le contexte avec have, let, show
4. Utiliser l’analyse par cas avec cases et split
5. Reecrire avec rw et simplifier avec simp
6. Structurer les preuves avec points et combinateurs

Prerequis

• Notebooks Lean-1 a Lean-4 completes
• Comprendre la construction de preuves par termes

Duree estimée : 50-60 minutes

---

Le Paradigme Tactique

Termes vs Tactiques

Mode terme	Mode tactique
Construction directe	Construction guidee
Top-down (résultat -> composants)	Bottom-up (buts -> sous-buts)
Compact	Lisible étape par étape
Difficulte : voir la structure globale	Difficulte : verbeux

Le mot-cle by introduit le mode tactique.

1. Introduction au Mode Tactique

1.1 Le mot-cle by

On entre en mode tactique avec by. L’état de preuve contient : - Le but (goal) : la proposition a prouver - Le contexte : les hypotheses disponibles

-- Meme theoreme, deux styles

-- Style terme
theorem impl_refl_term (p : Prop) : p -> p :=
  fun hp => hp

-- Style tactique
theorem impl_refl_tactic (p : Prop) : p -> p := by
  intro hp      -- Introduire l'hypothese hp : p
  exact hp      -- Fournir exactement hp comme preuve

#check impl_refl_term   -- impl_refl_term : (p : Prop) -> p -> p
#check impl_refl_tactic -- meme type

-- Meme theoreme, deux styles

-- Style terme

theorem impl_refl_term (p : Prop) : p -> p :=

  fun hp => hp

-- Style tactique

theorem impl_refl_tactic (p : Prop) : p -> p := by

  intro hp      -- Introduire l'hypothese hp : p

  exact hp      -- Fournir exactement hp comme preuve

#check impl_refl_term   -- impl_refl_term : (p : Prop) -> p -> p
 impl_refl_term (p : Prop) : p → p

#check impl_refl_tactic -- meme type
 impl_refl_tactic (p : Prop) : p → p

--% env 0

Raw input

{"cmd": "-- Meme theoreme, deux styles\n\n-- Style terme\ntheorem impl_refl_term (p : Prop) : p -> p :=\n fun hp => hp\n\n-- Style tactique\ntheorem impl_refl_tactic (p : Prop) : p -> p := by\n intro hp -- Introduire l'hypothese hp : p\n exact hp -- Fournir exactement hp comme preuve\n\n#check impl_refl_term -- impl_refl_term : (p : Prop) -> p -> p\n#check impl_refl_tactic -- meme type"}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "impl_refl_term (p : Prop) : p → p"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 6}, "data": "impl_refl_tactic (p : Prop) : p → p"}], "env": 0}

1.2 L’état de preuve

A chaque étape, Lean affiche l’état de preuve : - context : les hypotheses disponibles (au-dessus de la barre) - goal : ce qu’il reste a prouver (en-dessous de la barre)

p : Prop
hp : p
⊢ p          <-- le but courant

-- Exemple avec plusieurs buts
theorem and_intro_tactic (p q : Prop) (hp : p) (hq : q) : p /\ q := by
  -- But initial : ⊢ p /\ q
  constructor   -- Divise en deux buts : ⊢ p et ⊢ q
  -- Premier but : ⊢ p
  exact hp
  -- Deuxieme but : ⊢ q
  exact hq

-- Exemple avec plusieurs buts

theorem and_intro_tactic (p q : Prop) (hp : p) (hq : q) : p /\ q := by

  -- But initial : ⊢ p /\ q

  constructor   -- Divise en deux buts : ⊢ p et ⊢ q

  -- Premier but : ⊢ p

  exact hp

  -- Deuxieme but : ⊢ q

  exact hq

--% env 1

Raw input

{"cmd": "-- Exemple avec plusieurs buts\ntheorem and_intro_tactic (p q : Prop) (hp : p) (hq : q) : p /\\ q := by\n -- But initial : \u22a2 p /\\ q\n constructor -- Divise en deux buts : \u22a2 p et \u22a2 q\n -- Premier but : \u22a2 p\n exact hp\n -- Deuxieme but : \u22a2 q\n exact hq", "env": 0}

Raw output

{"env": 1}

2. Tactiques de Base

2.1 exact : fournir le terme exact

Si on a un terme t de type exactement egal au but, exact t ferme le but.

Pourquoi cette tactique ouvre le chapitre ? Dans Lean, prouver une proposition P revient a construire un terme de type P : c’est la correspondance de Curry-Howard, le coeur du langage. exact t est la tactique la plus directe : elle dit « le terme qui prouve le but existe déjà, le voici ». Elle ne reflechit pas, ne transforme pas : elle vérifie que le type de t coincide avec le but, puis clot. C’est la tactique de fin de preuve — après intro, apply, cases ou constructor, on aboutit presque toujours a un but simple qu’un exact règle.

Comment lire le message de Lean ? Quand le terme fourni n’a pas le bon type, Lean repond type mismatch : relisez alors la ligne ⊢, elle dit exactement ce qu’il reste a prouver. Si la reponse est unsolved goals, c’est qu’il reste d’autres buts — un exact n’en clos qu’un a la fois. Cette lecture de l’état de preuve (section 1.2) est la competence centrale du notebook : c’est elle qui rendra lisibles les preuves des notebooks appliques, comme Lean-14-Finiteness-Derivatives, dont les théorèmes s’achevent par des termes précis fournis au by.

L’exemple exact_example est volontairement minimal : hp : p a exactement le type du but p, donc exact hp est une preuve complète. exact_calc montre que la vérification inclut le calcul : 2 + 2 se reduit a 4, et l’égalité est produite par rfl (section 2.5) — exact accepte donc aussi les égalités calculables.

theorem exact_example (p : Prop) (hp : p) : p := by
  exact hp   -- hp a exactement le type du but

-- Avec un calcul
theorem exact_calc : 2 + 2 = 4 := by
  exact rfl  -- rfl prouve une egalite par calcul

theorem exact_example (p : Prop) (hp : p) : p := by

  exact hp   -- hp a exactement le type du but

-- Avec un calcul

theorem exact_calc : 2 + 2 = 4 := by

  exact rfl  -- rfl prouve une egalite par calcul

--% env 2

Raw input

{"cmd": "theorem exact_example (p : Prop) (hp : p) : p := by\n exact hp -- hp a exactement le type du but\n\n-- Avec un calcul\ntheorem exact_calc : 2 + 2 = 4 := by\n exact rfl -- rfl prouve une egalite par calcul", "env": 1}

Raw output

{"env": 2}

2.2 intro : introduction d’hypotheses

intro fonctionne pour : - Les implications P -> Q : introduit une hypothese de type P - Les forall \forall x, P x : introduit une variable x

Ce que construit intro. Une implication P -> Q EST une fonction : sa preuve prend une preuve de P et retourne une preuve de Q. intro hp transforme donc le but P -> Q en « hypothese hp : P ajoutee au contexte, but restant Q » — exactement comme fun hp => ... dans un terme. De même, \forall x, P x est une fonction dependante : intro x ajoute la variable x au contexte et le but devient P x. Cette correspondance fait le pont avec exact (section 2.1) : intro fabrique le debut du terme de preuve, exact en fournit la fin.

Nombre et ordre. Chaque intro consomme une premisse, dans l’ordre. intro hp hq les introduit d’un coup — la forme a préférer quand le contexte a ajouter est evident ; sinon, on introduit au fur et a mesure pour garder un contexte lisible. Dans intro_impl, le but p -> q -> p est decompose en deux implications successives : intro hp donne hp : p et le but q -> p, puis intro hq donne hq : q et le but p, clos par exact hp.

Que lit-on ? Après intro, le contexte affiche la nouvelle hypothese avec son type (hp : p), et le ⊢ change : c’est la trace de la tactique. Si intro echoue, c’est que le but n’est ni une implication ni un forall — il est déjà « pointe vers le résultat » et une autre tactique est necessaire.

-- Introduction d'implication
theorem intro_impl (p q : Prop) : p -> q -> p := by
  intro hp     -- hp : p ajoute au contexte, but devient q -> p
  intro hq     -- hq : q ajoute, but devient p
  exact hp

-- intro multiple
theorem intro_multi (p q : Prop) : p -> q -> p := by
  intro hp hq  -- Introduit les deux d'un coup
  exact hp

-- Introduction de forall
theorem intro_forall : forall n : Nat, n + 0 = n := by
  intro n      -- n : Nat ajoute au contexte
  rfl          -- Preuve par reflexivite (calcul)

-- Introduction d'implication

theorem intro_impl (p q : Prop) : p -> q -> p := by

  intro hp     -- hp : p ajoute au contexte, but devient q -> p

  intro hq     -- hq : q ajoute, but devient p

  exact hp

-- intro multiple

theorem intro_multi (p q : Prop) : p -> q -> p := by

  intro hp hq  -- Introduit les deux d'un coup

  exact hp

-- Introduction de forall

theorem intro_forall : forall n : Nat, n + 0 = n := by

  intro n      -- n : Nat ajoute au contexte

  rfl          -- Preuve par reflexivite (calcul)

--% env 3

Raw input

{"cmd": "-- Introduction d'implication\ntheorem intro_impl (p q : Prop) : p -> q -> p := by\n intro hp -- hp : p ajoute au contexte, but devient q -> p\n intro hq -- hq : q ajoute, but devient p\n exact hp\n\n-- intro multiple\ntheorem intro_multi (p q : Prop) : p -> q -> p := by\n intro hp hq -- Introduit les deux d'un coup\n exact hp\n\n-- Introduction de forall\ntheorem intro_forall : forall n : Nat, n + 0 = n := by\n intro n -- n : Nat ajoute au contexte\n rfl -- Preuve par reflexivite (calcul)", "env": 2}

Raw output

{"env": 3}

2.3 apply : appliquer un lemme/hypothese

Si on a h : A -> B et le but est B, alors apply h change le but en A.

Le sens de la marche. apply travaille a rebours, du but vers les hypotheses (raisonnement backward) : au lieu de construire le terme complet d’un coup comme exact, il reduit le but a une precondition plus simple. h : A -> B dit « pour obtenir B, il suffit de fournir A » — apply h traduit donc le but ⊢ B en ⊢ A. C’est le modus ponens lu dans le sens de la recherche de preuve, et c’est la tactique de decomposition des enonces composees.

Plusieurs premisses. Si h : A -> B -> C et le but est C, apply h genere deux buts : ⊢ A et ⊢ B, traites ensuite independamment — par un autre apply, un intro, ou un exact. C’est ainsi que se decomposent les théorèmes longs : apply transforme une cible complexe en une liste de sous-buts simples, exactement la mecanique qu’on retrouve dans les preuves de Lean-13-Kochen-Specker.

apply vs exact. exact exige le terme complet ; apply construit la preuve par étapes, en laissant Lean reorganiser les premisses. En pratique on les enchaîne : des apply pour decomposer, un exact pour conclure — cette paire se retrouve a la fin de presque toutes les preuves du notebook.

-- apply reduit le but
theorem apply_example (p q r : Prop)
  (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by
  apply hqr    -- But : r devient q (car hqr : q -> r)
  apply hpq    -- But : q devient p
  exact hp     -- hp a type p

-- apply avec plusieurs arguments
theorem apply_multi (p q r : Prop)
  (hpqr : p -> q -> r) (hp : p) (hq : q) : r := by
  apply hpqr   -- Cree deux buts : p et q
  exact hp
  exact hq

-- apply reduit le but

theorem apply_example (p q r : Prop)

  (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by

  apply hqr    -- But : r devient q (car hqr : q -> r)

  apply hpq    -- But : q devient p

  exact hp     -- hp a type p

-- apply avec plusieurs arguments

theorem apply_multi (p q r : Prop)

  (hpqr : p -> q -> r) (hp : p) (hq : q) : r := by

  apply hpqr   -- Cree deux buts : p et q

  exact hp

  exact hq

--% env 4

Raw input

{"cmd": "-- apply reduit le but\ntheorem apply_example (p q r : Prop)\n (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by\n apply hqr -- But : r devient q (car hqr : q -> r)\n apply hpq -- But : q devient p\n exact hp -- hp a type p\n\n-- apply avec plusieurs arguments\ntheorem apply_multi (p q r : Prop)\n (hpqr : p -> q -> r) (hp : p) (hq : q) : r := by\n apply hpqr -- Cree deux buts : p et q\n exact hp\n exact hq", "env": 3}

Raw output

{"env": 4}

2.4 assumption : chercher dans le contexte

La tactique assumption cherche automatiquement dans le contexte une hypothese qui correspond exactement au but courant. C’est un raccourci pratique quand la preuve est déjà dans les hypotheses.

Le pendant de exact. Si exact dit « voici le terme nomme », assumption dit « trouve le terme tout seul ». Elle parcourt le contexte et, si une hypothese a exactement le type du but, elle la fournit et clot. Dans assumption_example, hp : p est dans le contexte et le but est p : l’appariement est immediat, la preuve est complète.

Pourquoi s’en servir ? La robustesse au renommage : si l’on modifie plus tard les noms des hypotheses (en changeant l’ordre des arguments d’un théorème, par exemple), un exact hp casse alors qu’un assumption survit — il ne depend pas d’un nom, seulement d’un type. On l’utilise donc pour les conclusions « evidentes depuis le contexte », notamment en fin de chaîne : dans assumption_chain, après deux apply, le but restant p est exactement hp, et assumption le clot sans qu’on ait a nommer quoi que ce soit.

Quand echoue-t-elle ? Quand aucune hypothese n’a exactement le type du but. Une hypothese h : A -> B n’est pas une preuve de B : il faut d’abord apply h. L’echec est instructif — il dit que le but n’est pas déjà la : il reste du travail de transformation avant qu’une hypothese ne s’applique directement.

-- assumption trouve automatiquement l'hypothese
theorem assumption_example (p q : Prop) (hp : p) (hq : q) : p := by
  assumption   -- Trouve hp : p dans le contexte

-- Utile quand on ne veut pas nommer
theorem assumption_chain (p q r : Prop)
  (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by
  apply hqr
  apply hpq
  assumption

-- assumption trouve automatiquement l'hypothese

theorem assumption_example (p q : Prop) (hp : p) (hq : q) : p := by
🟨 unused variable `hq`

Note: This linter can be disabled with `set_option linter.unusedVariables false`

  assumption   -- Trouve hp : p dans le contexte

-- Utile quand on ne veut pas nommer

theorem assumption_chain (p q r : Prop)

  (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by

  apply hqr

  apply hpq

  assumption

--% env 5

Raw input

{"cmd": "-- assumption trouve automatiquement l'hypothese\ntheorem assumption_example (p q : Prop) (hp : p) (hq : q) : p := by\n assumption -- Trouve hp : p dans le contexte\n\n-- Utile quand on ne veut pas nommer\ntheorem assumption_chain (p q r : Prop)\n (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by\n apply hqr\n apply hpq\n assumption", "env": 4}

Raw output

{"messages": [{"severity": "warning", "pos": {"line": 2, "column": 50}, "endPos": {"line": 2, "column": 52}, "data": "unused variable `hq`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 5}

2.5 rfl : reflexivite

La tactique rfl (reflexivite) prouve les égalités triviales ou calculables. Lean reduit les deux cotes de l’égalité et vérifie qu’ils sont identiques. Fonctionne pour 2 + 2 = 4, n + 0 = n, etc.

Une égalité par définition. rfl ne prouve pas n’importe quelle égalité : elle ferme les buts de la forme t = t après reduction calculatoire (égalité definitionnelle — le noyau de Lean exécute les définitions). 2 + 2 = 5 est impossible, mais 2 + 3 = 5 : le calcul de 2 + 3 donne 5, les deux cotes sont identiques, rfl clot. C’est la tactique de la vérification arithmetique immediate, et elle intervient partout en fin de preuve, quand une chaîne de rw (section 5) aboutit a une égalité triviale.

Pourquoi n + 0 = n et pas 0 + n = n ? L’addition de Nat est définie par recurrence sur le second argument : a + 0 se reduit a a (clause de base), donc n + 0 = n est bien definitionnelle — c’est ce qui fait tourner l’exemple intro_forall de la section 2.2 avec un simple rfl. En revanche 0 + n, dont le second argument est une variable, ne peut pas se reduire : il faut le théorème Nat.zero_add, applique par rw (section 5). Cette dissymetrie — Nat.add_zero est ferme par rfl quand Nat.zero_add ne l’est pas — est un des pieges classiques du debutant Lean.

Le message d’erreur type. Si rfl echoue, Lean affiche les deux cotes de l’égalité separes : ils ne sont pas definitionnellement egaux. Ce message est une des lectures d’état les plus utiles du notebook : il dit précisément quoi chercher — un lemme de bibliotheque, une hypothese — pour combler l’ecart.

-- rfl ferme les buts de la forme t = t (apres reduction)
theorem rfl_examples : 2 + 3 = 5 := by rfl

theorem rfl_list : [1, 2, 3].length = 3 := by rfl

-- rfl echoue si pas definitionnellement egal
-- theorem fail_rfl (n : Nat) : n + 0 = n := by rfl  -- ERREUR

-- rfl ferme les buts de la forme t = t (apres reduction)

theorem rfl_examples : 2 + 3 = 5 := by rfl

theorem rfl_list : [1, 2, 3].length = 3 := by rfl

-- rfl echoue si pas definitionnellement egal

-- theorem fail_rfl (n : Nat) : n + 0 = n := by rfl  -- ERREUR

--% env 6

Raw input

{"cmd": "-- rfl ferme les buts de la forme t = t (apres reduction)\ntheorem rfl_examples : 2 + 3 = 5 := by rfl\n\ntheorem rfl_list : [1, 2, 3].length = 3 := by rfl\n\n-- rfl echoue si pas definitionnellement egal\n-- theorem fail_rfl (n : Nat) : n + 0 = n := by rfl -- ERREUR", "env": 5}

Raw output

{"env": 6}

3. Gestion du Contexte

Les tactiques de cette section permettent de manipuler le contexte de preuve : ajouter des hypotheses intermediaires, modifier le but, ou reorganiser les variables.

-- have introduit un fait intermediaire
theorem have_example (p q r : Prop)
  (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by
  have hq : q := hpq hp   -- Introduit hq : q
  have hr : r := hqr hq   -- Introduit hr : r
  exact hr

-- have avec preuve tactique
theorem have_tactic (p q : Prop) (hpq : p -> q) (hp : p) : q /\ p := by
  have hq : q := by
    apply hpq
    exact hp
  exact ⟨hq, hp⟩

-- have introduit un fait intermediaire

theorem have_example (p q r : Prop)

  (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by

  have hq : q := hpq hp   -- Introduit hq : q

  have hr : r := hqr hq   -- Introduit hr : r

  exact hr

-- have avec preuve tactique

theorem have_tactic (p q : Prop) (hpq : p -> q) (hp : p) : q /\ p := by

  have hq : q := by

    apply hpq

    exact hp

  exact ⟨hq, hp⟩

--% env 7

Raw input

{"cmd": "-- have introduit un fait intermediaire\ntheorem have_example (p q r : Prop)\n (hpq : p -> q) (hqr : q -> r) (hp : p) : r := by\n have hq : q := hpq hp -- Introduit hq : q\n have hr : r := hqr hq -- Introduit hr : r\n exact hr\n\n-- have avec preuve tactique\ntheorem have_tactic (p q : Prop) (hpq : p -> q) (hp : p) : q /\\ p := by\n have hq : q := by\n apply hpq\n exact hp\n exact \u27e8hq, hp\u27e9", "env": 6}

Raw output

{"env": 7}

3.2 let : définitions locales

La tactique let introduit une définition locale (variable avec sa valeur) dans le contexte. Utile pour nommer des expressions complexes reutilisees plusieurs fois.

Quand l’utiliser ? Dans une preuve, une même expression peut revenir plusieurs fois, ou devenir illisible une fois enchaînee dans des rw. let x := e enregistre x comme alias local de e : le contexte contient desormais x := e (avec sa valeur, pas seulement son type), et les references a x se reduisent a e quand c’est necessaire. C’est l’equivalent tactique du let du langage fonctionnel : nommer pour clarifier, sans changer la logique.

Différence avec intro. intro ajoute une hypothese (dont on ne connaît pas la valeur) ; let ajoute une définition (dont on connaît la valeur). La première sert a consommer une premisse, la seconde a organiser le raisonnement — on les combine d’ailleurs : un let pour nommer un sous-calcul, puis des rw ou un exact sur ce nom.

Lire le contexte. Après let x := e, le contexte affiche x := e — la valeur est visible, c’est ce qui distingue la définition de l’hypothese h : T, qui n’en montre pas. Quand le but contient une expression complexe repetee et que la preuve devient illisible, le reflexe let evite de la recopier et rend la preuve facile a relire — un soin qui paye dans les preuves longues des notebooks appliques comme Lean-14-Finiteness-Derivatives.

-- let pour des valeurs calculees
theorem let_example (n : Nat) : (n + 1) * 2 = 2 * n + 2 := by
  let m := n + 1     -- m = n + 1 visible dans le contexte
  -- On peut prouver manuellement avec les lemmes de Nat
  show m * 2 = 2 * n + 2
  have h1 : m * 2 = 2 * m := Nat.mul_comm m 2
  have h2 : 2 * m = 2 * (n + 1) := rfl
  have h3 : 2 * (n + 1) = 2 * n + 2 := Nat.mul_add 2 n 1
  calc m * 2 = 2 * m := h1
       _ = 2 * (n + 1) := rfl
       _ = 2 * n + 2 * 1 := Nat.mul_add 2 n 1
       _ = 2 * n + 2 := by rfl

-- let pour des valeurs calculees

theorem let_example (n : Nat) : (n + 1) * 2 = 2 * n + 2 := by

  let m := n + 1     -- m = n + 1 visible dans le contexte

  -- On peut prouver manuellement avec les lemmes de Nat

  show m * 2 = 2 * n + 2

  have h1 : m * 2 = 2 * m := Nat.mul_comm m 2

  have h2 : 2 * m = 2 * (n + 1) := rfl

  have h3 : 2 * (n + 1) = 2 * n + 2 := Nat.mul_add 2 n 1

  calc m * 2 = 2 * m := h1

       _ = 2 * (n + 1) := rfl

       _ = 2 * n + 2 * 1 := Nat.mul_add 2 n 1

       _ = 2 * n + 2 := by rfl

--% env 8

Raw input

{"cmd": "-- let pour des valeurs calculees\ntheorem let_example (n : Nat) : (n + 1) * 2 = 2 * n + 2 := by\n let m := n + 1 -- m = n + 1 visible dans le contexte\n -- On peut prouver manuellement avec les lemmes de Nat\n show m * 2 = 2 * n + 2\n have h1 : m * 2 = 2 * m := Nat.mul_comm m 2\n have h2 : 2 * m = 2 * (n + 1) := rfl\n have h3 : 2 * (n + 1) = 2 * n + 2 := Nat.mul_add 2 n 1\n calc m * 2 = 2 * m := h1\n _ = 2 * (n + 1) := rfl\n _ = 2 * n + 2 * 1 := Nat.mul_add 2 n 1\n _ = 2 * n + 2 := by rfl", "env": 7}

Raw output

{"env": 8}

3.3 show : annoter le but

La tactique show permet d’indiquer explicitement le but que l’on prouve. Utile pour la clarte ou quand Lean n’infere pas correctement le type attendu.

-- show clarifie le but (utile pour la lisibilite)
theorem show_example (p q : Prop) (hp : p) (hq : q) : q /\ p := by
  constructor
  show q        -- Annonce qu'on prouve q
  exact hq
  show p        -- Annonce qu'on prouve p
  exact hp

-- show clarifie le but (utile pour la lisibilite)

theorem show_example (p q : Prop) (hp : p) (hq : q) : q /\ p := by

  constructor

  show q        -- Annonce qu'on prouve q

  exact hq

  show p        -- Annonce qu'on prouve p

  exact hp

--% env 9

Raw input

{"cmd": "-- show clarifie le but (utile pour la lisibilite)\ntheorem show_example (p q : Prop) (hp : p) (hq : q) : q /\\ p := by\n constructor\n show q -- Annonce qu'on prouve q\n exact hq\n show p -- Annonce qu'on prouve p\n exact hp", "env": 8}

Raw output

{"env": 9}

3.4 revert : remettre dans le but

La tactique revert est l’inverse de intro : elle deplace une hypothese du contexte vers le but, transformant h : P |- Q en |- P -> Q.

-- revert est l'inverse de intro
theorem revert_example (p q : Prop) : p -> q -> p := by
  intro hp hq
  -- Contexte : hp : p, hq : q. But : p
  revert hq      -- But devient : q -> p
  intro _        -- Reintroduit (avec nom anonyme)
  exact hp

-- revert est l'inverse de intro

theorem revert_example (p q : Prop) : p -> q -> p := by

  intro hp hq

  -- Contexte : hp : p, hq : q. But : p

  revert hq      -- But devient : q -> p

  intro _        -- Reintroduit (avec nom anonyme)

  exact hp

--% env 10

Raw input

{"cmd": "-- revert est l'inverse de intro\ntheorem revert_example (p q : Prop) : p -> q -> p := by\n intro hp hq\n -- Contexte : hp : p, hq : q. But : p\n revert hq -- But devient : q -> p\n intro _ -- Reintroduit (avec nom anonyme)\n exact hp", "env": 9}

Raw output

{"env": 10}

4. Tactiques pour la Logique

4.1 constructor : introduction de structures

La tactique constructor est l’introduction générique d’un connecteur logique : elle regarde le but, identifie le constructeur principal (And, Or, Ex, Subtype, …) et le décompose en un sous-but pour chaque argument du constructeur. C’est l’inverse de exact ⟨a, b⟩ qui les rassemble en un tuple.

Fonctionnement :

1. Si le but est P ∧ Q, constructor génère deux sous-buts : ⊢ P puis ⊢ Q. Vous prouvez chacun, et Lean les recombine.
2. Si le but est P ∨ Q, constructor se ramène à Left (prouver P) — il faut alors left ou right pour choisir le côté de la disjonction (c’est 4.3).
3. Si le but est ∃ x, P x, constructor génère un sous-but ⊢ P ?y avec un ?y мета, et l’inférence de Lean trouve une valeur (souvent par unification).
4. Pour le constructeur inductif Sum, Prod, etc., la décomposition suit la même logique.

Pourquoi constructor plutôt que exact ⟨...⟩ ? En pédagogie, on voit la structure se déplier sous nos yeux : chaque sous-but est un problème plus simple, et l’écran de Lean affiche la liste au fur et à mesure. En pratique, dans une longue preuve, constructor rend visible la structure de la preuve que vous construisez.

Attention au scope de décomposition : constructor ne décompose qu’un seul niveau à la fois. Pour un but comme P ∧ Q ∧ R, il faut deux constructor successifs (ou un refine ⟨?_, ?_, ?_⟩ qui spécifie la structure complète). La tactique constructor répété deux fois est d’ailleurs le pattern dominant dans Lean-6 (Mathlib) pour les structures imbriquées.

Le pont : constructor est omniprésent dans Lean-12 (Sensitivity Theorem) sur les buts ∃ ε, ... où il faut exhiber un témoin avant de prouver la borne. Il est aussi la brique de base de refine (mode tactic), que vous croiserez à chaque preuve Mathlib.

-- constructor pour And (conjonction)
theorem and_tactic (p q : Prop) (hp : p) (hq : q) : p /\ q := by
  constructor    -- Divise en deux buts
  · exact hp     -- Premier but avec point
  · exact hq     -- Deuxieme but

-- constructor pour Iff (equivalence)
theorem iff_tactic (p q : Prop) (hpq : p -> q) (hqp : q -> p) : p <-> q := by
  constructor
  · exact hpq
  · exact hqp

-- constructor pour Exists
-- Note: Pour les preuves existentielles, la tactique `use` (Mathlib) est
-- plus pratique que constructor car elle permet de specifier le temoin.
-- Sans Mathlib, on utilise le terme de preuve directement :
theorem exists_tactic : ∃ n : Nat, n > 5 := by
  exact ⟨6, by decide⟩  -- Temoin 6, preuve que 6 > 5

-- Avec Mathlib, on ecrirait :
-- theorem exists_tactic_mathlib : ∃ n : Nat, n > 5 := by
--   use 6      -- Fournit le temoin 6
--   decide     -- Prouve 6 > 5

-- constructor pour And (conjonction)

theorem and_tactic (p q : Prop) (hp : p) (hq : q) : p /\ q := by

  constructor    -- Divise en deux buts

  · exact hp     -- Premier but avec point

  · exact hq     -- Deuxieme but

-- constructor pour Iff (equivalence)

theorem iff_tactic (p q : Prop) (hpq : p -> q) (hqp : q -> p) : p <-> q := by

  constructor

  · exact hpq

  · exact hqp

-- constructor pour Exists

-- Note: Pour les preuves existentielles, la tactique `use` (Mathlib) est

-- plus pratique que constructor car elle permet de specifier le temoin.

-- Sans Mathlib, on utilise le terme de preuve directement :

theorem exists_tactic : ∃ n : Nat, n > 5 := by

  exact ⟨6, by decide⟩  -- Temoin 6, preuve que 6 > 5

-- Avec Mathlib, on ecrirait :

-- theorem exists_tactic_mathlib : ∃ n : Nat, n > 5 := by

--   use 6      -- Fournit le temoin 6

--   decide     -- Prouve 6 > 5

--% env 11

Raw input

{"cmd": "-- constructor pour And (conjonction)\ntheorem and_tactic (p q : Prop) (hp : p) (hq : q) : p /\\ q := by\n constructor -- Divise en deux buts\n \u00b7 exact hp -- Premier but avec point\n \u00b7 exact hq -- Deuxieme but\n\n-- constructor pour Iff (equivalence)\ntheorem iff_tactic (p q : Prop) (hpq : p -> q) (hqp : q -> p) : p <-> q := by\n constructor\n \u00b7 exact hpq\n \u00b7 exact hqp\n\n-- constructor pour Exists\n-- Note: Pour les preuves existentielles, la tactique `use` (Mathlib) est\n-- plus pratique que constructor car elle permet de specifier le temoin.\n-- Sans Mathlib, on utilise le terme de preuve directement :\ntheorem exists_tactic : \u2203 n : Nat, n > 5 := by\n exact \u27e86, by decide\u27e9 -- Temoin 6, preuve que 6 > 5\n\n-- Avec Mathlib, on ecrirait :\n-- theorem exists_tactic_mathlib : \u2203 n : Nat, n > 5 := by\n-- use 6 -- Fournit le temoin 6\n-- decide -- Prouve 6 > 5", "env": 10}

Raw output

{"env": 11}

4.2 cases : analyse par cas

La tactique cases decompose une hypothese selon sa structure. Pour Or elle créé deux buts, pour And elle extrait les composantes, pour Exists elle extrait le temoin.

-- cases pour Or (disjonction)
theorem or_cases (p q r : Prop)
  (hpq : p \/ q) (hpr : p -> r) (hqr : q -> r) : r := by
  cases hpq with
  | inl hp => exact hpr hp    -- Cas p
  | inr hq => exact hqr hq    -- Cas q

-- cases pour And (destructure)
theorem and_cases (p q : Prop) (hpq : p /\ q) : q /\ p := by
  cases hpq with
  | intro hp hq => exact ⟨hq, hp⟩

-- cases pour Exists
theorem exists_cases (P : Nat -> Prop)
  (h : ∃ n, P n) : ∃ n, P n := by
  cases h with
  | intro w hw => exact ⟨w, hw⟩

-- cases pour Or (disjonction)

theorem or_cases (p q r : Prop)

  (hpq : p \/ q) (hpr : p -> r) (hqr : q -> r) : r := by

  cases hpq with

  | inl hp => exact hpr hp    -- Cas p

  | inr hq => exact hqr hq    -- Cas q

-- cases pour And (destructure)

theorem and_cases (p q : Prop) (hpq : p /\ q) : q /\ p := by

  cases hpq with

  | intro hp hq => exact ⟨hq, hp⟩

-- cases pour Exists

theorem exists_cases (P : Nat -> Prop)

  (h : ∃ n, P n) : ∃ n, P n := by

  cases h with

  | intro w hw => exact ⟨w, hw⟩

--% env 12

Raw input

{"cmd": "-- cases pour Or (disjonction)\ntheorem or_cases (p q r : Prop)\n (hpq : p \\/ q) (hpr : p -> r) (hqr : q -> r) : r := by\n cases hpq with\n | inl hp => exact hpr hp -- Cas p\n | inr hq => exact hqr hq -- Cas q\n\n-- cases pour And (destructure)\ntheorem and_cases (p q : Prop) (hpq : p /\\ q) : q /\\ p := by\n cases hpq with\n | intro hp hq => exact \u27e8hq, hp\u27e9\n\n-- cases pour Exists\ntheorem exists_cases (P : Nat -> Prop)\n (h : \u2203 n, P n) : \u2203 n, P n := by\n cases h with\n | intro w hw => exact \u27e8w, hw\u27e9", "env": 11}

Raw output

{"env": 12}

4.3 left et right : introduction de Or

Les tactiques left et right choisissent quel cote d’une disjonction prouver. left transforme le but P \/ Q en P, right le transforme en Q.

-- Choisir le cote de la disjonction
theorem left_example (p q : Prop) (hp : p) : p \/ q := by
  left           -- But devient p
  exact hp

theorem right_example (p q : Prop) (hq : q) : p \/ q := by
  right          -- But devient q
  exact hq

-- Choisir le cote de la disjonction

theorem left_example (p q : Prop) (hp : p) : p \/ q := by

  left           -- But devient p

  exact hp

theorem right_example (p q : Prop) (hq : q) : p \/ q := by

  right          -- But devient q

  exact hq

--% env 13

Raw input

{"cmd": "-- Choisir le cote de la disjonction\ntheorem left_example (p q : Prop) (hp : p) : p \\/ q := by\n left -- But devient p\n exact hp\n\ntheorem right_example (p q : Prop) (hq : q) : p \\/ q := by\n right -- But devient q\n exact hq", "env": 12}

Raw output

{"env": 13}

4.4 contradiction : detecter l’absurdite

La tactique contradiction cherche automatiquement une contradiction dans le contexte (ex: h : P et hn : Not P). Si trouvee, le but est resolu.

-- contradiction trouve p et ¬ p dans le contexte
theorem contradiction_example (p q : Prop) (hp : p) (hnp : ¬ p) : q := by
  contradiction

-- Fonctionne aussi avec False
theorem false_contradiction (p : Prop) (hf : False) : p := by
  contradiction

-- contradiction trouve p et ¬ p dans le contexte

theorem contradiction_example (p q : Prop) (hp : p) (hnp : ¬ p) : q := by

  contradiction

-- Fonctionne aussi avec False

theorem false_contradiction (p : Prop) (hf : False) : p := by

  contradiction

--% env 14

Raw input

{"cmd": "-- contradiction trouve p et \u00ac p dans le contexte\ntheorem contradiction_example (p q : Prop) (hp : p) (hnp : \u00ac p) : q := by\n contradiction\n\n-- Fonctionne aussi avec False\ntheorem false_contradiction (p : Prop) (hf : False) : p := by\n contradiction", "env": 13}

Raw output

{"env": 14}

5. Reecriture avec rw

5.1 Utilisation de base

rw [h] remplace le cote gauche de l’égalité h par le cote droit dans le but.

L’outil du raisonnement par égalités. rfl (section 2.5) prouve les égalités calculables ; rw prouve les égalités grace a des hypotheses ou des lemmes : elle substitue un cote d’une égalité par l’autre dans le but. Avec h : a = b, rw [h] remplace chaque occurrence de a par b dans le but — qui devient une égalité plus simple, souvent une trivialite qu’un rfl clot. D’ou la paire rw ... ; rfl si frequente dans les preuves : on reecrit pour ramener le but a une forme calculable, puis on laisse le calcul conclure.

Sens et direction. Le remplacement va du cote gauche vers le cote droit. Pour le sens inverse (de b vers a), on ecrit rw [← h] (la fleche se tape \l). Dans rw_rev, h : a = b et le but b = a : rw [← h] remplace b par a, le but devient a = a, clos par reflexivite.

Enchainer. rw [h1, h2] applique les reecritures dans l’ordre — chaque étape se voit dans le ⊢, qui se simplifie au fil de la ligne. C’est le mode de preuve « calculatoire » des notebooks appliques : rw [Nat.zero_add], rw [Nat.add_comm] (section 5.2) transforment des enonces algébriques en trivialites. On le retrouve massivement dans Lean-06-Mathlib-Essentials-Lean, ou les propriétés de Nat s’utilisent précisément par ces reecritures.

-- Reecriture simple
theorem rw_example (a b c : Nat) (h : a = b) : a + c = b + c := by
  rw [h]         -- Remplace a par b, le but devient b + c = b + c

-- Reecriture inverse avec <-
theorem rw_rev (a b : Nat) (h : a = b) : b = a := by
  rw [← h]      -- Remplace b par a (inverse), utilise ← (backslash l)

-- Enchainer les reecritures
theorem rw_chain (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  rw [h1, h2]   -- Applique les deux en sequence

-- Reecriture simple

theorem rw_example (a b c : Nat) (h : a = b) : a + c = b + c := by

  rw [h]         -- Remplace a par b, le but devient b + c = b + c

-- Reecriture inverse avec <-

theorem rw_rev (a b : Nat) (h : a = b) : b = a := by

  rw [← h]      -- Remplace b par a (inverse), utilise ← (backslash l)

-- Enchainer les reecritures

theorem rw_chain (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by

  rw [h1, h2]   -- Applique les deux en sequence

--% env 15

Raw input

{"cmd": "-- Reecriture simple\ntheorem rw_example (a b c : Nat) (h : a = b) : a + c = b + c := by\n rw [h] -- Remplace a par b, le but devient b + c = b + c\n\n-- Reecriture inverse avec <-\ntheorem rw_rev (a b : Nat) (h : a = b) : b = a := by\n rw [\u2190 h] -- Remplace b par a (inverse), utilise \u2190 (backslash l)\n\n-- Enchainer les reecritures\ntheorem rw_chain (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by\n rw [h1, h2] -- Applique les deux en sequence", "env": 14}

Raw output

{"env": 15}

5.2 Reecriture avec lemmes de la bibliotheque

On peut utiliser rw avec des lemmes nommes de la bibliotheque standard. Par exemple rw [Nat.add_comm] applique la commutativite de l’addition.

-- Utiliser les lemmes de Nat
theorem rw_lib (n : Nat) : n + 0 = n := by
  rw [Nat.add_zero]   -- Applique n + 0 = n

theorem rw_comm (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

-- Preuve plus complexe
theorem rw_complex (a b c : Nat) : (a + b) + c = (a + c) + b := by
  rw [Nat.add_assoc]          -- a + (b + c)
  rw [Nat.add_comm b c]       -- a + (c + b)
  rw [<- Nat.add_assoc]       -- (a + c) + b

-- Utiliser les lemmes de Nat

theorem rw_lib (n : Nat) : n + 0 = n := by

  rw [Nat.add_zero]   -- Applique n + 0 = n

theorem rw_comm (a b : Nat) : a + b = b + a := by

  rw [Nat.add_comm]

-- Preuve plus complexe

theorem rw_complex (a b c : Nat) : (a + b) + c = (a + c) + b := by

  rw [Nat.add_assoc]          -- a + (b + c)

  rw [Nat.add_comm b c]       -- a + (c + b)

  rw [<- Nat.add_assoc]       -- (a + c) + b

--% env 16

Raw input

{"cmd": "-- Utiliser les lemmes de Nat\ntheorem rw_lib (n : Nat) : n + 0 = n := by\n rw [Nat.add_zero] -- Applique n + 0 = n\n\ntheorem rw_comm (a b : Nat) : a + b = b + a := by\n rw [Nat.add_comm]\n\n-- Preuve plus complexe\ntheorem rw_complex (a b c : Nat) : (a + b) + c = (a + c) + b := by\n rw [Nat.add_assoc] -- a + (b + c)\n rw [Nat.add_comm b c] -- a + (c + b)\n rw [<- Nat.add_assoc] -- (a + c) + b", "env": 15}

Raw output

{"env": 16}

5.3 Reecriture dans le contexte avec at

La forme rw [h] at loc reecrit l’équation h a un endroit precis du contexte plutot que dans le but principal. Trois variantes principales :

1. rw [h] at hyp : reecrit dans l’hypothese hyp uniquement. Le but n’est pas touche. C’est utile pour preparer une hypothese avant une autre tactique (par exemple normaliser une hypothese avant un cases ou un rfl).
2. rw [h] at * : reecrit partout ou l’équation est applicable – dans toutes les hypotheses ET dans le but. C’est l’outil de nettoyage global quand une équation triviale apparait dans plusieurs endroits.
3. rw [h] at h ⊢ : reecrit dans h ET dans le but (note ⊢ = le symbole du but). C’est un raccourci pour les deux endroits les plus frequents.

Pourquoi cette granularite ? Quand vous travaillez sur un but complexe avec beaucoup d’hypotheses, reecrire dans le but peut le casser (introduire des termes parasites) ou rater une simplification possible dans une hypothese. La forme at loc vous laisse cibler la transformation.

Exemple canonique : la cellule de droite montre rw [Nat.add_zero] at h sur une hypothese h : a + 0 = b, qui reduit h en h : a = b. Sans at h, Lean reecrirait dans le but (qui ne contient pas a + 0) et la tactique serait un no-op silencieux.

Le pont : at est la meme logique que Lean-3 (cell 11) sur les cases with | intro hp hq => ... – vous nommez la cible de la transformation au lieu de l’inferer du contexte. Lean-12 (sensibilité Huang) utilise intensivement rw [...] at * pour normaliser des sommes avant chaque cas d’analyse.

-- rw at h reecrit dans l'hypothese h
theorem rw_at (a b : Nat) (h : a + 0 = b) : a = b := by
  rw [Nat.add_zero] at h   -- h devient a = b
  exact h

-- rw at * reecrit partout
theorem rw_at_star (a b c : Nat) (h1 : a = b) (h2 : a + c = 10) : b + c = 10 := by
  rw [h1] at *    -- Remplace a par b dans h2 et le but
  exact h2

-- rw at h reecrit dans l'hypothese h

theorem rw_at (a b : Nat) (h : a + 0 = b) : a = b := by

  rw [Nat.add_zero] at h   -- h devient a = b

  exact h

-- rw at * reecrit partout

theorem rw_at_star (a b c : Nat) (h1 : a = b) (h2 : a + c = 10) : b + c = 10 := by

  rw [h1] at *    -- Remplace a par b dans h2 et le but

  exact h2

--% env 17

Raw input

{"cmd": "-- rw at h reecrit dans l'hypothese h\ntheorem rw_at (a b : Nat) (h : a + 0 = b) : a = b := by\n rw [Nat.add_zero] at h -- h devient a = b\n exact h\n\n-- rw at * reecrit partout\ntheorem rw_at_star (a b c : Nat) (h1 : a = b) (h2 : a + c = 10) : b + c = 10 := by\n rw [h1] at * -- Remplace a par b dans h2 et le but\n exact h2", "env": 16}

Raw output

{"env": 17}

6. Simplification avec simp

6.1 Utilisation de base

simp applique automatiquement un ensemble de règles de simplification.

Une batterie de rw automatiques. La ou rw exige de nommer chaque égalité et chaque direction (section 5.1), simp applique tout seul une collection de règles de simplification : les théorèmes marques [simp] (comme Nat.add_zero, Nat.mul_zero, les tautologies logiques, les reductions de if, and, or, de listes). Elle simplifie les deux cotes d’une égalité, une inégalité, ou une conjonction de sous-buts. C’est la tactique « nettoyage » par excellence : elle degonfle les enonces qui paraissent imposants jusqu’a une forme triviale — simp_example ramene ainsi n + 0 = n directement a rfl, sans qu’on nomme Nat.add_zero.

simp vs rw. rw est chirurgicale et lisible — chaque étape est visible dans le ⊢ ; simp est globale et aveugle — on ne voit que le résultat. Rele pratique : rw quand la preuve doit montrer les étapes, simp quand il s’agit de deblayer un but encombre avant la tactique decisive. Dans simp_list, la liste [1, 2] ++ [3] se reduit et se compare par reflexivite, encore un coup de simp.

Lire la sortie. Quand simp declare no progress, aucun but n’a change : rien n’etait simplifiable, il faut une autre tactique. La combinaison simp puis cloture est la signature des preuves courtes : un simp suffit souvent a ramener un but encombre a une trivialite — on la retrouve dans les notebooks appliques comme Lean-16b-Conway-Game-of-Life-Lean, ou les propriétés booleennes des cellules se reglent d’un trait.

-- simp simplifie automatiquement
theorem simp_example (n : Nat) : n + 0 = n := by
  simp   -- Connait n + 0 = n

-- simp sur des listes
theorem simp_list : [1, 2] ++ [3] = [1, 2, 3] := by
  simp

-- simp ne resout pas tout
-- theorem simp_fail (n m : Nat) : n + m = m + n := by simp  -- FAIL

-- simp simplifie automatiquement

theorem simp_example (n : Nat) : n + 0 = n := by

  simp   -- Connait n + 0 = n

-- simp sur des listes

theorem simp_list : [1, 2] ++ [3] = [1, 2, 3] := by

  simp

-- simp ne resout pas tout

-- theorem simp_fail (n m : Nat) : n + m = m + n := by simp  -- FAIL

--% env 18

Raw input

{"cmd": "-- simp simplifie automatiquement\ntheorem simp_example (n : Nat) : n + 0 = n := by\n simp -- Connait n + 0 = n\n\n-- simp sur des listes\ntheorem simp_list : [1, 2] ++ [3] = [1, 2, 3] := by\n simp\n\n-- simp ne resout pas tout\n-- theorem simp_fail (n m : Nat) : n + m = m + n := by simp -- FAIL", "env": 17}

Raw output

{"env": 18}

6.2 Options de simp

simp accepte plusieurs modificateurs qui précisent comment simplifier, au-delà du simple simp :

• simp [h] : ajoute l’hypothèse h à la base de lemmes simp pour cette occurrence. Lean tente alors d’utiliser h à côté des lemmes @[simp] enregistrés. La base elle-même n’est pas modifiée — c’est un ajout local pour ce but.
• simp only [l1, l2, ...] : restreint la base aux lemmes explicitement listés. Lean n’utilise que ces lemmes, pas l’ensemble des @[simp]. C’est l’outil de debugging : on voit exactement quels lemmes ont été déclenchés, et on évite les simplifications « magiques » qui obscurcissent la logique.
• simp at h : simplifie l’hypothèse h (de la même façon qu’avec rw [h] at loc). Combiné avec simp at *, on simplifie tout le contexte ET le but.
• simp_all : applique simp au but et à toutes les hypothèses. C’est l’outil de « finition » : quand le but devrait être trivial après simplification de tout, simp_all tente la passe complète.

Stratégie de choix :

1. But simple après lemmes standards : simp suffit. Lean applique @[add_zero] (n + 0 = n), @[mul_one] (n * 1 = n), etc.
2. But dépend d’une hypothèse métier : simp [h] pour inclure cette hypothèse.
3. Preuve fragile / non-reproductible : simp only [liste] pour traçabilité. Dans une preuve Mathlib sérieuse, c’est souvent exigé pour éviter les ruptures de compatibilité.
4. Simplification dans le contexte : simp at h ou simp at *.

Pièges courants :

• simp peut boucler si on ajoute une équivalence @[simp] qui crée un cycle. La parade est simp only ou marquer le lemme comme @[simp high] pour le rendre découvable mais pas systématiquement tenté.
• simp est non-déterministe : deux exécutions peuvent produire des états intermédiaires différents. Pour les preuves critiques, decide ou omega sont préférables.

Le pont : simp only est la tactique dominante dans Lean-6 (Mathlib Essentials) pour les preuves de notations arithmétiques. Lean-12 (Sensitivity) combine simp only [Fin.sum_univ_succ, Fin.val_zero, ...] avec une liste explicite de lemmes pour traçabilité.

-- simp avec lemmes additionnels
theorem simp_with (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  simp [h]   -- Ajoute h aux regles

-- simp only : restreint les regles
theorem simp_only_example (n : Nat) : n + 0 + 0 = n := by
  simp only [Nat.add_zero]

-- simp_all : simplifie aussi le contexte
theorem simp_all_example (a b : Nat) (h : a + 0 = b) : a = b := by
  simp_all

-- simp avec lemmes additionnels

theorem simp_with (a b : Nat) (h : a = b) : a + 1 = b + 1 := by

  simp [h]   -- Ajoute h aux regles

-- simp only : restreint les regles

theorem simp_only_example (n : Nat) : n + 0 + 0 = n := by

  simp only [Nat.add_zero]

-- simp_all : simplifie aussi le contexte

theorem simp_all_example (a b : Nat) (h : a + 0 = b) : a = b := by

  simp_all

--% env 19

Raw input

{"cmd": "-- simp avec lemmes additionnels\ntheorem simp_with (a b : Nat) (h : a = b) : a + 1 = b + 1 := by\n simp [h] -- Ajoute h aux regles\n\n-- simp only : restreint les regles\ntheorem simp_only_example (n : Nat) : n + 0 + 0 = n := by\n simp only [Nat.add_zero]\n\n-- simp_all : simplifie aussi le contexte\ntheorem simp_all_example (a b : Nat) (h : a + 0 = b) : a = b := by\n simp_all", "env": 18}

Raw output

{"env": 19}

6.3 L’attribut @[simp]

On peut ajouter ses propres lemmes a la base de simp.

L’attribut @[simp] (dans Lean 4 Mathlib, c’est @[simp]) enregistre un théorème dans la base de lemmes simp. Une fois marqué, ce lemme est automatiquement candidat à chaque appel de simp — sans avoir besoin de le lister à chaque occurrence. C’est l’outil qui transforme un lemme « utile en ce moment » en lemme « connu du simplifieur ».

Comment ça marche en Lean 4 :

@[simp] theorem my_lemma (n : Nat) : f n = g n := ...
-- Apres cette declaration, `simp` applique `my_lemma` quand f n ou g n apparait.

Pourquoi enregistrer un lemme @[simp] ?

• Réciproque publique : si vous venez de prouver n + 0 = n ou f x = g x, le marquer @[simp] le rend disponible à toute preuve ultérieure du projet.
• Lemme d’usage fréquent : @[add_zero] (n + 0 = n), @[mul_one] (n * 1 = n), @[and_self] (p ∧ p ↔︎ p) — tous enregistrés pour cette raison.
• Équivalence standard : even_iff_two_dvd, prime_two, etc. — toute équivalence qui simplifie une expression à sa forme canonique.

Pièges et limites :

• Ne pas abuser : marquer @[simp] un lemme « lourd » ralentit chaque simp du projet, et peut créer des cycles (lemme A appelle simp pour prouver B, B appelle simp qui retrouve A, …). Mathlib a un système de Simp.lemmas.addSimpProof-tracking pour détecter ces cas.
• Variantes conditionnelles : @[simp high] (lemme à utiliser seulement si la cible est explicitement @[simp]). @[simp low] (lemme à utiliser seulement en dernier recours). @[simp norm_cast] pour les lemmes de coercion.
• Réversibilité : si un lemme @[simp] s’avère problématique, on peut le désactiver localement avec simp [-mon_lemme] ou globalement avec @[simp ← mon_lemme].

Quand NE PAS marquer @[simp] :

• Un lemme dont l’application n’est pas définitionnellement triviale (par exemple un test de primalité nécessitant decide). Le simplifier ne peut pas l’appliquer rapidement.
• Un lemme « utile » mais qui éclate la structure que vous voulez préserver (par exemple nat_succ_eq_add_one parfois).
• Un lemme non-réversible (équivalence d’ordre ≠ équivalence numérique) : simp pourrait l’appliquer dans le mauvais sens.

Le pont : la convention @[simp] est omniprésente dans Lean-6 (Mathlib). Lean-12 (Sensitivity) introduit @[simp] custom pour les lemmes de borne sur Fin.sum_univ_*. Lean-14 (Finiteness) en utilise une centaines pour les théorèmes d’analyse combinatoire.

Inspection : pour voir quels lemmes simp sont actifs dans votre contexte, utilisez simp_wf ou explorez la documentation de Mathlib.Tactic.Simps.

-- Definir un lemme simp
@[simp] theorem my_simp_lemma (n : Nat) : n * 1 = n := Nat.mul_one n

-- Maintenant simp l'utilise automatiquement
theorem use_my_simp (a : Nat) : a * 1 + 0 = a := by
  simp   -- Utilise my_simp_lemma et add_zero

-- Definir un lemme simp

@[simp] theorem my_simp_lemma (n : Nat) : n * 1 = n := Nat.mul_one n

-- Maintenant simp l'utilise automatiquement

theorem use_my_simp (a : Nat) : a * 1 + 0 = a := by

  simp   -- Utilise my_simp_lemma et add_zero

--% env 20

Raw input

{"cmd": "-- Definir un lemme simp\n@[simp] theorem my_simp_lemma (n : Nat) : n * 1 = n := Nat.mul_one n\n\n-- Maintenant simp l'utilise automatiquement\ntheorem use_my_simp (a : Nat) : a * 1 + 0 = a := by\n simp -- Utilise my_simp_lemma et add_zero", "env": 19}

Raw output

{"env": 20}

7. Structuration des Preuves

7.1 Points (bullets) pour focaliser

À ce stade du notebook, on a vu comment chaque tactique résout un sous-but à la fois : constructor découpe, exact ferme. Quand une preuve génère plusieurs sous-buts simultanés (par exemple après un cases sur une disjonction), il devient vite fastidieux d’écrire la tactique pour chaque but en séquence — Lean perdrait le fil, et la lecture serait pénible.

La section 7 introduit trois mécanismes de structuration qui répondent à ce problème :

• 7.1 Points (·) : un bullet · ouvre un bloc dédié à un sous-but ; Lean vérifie que ce bloc est clos avant de passer au suivant. C’est la version lisible et sûre de l’enchaînement nu.
• 7.2 case : permet de nommer explicitement chaque branche issue d’un cases. La lecture du code de preuve devient auto-documentée.
• 7.3 Combinateurs ; et <;> : chaînent plusieurs tactiques sans avoir à dupliquer. <;> distribue sur tous les sous-buts générés, ce qui est l’idiome dominant dans les preuves Mathlib sérieuses.

L’objectif : passer d’une preuve « chaque sous-but ligne par ligne » à une preuve « chaque sous-but clairement isolé et commenté ». C’est ce qui distingue une preuve pédagogique d’une preuve industrielle Mathlib.

Le pont : les points · sont la syntaxe par défaut dans Lean-12 (Sensitivity) pour les preuves cases h with | intro .... Lean-14 (Finiteness) les utilise systématiquement dans les induction à deux branches ou plus. Lean-16 (Conway Free Will) combine points + <;> pour distribuer omega sur 16 sous-buts générés par decide.

-- Les points separent les sous-buts
theorem bullets_example (p q : Prop) (hp : p) (hq : q) : p /\ q /\ p := by
  constructor
  · exact hp              -- Premier but : p
  · constructor           -- Deuxieme but : q /\ p
    · exact hq            -- Sous-but : q
    · exact hp            -- Sous-but : p

-- Les points separent les sous-buts

theorem bullets_example (p q : Prop) (hp : p) (hq : q) : p /\ q /\ p := by

  constructor

  · exact hp              -- Premier but : p

  · constructor           -- Deuxieme but : q /\ p

    · exact hq            -- Sous-but : q

    · exact hp            -- Sous-but : p

--% env 21

Raw input

{"cmd": "-- Les points separent les sous-buts\ntheorem bullets_example (p q : Prop) (hp : p) (hq : q) : p /\\ q /\\ p := by\n constructor\n \u00b7 exact hp -- Premier but : p\n \u00b7 constructor -- Deuxieme but : q /\\ p\n \u00b7 exact hq -- Sous-but : q\n \u00b7 exact hp -- Sous-but : p", "env": 20}

Raw output

{"env": 21}

Le point · (bullet) focalise un sous-but : chaque · ouvre un bloc dedie a un seul but restant, et Lean vérifie qu’il est entierement clos avant de passer au suivant. C’est plus sur que d’enchainer les tactiques nues, car une tactique laissant un but ouvert est immediatement signalee. On obtient une preuve lisible ou chaque branche est isolee.

7.2 case pour nommer les cas

La tactique cases h (vue en 4.2) génère des noms automatiques pour chaque branche — inl hp, inr hq, etc. Mais ces noms sont souvent opaques : impossible de deviner à quoi ils correspondent sans lire le contexte.

La forme case (et son équivalent with | nom => ...) permet de renommer explicitement chaque branche au moment où on la traite. Trois variantes principales :

1. cases h with | intro hp hq => ... : syntaxe classique de Lean 4. Chaque branche commence par | nom_constructeur (vars) =>, suivie de la tactique à appliquer.
2. cases h; case inl hp => ... case inr hq => ... : syntaxe en deux temps. Plus verbeuse mais plus claire quand les branches contiennent plusieurs lignes.
3. rcases h with ⟨...⟩ | ⟨...⟩ : la variante la plus expressive pour les inductive patterns imbriqués. rcases étend cases en reconnaissance de motifs (similaire à match).

Pourquoi nommer explicitement ?

• Légibilité : un lecteur voit immédiatement quelle branche fait quoi, sans avoir à deviner la sémantique des noms automatiques.
• Nommage cohérent : vous pouvez imposer une convention (hp, hq pour les hypothèses positives, hnp pour la négation, etc.) qui s’aligne avec le reste de la preuve.
• Documentation : le case agit comme un commentaire structuré : case inl (huge : False) => exact huge.elim indique « ici je traite le cas gauche, qui est une absurdité ».

Exemple canonique : la cellule de droite montre cases hpq with | inl hp => ... | inr hq => ... sur hpq : p ∨ q. La lecture est limpide : « si on a p, prouve la cible via hp ; si on a q, prouve via hq ». Sans les case, on lirait cases hpq; { exact ... }, { exact ... } — moins parlant.

Pièges :

• Oublier un case quand cases génère N branches : Lean signale « unsolved goals » et arrête la compilation. C’est un garde-fou, pas un bug.
• Mélanger case et · : les deux mécanismes cohabitent mal. Préferez l’un ou l’autre par bloc.
• Utiliser case sur une preuve de 1 ligne est surdimensionné ; cases simple suffit.

Le pont : la convention cases h with | intro ... est universelle dans Lean-12 (Sensitivity), Lean-14 (Finiteness), et Lean-16 (Conway Free Will). Lean-6 (Mathlib) pousse plus loin avec rcases pour les structures imbriquées (par exemple matcher simultanément sur Option et And).

-- case nomme explicitement les branches
theorem case_example (p q : Prop) (hpq : p \/ q) : q \/ p := by
  cases hpq
  case inl hp =>
    right
    exact hp
  case inr hq =>
    left
    exact hq

-- case nomme explicitement les branches

theorem case_example (p q : Prop) (hpq : p \/ q) : q \/ p := by

  cases hpq

  case inl hp =>

    right

    exact hp

  case inr hq =>

    left

    exact hq

--% env 22

Raw input

{"cmd": "-- case nomme explicitement les branches\ntheorem case_example (p q : Prop) (hpq : p \\/ q) : q \\/ p := by\n cases hpq\n case inl hp =>\n right\n exact hp\n case inr hq =>\n left\n exact hq", "env": 21}

Raw output

{"env": 22}

case (ou la syntaxe with | nom => ...) permet de nommer explicitement chaque branche issue d’un cases. Indispensable quand les branches appellent des tactiques différentes, ou simplement pour documenter l’intention : le lecteur voit immediatement quelle hypothese traite quel cas.

7.3 Combinateurs ; et <;>

Les combinateurs de tactiques enchainent plusieurs tactiques en evitant la duplication. Deux formes, deux semantiques distinctes :

1. tac1; tac2 : applique tac1, puis applique tac2 sur le meme but (ou le but restant si tac1 en a laisse un seul). Si tac1 genere plusieurs sous-buts, tac2 n’est applique qu’au premier sous-but.

2. tac1 <;> tac2 : applique tac1, puis applique tac2 a tous les sous-buts generes. C’est l’outil pour distribuer une tactique de cloture sur N branches.

3. Chainer N fois : pour distribuer sur 3 sous-buts, tac1 <;> tac2 <;> tac3. Chaque <;> propage tac3 aux sous-buts generes par tac2, et ainsi de suite. La lecture se fait de gauche a droite.

Pourquoi <;> plutot que ; ? La forme ; est hereditaire de la programmation imperative (sequence d’instructions). Mais en preuve, on manipule souvent plusieurs buts simultanement (chaque cases ou constructor peut en generer plusieurs). <;> adapte le paradigme : on distribue la tactique suivante sur tous les buts, pas seulement le premier.

Exemple canonique : la cellule de droite montre refine ⟨?_, ?_, ?_⟩ <;> exact hp pour prouver p ∧ p ∧ p. refine ⟨?_, ?_, ?_⟩ genere 3 sous-buts, et <;> exact hp cloture les trois d’un coup. Sans <;>, il faudrait trois exact successifs.

Le pont : <;> est l’equivalent proof-side de la comprehension de liste en programmation. Lean-12 (sensibilité) l’utilise 50+ fois dans les chaines d’analyse par cas. Lean-14 (Finiteness) l’utilise pour distribuer les bornes sur les cas de dérivées. C’est une brique de base de la preuve tactique en Lean 4.

-- ; enchaine les tactiques
theorem semi_example (p : Prop) (hp : p) : p := by
  exact hp

-- <;> applique a tous les buts generes
theorem all_goals (p : Prop) (hp : p) : p /\ p /\ p := by
  constructor <;> (try constructor) <;> exact hp

-- Plus lisible avec repeat
theorem repeat_example (p : Prop) (hp : p) : p /\ p /\ p := by
  refine ⟨?_, ?_, ?_⟩ <;> exact hp

-- ; enchaine les tactiques

theorem semi_example (p : Prop) (hp : p) : p := by

  exact hp

-- <;> applique a tous les buts generes

theorem all_goals (p : Prop) (hp : p) : p /\ p /\ p := by

  constructor <;> (try constructor) <;> exact hp

-- Plus lisible avec repeat

theorem repeat_example (p : Prop) (hp : p) : p /\ p /\ p := by

  refine ⟨?_, ?_, ?_⟩ <;> exact hp

--% env 23

Raw input

{"cmd": "-- ; enchaine les tactiques\ntheorem semi_example (p : Prop) (hp : p) : p := by\n exact hp\n\n-- <;> applique a tous les buts generes\ntheorem all_goals (p : Prop) (hp : p) : p /\\ p /\\ p := by\n constructor <;> (try constructor) <;> exact hp\n\n-- Plus lisible avec repeat\ntheorem repeat_example (p : Prop) (hp : p) : p /\\ p /\\ p := by\n refine \u27e8?_, ?_, ?_\u27e9 <;> exact hp", "env": 22}

Raw output

{"env": 23}

Deux combinateurs subtilement différents :

• t1 ; t2 exécute t1 puis t2 dans le même but (sequence simple).
• t1 <;> t2 exécute t1, puis applique t2 a chacun des sous-buts crees par t1 (distribution).

<;> est l’outil idiomatique pour traiter uniformement tous les cas ouverts par un cases ou un constructor.

8. Tactiques Avancees

8.1 induction : preuve par recurrence

La tactique induction est la brique de base de la preuve par récurrence structurelle. Elle génère un cas de base (constructeur zero ou nil) et un cas inductif (constructeur succ ou cons) avec une hypothèse de récurrence (souvent nommée ih).

Fonctionnement :

• Pour induction n with sur un n : Nat, Lean crée deux sous-buts :
  • | zero => ⊢ P 0 : cas de base.
  • | succ k ih => ⊢ P (k + 1) : cas inductif, avec k : Nat et ih : P k.
• Pour une liste : induction l with | nil => ... | cons hd tl ih => ... — hd : A, tl : List A, ih : P tl.
• Pour un inductif imbriqué (par exemple Tree), Lean génère un cas par constructeur.

Variantes utiles :

• induction n using Nat.strong_rec_on : récurrence forte où ih porte sur tous les m < n, pas seulement n - 1. Pour des bornes non-linéaires.
• induction n generalizing h : la variable h est restaurée dans le contexte après induction. Utile quand h est une hypothèse qui dépend de n.
• cases h; induction h' : induction sur un sous-terme destructuré.

Différences avec cases : cases décompose sans générer d’hypothèse de récurrence. induction crée l’hypothèse de récurrence et l’injecte dans le contexte. Une preuve par récurrence a besoin de induction (ou Nat.recOn), cases ne suffirait pas.

Pattern de preuve :

theorem my_thm : ∀ n : Nat, P n := by
  intro n
  induction n with
  | zero => -- cas de base
  | succ k ih => -- ih : P k, prouver P (k+1)

Le pont : induction est la tactique dominante dans Lean-12 (Sensitivity) pour les preuves sur ℕ, dans Lean-14 (Finiteness) pour les preuves sur les dérivées, et dans Lean-16 (Conway Free Will) pour les preuves sur les entiers de Conway. Lean-6 (Mathlib) introduit Nat.strong_induction et Nat.strong_rec_on pour les preuves non-linéaires.

-- Recurrence sur Nat
-- Exemple simple : 0 + n = n (deja dans la bibliotheque, on le reprouve)
theorem my_zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    -- But : 0 + (k + 1) = k + 1
    -- On utilise la definition de + pour Nat
    simp only [Nat.add_succ, ih]

-- Exemple : n + 0 = n
theorem my_add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ k ih => simp [ih]

-- Recurrence sur Nat

-- Exemple simple : 0 + n = n (deja dans la bibliotheque, on le reprouve)

theorem my_zero_add (n : Nat) : 0 + n = n := by

  induction n with

  | zero => rfl

  | succ k ih =>

    -- But : 0 + (k + 1) = k + 1

    -- On utilise la definition de + pour Nat

    simp only [Nat.add_succ, ih]

-- Exemple : n + 0 = n

theorem my_add_zero (n : Nat) : n + 0 = n := by

  induction n with

  | zero => rfl

  | succ k ih => simp [ih]
🟨 This simp argument is unused:
  ih

Hint: Omit it from the simp argument list.
  simp ̵[̵i̵h̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

--% env 24

Raw input

{"cmd": "-- Recurrence sur Nat\n-- Exemple simple : 0 + n = n (deja dans la bibliotheque, on le reprouve)\ntheorem my_zero_add (n : Nat) : 0 + n = n := by\n induction n with\n | zero => rfl\n | succ k ih =>\n -- But : 0 + (k + 1) = k + 1\n -- On utilise la definition de + pour Nat\n simp only [Nat.add_succ, ih]\n\n-- Exemple : n + 0 = n\ntheorem my_add_zero (n : Nat) : n + 0 = n := by\n induction n with\n | zero => rfl\n | succ k ih => simp [ih]", "env": 23}

Raw output

{"messages": [{"severity": "warning", "pos": {"line": 15, "column": 23}, "endPos": {"line": 15, "column": 25}, "data": "This simp argument is unused:\n ih\n\nHint: Omit it from the simp argument list.\n simp ̵[̵i̵h̵]̵\n\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`"}], "env": 24}

induction genere deux sous-buts canoniques : le cas de base (zero, ici n = 0) et le cas inductif (succ n ih, ou ih est l’hypothese de recurrence portant sur n). C’est le squelette universel des preuves par recurrence sur Nat ; la même structure s’applique aux listes, arbres et tout type inductif.

8.2 decide : propositions decidables

La tactique decide prouve une proposition décidable en l’évaluant par calcul sur l’interpréteur Lean. Elle vérifie algorithmiquement la proposition et ferme le but par réfutation ou confirmation. C’est l’équivalent proof-side de rfl pour les propositions booléennes.

Fonctionnement :

• decide est implémenté en Lean 4 par un appel à l’évaluateur natif (Lean.Expr). Pour n ≤ m ou n + m = p, il calcule littéralement et vérifie.
• Le but doit être de type Prop et avoir une instance Decidable (que Lean peut dériver par decidable_prop ou inferInstance).
• Les propositions quantifiées sur des univers infinis (∀ n : Nat, n + 0 = n) ne sont pas décidables en général — decide échoue.

Exemples d’utilisation :

• decide pour les inégalités numériques : 3 ≤ 5, 10 % 3 = 1, etc.
• decide pour les propositions booléennes : true ∧ false = false, ¬ true = false.
• decide pour les propositions sur des structures finies : List.length [1,2,3] = 3, Option.isNone (some 5) = false.

Différences avec rfl : rfl prouve une égalité définitionnelle (réductible par βδιζη). decide traite les propositions avec une Decidable instance — y compris celles non définitionnellement closes. Donc decide est strictement plus puissant : n + 0 = n peut être decide-prouvé (Lean calcule littéralement), alors que rfl échoue (il faut une étape de preuve).

Pièges :

• decide peut être lent sur de grands arguments (calcul proportionnel à la taille).
• decide ne fournit pas de witness — il prouve seulement la proposition. Si vous avez besoin du témoin (par exemple n = 5 après preuve que n satisfait une certaine propriété), il faut omega ou nlinarith.
• decide sur une proposition non décidable : Lean renvoie failed, pas un faux positif.

Le pont : decide est utilisé en abondance dans Lean-6 (Mathlib) pour les lemmes sur Nat.Prime et les propositions finies. Lean-12 (Sensitivity) l’emploie sur les lemmes de cardinalité booléenne. Lean-16 (Conway Free Will) l’utilise sur les équations de Gödel pour des preuves courtes et mécaniques.

-- decide resout les propositions decidables
-- (qui peuvent etre evaluees par calcul)
theorem decide_example : 3 < 5 := by decide
theorem decide_bool : true && false = false := by decide
theorem decide_mod : 10 % 3 = 1 := by decide

-- Note : Nat.Prime est defini dans Mathlib, pas dans Lean 4 standard.
-- Avec Mathlib : theorem decide_prime : Nat.Prime 7 := by decide

-- decide resout les propositions decidables

-- (qui peuvent etre evaluees par calcul)

theorem decide_example : 3 < 5 := by decide

theorem decide_bool : true && false = false := by decide

theorem decide_mod : 10 % 3 = 1 := by decide

-- Note : Nat.Prime est defini dans Mathlib, pas dans Lean 4 standard.

-- Avec Mathlib : theorem decide_prime : Nat.Prime 7 := by decide

--% env 25

Raw input

{"cmd": "-- decide resout les propositions decidables\n-- (qui peuvent etre evaluees par calcul)\ntheorem decide_example : 3 < 5 := by decide\ntheorem decide_bool : true && false = false := by decide\ntheorem decide_mod : 10 % 3 = 1 := by decide\n\n-- Note : Nat.Prime est defini dans Mathlib, pas dans Lean 4 standard.\n-- Avec Mathlib : theorem decide_prime : Nat.Prime 7 := by decide", "env": 24}

Raw output

{"env": 25}

decide prouve une proposition decidable en l’evaluant par calcul. Puissant pour les inégalités numériques et les propriétés finies, mais impuissant sur les propositions quantifiees ou non calculables (il echoue alors proprement plutot que de boucler). C’est l’equivalent preuve-par-calcul de rfl pour les booléens.

8.3 omega : arithmetique linéaire

La tactique omega est un décideur d’arithmétique de Presburger : elle résout automatiquement les buts d’arithmétique linéaire (additions, soustractions, comparaisons, constantes entières) sans aucune aide.

Portée de omega :

• Additions et soustractions : n + m, n - m, 0, 1, …, (n : Int).
• Multiplications par constantes : 2 * n, n * 5, mais pas n * m.
• Comparaisons : <, ≤, >, ≥, =, ≠.
• Variables naturelle et entière : Nat, Int, surchargées.

Exemples d’utilisation :

example (n m : Nat) (h : n < m) : n + 1 ≤ m := by omega
example (n m : Nat) (h : n + m = 10) (h' : n > 5) : m < 5 := by omega
example (n m k : Nat) (h1 : n < m) (h2 : m < k) : n + 1 < k := by omega

Algorithme : omega réduit d’abord le but à des inégalités linéaires, puis applique l’algorithme de Cooper (un décideur en arithmétique de Presburger) pour réfuter la négation. Si la négation est réfutable, omega ferme le but. Sinon, omega échoue.

Limites :

• Pas de multiplication de variables : n * m = 0 n’est pas décidable en Presburger général. Pour cela, il faut nlinarith (Mathlib) ou combiner omega avec nlinarith.
• Pas de quantification imbriquée : omega réussit sur ∀ n, ..., pas sur ∀ ∃, ... qui implique la satisfaisabilité dans une structure plus riche.
• Pas de fonctions définies par récursion : omega ne sait pas quelles sont les propriétés de fib n ou ack n.

Le pont : omega est l’une des tactic les plus utilisées dans Lean-6 (Mathlib) pour les sous-buts arithmétiques. Lean-12 (Sensitivity) l’utilise pour les preuves sur les sommes de booléens. Lean-14 (Finiteness) l’emploie sur les polynômes de degré 1 (au-delà, c’est nlinarith ou polyrith). Lean-16 (Conway Free Will) l’utilise pour les preuves sur les entiers de Conway qui restent dans l’arithmétique linéaire.

-- omega resout automatiquement l'arithmetique lineaire
theorem omega_example (n m : Nat) (h : n < m) : n + 1 <= m := by
  omega

theorem omega_complex (a b c : Nat)
  (h1 : a + b < c) (h2 : c < 2 * a + b) : a > 0 := by
  omega

-- omega resout automatiquement l'arithmetique lineaire

theorem omega_example (n m : Nat) (h : n < m) : n + 1 <= m := by

  omega

theorem omega_complex (a b c : Nat)

  (h1 : a + b < c) (h2 : c < 2 * a + b) : a > 0 := by

  omega

--% env 26

Raw input

{"cmd": "-- omega resout automatiquement l'arithmetique lineaire\ntheorem omega_example (n m : Nat) (h : n < m) : n + 1 <= m := by\n omega\n\ntheorem omega_complex (a b c : Nat)\n (h1 : a + b < c) (h2 : c < 2 * a + b) : a > 0 := by\n omega", "env": 25}

Raw output

{"env": 26}

omega est un décideur d’arithmetique de Presburger : il resout automatiquement les buts melant +, -, comparaisons (<, <=, =) et variables entières/naturelles. Sa limite : il ne traite pas la multiplication de deux variables (n * m). Pour l’algebre non-linéaire, il faut ring (Mathlib) ou nlinarith.

8.4 ring : algebre

La tactique ring est un décideur d’anneaux commutatifs : elle prouve les égalités polynomiales sur ℕ, ℤ, ℚ, ℝ, et plus généralement tout CommRing, sans aucune aide.

Portée de ring :

• Anneau sous-jacent : Nat, Int, Rat, Real, toute instance CommRing.
• Opérations : +, -, *, ^, 0, 1.
• Variables : x, y, z, … .
• Constantes : 0, 1, 2, …, (2 : Int), (3 : ℚ), etc.

Exemples :

example (x y : ℤ) : (x + y) * (x + y) = x*x + 2*x*y + y*y := by ring
example (a b c : ℚ) : (a + b + c) * (a + b + c) = a^2 + 2*a*b + 2*a*c + b^2 + 2*b*c + c^2 := by ring
example (n : Nat) : (n + 1) * (n + 1) = n*n + 2*n + 1 := by ring

Algorithme : ring réduit les deux côtés de l’égalité à une forme normale polynomiale (somme de monômes ordonnés), puis compare les arbres syntaxiquement. C’est l’équivalent proof-side de la réduction polynomiale des CAS.

Limites :

• Pas de division : ring ne sait pas gérer /. Si le but contient a / b, il faut field_simp ou norm_cast + ring.
• Pas d’inégalités : ring est uniquement pour les égalités. Pour a < b, il faut nlinarith ou polyrith.
• Polynômes seulement : les expressions avec sin, cos, log, etc. ne passent pas.

Le pont : ring est exposé en Lean-6 (Mathlib Essentials) — d’où la mention dans le code que c’est une tactique Mathlib. Lean-9 (Lean in the Real World) l’utilise pour les preuves sur les expressions algébriques. Lean-12 (Sensitivity) l’emploie pour les preuves de degré polynomial sur les réels. Lean-14 (Finiteness) le combine avec nlinarith pour les bornes non-linéaires.

-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.
-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.

-- Voici ce que `ring` ferait automatiquement :
-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring

-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards
-- pour des egalites plus simples
theorem double_eq (n : Nat) : n + n = 2 * n := by
  simp [Nat.two_mul]

theorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by
  rw [Nat.two_mul, Nat.add_assoc]

-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.

-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.

-- Voici ce que `ring` ferait automatiquement :

-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring

-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards

-- pour des egalites plus simples

theorem double_eq (n : Nat) : n + n = 2 * n := by

  simp [Nat.two_mul]

theorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by

  rw [Nat.two_mul, Nat.add_assoc]

--% env 27

Raw input

{"cmd": "-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\n-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.\n\n-- Voici ce que `ring` ferait automatiquement :\n-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\n\n-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards\n-- pour des egalites plus simples\ntheorem double_eq (n : Nat) : n + n = 2 * n := by\n simp [Nat.two_mul]\n\ntheorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by\n rw [Nat.two_mul, Nat.add_assoc]", "env": 26}

Raw output

{"env": 27}

9. Melange Termes et Tactiques

9.1 by dans un terme

La section 9 complète le notebook en montrant que mode terme et mode tactique ne sont pas mutuellement exclusifs : Lean 4 permet le mode hybride où by ... ouvre un bloc tactique au milieu d’un terme, et inversement, on peut invoquer un terme de preuve à l’intérieur d’une tactique.

Le by dans un terme : la forme by tac retourne un terme de preuve en exécutant les tactiques tac. On peut donc écrire ⟨by exact hp, by exact hq⟩ pour assembler deux preuves via leurs sous-bloc tactiques. C’est la forme la plus courante du mélange.

Pourquoi mélanger ?

• Lisibilité : un terme pur peut être obscur ; ouvrir un by sur le point délicat rend la preuve pédagogique.
• Subset d’une preuve complexe : si une sous-preuve est facile en tactique et le reste en terme, le mode hybride évite de tout convertir.
• Inférence de type : Lean peut typer le by à la volée, laisse la place pour le contexte.

Trois patterns principaux :

1. by dans un constructeur : ⟨by exact hp, by assumption⟩ — assembler deux preuves via leurs sous-bloc tactiques.
2. by dans un f (lambda) : f := fun x => by intro h; exact h — preuve locale d’une lambda.
3. by dans un match : match n with | 0 => by decide | k+1 => by omega — tactic par cas.

Le pont : le mode hybride est très utilisé dans Lean-6 (Mathlib) où les constructeurs anonymes ⟨...⟩ contiennent souvent des by. Lean-12 (Sensitivity) mélange by et exact pour les preuves sur les sommes finies. Lean-14 (Finiteness) utilise by pour les sous-buts dans les match sur les dérivées.

-- Utiliser by au milieu d'un terme
theorem hybrid_proof (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
  ⟨by exact hp, by assumption⟩

-- Preuve partiellement tactique
-- Note: Pour la division sure, on utilise Nat.div directement
-- Lean 4 standard n'a pas de division sure avec preuve integree
def safeDivide (a b : Nat) : Nat :=
  if b = 0 then 0 else a / b

-- Utiliser by au milieu d'un terme

theorem hybrid_proof (p q : Prop) (hp : p) (hq : q) : p ∧ q :=

  ⟨by exact hp, by assumption⟩

-- Preuve partiellement tactique

-- Note: Pour la division sure, on utilise Nat.div directement

-- Lean 4 standard n'a pas de division sure avec preuve integree

def safeDivide (a b : Nat) : Nat :=

  if b = 0 then 0 else a / b

--% env 28

Raw input

{"cmd": "-- Utiliser by au milieu d'un terme\ntheorem hybrid_proof (p q : Prop) (hp : p) (hq : q) : p \u2227 q :=\n \u27e8by exact hp, by assumption\u27e9\n\n-- Preuve partiellement tactique\n-- Note: Pour la division sure, on utilise Nat.div directement\n-- Lean 4 standard n'a pas de division sure avec preuve integree\ndef safeDivide (a b : Nat) : Nat :=\n if b = 0 then 0 else a / b", "env": 27}

Raw output

{"env": 28}

Le mode tactique peut s’imbriquer au c?ur d’un terme : by ... ouvre un bloc tactique n’importe ou un terme est attendu. Cela permet le style hybride – construire la preuve majoritairement en mode terme (ici un couple anonyme) tout en reservant by aux sous-buts qui beneficient d’une approche tactique.

9.2 Termes dans les tactiques

Le symétrique du by est d’utiliser un terme de preuve à l’intérieur d’une tactique. La forme la plus simple est exact t où t est un terme pur, mais on peut aussi développer des termes complexes au milieu d’une preuve.

Patterns fréquents :

• exact ⟨hp, hq⟩ : clore un but p ∧ q avec un constructeur de conjonction.
• exact And.intro hp hq : équivalent plus explicite que ⟨hp, hq⟩.
• exact (h : P → Q) hp : annoter le type intermédiaire avec (h : ...) pour forcer Lean à accepter la conversion.
• exact ⟨w, hw⟩ : témoin implicite pour une preuve existentielle.

Pourquoi garder un terme pur ?

• Court : si la preuve est triviale (1 à 3 étapes), un terme est plus compact qu’une tactique.
• Préféré en définition : les def et abbrev mathématiques s’écrivent en mode terme, sans tactique.
• Inductif simple : pour un constructeur unique, exact ⟨...⟩ est la norme.

Choix tactique vs terme :

Critère	Préférer tactique	Préférer terme
Preuve ≥ 3 étapes	X
Cas multiples à explorer	X (cases, induction)
Témoin à exhiber	X (use, exact)
Convertir un objet	X (norm_cast, ring)
Constructeur trivial		X (exact)
Spécification mathématique		X (def, abbrev)
Calcul direct		X (term-mode)

Le pont : Lean-6 (Mathlib) mélange systématiquement termes et tactiques — par exemple exact (h.symm.trans h') ou exact ⟨by omega, by omega⟩. Lean-12 (Sensitivity) privilégie les tactiques, mais accepte des termes dans les lemmes d’aménagement. Lean-14 (Finiteness) utilise des termes pour les constructions mathématiques et des tactiques pour les preuves.

Conclusion : choisir entre mode terme et mode tactic est une décision de lisibilité : on privilégie le mode qui rend la preuve la plus claire pour le lecteur. En Lean 4, les deux modes sont citoyens de première classe et interchangeables à tout moment.

-- exact accepte n'importe quel terme
theorem term_in_tactic (p q : Prop) (hp : p) (hq : q) : p /\ q := by
  exact ⟨hp, hq⟩   -- Terme structure

-- show ... from ... dans by
theorem show_from (p q : Prop) (hp : p) (hq : q) : p /\ q := by
  show p /\ q
  exact And.intro hp hq

-- exact accepte n'importe quel terme

theorem term_in_tactic (p q : Prop) (hp : p) (hq : q) : p /\ q := by

  exact ⟨hp, hq⟩   -- Terme structure

-- show ... from ... dans by

theorem show_from (p q : Prop) (hp : p) (hq : q) : p /\ q := by

  show p /\ q

  exact And.intro hp hq

--% env 29

Raw input

{"cmd": "-- exact accepte n'importe quel terme\ntheorem term_in_tactic (p q : Prop) (hp : p) (hq : q) : p /\\ q := by\n exact \u27e8hp, hq\u27e9 -- Terme structure\n\n-- show ... from ... dans by\ntheorem show_from (p q : Prop) (hp : p) (hq : q) : p /\\ q := by\n show p /\\ q\n exact And.intro hp hq", "env": 28}

Raw output

{"env": 29}

Reciproquement, exact accepte n’importe quel terme en mode tactique : on peut clore un but en mode tactique avec un terme de preuve pur (le constructeur anonyme de la conjonction). Les deux modes sont donc interchangeables au niveau des feuilles de preuve ; le choix est une question de lisibilite et de style.

Exemples guides : Preuves tactiques

Voici des exemples complets illustrant les tactiques constructor, rw et cases.

Ces exemples reprennent les preuves soumises par @thorgal27 dans le PR #2510, promues en exemples guides. Les solutions integrent : constructor pour les equivalences, intro/cases pour la decomposition, exact pour la fourniture de termes, rw pour la reecriture arithmetique, et left/right pour les disjonctions.

-- Exemple guide 1 : Associativite de la conjonction (avec tactics)
-- Demonstrateur : constructor, intro, cases, exact
theorem and_assoc_practice (p q r : Prop) : (p /\ q) /\ r <-> p /\ (q /\ r) := by
  constructor
  · intro h
    cases h with
    | intro hpq hr =>
      cases hpq with
      | intro hp hq =>
        constructor
        · exact hp
        · constructor
          · exact hq
          · exact hr
  · intro h
    cases h with
    | intro hp hqr =>
      cases hqr with
      | intro hq hr =>
        constructor
        · constructor
          · exact hp
          · exact hq
        · exact hr

-- Exemple guide 2 : Manipulation arithmetique avec rw
-- Demonstrateur : rw avec Nat.two_mul et Nat.add_comm
theorem arith_rw_practice (a b : Nat) : (a + b) + (b + a) = 2 * (a + b) := by
  rw [Nat.two_mul]
  rw [Nat.add_comm b a]

-- Exemple guide 3 : Distribution avec tactics
-- Demonstrateur : constructor, intro, cases, left/right
theorem or_distrib_practice (p q r : Prop) :
  p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r) := by
  constructor
  · intro h
    cases h with
    | intro hp hqr =>
      cases hqr with
      | inl hq =>
        left
        constructor
        · exact hp
        · exact hq
      | inr hr =>
        right
        constructor
        · exact hp
        · exact hr
  · intro h
    cases h with
    | inl hpq =>
      cases hpq with
      | intro hp hq =>
        constructor
        · exact hp
        · left
          exact hq
    | inr hpr =>
      cases hpr with
      | intro hp hr =>
        constructor
        · exact hp
        · right
          exact hr

-- Exemple guide 1 : Associativite de la conjonction (avec tactics)

-- Demonstrateur : constructor, intro, cases, exact

theorem and_assoc_practice (p q r : Prop) : (p /\ q) /\ r <-> p /\ (q /\ r) := by

  constructor

  · intro h

    cases h with

    | intro hpq hr =>

      cases hpq with

      | intro hp hq =>

        constructor

        · exact hp

        · constructor

          · exact hq

          · exact hr

  · intro h

    cases h with

    | intro hp hqr =>

      cases hqr with

      | intro hq hr =>

        constructor

        · constructor

          · exact hp

          · exact hq

        · exact hr

-- Exemple guide 2 : Manipulation arithmetique avec rw

-- Demonstrateur : rw avec Nat.two_mul et Nat.add_comm

theorem arith_rw_practice (a b : Nat) : (a + b) + (b + a) = 2 * (a + b) := by

  rw [Nat.two_mul]

  rw [Nat.add_comm b a]

-- Exemple guide 3 : Distribution avec tactics

-- Demonstrateur : constructor, intro, cases, left/right

theorem or_distrib_practice (p q r : Prop) :

  p /\ (q \/ r) <-> (p /\ q) \/ (p /\ r) := by

  constructor

  · intro h

    cases h with

    | intro hp hqr =>

      cases hqr with

      | inl hq =>

        left

        constructor

        · exact hp

        · exact hq

      | inr hr =>

        right

        constructor

        · exact hp

        · exact hr

  · intro h

    cases h with

    | inl hpq =>

      cases hpq with

      | intro hp hq =>

        constructor

        · exact hp

        · left

          exact hq

    | inr hpr =>

      cases hpr with

      | intro hp hr =>

        constructor

        · exact hp

        · right

          exact hr

--% env 30

Raw input

{"cmd": "-- Exemple guide 1 : Associativite de la conjonction (avec tactics)\n-- Demonstrateur : constructor, intro, cases, exact\ntheorem and_assoc_practice (p q r : Prop) : (p /\\ q) /\\ r <-> p /\\ (q /\\ r) := by\n constructor\n \u00b7 intro h\n cases h with\n | intro hpq hr =>\n cases hpq with\n | intro hp hq =>\n constructor\n \u00b7 exact hp\n \u00b7 constructor\n \u00b7 exact hq\n \u00b7 exact hr\n \u00b7 intro h\n cases h with\n | intro hp hqr =>\n cases hqr with\n | intro hq hr =>\n constructor\n \u00b7 constructor\n \u00b7 exact hp\n \u00b7 exact hq\n \u00b7 exact hr\n\n-- Exemple guide 2 : Manipulation arithmetique avec rw\n-- Demonstrateur : rw avec Nat.two_mul et Nat.add_comm\ntheorem arith_rw_practice (a b : Nat) : (a + b) + (b + a) = 2 * (a + b) := by\n rw [Nat.two_mul]\n rw [Nat.add_comm b a]\n\n-- Exemple guide 3 : Distribution avec tactics\n-- Demonstrateur : constructor, intro, cases, left/right\ntheorem or_distrib_practice (p q r : Prop) :\n p /\\ (q \\/ r) <-> (p /\\ q) \\/ (p /\\ r) := by\n constructor\n \u00b7 intro h\n cases h with\n | intro hp hqr =>\n cases hqr with\n | inl hq =>\n left\n constructor\n \u00b7 exact hp\n \u00b7 exact hq\n | inr hr =>\n right\n constructor\n \u00b7 exact hp\n \u00b7 exact hr\n \u00b7 intro h\n cases h with\n | inl hpq =>\n cases hpq with\n | intro hp hq =>\n constructor\n \u00b7 exact hp\n \u00b7 left\n exact hq\n | inr hpr =>\n cases hpr with\n | intro hp hr =>\n constructor\n \u00b7 exact hp\n \u00b7 right\n exact hr", "env": 29}

Raw output

{"env": 30}

Exercices a completer

Remplacez sorry par votre preuve en utilisant les tactiques vues dans les exemples ci-dessus.

Exercice 1 : Commutativite de la conjunction

Prouvez que p /\ q <-> q /\ p en utilisant constructor, intro, cases et exact.

-- Exercice 1 : Commutativite de la conjunction
-- TODO etudiant : prouvez p /\ q <-> q /\ p
theorem and_comm_exercise (p q : Prop) : p /\ q <-> q /\ p := sorry

-- Exercice 1 : Commutativite de la conjunction

-- TODO etudiant : prouvez p /\ q <-> q /\ p

theorem and_comm_exercise (p q : Prop) : p /\ q <-> q /\ p := sorry
🟨 declaration uses `sorry`

--% env 31

--% prove 0

Raw input

{"cmd": "-- Exercice 1 : Commutativite de la conjunction\n-- TODO etudiant : prouvez p /\\ q <-> q /\\ p\ntheorem and_comm_exercise (p q : Prop) : p /\\ q <-> q /\\ p := sorry\n", "env": 30}

Raw output

{"sorries": [{"proofState": 0, "pos": {"line": 3, "column": 62}, "goal": "p q : Prop\n⊢ p ∧ q ↔ q ∧ p", "endPos": {"line": 3, "column": 67}}], "messages": [{"severity": "warning", "pos": {"line": 3, "column": 8}, "endPos": {"line": 3, "column": 25}, "data": "declaration uses `sorry`"}], "env": 31}

Exercice 2 : Addition avec associativite et commutativite

Prouvez que (a + b) + c = (c + a) + b en utilisant rw avec les lemmes de Nat.

-- Exercice 2 : Rearrangement avec rw
-- TODO etudiant : prouvez (a + b) + c = (c + a) + b
-- Indice : Nat.add_assoc, Nat.add_comm
theorem rearrange_exercise (a b c : Nat) : (a + b) + c = (c + a) + b := sorry

-- Exercice 2 : Rearrangement avec rw

-- TODO etudiant : prouvez (a + b) + c = (c + a) + b

-- Indice : Nat.add_assoc, Nat.add_comm

theorem rearrange_exercise (a b c : Nat) : (a + b) + c = (c + a) + b := sorry
🟨 declaration uses `sorry`

--% env 32

--% prove 1

Raw input

{"cmd": "-- Exercice 2 : Rearrangement avec rw\n-- TODO etudiant : prouvez (a + b) + c = (c + a) + b\n-- Indice : Nat.add_assoc, Nat.add_comm\ntheorem rearrange_exercise (a b c : Nat) : (a + b) + c = (c + a) + b := sorry\n", "env": 31}

Raw output

{"sorries": [{"proofState": 1, "pos": {"line": 4, "column": 72}, "goal": "a b c : Nat\n⊢ a + b + c = c + a + b", "endPos": {"line": 4, "column": 77}}], "messages": [{"severity": "warning", "pos": {"line": 4, "column": 8}, "endPos": {"line": 4, "column": 26}, "data": "declaration uses `sorry`"}], "env": 32}

Exercice 3 : De Morgan avec tactics

Prouvez que ¬(p ∨ q) <-> ¬p ∧ ¬q en utilisant constructor, intro, cases, contradiction.

-- Exercice 3 : De Morgan
-- TODO etudiant : prouvez la premiere direction de De Morgan
theorem de_morgan_exercise (p q : Prop) : ¬(p \/ q) -> ¬p /\ ¬q := sorry

-- Exercice 3 : De Morgan

-- TODO etudiant : prouvez la premiere direction de De Morgan

theorem de_morgan_exercise (p q : Prop) : ¬(p \/ q) -> ¬p /\ ¬q := sorry
🟨 declaration uses `sorry`

--% env 33

--% prove 2

Raw input

{"cmd": "-- Exercice 3 : De Morgan\n-- TODO etudiant : prouvez la premiere direction de De Morgan\ntheorem de_morgan_exercise (p q : Prop) : \u00ac(p \\/ q) -> \u00acp /\\ \u00acq := sorry\n", "env": 32}

Raw output

{"sorries": [{"proofState": 2, "pos": {"line": 3, "column": 67}, "goal": "p q : Prop\n⊢ ¬(p ∨ q) → ¬p ∧ ¬q", "endPos": {"line": 3, "column": 72}}], "messages": [{"severity": "warning", "pos": {"line": 3, "column": 8}, "endPos": {"line": 3, "column": 26}, "data": "declaration uses `sorry`"}], "env": 33}

Resume des Tactiques

Tactique	Usage	Exemple
exact t	Fournir le terme exact	exact hp
intro x	Introduire hypothese/variable	intro hp hq
apply h	Appliquer un lemme	apply Nat.add_comm
assumption	Chercher dans contexte	assumption
rfl	Reflexivite/calcul	rfl
constructor	Introduction structure	constructor
cases h	Analyse par cas	cases h with ...
left/right	Choisir branche Or	left
have h : P := ...	Lemme intermediaire	have hq := ...
rw [h]	Reecriture	rw [Nat.add_zero]
simp	Simplification auto	simp [h]
contradiction	Detecter absurdite	contradiction
induction n	Recurrence	induction n with ...
omega	Arithmetique linéaire	omega
ring	Algebre polynomiale	ring

Prochaine étape

Dans le notebook Lean-06-Mathlib-Essentials-Lean, nous explorerons Mathlib4, la bibliotheque mathematique communautaire de Lean 4, avec ses tactiques puissantes et sa vaste collection de théorèmes.

---

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

---

Navigation : ← Lean-04-Quantifiers-Lean | Index | Lean-06-Mathlib-Essentials-Lean →

Lire une preuve : classifier par tactique d’ouverture

Le tableau ci-dessus classe les tactiques par ce qu’elles font. Une autre grille, complémentaire, classe par ce qui ouvre la preuve — c’est-à-dire la première tactique qui apparaît après by. Cette vue aide à lire un théorème dont on voit la preuve : avant de suivre les étapes, on identifie la forme de la preuve.

Première tactique	Forme de la preuve	Signal dans ⊢	Exemple typique
rfl	Triviale par définition	Le but est x = x (après réduction)	rfl : réflexivité de Eq
exact	Terme explicite	Le but correspond directement à un terme connu	exact hp : utilise une hypothèse
intro	Assume-and-show	Le but est ∀ x, P x ou P → Q	intro n puis induction
apply	Délégation à un lemme	Le but est la conclusion d’un lemme connu	apply Nat.add_comm
cases	Analyse par cas	Le but dépend d’un ∨ ou d’un type inductif	cases h with \| inl hp \| inr hq
constructor	Construction pièce par pièce	Le but est P ∧ Q ou ⟨A, B⟩	constructor pour les introductions
induction	Récurrence	Le but porte sur un type inductif (Nat, List, etc.)	induction n with \| zero => ... \| succ n ih => ...
simp / omega / ring / norm_num	Décision automatique	Le but est dans le domaine du décideur	omega pour l’arithmétique linéaire
rw [...]	Réécriture	Le but est une égalité où un côté contient un sous-terme	rw [Nat.add_comm]
have / let	Lemme intermédiaire	Le but complet est dur, on le décompose	have hq := hpq hp

Application : face à une preuve comme

theorem exemple (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [ih]

la lecture est : forme = récurrence sur Nat (opening = induction), cas de base trivial (rfl), cas inductif par simplification utilisant l’hypothèse d’induction (simp avec ih). On n’a pas besoin de comprendre chaque étape pour saisir la structure.

Lien avec Lean-3 et Lean-4 : cette grille s’applique aussi en term-style (fun h => ...) et avec quantificateurs (intro = ∀, use/⟨_, _⟩ = ∃, obtain = destruction de ∃). Le réflexe « lire la première tactique / le premier mot-clé » est universel.