The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Salut salut,

Le 5 mars 2013 21:18, rooster <tidus_franck AT hotmail.com> a écrit :

La raison me semble être que "Equality Scheme" ne peut pas marcher dans le cas
général pour les types inductifs dépendants.
Cependant, dans le cas particulier du type Vector, cette fonction doit
clairement pouvoir être générée automatiquement.

Exactement. Le fait que ce ne soit pas faisable dans le cas général des types dépendants complique beaucoup les choses.
L'algo essaie n'a pas été écrit pour "essayer voir si c'est possible et échouer sinon" dans ce cas là, désolé. Le principal problème
avec les types dépendants vient des indices. Tu veux une égalité qui ait la signature
Vector n A -> Vector n A -> bool ou Vector m A -> Vector n A -> bool ?

Coq ne peut pas deviner quelle instanciation d'indice tu veux, donc on peut difficilement faire mieux de manière complètement automatique.
 

Mes questions sont donc :

1) Existe t'il un moyen de forcer la définition automatique d'une égalité
décidable t_eq (ou Vector_eq) de type Vector -> Vector -> bool, ainsi que les
preuves de corrections et de décidabilité qui vont bien ?

2) Si ce n'est pas le cas, d'accord, je peux le faire à la main pour Vector.
Mais quand bien même je définie "Vector_eq" à la main, Coq n'est pas capable
de me générer automatiquement l'égalité décidable pour mon type A, comme
c'était le cas avec des listes.
Y a t'il un nommage particulier à respecter ?

Pas de solution pour aider Coq à générer les égalités et les lemmes qui vont bien (toute idée/ aide est la bienvenue, vu que
je ne développe plus du tout dans Coq, ça risque de ne pas de bouger avant un moment). Par contre, à défaut d'automatiser la chose
tu peux t'inspirer de l'algo et prouver les lemmes de correction à coup de grosses tactiques violentes (de mémoire c'est grosso modo
induction; destruct; eauto en un peu plus intelligent pour appliquer l'hypothèse d'induction aux bons endroits).

Par contre tu n'échapperas pas à l'écriture de la fonction d'égalité (qui n'est pas trop compliqué dans le cas des Vector, mais qui peut
devenir verbeuse si tu as plus de constructeurs).

Désolé de ne pas pouvoir faire plus dans l'immédiat, mais n'hésite pas à me demander des précisions si je n'ai pas été clair.

++
V.

Je recherche la solution la plus simple et la plus directe pour mon but
initial : avoir le plus aisément possible l'égalité décidable sur mon type
inductif A, en définissant le moins de chose possible à la main, vu que mon
but est de voir jusqu'au Scheme peut aller à l'heure actuelle.

Merci par avance pour vos conseils.