Accès à Coq (narrhavas uniquement!)

Attention! La version de Coq accessible à l'ENSEIRB est une version assez ancienne (version 6); pour une version récente, aller sur le site de Coq.

Le plus simple est de travailler sous "emacs", avec une région pour le fichier source Coq, et une région pour le shell Coq dans laquelle on introduit les commandes Coq par des "couper/coller" à partir du fichier source:

consulter le fichier ~gloess/coq/ALIRE pour toutes les précisions.

Retour en haut

Information sur Coq

Coq est développé à l'I.N.R.I.A.: on trouvera sur le site de Coq à l'INRIA la documentation la plus récente.

De la documentation (ancienne mais toujours intéressante) par les auteurs est accessible localement à partir de ~gloess/coq/doc, comprenant entre autres:

tous les manuels en ligne sous /net/opt/local/doc/coq/ à l'ENSEIRB);
une présentation postscript de Coq par Gérard Huet (formation Coq 1996 à Lyon):

slides1;
slides2.

une liste d'exercices proposée lors de cette formation (contenant en particulier un tableau des commandes de preuve les plus courantes).

Retour en haut

Exercices d'initiation à Coq

Attention! Les exercices (classiques) proposés ci-dessous utilisent l'ancienne syntaxe de Coq (antérieure à la version 8): il existe un convertisseur de l'ancienne syntaxe vers la nouvelle.

Les fichiers suivants du répertoire ~gloess/coq/exercices/ contiennent des exercices et leurs solutions:

td1.v: les commandes pour examiner l'environnement, des preuves directes de types, quelques types inductifs prédéfinis;
td2.v: types inductifs, récursivité primitive, conception interactive de preuves, extraction.

Retour en haut