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.

1. À la découverte de COQ,
2. Prédicats inductifs (la solution des profs, ainsi qu'une autre solution de François Dross, merci à lui),
3. Équivalence petit pas-grand pas d'un langage arithmétique (solution, une solution plus linéaire),
4. Équivalence petit pas-grand pas dans IMP (corrigé),
5. Équivalence petit pas-grand pas dans IMP (suite) et logique de Hoare (corrigé),
6. Hoare en action : l'outil Why,
7. Elimination des références et des exceptions dans MINI-ML,
8. Un interpréteur de MINI-ML (miniml.tgz, code corrigé),
9. Unification (archive, code corrigé),
10. Inférence de type dans MINIML (archive, corrigé),
11. Réécriture (corrigé),
12. Réécriture,
13. Analyse lexicale et syntaxique ( archive),
14. Réécriture,
15. Réécriture en coq.

Vous avez un devoir à rendre: certifiez votre premier compilateur !.

• 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.

• 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.