Logique

Slides in pdf

  1. Introduction to Coq
  2. Propositional Logic
  3. Quantifiers, equality and all that
  4. Basic programming with simple data types
  5. Inductive types : proving and programming
  6. Simple proofs by induction
  7. Inductive Predicates

Archives

Coq quick reference sheet

Principales commandes

Le Coq'Art en V.F.

Download

Lab sessions

  1. Simple programming in Coq
  2. Your first proofs
  3. First Order Logic
  4. Higher Order Logic
  5. Basic programming with simple data types
  6. Inductive types : proving and programming
  7. Proofs by induction on nat
  8. Inductive Predicates

Solutions of some exercises

Détails pratiques

Il y a deux outils pour travailler en Coq.
Pour les habitués d'Emacs : utiliser Proof General (voir note en bas de page), qui est un mode Emacs spécialisé dans les preuves interactives.

Ceux qui préfèrent les "ide" , utiliser coqide, l'environnement de développement intégré pour Coq.
coqide est moins usine à gaz qu'Eclipse. Si un bug provoqué par la diabolique touche MOD4 (celle avec une fenêtre tordue) de votre clavier se produit, alors éditer votre fichier $HOME/.coqiderc et remplacer toutes les occurrences de MOD4 par MOD1, puis relancer.

Liens et informations utiles