Travaux dirigés de théorie de la programmation
Ioana Pasca et
moi-même
sommes chargés des travaux dirigés du cours
Théorie de la programmation
assuré par Daniel Hirschkoff.
Voici la listes des énoncés de chacune des séances:
- À la découverte de COQ,
- Prédicats inductifs (la solution des profs, ainsi qu'une autre solution de François Dross, merci à lui),
- Équivalence petit pas-grand pas d'un langage arithmétique (solution, une solution plus linéaire),
- Équivalence petit pas-grand pas dans IMP (corrigé),
- Équivalence petit pas-grand pas dans IMP (suite) et logique de Hoare (corrigé),
- Hoare en action : l'outil Why,
- Elimination des références et des exceptions dans MINI-ML,
- Un interpréteur de MINI-ML (miniml.tgz,
code corrigé),
- Unification
(archive,
code corrigé),
- Inférence de type dans MINIML
(archive, corrigé),
- Réécriture (corrigé),
- Réécriture,
- Analyse lexicale et syntaxique (
archive),
- Réécriture,
- Réécriture en coq.
Vous avez un devoir à rendre: certifiez votre premier compilateur !.
Voici la liste des tactiques indispensables:
Puis voici une liste de tactiques utiles:
- induction:
induction x
invoque le bon principe d'induction
pour prouver le but par induction sur x
.
- inversion:
inversion H
devine toutes les formes
possible du paramètre du prédicat inductifs prouvé par l'hypothèse
H
.
- simpl: simplifie le but (ou une hypothèse via la syntaxe
simpl in H
) en effectuant un calcul.
- unfold:
unfold def
déplie la définition def
dans l'énoncé du but à prouver (ou dans une hypothèse via la syntaxe unfold def in H
).
- assumption: regarde si une hypothèse permet de prouver directement le but.
- assert:
assert P
créé un nouveau but
pour prouver P
et rajoute P
dans la liste des hypothèses des autres buts. Utile pour raisonner en avant.
On peut également préciser le nom de l'hypothèse grâce à la syntaxe suivante assert (H : P)
.
- replace:
replace t₁ with t₂
équivalent
de assert (H : t₁ = t₂). rewrite H.
Enfin, voici la liste des tactiques "interdites" (ce sont les tactiques automatiques):
- auto: cherche à prouver le but en appliquant
récursivement les théorèmes du contexte.
- omega: prouve toutes les formules de
l'arithmétique de Presburger. Nécessite de charger la bibliothèque adéquate grâce à
Require Import Omega.
- ring: prouve toutes les formules sans quantificateur
vraies dans tous les anneaux. Nécessite de charger la bibliothèque adéquate grâce à
Require Import Ring.
Dans tous les cas n'hésitez jamais à consulter le manuel de coq ainsi que
la bibliothèque standard.