Atelier sur l'assistant à la preuve Coq, pour les journées nationales de l'APMEP

Damien Pous, Grenoble, le 24 octobre 2011

Résumé

Comment vérifier une démonstration à l'aide d'un ordinateur ?

Comment trouver une démonstration à l'aide d'un ordinateur ?

L'assistant à la preuve Coq, développé en France depuis une trentaine d'années, permet aujourd'hui de formaliser de vastes pans des mathématiques. Encore mieux, il permet d'automatiser certaines étapes de raisonnement, et d'éviter ainsi de longs et laborieux calculs.

Après une brève présentation de cet assistant de preuve, l'atelier consistera ensuite en une courte initiation durant laquelle les participants pourront formaliser de petits théorèmes du programme de terminale.

Fichiers pour l'atelier

Les fichiers troués, que l'on va boucher pendant l'atelier:
1. Logic (logique propositionelle de base);
2. Primes (petits exercices sur les nombres premiers);
3. Gauss (démonstration des théorèmes de Bachet-Bézout et Gauss).
Une version en html de toutes les solutions.
Les transparents d'introduction (au format PDF).

Petit mémo des différentes commandes et tactiques Coq utilisées:

Tactiques de base
intros a b H.	(introduire des variables ou des hypothèses)
apply H.	(appliquer une hypothèse)
apply nom.	(appliquer un théorème ou un lemme)
split.	(casser en deux un but qui est une conjonction)
left / right.	(choisir la branche gauche ou droite quand le but est une disjonction)
exists t.	(donner un témoin quand le but est une existentielle)
destruct H as [H1 H2].	(casser une hypothèse qui est une conjonction)
destruct H as [H1 \| H2].	(casser une hypothèse qui est une disjonction -- génère deux sous-buts)
destruct H as [x Hx].	(casser une hypothèse qui est une existentielle)
intros [H \| [H1 H2]] [x Hx].	(introduire des hypothèses en les cassant immédiatement)
compute.	(simplifier le but par calcul)
unfold nom.	(dérouler une définition)
transitivity t.	(passer par t dans une preuve d'égalité)
rewrite H.	(réécrire le but en utilisant l'hypothèse H)

Tactiques automatiques
easy.	(résoudre un but très facile)
ring.	(prouver une égalité d'anneau)
tauto.	(prouver une tautologie du premier ordre)
auto using nom1, nom2, ...	(rechercher automatique, en utilisant les lemmes donnés)

Commandes
Check t.	(vérifier et afficher le type de [t])
Compute t.	(simplifier et afficher [t])
Definition nom args := valeur.	(poser une définition)
Theorem nom: énoncé.	(démarrer la preuve interactive d'un théorème)
Lemma nom: énoncé.	(démarrer la preuve interactive d'un lemme)
Qed.	(indiquer la fin d'une preuve)
Admitted.	(abandonner et admettre la preuve en cours)
Hint Resolve nom.	(déclarer un lemme comme indice pour [auto])






Tacticielles
tac1; tac2.	(appliquer [tac2] à tous les sous-buts générés par [tac1])
tac1 \|\| tac2.	(essayer [tac1] et faire [tac2] en cas d'échec)
try tac.	(essayer [tac], sans râler en cas d'échec)
repeat tac.	(faire [tac] jusqu'à un échec)
Ltac mytac [args] := tac.	(definir une tactique personelle)

Atelier sur l'assistant à la preuve Coq, pour les journées nationales de l'APMEP

Résumé

Fichiers pour l'atelier

Petit mémo des différentes commandes et tactiques Coq utilisées:

Tactiques de base

Tactiques automatiques

Commandes

Tacticielles

Divers liens à propos de Coq