Licence CC BY

Equivalence, morphisme et réécriture en Coq

Où l’on apprend comment étendre le fonctionnement de la tactique `rewrite`

Publié :
Auteur :
Catégories :
Temps de lecture estimé : 11 minutes

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 !


  1. 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 ?

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.

  1. 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 :

  1. Reflexive : gate_eq g g
  2. Symmetrique : gate_eq g g' -> gate_eq g' g
  3. 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.

10 commentaires

Staff

Intéressant comme billet, dommage que le site ne contient pas de billet introductif aux assistants de preuves et en l’occurence Coq.

Seulement, au début tu parles de prouver des théorèmes en rajoutant des axiomes, mais tu n’en reparles pas ensuite, du coup je n’ai pas trop compris.

+0 -0

Les axiomes étaient ma manière « sale » de contourner les « limitations de rewrite » ; depuis, j’ai découvert que la bonne solution n’est pas de contourner, mais d’étendre rewrite comme je le montre dans ce billet.Je vais essayer de modifier un peu l’intro pour rendre tout ça plus clair.


En attendant, petite découverte personnelle du matin : comment transformer R g en R g' quand gate_eq g g'. Le billet ne le couvre pas car il n’est fait mention que de réécriture dans des relations binaires, mais ça marche aussi avec des relations unaires !

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
Parameter (R: Gate -> Prop).

Add Parametric Morphism: (R)
    with signature (gate_eq) ==> (Basics.impl)
      as r_morphism.
Admitted.

