Énoncés des TD/TP
- TD1 : un TD plutôt théorique de familiarisation avec le lambda-calcul et le système F. Mise en application sous COQ.
- TD2 : logique propositionnelle. Les tactiques intros, apply, exact et unfold. Définitions par pattern matching.
- TD6bis : la suite du TD sur les liste triées.
- TD7 : sémantique d'un petit langage de programmation.
- TD7bis : la suite du TD 7.
- TD10 : spécification de la racine carrée entière.
Éléments de corrections
Petit mémo
Le manuel de référence de Coq en PDF et en ligne.
- Sections :
Section Nom. [...] End Nom.
- Déclaration locale : Variable, Variables, Hypothesis, Hypotheses
- Déclaration globale : Parameter, Parameters, Axiom
- Affectation locale : Let
- Affectation globale : Definition
- But anonyme : Goal
- Changer de sous-but lorsqu'il y en a plusieurs : Focus
- Vérifier le type d'un terme : Check
- Afficher un terme : Print
- Arguments possibles de cbv :
- delta déplie les définitions
- beta réduit les redex
- zeta réduit les définitions let [...] in
- iota récurse dans les objets inductifs
- Calculer :
- Eval compute in expression : synonyme de Eval cbv delta beta iota zeta in expression
- Eval simpl in expression : synonyme de Eval cbv beta iota in expression
- Tactiques utiles
- tac1 ; tac2 applique tac2 à tous les sous-buts générés par tac1. Échoue complètement en cas de problème.
- cut : le lemme coupé est démontré à la fin
- assert : le lemme coupé est démontré tout de suite
- apply myTh with (arg1 := val1) (argn := valn)
- unfold myDef in myHypo at position
- Rechercher un théorème
- SearchAbout plus : recherche les théorèmes où l'identifiant plus intervient
- SearchPattern (_ + ?X1 = ?X1) : recherche les théorèmes dont la conclusion a cette forme
- SearchRewrite (_ + _) : recherche un égalité dont un des membres a cette forme