Planners-5b — Admissibilité de la relaxation sans-delete (companion formel natif)

Ce notebook est le companion formel du lake planning_lean, dont la lib Planning prouve l’admissibilité de la relaxation (heuristique \(h^+\)) : la relaxation sans-delete ne surestime jamais le coût réel (\(h^+ \le h^*\)) — un résultat central de la planification classique (Pearl 1984, Bonet & Geffner 2001), sans sorry.

L’idée : dans la transition relaxée stepR, on ignore les effets de deletion des actions STRIPS. Comme step a s ⊆ stepR a s (on enlève moins), tout plan réel est atteignable en relaxation, d’où \(h^+ \le h^*\).

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 planning_lean

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

import Planning.Strips
import Planning.Relaxation
import Planning.Admissibility
open PlanningLean

2. Preuve sans sorry — #print axioms

Le théorème phare relaxed_plan_admissible (admissibilité \(h^+ \le h^*\)) ne dépend que des 3 axiomes standards de Lean (propext, Classical.choice, Quot.sound) — pas de sorryAx — ce qui prouve que la preuve est complète.

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

3. Le modèle STRIPS — fluents, états, actions, transitions

Le module Planning/Strips.lean pose le cadre de la planification STRIPS :

  • State F = Finset F — un état = l’ensemble des fluents actuellement vrais.
  • Action F — une action : préconditions pre, effets additifs add, deletions del.
  • step a s = (s \ a.del) ∪ a.add — la transition réelle (on retire les deletions).
  • stepR a s = s ∪ a.add — la transition relaxée (on ignore les deletions).

Le lemme clé step_subset_stepR : step a s ⊆ stepR a s car s \ a.del ⊆ s.

#check State
#check Action
#check step
#check stepR
#check step_subset_stepR
PlanningLean.State (F : Type) : Type
PlanningLean.Action (F : Type) : Type
PlanningLean.step {F : Type} [DecidableEq F] (a : PlanningLean.Action F) (s : State F) : State F
PlanningLean.stepR {F : Type} [DecidableEq F] (a : PlanningLean.Action F) (s : State F) : State F
PlanningLean.step_subset_stepR {F : Type} [DecidableEq F] (a : PlanningLean.Action F) (s : State F) :
  step a s ⊆ stepR a s

Lecture : réel vs relaxé, au niveau d’une action

Symbole Lean Lecture
State F état = ensemble de fluents (Finset F)
Action F action (pre/add/del)
step a s transition réelle : (s \ del) ∪ add
stepR a s transition relaxée : s ∪ add (ignore del)
step_subset_stepR step a s ⊆ stepR a s (cœur de la relaxation)

4. Exécution relaxée des plans — monotonie et lemme central

Le module Planning/Relaxation.lean étend la transition au plan entier :

  • run π s / runR π s — exécution (réelle / relaxée) d’une séquence d’actions.
  • reaches π s g / reachesR π s g — le plan atteint le but g depuis s.
  • runR_mono — l’exécution relaxée est monotone en l’état initial (s ⊆ s' ⟹ runR π s ⊆ runR π s'), ce qui rend le calcul relaxé polynomial.
  • run_subset_runR — le lemme central : toute exécution réelle est incluse dans la relaxation (run π s ⊆ runR π s), par induction sur la longueur du plan.
#check run
#check runR
#check reaches
#check reachesR
#check runR_mono
#check run_subset_runR
PlanningLean.run {F : Type} [DecidableEq F] : List (PlanningLean.Action F) → State F → State F
PlanningLean.runR {F : Type} [DecidableEq F] : List (PlanningLean.Action F) → State F → State F
PlanningLean.reaches {F : Type} [DecidableEq F] (π : List (PlanningLean.Action F)) (s g : State F) : Prop
PlanningLean.reachesR {F : Type} [DecidableEq F] (π : List (PlanningLean.Action F)) (s g : State F) : Prop
PlanningLean.runR_mono {F : Type} [DecidableEq F] (π : List (PlanningLean.Action F)) {s s' : State F} (h : s ⊆ s') :
  runR π s ⊆ runR π s'
PlanningLean.run_subset_runR {F : Type} [DecidableEq F] (π : List (PlanningLean.Action F)) (s : State F) :
  run π s ⊆ runR π s

Lecture : du pas local au plan entier

Symbole Lean Lecture
run π s exécution réelle du plan π depuis s
runR π s exécution relaxée (sans-delete)
reaches π s g π atteint g en exécution réelle
runR_mono monotonie relaxée (calcul polynomial)
run_subset_runR run π s ⊆ runR π s (induction sur π)

4bis. Monotonie en l’état initial — step_mono / run_mono du lake, illustrés sur un domaine jouet

