Débuter avec le coq

Une preuve simple

Theorem my_first_theorem : 1 + 1 = 2.
Proof.
  reflexivity.
Qed.

Essayez-le dans votre navigateur.

Installation avec Nix

Attention : ce n’est pas la manière standard d’installer Coq.

Pour les utilisateurs de Linux (et MacOS) qui souhaitent avoir accès à des versions à jour de Coq ou pouvoir utiliser plusieurs versions de Coq sur la même machine, sans avoir à utiliser opam, et sans avoir à compiler depuis source, il s’agit d’une solution alternative.

Nix est un gestionnaire de packages pour les systèmes d’exploitation de type Unix tels que Linux et MacOS. Il est livré avec sa propre collection de paquets qui est généralement bien plus à jour que ceux de Debian ou d’Ubuntu. Il n’entre pas en conflit avec le gestionnaire de paquets de votre distribution car il n’installe rien dans /usr/bin et autres.

Tout d’abord, vous devez installer Nix :

$ curl https://nixos.org/nix/install | sh

Pour vous assurer que les variables d’environnement nécessaires sont définies, connectez-vous à nouveau ou tapez :

. $HOME/.nix-profile/etc/profile.d/nix.sh

Ensuite, la commande suivante installera la dernière version de Coq :

$ nix-env -iA nixpkgs.coq_8_6

Vous pouvez également exécuter CoqIDE sans rien ajouter à votre PATH :

$ nix-shell -p coq_8_6 --run coqide

De même (en supposant que vous ayez déjà installé Emacs et Proof-General):

$ nix-shell -p coq_8_6 --run emacs

Ceci est très utile pour exécuter différentes versions lorsque vous en avez besoin. Par exemple, pour exécuter Coq 8.5, utilisez la commande suivante :

$ nix-shell -p coq_8_5 --run coqide

Installer Coq sur MacOS

Vous pouvez installer l’ensemble du bundle en téléchargeant le package dmg depuis ici.

Le bundle contient un CoqIDE qui peut être utilisé pour écrire vos preuves ou vous pouvez utiliser la commande coqtop pour exécuter l’interpréteur sur votre terminal

L’installation de Coq sur MacOS est également facile en utilisant l’homebrew

brew install coq

ou si vous utilisez MacPorts

sudo port installer coq

Il n’y a pas de bon support vi pour Coq. Vous pouvez utiliser Proof General dans emacs qui a une bonne convivialité.

Pour installer Proof General, supprimez les anciennes versions de Proof General, clonez la nouvelle version de GitHub

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

Ajoutez ensuite ce qui suit à votre .emacs :

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

Assurez-vous que l’emacs que vous utilisez est bien l’Emacs. Si vous rencontrez des problèmes d’incompatibilité de version, vous devrez peut-être exécuter à nouveau le makefile en spécifiant explicitement le chemin Emacs

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

Tester et installer Coq

Tester sans installer

Pour les nouveaux utilisateurs qui souhaitent commencer à tester Coq sans l’installer sur leur machine, il existe un IDE en ligne appelé JsCoq (présentation [ici](https://x80.org /rhino-coq/)). La sous-fenêtre package permet de tester divers packages supplémentaires bien connus.

Installation

La page de téléchargement contient les installateurs pour Windows et MacOS.

Il est généralement conseillé aux utilisateurs de Linux de compiler à partir des sources en utilisant opam, afin d’obtenir la dernière version. Des instructions de base sur la façon de le faire sont données ici.

Exemple de preuve par induction

Voici une preuve simple par induction.

Require Import Coq.Setoids.Setoid.
Require Import Coq.Arith.Lt.

(* A number is less than or equal to itself *)
Theorem aLTEa : forall a,
    a <= a.
    auto with arith. (* This follows by simple arithmetic *)
    Qed.

Theorem simplALTE : forall a b,
    S a <= S b <-> a <= b. (* If a <= b, then a + 1 <= b + 1 *)
Proof.
Admitted.

Theorem ltAlwaysLt: forall a b,
    a <= a + b.
Proof.
  intros. (* Introduce relevant variables *)
  induction a, b. (* Induction on every variable *)
  simpl. apply aLTEa. (* 0 <= 0 + S b *)
  rewrite -> plus_O_n. auto with arith. (* 0 <= S b *)
  rewrite <- plus_n_O. apply aLTEa. (* S a <= S a + 0 *)
  rewrite <- simplALTE in IHa. (* IHa: a <= a + S b. Goal: S a <= S a + S b. *)
  apply IHa. (* We rewrote the induction hypothesis to be in the same form as the goal, so it applies immediately now *)
  Qed.