CRGTCoq20110706

Présentation de Pierre Courtieu

But: utiliser les accolades pour décrire la structure des scripts. Ceci remplace "Begin subproof." et "End subproof."

Sous Emacs, cela donne la navigation de parenthèse à parenthèse. Les accolades doivent être fermées, c'est forcé par la vérification. Emacs fournit aussi l'indentation automatique.

Au niveau Coq, cela représente trois lignes de changement. Apparemment ça n'interfère pas avec les puces. Il reste une question sur l'interaction avec les accolades.

Proposition ajouter la possibilité de préfixer une accolade ouvrante avec un numéro pour indiquer que l'on travaillera sur un but. On peut également ajouter un mot-clef abstract. Bruno, pas sûr de comprendre la sémantique de 2,3:{ ...; [tac1 ; tac2] }

Une remarque: ceci permet de mieux envisager l'exécution en parallèle de plusieurs parties du script.

Il peut y avoir un bug entre les accolades et les puces.

L'interface devrait fournir des commandes pour aller rapidement à la résolution d'une sous-preuve.

Revoir les arguments de Georges qui considère que le langage de script devrait rester un langage de script avec peu de structure.

Avis favorable pour l'implémentation.

Hugo: question reliée. On peut avoir un caractère pour indiquer que l'on termine l'utilisation de puces. par exemple [] qui ressemble à une boîte carrée.

Présentation d'Enrico Tassi

But: ajouter du contrôle dans la tactique simpl, et ajouter du contrôle dans la réécriture.

Parfois simpl est trop agressif. Par exemple, si l'on appelle simpl sur (S x - y) ou de façon similaire sur (List.nth (a::tl) n)

Des exemples de formules sont donnés sur le transparent.

Bruno: pas de changement sur le re-folding? Enrico: non, seulement sur la décision de faire l'unfolding.

Cela correspond à un besoin de ssreflect. Il voudrait avoir une commande pour décrire les arguments implicite, les scopes, et le nombre d'arguments qui sont requis pour que simpl apparaisse. La commande Arguments dans le transparent d'Enrico. Possibilité d'ajouter des directives à la fin de la commande Arguments (par exemple pour détection automatique).

Question sur le fait que l'on soit parfois obligé de donner des arguments implicites.

Bruno: les réglages fins sur les arguments, implicites, scopes, etc.. peuvent aussi être donnés directement à la définition des fonctions (catégorie syntaxique binder).

Choix syntaxique:

[A B] : implicites {A B} : implicite maximal

second part: occurrences for rewriting and matching

standard Coq matching uses question marks. Comment from Pierre: opens the reflexion to shorter syntax for "match goal with ...".

Conclusion is yes.

Hugo

Beaucoup parlé de Coq à l'école d'Oregon. Compcert s'étend beaucoup. Greg Morrissett, discussions avec Voevodsky.

Mentionne un problème levé par A. Appel : Qed slow while tactic proofs are fast. Problem is that conversions go in any direction in proofs, while Qed does conversions always in the same direction.