La relaxation rend l’état croissant le long du plan (stepR a s = s ∪ a.add ne retire jamais rien). Mais il existe une seconde monotonie, plus discrète, que le lake prouve aussi pour la transition réelle (celle qui applique les deletions) :

\[s \subseteq s' \quad\Longrightarrow\quad \texttt{step}\ a\ s \subseteq \texttt{step}\ a\ s'\]

Un état de départ mieux informé (plus de fluents vrais) reste mieux informé après une action, même destructrice. Ce sont step_mono (niveau action, Strips.lean:69) et run_mono (niveau plan, Relaxation.lean:41, par induction sur la longueur du plan) — les contreparties réelles de stepR_mono/runR_mono du lemme central.

Encadré par le vrai : le lake est chargé depuis la cellule 3 (import Planning.Strips / Planning.Relaxation / Planning.Admissibility) — un #check @PlanningLean.step_mono dans le kernel lean4-wsl rendrait la signature canonique. Le kernel lean4-wsl n’est pas exécutable sur ce runner (RECOVERABLE-MACHINE : wrapper /home/jesse/... codé en dur v6, repl binaire absent d’elan install, cf MEMORY.md c.380) — les signatures des deux lemmes sont donc reproduites ici en markdown depuis le source du lake (lecture directe Strips.lean:69 et Relaxation.lean:41), pas générées par #check :

-- Strips.lean:69
lemma step_mono (a : Action F) {s s' : State F} (h : s ⊆ s') : step a s ⊆ step a s'

-- Relaxation.lean:41 (preuve par induction sur π)
lemma run_mono (π : List (Action F)) {s s' : State F} (h : s ⊆ s') : run π s ⊆ run π s'
  | cons a π ih => exact ih (step_mono a h)

