Ce billet a été originellement posté en anglais sur mon site personnel.
Je dois le confesser : j’ai un secret. De ceux que l’on cache, de ceux qui couvrent de honte. Dans SpecCert, j’ai triché. En effet, dans les preuves que j’ai publié sur Github, j’utilise à plusieurs reprises des axiomes que rien ne justifie. Voilà, c’est dit.
Après, que les choses soient bien claires entre nous : si j’ai introduit des axiomes dans mes preuves, c’est moins par faignantise que par ignorance. À l’époque, je ne voyais pas comment faire autrement. Depuis, j’ai appris. Je me suis initié aux setoids, aux morphismes et à cette magie noire qu’est la généralisation de la tactique rewrite. Ce savoir nouvellement acquis m’oblige et il me faudra un jour corriger mon infamie1. Mais, en attendant, je me propose de partager avec vous mes découvertes.
Je ne suis pas forcément familier avec les notions mathématiques sous-jacentes aux mécanismes dont je vais vous parler dans ce billet. Mon objectif n’est de toute façon pas d’écrire un cours théorique, mais que cela ne vous empêche pas, si vous décelez une erreur dans ce qui suit, de me la faire remarquer !
-
Les Anglo-saxons ont un mot pour ça : eventually. À mes oreilles, cela sonne bien souvent comme une creuse promesse, du coup il convient parfaitement ici. ↩
- Pourquoi a-t-on besoin d’étendre la tactique de réécriture ?
- Être ou ne pas être égaux, telle est la question.
- Coq et la réécriture de termes équivalents
Pourquoi a-t-on besoin d’étendre la tactique de réécriture ?
La question est légitime. Après tout, vous n’avez peut-être jamais eu à vous confronter à un cas où la tactique rewrite ne fonctionne pas directement. Quand deux valeurs sont égales, on peut remplacer l’une par l’autre dans une expression sans changer son résultat. Point.
Sauf que non. Parfois, ce que Coq comprend lorsque l’on parle d’égalité n’est pas ce que nous pouvons avoir, nous autres mortels perclus de biais et d’heuristiques, avons en tête. C’est assez facile à mettre en évidence avec des valeurs qui ressemblent à ça :
1 2 3 4 | Record Gate := { open: bool ; lock: bool ; lock_is_close: lock = true -> open = false }. |
Une porte peut être ouverte ou fermée, mais aussi verrouillée ou non. Seulement, nous affirmons que la porte ouverte et verrouillée n’existe pas. Ajouter ce type de contrainte est assez facile et se fait en ajoutant une proposition dans la liste des champs du record Gate (ici, lock_is_close). En procédant ainsi, on sait qu’on ne pourra pas rencontrer par la suite une porte g telle que open g = true et lock g = true.
Travailler avec ce genre d’objet est rendu assez simple grâce à la directive Program ; il s’agit d’une fonctionnalité assez récente de Coq, par conséquent elle peut manquer de maturité1. En attendant, elle nous aide quand même beaucoup quand elle fait correctement son travail.
Définir la porte ouverte peut par exemple se faire en ignorant totalement la proposition lock_is_close :
1 2 3 4 5 6 | Require Import Coq.Program.Tactics. Program Definition open_gate := {| open := true ; lock := false |}. |
Il est intéressant dans ce cas de regarder la sortie de notre assistant de preuves préféré :
1 2 3 4 5 | open_gate has type-checked, generating 1 obligation(s) Solving obligations automatically... open_gate_obligation_1 is defined No more obligations remaining open_gate is defined |
Globalement, ce que Program nous dit est qu’il a trouvé une obligation de preuve à résoudre (lock_is_close en l’occurrence)… et qu’il s’en dépatouille tout seul comme un grand ! Pour des propositions moins triviales, il faudra néanmoins mettre la main à la pâte, mais ce n’est pas le sujet de cet article.
D’aucuns pourraient arguer avec raison qu’utiliser Program pour quelque chose d’aussi simple est un peu exagéré. C’est vrai : on peut très bien définir notre porte ouverte sans, grâce à la tactique refine :
1 2 3 4 5 6 7 | Definition open_gate': Gate. refine ({| open := true ; lock := false |}). intro Hfalse. discriminate Hfalse. Defined. |
-
Votre serviteur a déjà pu mettre en évidence une erreur dans son implémentation quand il jouait avec les types dépendants. Mais ça, c’est une autre histoire. ↩
Être ou ne pas être égaux, telle est la question.
Lorsque nous écrivons a = b dans Coq, cela a une signification bien particulière qui ne vient pas forcément à l’esprit de celui qui utilise le logiciel… tout de moins, pas tant qu’il se confronte à ses limitations.
L’égalité de Leibniz est trop forte
Note objet Gate est relativement simple et l’ensemble de ses valeurs n’est pas très important, notamment grâce à la proposition lock_is_close. Notamment, si deux portes sont ouvertes, alors elles ont forcément le même état, parce qu’elles ne peuvent par définition pas être verrouillées.
Essayons de prouver ce lemme.
1 2 3 4 5 | Lemma open_gates_are_equal: forall (g g': Gate), open g = true -> open g' = true -> g = g'. |
Voici une tentative de résoudre cette preuve :
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 | Proof. induction g; induction g'. cbn. intros H0 H2. assert (lock0 = false). + case_eq lock0; [ intro H; apply lock_is_close0 in H; rewrite H0 in H; discriminate H | reflexivity ]. + assert (lock1 = false). * case_eq lock1; [ intro H'; apply lock_is_close1 in H'; rewrite H2 in H'; discriminate H' | reflexivity ]. * subst. |
Dans un premier temps, nous prouvons qu’effectivement, les deux portes ne sont pas verrouillées. La tentation ensuite est d’utiliser la tactique reflexivity, qui dit globalement à Coq « rappelle-toi, l’égalité est reflexive et j’ai bien deux fois la même chose à droite et à gauche de =, donc fais ta magie. »
Sauf que…
1 2 3 4 | Error: In environment
lock_is_close0, lock_is_close1 : false = true -> true = false
Unable to unify "{| open := true; lock := false; lock_is_close := lock_is_close1 |}" with
"{| open := true; lock := false; lock_is_close := lock_is_close0 |}".
|
Sauf que Coq refuse d’unifier lock_is_close0 et lock_is_close1.
La tentation qui a été longtemps la mienne et qui peut-être a aussi été la vôtre ici a été d’oublier lock_is_close. Sauf que ça ne marche pas comme ça. Même si cette proposition est effacée lors de l’extraction, elle n’en existe pas moins dans le monde de Coq et nous devons la prendre en compte. Quand nous demandons à Coq de vérifier qu’effectivement, lock_is_close0 est bien la même chose que lock_is_close1, il ne peut pas le faire. Ce n’est pas parce que deux preuves ont le même type (le même énoncé) qu’elles sont égales !
En d’autres termes, l’égalité de Coq (le symbole =) implémente une certaine définition de l’égalité, dite de Leibniz (nous y reviendrons) qui est beaucoup plus restrictive que ce dont nous avons besoin.
Définir sa propre relation d’équivalence
Ceux qui ont un peu l’habitude de Coq le savent bien : utiliser l’assistant de preuve, c’est passer son temps à lui expliquer des évidences.
Fort heureusement, notre définition de « l’égalité » entre deux portes est très simple à exprimer :
1 2 3 4 | Definition gate_eq (g g': Gate) : Prop := open g = open g' /\ lock g = lock g'. |
Sauf que, on l’a vu, le terme « égalité » a un sens bien précis en Coq. Aussi, à partir de maintenant, nous allons préférer l’adjectif « équivalent » à « égal ». Car, de fait, gate_eq est une relation d’équivalence. Mais l’est-elle réellement ? Pour nous en assurer, il convient de montrer qu’elle est :
- Reflexive :
gate_eq g g - Symmetrique :
gate_eq g g' -> gate_eq g' g - Transitive :
gate_eq g g' -> gate_eq g' g'' -> gate_eq g g''
La construction de notre relation d’équivalence fait qu’il est très facile de prouver ces bonnes propriétés.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 | Lemma gate_eq_refl : forall (g: Gate), gate_eq g g. Proof. split; reflexivity. Qed. Lemma gate_eq_sym : forall (g g': Gate), gate_eq g g' -> gate_eq g' g. Proof. intros g g' [Hop Hlo]. symmetry in Hop; symmetry in Hlo. split; assumption. Qed. Lemma gate_eq_trans : forall (g g' g'': Gate), gate_eq g g' -> gate_eq g' g'' -> gate_eq g g''. Proof. intros g g' g'' [Hop Hlo] [Hop' Hlo']. split. + transitivity (open g'); [exact Hop|exact Hop']. + transitivity (lock g'); [exact Hlo|exact Hlo']. Qed. |
Le module Coq.Setoids.Setoid fournit une syntaxe particulière qui permet de déclarer une nouvelle relation d’équivalence à Coq, pour que ce dernier sache qu’il peut l’utiliser lorsque vous utilisez les tactiques symmetry, reflexivity et transitivity.
1 2 3 4 5 6 7 | Require Import Coq.Setoids.Setoid. Add Parametric Relation: (Gate) (gate_eq) reflexivity proved by (gate_eq_refl) symmetry proved by (gate_eq_sym) transitivity proved by (gate_eq_trans) as gate_eq_rel. |
Voilà, nous avons défini une relation d’équivalence ad hoc pour nos Gates. Maintenant, utilisons-la pour formuler le lemme qui nous intéressait :
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 | Lemma open_gates_are_the_same: forall (g g': Gate), open g = true -> open g' = true -> gate_eq g g'. Proof. induction g; induction g'. cbn. intros H0 H2. assert (lock0 = false). + case_eq lock0; [ intro H; apply lock_is_close0 in H; rewrite H0 in H; discriminate H | reflexivity ]. + assert (lock1 = false). * case_eq lock1; [ intro H'; apply lock_is_close1 in H'; rewrite H2 in H'; discriminate H' | reflexivity ]. * subst. split; reflexivity. Qed. |
Coq et la réécriture de termes équivalents
Les propriétés des relations d’équivalence sont très pratiques et on s’en sert plus souvent qu’on le croit. Néanmoins, il y a quelque chose qui va très rapidement vous manquer si vous vous arrêtez là : la possibilité de réécrire un terme par un autre, s’ils sont égaux. Ou, dans notre cas, équivalents ! Car, comme nous allons le voir, il est possible d’étendre la tactique rewrite pour, sous certaines conditions, pouvoir se baser sur une preuve que deux termes sont équivalents pour remplacer l’un par l’autre.
Ouvrons nos portes
Pour l’illustrer, considérons la fonction suivante :
1 2 3 4 5 6 7 8 9 10 | Require Import Coq.Bool.Bool. Program Definition try_open (g: Gate) : Gate := if eqb (lock g) false then {| lock := false ; open := true |} else g. |
Si la porte passée en argument n’est pas verrouillée, alors la fonction retourne la porte ouverte. Sinon, la fonction retourne la porte passée en argument telle quelle. Intuitivement,
1 2 3 4 5 6 | Lemma gate_eq_try_open_eq : forall (g g': Gate), gate_eq g g' -> gate_eq (try_open g) (try_open g'). Proof. intros g g' Heq. |
Ce que l’on aimerait faire à cet instant précis, c’est écrire rewrite Heq. Après tout, les deux portes sont équivalentes, donc le résultat de try_open a toutes les chances de retourner la même chose qu’on lui passe g ou g'. Sauf que…
1 2 3 4 5 6 7 8 9 10 11 | Error: Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X49==[g g' Heq |- relation Gate] (internal placeholder) {?r}
?X50==[g g' Heq (do_subrelation:=Morphisms.do_subrelation)
|- Morphisms.Proper (gate_eq ==> ?X49@{__:=g; __:=g'; __:=Heq}) try_open] (internal placeholder) {?p}
?X52==[g g' Heq |- relation Gate] (internal placeholder) {?r0}
?X53==[g g' Heq (do_subrelation:=Morphisms.do_subrelation)
|- Morphisms.Proper (?X49@{__:=g; __:=g'; __:=Heq} ==> ?X52@{__:=g; __:=g'; __:=Heq} ==> Basics.flip Basics.impl) eq]
(internal placeholder) {?p0}
?X54==[g g' Heq |- Morphisms.ProperProxy ?X52@{__:=g; __:=g'; __:=Heq} (try_open g')] (internal placeholder) {?p1}
.
|
Il ne s’agit pas là du message d’erreur le plus compréhensible que j’ai eu l’occasion de lire, je dois l’avouer. Pourtant, ce que Coq essaie de nous dire est finalement assez simple. Il se plaint qu’il ne peut pas faire de réécriture parce qu’il lui manque la preuve que deux portes équivalentes rendent bien le même résultat une fois passée à try_open. Dit autrement : pour pouvoir utiliser rewrite Heq dans ces conditions, il faut d’abord… prouver le lemme que nous cherchons justement à résoudre !
La raison est en fait assez simple : nos deux portes ne sont pas égales, elles sont équivalentes, selon une certaine notion de l’équivalence. Nous savons intuitivement que cette relation est assez « forte », en ce sens que deux portes équivalentes sont effectivement les mêmes. Sauf que ! C’est loin d’être le cas pour toute les relations d’équivalence envisageables. J’en veux pour preuve la relation R telle que pour toutes portes g et g', R g g' est vérifiée. Une telle relation est réflexive, symétrique et transitive, mais il est assez évident que try_open g et try_open g' ne seront pas égaux.
Si Coq permet de réécrire un terme g par un terme g' dans une expression à la condition que g = g' sans plus se poser de question, c’est parce que la définition sous-jacente de son égalité le permet. Cette dernière est équivalente à l’égalité de Leibniz. Le manuel de Coq déclare ainsi :
$x$ and $y$ are equal iff every property on $A$ which is true of $x$ is also true of $y$
Cette propriété est assez forte pour que, peu importe la fonction considérée, deux arguments égaux donnent deux résultats égaux. Dans notre cas, nous n’utilisons plus l’égalité, mais notre équivalence… donc il faut commencer par démontrer que try_open, considérant deux portes équivalentes, retourne deux portes équivalentes ; une fois cette « formalité » évacuée, nous pourrons effectivement utiliser rewrite.
Déclarer un nouveau morphisme
Considérons deux ensembles, $A$ l’ensemble de départ et $B$ l’ensemble d’arrivée. Considérons $R_A$ une relation d’équivalence sur $A$ et $R_B$ une relation d’équivalence sur $B$. Enfin, considérons $f : A \rightarrow B$ une fonction.
On dira que $f$ est un morphisme si, $\forall (a, a') \in (A \times A)$, $R(a, a') \Rightarrow R'(f(a), f(a'))$. En déclarant $f$ comme un morphisme à Coq, l’assistant de preuve acceptera de transformer $R'(x, g)$ en $R'(x, g')$ si $R'(g, g')$, justement parce que $R'$ est une relation d’équivalence par définition réflexive.
Coq possède une syntaxe pour déclarer un morphisme ; elle est assez déroutante au premier abord, parce qu’éloignée de ce que l’on peut lire d’ordinaire, mais finalement assez simple à comprendre :
1 2 3 | Add Parametric Morphism: (f) with signature (R) ==> (R') as <name>. |
Cette notation est assez générique : f peut prendre plus d’un argument, il faudra simplement ajouter les bonnes relations d’équivalence pour les arguments supplémentaires avant le ==> (R').
Pour le cas qui nous intéresse, à savoir try_open : $A$ et $B$ sont tous deux Gate, si bien que $R$ et $R'$ sont gate_eq.
1 2 3 | Add Parametric Morphism: (try_open) with signature (gate_eq) ==> (gate_eq) as open_morphism. |
Cela nous donne le but suivi à démontrer :
1 2 3 4 | 1 subgoal, subgoal 1 (ID 50) ============================ forall x y : Gate, gate_eq x y -> gate_eq (try_open x) (try_open y) |
But que l’on peut prouver comme suit :
1 2 3 4 5 6 7 8 9 10 11 12 13 | Proof. intros g g' Heq. assert (gate_eq g g') as [Hop Hlo] by (exact Heq). unfold try_open. rewrite <- Hlo. destruct (bool_dec (lock g) false) as [Hlock|Hnlock]; subst. + rewrite Hlock. split; cbn; reflexivity. + apply not_false_is_true in Hnlock. rewrite Hnlock. cbn. exact Heq. Qed. |
Maintenant, nous allons reprendre le lemme que nous voulions prouver initialement ; c’est exactement le même but que le précédent, mais nous allons le prouver beaucoup plus rapidement grâce à rewrite et `reflexivity :
1 2 3 4 5 6 7 8 9 | Lemma gate_eq_try_open_eq : forall (g g': Gate), gate_eq g g' -> gate_eq (try_open g) (try_open g'). Proof. intros g g' Heq. rewrite Heq. reflexivity. Qed. |
Cela conclut notre tour d’horizon de ce monde obscur, mais néanmoins merveilleux, de la réécriture en Coq. J’espère que vous aurez pu mieux saisir ce qui se cache exactement derrière rewrite, qui est sans doute une des tactiques les plus utiles. Même si vous n’utilisez pas ce que vous venez d’apprendre, je me suis rendu compte en écrivant cet article que ces explications permettaient de mieux comprendre comment la réécriture fonctionne « sous le capot », ce qui n’est jamais un mal quand on s’intéresse aux méthodes formelles et à des outils complexes comme peut l’être Coq.
