Une introduction à Coq

Ressources

JSCoq, Coq dans le navigateur (utiliser Firefox ou Google Chrome et attendre quelques secondes la fin du téléchargement)
Coq, définition Wikipedia
De l'INRIA : Coq, téléchargement, documentation, cours multimédia Coq (Yves Bertot), les diapos 1 2 3 4 5 6 7 8
Propositions as Types, résumé, vidéo YT de Philip Wadler
Un interprète OCaml en ligne, au cas où
Coq, assistant de preuve, un article introductif de la revue Techniques de l'Ingénieur, preuve Coq, idem en version HTML via coqdoc, idem en version PDF via coqdoc
Quelques tactiques de Coq : le Coq Survival Kit et la Coq Tactics Cheatsheet.

TP1 : énoncé, squelette
Indications :
- Exo 1 : intro, intros, assumption, apply hyp, destruct hyp, split, left, right, unfold not
- Exo 2 : destruct hyp with term, exists term
- Exo 3 : specialize hyp with term, assert (hyp:formula), assert(formula), Search(eq_sym)
TP2 : énoncé, squelette
Indications :
- simpl, induction var, rewrite hyp, rewrite prop. Require Import Lia. Lemma mult_n_0:forall n, n*0=0.
TP2bis : squelette
TP3 : énoncé, squelette
Indications :
- unfold, fold, rewrite
TP4 : énoncé (envisager de faire le TP5 avant)
TP5 : énoncé (remplacer Omega par Lia lors de l'import des bibliothèques)

Les trois premiers chapitres de Logical Foundations (Benjamin Pierce et al.) de la série Software Foundations, traduits en français par Tom Hirschowitz.