Logique

Slides in pdf

  1. Introduction au cours
  2. Introduction to Coq
  3. Propositional Logic
  4. Quantifiers, equality and all that
  5. Basic programming with simple data types
  6. Inductive types : proving and programming
  7. Induction over natural numbers
  8. Simple proofs by induction
  9. Simple proofs by induction (compléments)
  10. Inductive Predicates

Coq quick reference sheet

Principales commandes

Le Coq'Art en V.F.

Download

Exercices

  1. Pogrammer en Coq
  2. Premières preuves
  3. Logique du premier ordre
  4. Logique d'ordre supérieur
  5. Basic programming with simple data types
  6. Inductive types : proving and programming
  7. Proofs by induction on nat
  8. Préparation au TP noté

Solutions of some exercises

Nous déconseillons formellement de regarder prémaurément ces solutions

Archives examens

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