Le domaine jouet qui suit (ToyAction / toyStep / toyRun, List au lieu de Finset, sans Mathlib) illustre l’instance sur un exemple concret decide-able — decide ne marche pas sur Finset général, c’est pourquoi le jouet existe. Les preuves génériques restent dans le lake (et sont rejouables par un futur #check quand le kernel sera disponible sur ce runner).

Démonstration sur le domaine jouet : un monde à trois fluents où l’action pickup exige onTable et clear, ajoute held et détruit onTable et clear.

-- Version simplifiee du lake : List au lieu de Finset, sans Mathlib
structure ToyAction (F : Type) where
  pre : List F
  add : List F
  del : List F

/-- Transition reelle : on retire les deletions puis on ajoute les add. -/
def toyStep {F : Type} [BEq F] (a : ToyAction F) (s : List F) : List F :=
  (s.filter (fun x => !a.del.contains x)) ++ a.add

/-- Execution d'un plan : pli sur les actions. -/
def toyRun {F : Type} [BEq F] (acts : List (ToyAction F)) (s : List F) : List F :=
  acts.foldl (fun s' a => toyStep a s') s

-- Domaine jouet : monde des blocs a un seul bloc (3 fluents)
inductive Fl where
  | onTable | clear | held
  deriving DecidableEq, Repr

-- pickup : prendre le bloc pose sur la table (il doit etre degage)
def pickup : ToyAction Fl where
  pre := [Fl.onTable, Fl.clear]
  add := [Fl.held]
  del := [Fl.onTable, Fl.clear]

-- un etat mieux informe : s inclus dans s'
example : [Fl.onTable] ⊆ [Fl.onTable, Fl.clear] := by decide

-- step_mono SUR L'INSTANCE : meme avec deux deletions, l'ordre est preserve
example : toyStep pickup [Fl.onTable] ⊆ toyStep pickup [Fl.onTable, Fl.clear] := by
  decide

-- Les deux transitions calculees : l'egalite des images
#eval toyStep pickup [Fl.onTable]
#eval toyStep pickup [Fl.onTable, Fl.clear]

-- Version simplifiee du lake : List au lieu de Finset, sans Mathlib
structure ToyAction (F : Type) where
  pre : List F
  add : List F
  del : List F
/-- Transition reelle : on retire les deletions puis on ajoute les add. -/
def toyStep {F : Type} [BEq F] (a : ToyAction F) (s : List F) : List F :=
  (s.filter (fun x => !a.del.contains x)) ++ a.add
/-- Execution d'un plan : pli sur les actions. -/
def toyRun {F : Type} [BEq F] (acts : List (ToyAction F)) (s : List F) : List F :=
  acts.foldl (fun s' a => toyStep a s') s
-- Domaine jouet : monde des blocs a un seul bloc (3 fluents)
inductive Fl where
  | onTable | clear | held
  deriving DecidableEq, Repr
-- pickup : prendre le bloc pose sur la table (il doit etre degage)
def pickup : ToyAction Fl where
  pre := [Fl.onTable, Fl.clear]
  add := [Fl.held]
  del := [Fl.onTable, Fl.clear]
-- un etat mieux informe : s inclus dans s'
example : [Fl.onTable] ⊆ [Fl.onTable, Fl.clear] := by decide
-- step_mono SUR L'INSTANCE : meme avec deux deletions, l'ordre est preserve
example : toyStep pickup [Fl.onTable] ⊆ toyStep pickup [Fl.onTable, Fl.clear] := by
  decide
-- Les deux transitions calculees : l'egalite des images
 [Fl.held]
 [Fl.held]
--% env 0
Raw input {"cmd": "-- Version simplifiee du lake : List au lieu de Finset, sans Mathlib\nstructure ToyAction (F : Type) where\n pre : List F\n add : List F\n del : List F\n\n/-- Transition reelle : on retire les deletions puis on ajoute les add. -/\ndef toyStep {F : Type} [BEq F] (a : ToyAction F) (s : List F) : List F :=\n (s.filter (fun x => !a.del.contains x)) ++ a.add\n\n/-- Execution d'un plan : pli sur les actions. -/\ndef toyRun {F : Type} [BEq F] (acts : List (ToyAction F)) (s : List F) : List F :=\n acts.foldl (fun s' a => toyStep a s') s\n\n-- Domaine jouet : monde des blocs a un seul bloc (3 fluents)\ninductive Fl where\n | onTable | clear | held\n deriving DecidableEq, Repr\n\n-- pickup : prendre le bloc pose sur la table (il doit etre degage)\ndef pickup : ToyAction Fl where\n pre := [Fl.onTable, Fl.clear]\n add := [Fl.held]\n del := [Fl.onTable, Fl.clear]\n\n-- un etat mieux informe : s inclus dans s'\nexample : [Fl.onTable] \u2286 [Fl.onTable, Fl.clear] := by decide\n\n-- step_mono SUR L'INSTANCE : meme avec deux deletions, l'ordre est preserve\nexample : toyStep pickup [Fl.onTable] \u2286 toyStep pickup [Fl.onTable, Fl.clear] := by\n decide\n\n-- Les deux transitions calculees : l'egalite des images\n#eval toyStep pickup [Fl.onTable]\n#eval toyStep pickup [Fl.onTable, Fl.clear]\n"}
Raw output {"messages": [{"severity": "info", "pos": {"line": 34, "column": 0}, "endPos": {"line": 34, "column": 5}, "data": "[Fl.held]"}, {"severity": "info", "pos": {"line": 35, "column": 0}, "endPos": {"line": 35, "column": 5}, "data": "[Fl.held]"}], "env": 0} 
-- Et au niveau d'un plan : pickup puis une pose (putdown, symetrique)
def putdown : ToyAction Fl where
  pre := [Fl.held]
  add := [Fl.onTable, Fl.clear]
  del := [Fl.held]

example : toyRun [pickup, putdown] [Fl.onTable]
        ⊆ toyRun [pickup, putdown] [Fl.onTable, Fl.clear] := by
  decide

-- Le plan complet depuis chaque depart : l'inclusion est une egalite ici
#eval toyRun [pickup, putdown] [Fl.onTable]
#eval toyRun [pickup, putdown] [Fl.onTable, Fl.clear]

-- Et au niveau d'un plan : pickup puis une pose (putdown, symetrique)
def putdown : ToyAction Fl where
  pre := [Fl.held]
  add := [Fl.onTable, Fl.clear]
  del := [Fl.held]
example : toyRun [pickup, putdown] [Fl.onTable]
        ⊆ toyRun [pickup, putdown] [Fl.onTable, Fl.clear] := by
  decide
-- Le plan complet depuis chaque depart : l'inclusion est une egalite ici
 [Fl.onTable, Fl.clear]
 [Fl.onTable, Fl.clear]
--% env 1
Raw input {"cmd": "-- Et au niveau d'un plan : pickup puis une pose (putdown, symetrique)\ndef putdown : ToyAction Fl where\n pre := [Fl.held]\n add := [Fl.onTable, Fl.clear]\n del := [Fl.held]\n\nexample : toyRun [pickup, putdown] [Fl.onTable]\n \u2286 toyRun [pickup, putdown] [Fl.onTable, Fl.clear] := by\n decide\n\n-- Le plan complet depuis chaque depart : l'inclusion est une egalite ici\n#eval toyRun [pickup, putdown] [Fl.onTable]\n#eval toyRun [pickup, putdown] [Fl.onTable, Fl.clear]\n", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 5}, "data": "[Fl.onTable, Fl.clear]"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 5}, "data": "[Fl.onTable, Fl.clear]"}], "env": 1}

Lecture : monotonie en l’état ≠ croissance le long du plan

Les deux example ... := by decide ci-dessus sont prouvés par évaluation : Lean calcule les listes concrètes et vérifie l’inclusion. Sur l’instance : toyStep pickup [Fl.onTable] = [Fl.held] et toyStep pickup [Fl.onTable, Fl.clear] = [Fl.held] — l’inclusion tient (ici même l’égalité).

