Question
Je me demande comment implanter la WHNF de `Eq.cast`, j'ai l'impression, intuitivement, qu'il suffit de vérifier que son argument `p` est bel et bien convertible à `Eq.refl` (autrement dit, ce n'est pas simplement une variable/hypothèse), auquel cas, il me paraît correct d'ignorer l'argument `f` et de se réduire à l'argument explicite.
Évidemment, si `p` n'est pas convertible à `Eq.refl`, la réduction doit bloquer.
Est-ce que cette approche peut causer des problèmes au niveau théorique?
Ça ne va pas casser la cohérence de la logique (qui dans notre cas est déjà cassée par le manque de termination-checker, de toute façon), non.
Par contre, ça pose un problème au moins conceptuel et potentiellement pratique dans le sens que ça signifie qu'on ne peut pas faire cette réduction après avoir effacé les argument effaçables.
Si on décide que l'effacement se fait après la vérification de types (et donc que la convertibilité est vérifiée sur des termes avant-effacement), alors cette règle ne pose aucun problème. Si par contre on aimerait faire l'effacement avant la vérification (ce qui donne une notion de convertibilité un peu plus forte vu qu'elle va permet de convertir des termes qui ont des parties effaçable non-convertibles), ça pourrait poser problème.
Ceci dit, peut-être qu'on peut avoir le beurre et l'argent du beurre: en fait, actuellement la notion de convertibilité "forte" (contrôlée par la variable `conv_erase`) est utilisée sans effectuer l'effacement en tant que tel, donc on peut utiliser la règle que tu suggères tout en fermant les yeux sur les arguments effaçables lorsqu'on teste la convertibilité de 2 termes.
La méta-théorie d'un tel système n'est probablement pas très jolie par contre: `conv_erase` nous dirait normalement qqch comme
e₁ ≃ e₂ ------------------------------------------- Eq.cast _ _ _ _ _ e₁ ≃ Eq.cast _ _ _ _ _ e₂
quelque soient les arguments `_`, donc ça nous dit aussi que
Eq.cast _ _ _ _ _ e₁ ≃ Eq.cast _ _ _ _ (Eq.refl _) e₁
et donc qu'on peut *toujours* réduire `Eq.cast` sans même regarder si la preuve est `Eq.refl`, et ça on sait que c'est pas sound :-(
Donc en théorie `conv_erase` est incompatible avec la règle que tu proposes, est-ce que ça s'applique aussi à notre implantation de `conv_p`, je ne sais pas.
Mais, je ne vois pas de bonne alternative, alors: ¡Go for it!
- Exemple
Merci pour l'exemple détaillé. Je ne vois pas de manière satisfaisante de résoudre ce problème autre que de faire la réduction que tu suggères.
Stefan