Vous trouverez dans ce fichier un script de commande pour Coq qu'il s'agit de compléter
L'objectif de ces travaux dirigés est de se familiariser avec les démonstrations de sémantique et leur vérification dans un système de démonstration sur ordinateur. Toute démonstration de sémantique ne doit pas nécessairement être vérifiée par ordinateur, mais cet aspect permet de se convaincre que l'on a bien effectué une démonstration complète.
Dans le cours, nous avons utilisés plusieurs formes de raisonnement sur les dérivations, comme des raisonnements par récurrence et des raisonnements par analyse de dérivations (quelles règles peuvent être appliquées? quelles égalités entre les variables ceci implique-t-il?). Ici, il importe de se souvenir que les jugements pour lesquels ce type de raisonnement doit être fourni sont définis par une définition inductive, que les raisonnements par récurrence sont faits par elim, et que les raisonnements par analyse de dériviation sont faits par inversion.
Pour des raisons pédagogiques, j'ai volontairement réduit le nombre de commande de Coq qui sont utilisés dans mes exemples. Vous pourrez normalement effectuer tous les exercices proposés avec ces commandes. Mais l'objectif pédagogique n'est peut-être pas parfaitement atteint car certaines opérations pourraient être faites plus rapidement et de façon plus intuitive par d'autres commandes. Aux plus curieux d'entre vous, je suggère d'étudier les commandes induction (à la place de elim), subst (à la place de rewrite).
Il existe une documentation en ligne pour Coq, disponible à l'adresse suivantehttp://pauillac.inria.fr/coq/doc-fra.html
L'objectif principal est de démontrer la correction d'une transformation de programme par réécriture. Il s'agit de montrer que toute instance d'un certain fragment de programme peut être remplacée par un autre fragment de programme. Le fragment de programme que j'ai choisi est le suivant:
x:= 1; while 0 < x do i
le remplacement est le suivant:
x:=1; i ; while 0 < x do i
Il s'agit de démontrer la phrase suivante: Si I' est le même que le programme I sauf que certaines instances du premier fragment sont remplacées par le second fragment, alors toute exécution du premier programme peut être reproduite par une exécution du second programme. Ce théorème sera obtenu par une combinaison des théorèmes subst_equiv et ex_transformation. Les autres théorèmes sont des lemmes annexes dont j'ai eu besoin en faisant moi-même l'exercice.