Un guide de survie pour les tactiques ssr de Coq.
Les solutions données ne sont qu'une possibilité parmi d'autres. Elles sont souvent formulées de manière à illustrer certaines possibilités du langage de preuve.
TD2 (Le Damier de Cachan)
TD3, le tri: exercice et solution.
Formalisation de PCF; squelette et une solution
exo reflection puis types dans PCF. Une solution.
Compilation: Le rapport de recherche de X. Leroy; le chapitre 3 est une bonne présentation de la machine abstraite KAM et de sa preuve de correction. Une version de départ possible pour la preuve de correction.
1) Partir du corrigé, de la correction de la KAM vis-à-vis de la sémantique à petits pas, et étendre la machine:
* Transformer la machine en appel par valeurs. Pour cela, ajouter l'instruction reduce, telle que décrite à la page 27 du rapport ZINC.
Etendre la machine se fait simplement en suivant le texte du rapport. Il faut réfléchir un peu pour définir la décompilation des piles.
On peut ensuite reprendre les preuves en ajoutant les nouveaux cas. Il n'y a pas trop de pièges.
* On peut ensuite ajouter les entiers primitifs et les opérateurs. Cela demande de réfléchir ou chercher un peu pour trouver une machine qui traite les entiers.
Attention, il vaut mieux réflechir d'abord à la machine, puis proposer une extension du langage source qui permette de bien définir la décompilation. Ensuite faire les preuves.
* Enfin on peut ajouter ensuite le test à zéro.
2) Définir une sémantique à grands pas en suivant le chapitre 3 du cours de G. Dowek. On le faire soit pour le langage riche (des premiers TDs), soit le langage réduit (que l'on a compilé).
Il est sans doute plus facile de le faire pour le langage réduit. Dans ce cas, on peut continuer en prouvant la correction de la KAM par rapport à cette sémantique.