Sudoku-19 — Soundness de la propagation de contraintes (companion formel natif)

Ce notebook est le companion formel du lake sudoku_lean, dont la lib Sudoku prouve la soundness des règles de propagation d’un Sudoku (naked single, hidden single) : ces règles, utilisées par tous les solveurs (backtracking, OR-Tools, .NET), ne retirent aucune solution valide — elles n’éliminent que des affectations impossibles. Résultat central de la série Sudoku (issue #4055), avec zéro sorry.

L’idée : une cellule affectée exclut sa valeur de toutes ses cellules paires (clé de voûte peer_excludes_value). De là dérivent par l’absurde les deux règles de propagation, qui ne perdent donc jamais une solution.

Convention de vérification — `#check` natif dans le kernel Lean

Ce notebook est un notebook Lean natif (kernel lean4-wsl) : il importe les modules du lake directement et le compilateur Lean rend les signatures dans le notebook. C’est rendu possible par l’UNLOCK (patch lean4_jupyter + jonction Mathlib #2611).

⚠️ À l’exécution, la première cellule (import) peut prendre ~3 min : le kernel charge les oleans Mathlib via la jonction NTFS. Les suivantes sont instantanées.

1. Import des modules du lake `sudoku_lean`

Le lake est structuré en 2 modules (Basic, Propagation) sous le namespace Sudoku. On importe les 2 modules (la config submodules du lake ne build pas l’umbrella racine — on cible directement les modules qui portent les définitions).

import Sudoku.Basic
import Sudoku.Propagation
import Sudoku.ExactCover
open Sudoku

import Sudoku.Basic

import Sudoku.Propagation

import Sudoku.ExactCover

open Sudoku

--% env 0

Raw input

{"cmd": "import Sudoku.Basic\nimport Sudoku.Propagation\nimport Sudoku.ExactCover\nopen Sudoku\n"}

Raw output

{"env": 0}

2. Preuve sans `sorry` — `#print axioms`

La clé de voûte peer_excludes_value et les deux théorèmes de soundness qui en dérivent (naked_single_sound, hidden_single_sound) ne dépendent que de deux axiomes (propext, Quot.sound) — pas de sorryAx et pas même de Classical.choice — ce qui prouve que la preuve est complète (0 sorry) et constructive (par l’absurde via Classical.em, dérivable de propext + Quot.sound). Le lemme full_house_present (pigeonhole) utilise Classical.choice (card_image_of_injOn), donc 3 axiomes.

#print axioms peer_excludes_value
#print axioms naked_single_sound
#print axioms hidden_single_sound

#print axioms peer_excludes_value 'Sudoku.peer_excludes_value' depends on axioms: [propext, Quot.sound]

#print axioms naked_single_sound 'Sudoku.naked_single_sound' depends on axioms: [propext, Quot.sound]

#print axioms hidden_single_sound 'Sudoku.hidden_single_sound' depends on axioms: [propext, Quot.sound]

--% env 1

Raw input

{"cmd": "#print axioms peer_excludes_value\n#print axioms naked_single_sound\n#print axioms hidden_single_sound", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'Sudoku.peer_excludes_value' depends on axioms: [propext, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "'Sudoku.naked_single_sound' depends on axioms: [propext, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "'Sudoku.hidden_single_sound' depends on axioms: [propext, Quot.sound]"}],
 "env": 1}

3. La structure de contraintes abstraite d’un Sudoku

Le module Sudoku/Basic.lean formalise un Sudoku de façon abstraite : tout CSP « à portées toutes-distinctes ». Le 9×9 concret (lignes, colonnes, blocs) en est une instance, non un cas spécial — les théorèmes de soundness valent pour toute structure de ce type.

Scopes ι = Finset (Finset ι) — un ensemble fini de portées (chacune un Finset de cellules).
Solution ι V = ι → V — une affectation complète (une valeur par cellule).
AllDistinctOn σ s — σ est toutes-distinctes sur s (injectivité de σ sur s).
IsSolution scopes σ — σ est toutes-distinctes sur chacune des portées (invariant fondamental).
IsPeer scopes c c' — c' est une paire de c (distinctes, partagent une portée).
PresentIn σ s v — la valeur v est présente dans la portée s.

Le lemme full_house_present (pigeonhole) : une portée « pleine maison » (s.card = card V) porte toute valeur dans toute solution.

#check Scopes
#check Solution
#check AllDistinctOn
#check IsSolution
#check IsPeer
#check PresentIn
#check full_house_present

#check Scopes Sudoku.Scopes.{u_3} (ι : Type u_3) : Type u_3

#check Solution Sudoku.Solution.{u_3, u_4} (ι : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

#check AllDistinctOn Sudoku.AllDistinctOn.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (σ : Solution ι V) (s : Finset ι) : Prop

#check IsSolution Sudoku.IsSolution.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (scopes : Scopes ι) (σ : Solution ι V) : Prop

#check IsPeer Sudoku.IsPeer.{u_1} {ι : Type u_1} (scopes : Scopes ι) (c c' : ι) : Prop

#check PresentIn Sudoku.PresentIn.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (σ : Solution ι V) (s : Finset ι) (v : V) : Prop

#check full_house_present Sudoku.full_house_present.{u_3, u_4} {ι : Type u_3} {V : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (σ : Solution ι V) (s : Finset ι) (v : V) (hcard : s.card = Fintype.card V)
  (hAD : AllDistinctOn σ s) : PresentIn σ s v

--% env 2

Raw input

{"cmd": "#check Scopes\n#check Solution\n#check AllDistinctOn\n#check IsSolution\n#check IsPeer\n#check PresentIn\n#check full_house_present", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data": "Sudoku.Scopes.{u_3} (ι : Type u_3) : Type u_3"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Sudoku.Solution.{u_3, u_4} (ι : Type u_3) (V : Type u_4) : Type (max u_3 u_4)"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Sudoku.AllDistinctOn.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (σ : Solution ι V) (s : Finset ι) : Prop"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Sudoku.IsSolution.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (scopes : Scopes ι) (σ : Solution ι V) : Prop"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Sudoku.IsPeer.{u_1} {ι : Type u_1} (scopes : Scopes ι) (c c' : ι) : Prop"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Sudoku.PresentIn.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (σ : Solution ι V) (s : Finset ι) (v : V) : Prop"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "Sudoku.full_house_present.{u_3, u_4} {ι : Type u_3} {V : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (σ : Solution ι V) (s : Finset ι) (v : V) (hcard : s.card = Fintype.card V)\n  (hAD : AllDistinctOn σ s) : PresentIn σ s v"}],
 "env": 2}

Lecture : modéliser un CSP à portées toutes-distinctes

Symbole Lean	Lecture
`Scopes ι`	ensemble fini de portées (`Finset (Finset ι)`)
`Solution ι V`	affectation : une valeur par cellule (`ι → V`)
`AllDistinctOn σ s`	`σ` injective sur la portée `s`
`IsSolution scopes σ`	`σ` valide sur toutes les portées
`IsPeer scopes c c'`	`c'` paire de `c` (partagent une portée)
`full_house_present`	portée pleine maison ⟹ toute valeur présente (pigeonhole)

4. La clé de voûte et la soundness des règles de propagation

Le module Sudoku/Propagation.lean prouve la soundness des deux règles canoniques de propagation, à partir d’une unique clé de voûte :

peer_excludes_value (clé de voûte) : une cellule c portant v exclut v de toute paire c' (σ c' ≠ v). Preuve : c et c' partagent une portée ; σ toutes-distinctes dessus ⟹ σ c = σ c' impliquerait c = c', contredisant c ≠ c'.
naked_single_sound : si toutes les valeurs sauf v sont déjà portées par des paires de c, alors σ c = v (par l’absurde via peer_excludes_value).
hidden_single_sound : si v est présente dans la portée s et exclue de toute autre cellule de s, alors σ c = v où c est l’unique cellule possible.

Ces règles ne retirent aucune solution valide : elles identifient des valeurs forcées.

#check peer_excludes_value
#check naked_single_sound
#check hidden_single_sound

#check peer_excludes_value Sudoku.peer_excludes_value.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ) (c c' : ι) (v : V)
  (hpeer : IsPeer scopes c c') (hcv : σ c = v) : σ c' ≠ v

#check naked_single_sound Sudoku.naked_single_sound.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ) (c : ι) (v : V)
  (hcover : ∀ (w : V), w ≠ v → ∃ c', IsPeer scopes c c' ∧ σ c' = w) : σ c = v

#check hidden_single_sound Sudoku.hidden_single_sound.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ) (s : Finset ι) (_hs : s ∈ scopes)
  (c : ι) (v : V) (_hcs : c ∈ s) (hvin : PresentIn σ s v)
  (hexcl : ∀ c' ∈ s, c' ≠ c → ∃ c'', IsPeer scopes c' c'' ∧ σ c'' = v) : σ c = v

--% env 3

Raw input

{"cmd": "#check peer_excludes_value\n#check naked_single_sound\n#check hidden_single_sound", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Sudoku.peer_excludes_value.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ) (c c' : ι) (v : V)\n  (hpeer : IsPeer scopes c c') (hcv : σ c = v) : σ c' ≠ v"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Sudoku.naked_single_sound.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ) (c : ι) (v : V)\n  (hcover : ∀ (w : V), w ≠ v → ∃ c', IsPeer scopes c c' ∧ σ c' = w) : σ c = v"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Sudoku.hidden_single_sound.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ) (s : Finset ι) (_hs : s ∈ scopes)\n  (c : ι) (v : V) (_hcs : c ∈ s) (hvin : PresentIn σ s v)\n  (hexcl : ∀ c' ∈ s, c' ≠ c → ∃ c'', IsPeer scopes c' c'' ∧ σ c'' = v) : σ c = v"}],
 "env": 3}

Lecture : la propagation ne perd aucune solution

Théorème	Conclusion
`peer_excludes_value`	cellule affectée exclut sa valeur de ses paires (clé de voûte)
`naked_single_sound`	un seul candidat `v` restant ⟹ `σ c = v`
`hidden_single_sound`	`v` n’a qu’une cellule possible dans `s` ⟹ `σ c = v`

Le jalon restant (honnêtement)

La complétude des règles de propagation (suffisent-elles à résoudre tout Sudoku ? non en général — d’où le backtracking en complément) reste un jalon naturel ouvert, délibérément non sorry-backed : la lib reste entièrement sorry-free. La réduction à la couverture exacte est désormais prouvée (section suivante, sudoku_iff_exact_cover). Le résultat « 17 indices minimum » est hors scope (calcul massif, non formalisable).

5. La chaîne causale complète

Les deux modules composent une chaîne unique, de la structure abstraite à la soundness :

Basic — Scopes/Solution/AllDistinctOn/IsSolution/IsPeer/PresentIn
- full_house_present (pigeonhole : portée pleine maison ⟹ toute valeur présente).
Propagation — peer_excludes_value (clé de voûte) ⟶ naked_single_sound + hidden_single_sound (soundness des deux règles, par l’absurde).
ExactCover — toSelection + lemme-clé mem_toSelection_iff ⟶ solution_imp_exact_cover (sens direct) + exact_cover_imp_solution (sens retour) ⟶ sudoku_iff_exact_cover (équivalence complète avec la couverture exacte de Knuth, sous hypothèse « pleine maison » satisfaite par le 9×9).

6. La réduction Sudoku ⇔ couverture exacte (Knuth)

La couverture exacte (Knuth 2000, « Dancing Links ») encode le Sudoku comme un problème universel : chaque contrainte (cellule, portée×valeur) est un « élément » à couvrir, chaque placement (c, v) une option. Une solution Sudoku est alors exactement une couverture exacte — chaque élément couvert une et une seule fois.

Le théorème capstone sudoku_iff_exact_cover établit l’équivalence complète, sous l’hypothèse « pleine maison » ∀ s ∈ scopes, s.card = card V (satisfaite par le 9×9 où chaque portée a 9 cellules pour 9 valeurs) :

(∃ σ, IsSolution scopes σ) ↔︎ (∃ sel, IsExactCover sel scopes).

Lemme-clé mem_toSelection_iff : (c, v) ∈ toSelection σ ↔︎ σ c = v — toute question sur la sélection se ramène à une question sur σ. Le sens direct utilise la pige full_house_present (existence) + AllDistinctOn (unicité) ; le sens retour construit l’affectation inverse fromSelection et montre que deux cellules d’une même portée portant la même valeur violeraient l’unicité ∃! de la paire (portée, valeur).

0 sorry, axiomes = trio standard du noyau Lean (propext, Classical.choice, Quot.sound) — Classical.choice pour la construction non constructive fromSelection, aucun axiome ad hoc.

#check ExactCover.IsExactCover
#check toSelection
#check mem_toSelection_iff
#check solution_imp_exact_cover
#check exact_cover_imp_solution
#check sudoku_iff_exact_cover
#print axioms sudoku_iff_exact_cover

#check ExactCover.IsExactCover Sudoku.ExactCover.IsExactCover.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (sel : ExactCover.Sel ι V) (scopes : Scopes ι) :
  Prop

#check toSelection Sudoku.toSelection.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq V]
  (σ : Solution ι V) : ExactCover.Sel ι V

#check mem_toSelection_iff Sudoku.mem_toSelection_iff.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (σ : Solution ι V) (c : ι) (v : V) : (c, v) ∈ toSelection σ ↔ σ c = v

#check solution_imp_exact_cover Sudoku.solution_imp_exact_cover.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ)
  (hfull : ∀ s ∈ scopes, s.card = Fintype.card V) : ExactCover.IsExactCover (toSelection σ) scopes

#check exact_cover_imp_solution Sudoku.exact_cover_imp_solution.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (scopes : Scopes ι) (sel : ExactCover.Sel ι V) (hec : ExactCover.IsExactCover sel scopes) :
  ∃ σ, IsSolution scopes σ ∧ toSelection σ = sel

#check sudoku_iff_exact_cover Sudoku.sudoku_iff_exact_cover.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]
  [DecidableEq V] (scopes : Scopes ι) (hfull : ∀ s ∈ scopes, s.card = Fintype.card V) :
  (∃ σ, IsSolution scopes σ) ↔ ∃ sel, ExactCover.IsExactCover sel scopes

#print axioms sudoku_iff_exact_cover 'Sudoku.sudoku_iff_exact_cover' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 4

Raw input

{"cmd": "#check ExactCover.IsExactCover\n#check toSelection\n#check mem_toSelection_iff\n#check solution_imp_exact_cover\n#check exact_cover_imp_solution\n#check sudoku_iff_exact_cover\n#print axioms sudoku_iff_exact_cover\n", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Sudoku.ExactCover.IsExactCover.{u_1, u_2} {ι : Type u_1} {V : Type u_2} (sel : ExactCover.Sel ι V) (scopes : Scopes ι) :\n  Prop"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Sudoku.toSelection.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq V]\n  (σ : Solution ι V) : ExactCover.Sel ι V"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Sudoku.mem_toSelection_iff.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (σ : Solution ι V) (c : ι) (v : V) : (c, v) ∈ toSelection σ ↔ σ c = v"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Sudoku.solution_imp_exact_cover.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (scopes : Scopes ι) (σ : Solution ι V) (hσ : IsSolution scopes σ)\n  (hfull : ∀ s ∈ scopes, s.card = Fintype.card V) : ExactCover.IsExactCover (toSelection σ) scopes"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Sudoku.exact_cover_imp_solution.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (scopes : Scopes ι) (sel : ExactCover.Sel ι V) (hec : ExactCover.IsExactCover sel scopes) :\n  ∃ σ, IsSolution scopes σ ∧ toSelection σ = sel"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Sudoku.sudoku_iff_exact_cover.{u_1, u_2} {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype V]\n  [DecidableEq V] (scopes : Scopes ι) (hfull : ∀ s ∈ scopes, s.card = Fintype.card V) :\n  (∃ σ, IsSolution scopes σ) ↔ ∃ sel, ExactCover.IsExactCover sel scopes"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "'Sudoku.sudoku_iff_exact_cover' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 4}

6. Exemple guidé et exercices

Exercice 1 — Paires et exclusion de candidats (Python)

Ancrez l’intuition : modélisez un mini-Sudoku comme un ensemble de portées, et implémentez is_peer (deux cellules sont paires si distinctes ET partagent une portée) puis eliminate (une cellule affectée exclut sa valeur de tous ses pairs).

def is_peer(scopes, c, cprime):
    # c et cprime sont paires : distincts ET partagent au moins une portee
    if c == cprime:
        return False
    # TODO etudiant : existe-t-il une portee s contenant a la fois c et cprime ?
    return None  # TODO

def eliminate(scopes, candidates, c, v):
    # c porte v : retirer v des candidats de tous les pairs de c
    # TODO etudiant : pour chaque paire c' de c, retirer v de candidates[c']
    return None  # TODO

Exercice 2 — Une cellule n’est pas sa propre paire (Lean)

Prouvez qu’une cellule n’est jamais paire d’elle-même : ¬ IsPeer scopes c c. Indice : IsPeer exige c ≠ c' (première conjonction). Si c = c', cette conjonction est fausse.

-- TODO etudiant : remplacer le sorry
-- example : ¬ IsPeer scopes c c := by
--   intro h
--   exact h.1 rfl

Exercice 3 — Naked single et hidden single (Python)

Mettez en évidence la différence entre les deux règles sur un mini-Sudoku (candidats = ensemble de valeurs possibles par cellule). Implémentez naked_single (une cellule n’a plus qu’un candidat) et hidden_single (une valeur n’a qu’une seule cellule possible dans une portée). Vérifiez que les deux réduisent les candidats sans perte.

def naked_single(candidates):
    # Naked single : une cellule dont le seul candidat restant est v doit valoir v
    # TODO etudiant : retourne {cell: v} pour les cellules a candidat unique
    return None  # TODO

def hidden_single(candidates, scopes):
    # Hidden single : une valeur n'allant que dans une cellule d'une portee y va
    # TODO etudiant : pour chaque portee et valeur, si une seule cellule peut la porter
    return None  # TODO

Conclusion

Ce companion natif exhibe la preuve formelle 0-sorry de la soundness de la propagation de contraintes Sudoku dans le kernel Lean lui-même : #check et #print axioms rendent les signatures et les axiomes réels produits par le compilateur, sans intermédiaire Python.

La clé de voûte peer_excludes_value fonde les deux règles naked_single_sound et hidden_single_sound : la propagation ne retire aucune solution valide, elle n’élimine que des affectations qu’aucune solution n’utilise. C’est le fondement formel des solveurs Sudoku (backtracking, OR-Tools, .NET) enseignés dans la série.

Jalon ouvert : seule la complétude des règles (suffisent-elles à résoudre tout Sudoku ?) reste non formalisée ; la lib reste sorry-free. La réduction à la couverture exacte est prouvée (sudoku_iff_exact_cover, section 6).

Retour au sommet

Convention de vérification — #check natif dans le kernel Lean

1. Import des modules du lake sudoku_lean

2. Preuve sans sorry — #print axioms

3. La structure de contraintes abstraite d’un Sudoku

Lecture : modéliser un CSP à portées toutes-distinctes

4. La clé de voûte et la soundness des règles de propagation

Lecture : la propagation ne perd aucune solution

Le jalon restant (honnêtement)

5. La chaîne causale complète

6. La réduction Sudoku ⇔ couverture exacte (Knuth)

6. Exemple guidé et exercices

Exercice 1 — Paires et exclusion de candidats (Python)

Exercice 2 — Une cellule n’est pas sa propre paire (Lean)

Exercice 3 — Naked single et hidden single (Python)

Conclusion

Convention de vérification — `#check` natif dans le kernel Lean

1. Import des modules du lake `sudoku_lean`

2. Preuve sans `sorry` — `#print axioms`