Support de cours
Formation COQ 25-27 février 2002
1 Sources de Coq
Les sources
de la version de Coq utilisée dans la formation.
2 Utilisation de Proof General
-
http://zermelo.dcs.ed.ac.uk/~proofgen/
- Insérer les commandes suivantes
dans son fichier .emacs. Modifier si nécessaire le
chemin d'accès à Proof-General.
- Éditer un fichier Coq fichier.v
- Lancer Coq (Start Proof Assistant) dans le menu
Proof general
- Séparer sa fenêtre une fois verticalement
Ctrl X 3
et une
fois horizontalement Ctrl X 2
- Mettre dans chacune des fenêtres respectivement :
les buffers
*coqtop-goals*
*coqtop-response*
et le
fichier à éditer.
- Pour faire interpréter une phrase :
Ctrl Alt
¯
- Pour revenir en arrière :
Ctrl Alt
- Pour envoyer une phrase en tapant le point : Electric
Terminator
3 Documentation
La documentation Coq V7 au format HTML
4 Lundi 25 février
4.1 Cours
Copie des transparents
4.2 Exemple du damier
Le squelette de l'exemple du damier
La solution du damier-html(code source)
5 Mardi 26 février
5.1 Cours
Copie des transparents
5.2 Exemple en sémantique
Le squelette de l'exemple en sémantique
La solution de l'exemple en sémantique-html
(code source)
Le squelette des définitions sur les relations
La solution de l'exemple sur les relations
(code source)
La preuve de l'algorithme d'exclusion mutuelle
(code source)
6 Mercredi 27 février
6.1 Cours
Copie des transparents
6.2 Preuve de programmes
Solution de l'exercice de certification de
programmes-html
(code source)
6.3 Tactique réflexive
Le squelette de l'exemple de tactique réflexive
La solution de l'exemple-html
(code source)
7 Informations supplémentaires
This document was translated from LATEX by HEVEA.