The Coq mailing list

["rooster" <tidus_franck AT hotmail.com>]

Bonsoir,

J'essaye un peu avec la génération automatique d'égalités décidables.
Je commence donc mon fichier par :
Set Equality Scheme.

Je vais utiliser des vecteurs de la bibliothèque, que je renomme pour plus de
clarté:
Definition Vector := t.

Je définis le type inductif suivant :

Inductive A :=
    | C1 : A
    | C2 : A -> A -> A
    | C3 n : Vector A n -> A -> LType.

Je voudrais éviter de définir moi meme l'égalité décidable (A->A->bool), et
bénéficier du support de "Scheme".

Si j'utilise "list" à la place de vecteur, cela marche.
LType is defined
Warning: Ignoring recursive call
LType_rect is defined
LType_ind is defined
LType_rec is defined
LType_beq is defined (OK !)

L'avertissement "Ignoring recursive call" me semble être très craintif pour
rien cette fois ci : quand je regarde le code de A_beq, il me semble être
parfait : récursif pour le constructeur C2, ainsi que récursif pour C3 ET il
appelle l'égalité décidable sur les liste, en lui passant A_beq elle même
comme égalité sur les éléments.
Ça me semble être exactement ce que je veux.

Malheureusement, cela marche, car le principe list_beq existe si je définis
moi meme le type List en haut de mon fichier (après le "Set Equality Scheme"
tout de même).
Si j'utilise les listes prédéfinies, list_beq n'existe pas, mais dans le code
de A_beq généré automatiquement, il y a un appel à internal_list_beq qui est
j'imagine la même chose mais juste "locale" à la fonction A_beq.

Dans tous les cas, ce n'est pas le cas pour Vector : t_beq n'existe pas si je
définis moi même le type inductif (et dépendant) Vector et le système n'est
pas capable de générer un internal_t_beq si j'utilise les vecteurs prédéfinis
(nommés "t").

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.

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 ?


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.