Bonjour à tous, j'espère que vous allez bien. Voici des nouvelles de la formalisation en Coq. Après avoir écrit les définitions la semaine dernière, cette semaine j'ai attaqué l'écriture de preuves, en commençant avec les trois points du lemme 3.9 du document tt/asynch/source.pdf. Une fois le yoyo entre les définitions et les preuves terminé, j'ai prouvé 3.9 b) et le sens -> de la double implication de 3.9 c). Une bonne partie de la preuve pour 3.9 a) est écrite mais je bute sur le dernier cas, celui où (p | q) converges à s en faisant acvn-mu et p fait aussi une transition mu. J'y verrai sûrement plus clair demain avec un peu plus de recul. Pour le point 3.9 c) je pense qu'il y a un problème dans le sens <- avec la convergence de p. Je rédigerai un contre-exemple au propre demain dans la journée et essaierai de prouver le lemme avec un fix. Je vous remercie et vous souhaite une bonne soirée, Paul Laforgue --------------------------------------------------------------- Pour rappel ce dev se retrouve ici : .... Semaine dernière: première version des définitions Depuis ce lundi: début de preuve, le lemme 3.9, qui est une conjonction de trois éléments voir p.XX du YY.pdf ci-joint: - 3.9 a) preuve par induction sur s - si s = [] ok - si s = a :: s' alors par preuve par induction sur (p | q) converge avec (a : s') (voir definition X.Y) - si (p | q) converge avec (a : s') parce que (p | q) fini mais (p | q) ne fait pas a, alors ok (règle acvn-not) - si (p | q) converge avec (a : s') parce que (p | q) fini, (p | q) fait a, mais p ne fait pas a alors ok (règle acvn-not aussi) - si (p | q) converge avec (a : s') parce que (p | q) fini, (p | q) fait a, et p fait a alors bloqué - 3.9 b) fait - 3.9 c) est une double implication - -> ok Aujourd'hui - <- possible contre exemple + idée de fix - si (p | q) converge avec (a : s') parce que (p | q) fini mais (p | q) ne fait pas a, alors ok (règle acvn-not) - si (p | q) converge avec (a : s') parce que (p | q) fini, (p | q) fait a, mais p ne fait pas a alors ok (règle acvn-not aussi) - si (p | q) converge avec (a : s') parce que (p | q) fini, (p | q) fait a, et p fait a alors bloqué plutôt dans un style plus concis: - Les 2 premiers cas sont faits (règle acvn-not aussi) - Bloqué: - si (p | q) converge avec (a : s') parce que (p | q) fini, (p | q) fait a, et p fait, en particulier, il faudrait avoir "soit p fait a soit q fait a" (en cours) ----------------------------------------- Lemme 3.15 où il reste R: (a) et <-( c), nécessitant la formalisation de la congruence (mettre ref dans le papier) et de ses propriétés (lister les propriétés plus réf dans papier). Pour cela, j'étudie la formalisation en Coq HO-pi (Alan Schmitt & co.), voir [papier](https://hal.inria.fr/hal-02536463v2/file/jar.pdf) + [implementation Coq](https://passivation.inria.fr/hopi/nameless/html/Struct_congr.html#struct_congr). Short version CPP https://hal.inria.fr/hal-01614987v3/document Cela me pousse à reformuler notre définition dans une style plus adapté à la preuve. (reformuler) 1. congruence ACCS dans style HO-pi + propriétés 2. Voir si R passe Cependant, entre temps, Gio a changé qqs définitions, en particulier le lemme 3.15 devenu lemme 2.16 avec disparition de 3.15 a. Il reste le point 2.16(b) partie <- (anciennement 3.15 ( c) partie <-). Check si 3.16 est devenu 2.17 + corollary 2.3.