La nuance à retenir : step_mono compare deux départs différents pour la même action ; il ne dit PAS que l’état croît d’un pas au suivant. Le réel peut rétrécir (pickup détruit onTable et clear) : toyRun [pickup, putdown] [Fl.onTable, Fl.clear] repasse par un état à un seul fluent ([Fl.held]). Seule la relaxation garantit la croissance le long du plan (stepR_mono composé) — et c’est précisément cette croissance qui rend le calcul du plan relaxé polynomial (atteignabilité croissante → point fixe) et fonde l’admissibilité \(h^+ \le h^*\) de la section suivante.

5. Théorème phare : l’admissibilité de la relaxation (\(h^+ \\le h^*\))

Le module Planning/Admissibility.lean prouve le résultat central : si un plan réel π atteint le but g depuis s, alors le plan relaxé π atteint aussi g — en une transitivité run ⊆ runR puis goalSatisfied préserve l’inclusion.

  • relaxed_plan_admissible : reaches π s g → reachesR π s g (toute atteignabilité réelle est relaxée ⟹ \(h^+ \\le h^*\)).
  • relaxed_plan_witness : variante existentielle (le plan relaxé est un témoin d’atteignabilité).
#check PlanningLean.relaxed_plan_admissible
#check PlanningLean.relaxed_plan_witness
PlanningLean.relaxed_plan_admissible {F : Type} [DecidableEq F] (π : List (PlanningLean.Action F)) (s g : State F)
  (h : reaches π s g) : reachesR π s g
PlanningLean.relaxed_plan_witness {F : Type} [DecidableEq F] (π : List (PlanningLean.Action F)) (s g : State F)
  (h : reaches π s g) : reachesR π s g

Lecture : \(h^+ \\le h^*\), en une transitivité

Théorème Conclusion
relaxed_plan_admissible reaches π s g → reachesR π s g (h⁺ ≤ h*)
relaxed_plan_witness variante existentielle (témoin relaxé)

La relaxation ne surestime jamais le coût réel : tout plan réalisable en réalité l’est aussi en relaxation, donc l’heuristique \(h^+\) (coût relaxé) minore \(h^*\) (coût réel).

6. La chaîne causale complète

Les modules composent une chaîne unique, du modèle STRIPS à l’admissibilité :

  1. Strips — State/Action, transitions step/stepR, step ⊆ stepR.
  2. Relaxation — run/runR sur le plan, runR_mono, run ⊆ runR (induction).
  3. Admissibility — reaches → reachesR (transitivité) ⟹ \(h^+ \\le h^*\).

7. Exercices

Exercice 1 — Transitions réelle/relaxée sur un mini-STRIPS (Python)

Ancrez l’intuition : un domaine à 2 actions (load, unload) et observez que la transition relaxée est toujours un sur-ensemble de la transition réelle.

# action = (pre, add, del)
load = (pre={'at-truck'}, add={'loaded'}, del=set())
unload = (pre={'loaded'}, add={'delivered'}, del={'loaded'})
def step(action, state):
    # TODO etudiant : transition reelle (s \ del) ∪ add
    return None  # TODO
def stepR(action, state):
    # TODO etudiant : transition relaxee s ∪ add
    return None  # TODO

Exercice 2 — Monotonie de la transition relaxée

Prouvez en Lean que stepR est monotone : s ⊆ s' → stepR a s ⊆ stepR a s'. (C’est un cas particulier de stepR_mono sur une seule action.)

-- TODO etudiant : formaliser la monotonie de stepR
-- theorem stepR_mono_single (a : Action F) {s s' : State F} (h : s ⊆ s') :
--     stepR a s ⊆ stepR a s' := by sorry

Exercice 3 — La relaxation peut être strictement moins chère

Construisez un exemple où la relaxation permet un plan « impossible » en réalité (les deletions bloquent). Montrez que reachesR est vrai mais reaches faux : la relaxation est strictement plus optimiste (\(h^+ < h^*\)), sans jamais dépasser \(h^*\).

# TODO etudiant : domaine ou un plan relaxe atteint le but mais pas le plan reel
# (ex: action avec deletion qui bloque la re-application necessaire)

Conclusion

Ce companion natif exhibe la preuve formelle sans sorry de l’admissibilité de la relaxation (\(h^+ \\le h^*\)) 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.

Le résultat phare relaxed_plan_admissible formalise la propriété qui rend les heuristiques relaxées (h-add, h-max, h-FF) admissibles — un pilier de la planification classique moderne.

Jalon ouvert : la consistance de la relaxation (existence d’un plan relaxé) et la complexité algorithmique ne sont pas formalisées dans le lake ; la lib reste sorry-free.

Retour au sommet