Expérimentations autour de la variant de X. Leroy (CoqPL 2024) #6
Conversation
…of X. Leroy for CoqPL 2024
+ small correction in lr_rec (a Prop inductive is promotted to Type so needed to specify a bit more)
et dfs_xleroy_std_foldleft.v devient dfs_xleroy.v
presented as a list. Notice the special remark DLW -> JFM
indeed computes the smallest invariant, ie the refl-trans closure, when it terminates. Now remains to show that it terminates *ONLY IF* x is accessible ... not so easy it seems.
|
@moninje J'ai démontré que l'algo de XL calcule effectivement la clôture refl-trans, quand il termine. |
post-condition of foldleft dfs_acc ?
a factor of both dfs_xleroy and dfs_xlroy_nocycle
|
@moninje, sur |
|
Dérivation de dfs_book à partir de dfs_xleroy rectifié (fichier dfs_inloop.v) revue de fond en comble : les algos sont inchangés, mais leur "spec syntaxisue" est revenue à Braga pur, sans tricherie sur les G qui collent désormais aux algos, ce qui permet d'exprimer les équivalences entre algos au niveau des G. Il y a quand même à un endroit délicat, l'aplatissement de la pile en une seule liste, qui passe par la relation inductive iflatten afin de gérer sans douleur les éléments vides. |
|
@DmxLarchey J'ai refait une passe sur le README, où nous avions une discussion en suspension. Je pense avoir répondu à tes questions et j'ai aussi vérifié que l'algo de Xavier se transforme bien en rect term avec une pile appropriée. Il faudrait nettoyer ce README une fois que tu auras lu, si ça te va. |
|
Pas de souci. Je crois avoir compris après N commits que les commentaires markdown, ça doit pas être trop long, faut les couper un peu !!! |
Explications transférées dans le
README.mdlocal de la branche.