Lemma r_gate
  : forall (g g': Gate),
    gate_eq g g' -> R g -> R g'.
Proof.
  intros g g' Heq Hr.
  rewrite <- Heq.
  exact Hr.
Qed.

I am not a Unicorn · Blog · Image originale par Gallifreya · @lthms

+0 -0

Désolé, je réécris mon message et j’ajoute quelques trucs. Merci pour ton billet.

Je demandais premièrement si on ne pouvait pas utiliser la « proof irrelevance ». Est-ce que ce sont les axiomes que tu avais ajoutés ?

Ensuite, je demandais si on ne pouvait pas coder quelque chose de plus général : construire un setoïd à partir d’une fonction $f : A \to B$, avec comme ensemble sous-jacent $A$ et comme relation d’équivalence $x \equiv y \iff f(x) = f(y)$. Quand on quotiente $A$ par cette relation d’équivalence, on trouve l’image de $f$.
Ici, on est dans le cas où on a un ensemble $A$ et une propriété $P : A \to \mathrm{Prop}$, et on veut le sous-ensemble $\{x \in A\,|\,P(x)\}$. Le setoïd se construit en prenant la projection de la somme dépendante $\sum_{x \in A} P(x)$ sur $A$.
Je trouve sur internet plusieurs choses concernant les subset mais apparemment la notation {x:A | P(x)} est utilisée pour dénoter la somme paire dépendante $\sum_{x \in A} P(x)$ et pas le sous-ensemble image… Je ne connais pas coq, il n’y a pas de mécanisme pour parler de l’image d’une fonction et de sous-ensembles ?

(On peut aussi formuler ça de manière catégorique (avec des sous-catégories (co)réflexives ici par exemple) mais je crois qu’aucun langage dans le même genre (Epigram, Agda, Idris…) ne fait ça de cette façon.)

Édité par blo yhg

Écoutez les suites de l’OEIS : http://oeis.org/play.html

+0 -0

Je demandais premièrement si on ne pouvait pas utiliser la « proof irrelevance ». Est-ce que ce sont les axiomes que tu avais ajoutés ?

Je ne connaissais pas le principe de proof irrelevance ; mes axiomes, globalement, c’était quelque chose de la forme R x y <-> x = y, pratique pour passer d’une forme à l’autre… #Shame Il va falloir que je regarde, cela dit.

Pour ce qui est de la notation { x | P x }, c’est globalement un raccourci pour construire un terme semblable à ce que j’ai pour Gate.

Je ne suis pas certain de comprendre totalement ce que tu proposes. Est-ce que la relation d’équivalence que tu évoques se construit pour tout $f$ ou seulement une seule fonction donnée ?

Parce que je me vois mal, dans les cas qui m’intéressent, jongler entre plusieurs relations d’équivalence (une par fonction) ; prouver autant de fois que nécessaire que les fonctions manipulées sont bien des morphismes semble plus rapide à envisager.

Edit : okay, donc le proof_irrelevance semble être un axiome défini ici et qui permet, dans le cas d’usage que je présente dans mon billet, d’obtenir un résultat similaire plus rapidement. L’avantage étant que pour le coup, je n’ai plus besoin d’axiomes du tout, c’est important.

Édité par lthms

I am not a Unicorn · Blog · Image originale par Gallifreya · @lthms

+0 -0

Je crois comprendre qu’en fait les quotients et les sous-ensembles sont justement gérés avec des setoids comme tu le fais (rewrite généralisé) et qu’on ne peut pas construire l’ensemble quotient à partir du setoid en coq (rewrite normal). Voir par exemple dans l’introduction de http://www.cs.nott.ac.uk/~pszvc/publications/Setoids_JFP_2003.pdf (Il est dit que les tentatives pour faire ça sont insatisfaisantes, c’est étonnant.)

Ce que je disais, c’est qu’une fonction f : A → B donne la relation d’équivalence R f sur A définie par R f x y = (f x = f y). Si on a un ensemble A et un prédicat P dessus, le setoid-sous-ensemble correspondant se construit en appliquant ça à la projection {y:A & P y} → A qui oublie la preuve qu’on est dans le sous-ensemble. Ici, on souhaite construire un sous-ensemble de Bool × Bool, celui des éléments tels que si le deuxième booléen est vrai, alors le premier est faux. C’est le même setoid que celui de ton article.
Mais je ne trouve rien de standard pour faire ça. Ce sont de petits trucs sûrement faciles à ajouter mais ça me donne l’impression que coq est encore assez incomplet.

edit Pour la proof-irrelevance, voici un lien.

edit Je n’ai pas bien compris ta question « Est-ce que la relation d’équivalence que tu évoques se construit pour tout f ou seulement une seule fonction donnée ? » en fait.

Édité par blo yhg

Écoutez les suites de l’OEIS : http://oeis.org/play.html

+0 -0

L’égalité telle que définie par Coq est assez proche de ce que tu donnes comme définition(R f), à un pour tout près. Globalement, $x = y \triangleq \forall R : \mathcal{A} \rightarrow \text{Prop}, R(x) \rightarrow R(y)$. Mais en fait, je fais fausse piste.

Après réflexion, je crois comprendre ce que tu veux dire par « oublier la preuve », mais il faudrait que je creuse ça à tête reposée, parce que je n’arrive pas à me convaincre que je saisis complètement ce que tu proposes. Il faudra que je reprenne ça à tête reposée pour essayer de construire quelque chose à partir de ce que tu dis.

Édité par lthms

I am not a Unicorn · Blog · Image originale par Gallifreya · @lthms

+0 -0

Ce sont de petits trucs sûrement faciles à ajouter mais ça me donne l’impression que coq est encore assez incomplet.

Non, en fait c’est très difficile à ajouter et ça fait des (dizaines d’) années que la communauté des types dépendants travaille sur ces sujets. La notion d’égalité est nettement plus complexe qu’on ne pourrait le penser.

"Proof irrelevance" est facile à ajouter comme axiome, mais ne résoud pas le problème général du quotient et n’est globalement pas assez fort pour obtenir les égalités que l’on veut – ici en l’occurrence ça suffit pour le type Gate, et ça suffit dans les cas où on a une structure avec des données et des preuves et qu’on veut juste l’égalité sur les données en ignorant les preuves (et que les données sont à un type où l’égalité marche bien, comme les booléens; sur les fonctions il faut rajouter l’axiome d’extentionnalité en plus). Dans le cas général, on sent bien que quotienter sur des relations arbitraires ne peut pas se faire "facilement" parce qu’il faut nécessairement prouver que toute opération définie sur le quotient respecte l’équivalence – donc toute définition va forcément avoir une composante supplémentaire "preuve de fonctionnalité", à moins de construire une bijection entre le quotient et une représentation directe sans équations, ce qui ne peut se faire qu’au cas par cas.

Les grandes familles de solution aujourd’hui c’est l’égalité intentionnelle (comme en Coq), où il faut définir tes relations d’équivalence et prouver que tu les respectes au cas par cas, l’égalité extentionnelle où il y a une notion plus simple de quotient mais où la vérification du typage n’est plus décidable (puisqu’il faut peut-être, pour vérifier une preuve, "deviner" un raisonnement d’égalité en combinant des relations compliquées), et l’approche homotopique, qui prend le contre-pied de la "proof irrelevance" (elle est incompatible avec l’axiome d’irrelevance) et ne simplifie pas les preuves mais donne un système où il est plus facile de construire des égalités entre types (en gros il suffit de montrer une bijection entre les deux types).

Édité par gasche

+1 -0

Merci pour les détails supplémentaires. C’est, je trouve, un sujet vraiment intéressant, même si de fait, ça peut paraître parfois « stratosphérique » pour les personnes qui n’ont jamais utilisé des assistants de preuves ou ne se sont jamais confronté à ces problématiques.

Par curiosité, je peux avoir ton avis sur l’article en tant que tel ? Vois-tu des pistes pour l’améliorer, des erreurs, etc. ? Je n’ai jamais réussi à lire la documentation officielle de Coq sur ce sujet du generalized rewrite, en tout cas en entier. J’aimerai bien me servir de ce texte comme base pour avoir un document plus accessible.

I am not a Unicorn · Blog · Image originale par Gallifreya · @lthms

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte