Affirmation et certificat

Une affirmation

Une affirmation de conservation dit : « telle quantité ne change jamais ». La quantité est une densité. On lit chaque case, ou chaque fenêtre de quelques cases, on lui donne un poids, et on fait la somme sur tout l’anneau. Pour le trafic, le poids d’une case est 1 s’il y a une voiture, 0 sinon, et le total est le nombre de voitures.

Le problème : « ne change jamais » doit valoir pour des anneaux de 3 cases, de 1 000 cases, de toutes les tailles. On ne peut pas tous les simuler.

L’idée du certificat

Pensez à des pièces reliées par des portes. Si le nombre de personnes dans chaque pièce ne change que parce que des gens passent les portes, alors le nombre total de personnes ne change pas : chaque personne qui sort d’une pièce entre dans la voisine. Sur un anneau, il n’y a pas de bord par où quelqu’un pourrait partir.

Le certificat dit exactement cela pour une densité. Il donne un courant, un nombre sur chaque frontière entre deux cases, tel que la variation de chaque case égale ce qui entre moins ce qui sort.

Sur la figure, une voiture qui avance franchit une frontière. La case qu’elle quitte perd 1, la case où elle arrive gagne 1, et le courant compte 1 sur cette frontière. Chaque variation est expliquée par ce qui traverse les frontières, donc le total reste le même.

Pourquoi une vérification finie suffit

L’équation « variation de la case = ce qui entre − ce qui sort » ne dépend que de quelques cases voisines. Pour le trafic, il suffit de regarder des motifs de 4 cases, soit 16 motifs. Le noyau de Lean les vérifie tous, un par un.

Ensuite, un théorème démontré une fois pour toutes fait le passage du local au global. Il s’appelle conserved_of_fluxCheck et dit : si la densité et le courant vérifient l’équation sur chaque motif local, alors le total de la densité est conservé sur des anneaux de toutes les tailles, pour toutes les configurations. La preuve additionne les équations de toutes les cases : les courants se compensent deux à deux autour de l’anneau.

À quoi cela ressemble

theorem traffic :
    Conserved (eca 184) (tableFn 2 [0, 1]) 1 :=
  conserved_of_fluxCheck _ _
    (tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1
    (by decide +kernel)

• Conserved (eca 184) (tableFn 2 [0, 1]) 1 : dans la règle 184, la densité de largeur 1 qui vaut 0 pour une case vide et 1 pour une voiture est conservée.
• tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0] : le courant, une valeur pour chacun des 8 motifs de 3 cases.
• by decide +kernel : le noyau vérifie l’équation sur tous les motifs.

Le monde Lean lit la règle avec un décalage d’une case (voir Monde), donc sa table de courant ne ressemble pas mot pour mot aux flèches de la figure. Elle joue le même rôle. Un courant n’est défini qu’à une constante près : ajouter la même valeur partout ne change aucune différence. Le moteur peut donc imprimer une autre table, tout aussi valable.