coqAan de slag met coq


Opmerkingen

Deze sectie geeft een overzicht van wat coq is en waarom een ontwikkelaar het misschien wil gebruiken.

Het moet ook alle grote onderwerpen binnen coq vermelden en een link naar de gerelateerde onderwerpen bevatten. Aangezien de documentatie voor coq nieuw is, moet u mogelijk eerste versies van die gerelateerde onderwerpen maken.

Coq testen en installeren

Testen zonder te installeren

Voor nieuwe gebruikers die Coq willen testen zonder het op hun machine te installeren, is er een online IDE genaamd JsCoq (presentatie hier ). In het pakket-subvenster kunnen verschillende bekende extra pakketten worden getest.

Installatie

De downloadpagina bevat installatieprogramma's voor Windows en MacOS.

Gebruikers van Linux worden over het algemeen geadviseerd om met behulp van opam te compileren om de nieuwste versie te krijgen. Basic instructies over hoe dit te doen krijgen hier .

Een eenvoudig bewijs

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

Probeer het in uw browser .

Voorbeeld van een bewijs door inductie

Hier is een eenvoudig bewijs door inductie.

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.
 

Installeer Coq op MacOS

U kunt de hele bundel installeren door het dmg-pakket hier te downloaden.

De bundel bevat een CoqIDE die kan worden gebruikt voor het schrijven van uw proeven of u kunt het coqtop commando gebruiken om de tolk op uw terminal uit te voeren

Coq installeren op MacOS is ook eenvoudig met homebrew

brew install coq

of als u MacPorts gebruikt

sudo port install coq

Er is geen goede vi-ondersteuning voor Coq. Je kunt Proof General gebruiken binnen emacs met een goede bruikbaarheid.

Om Proof General te installeren, verwijdert u oude versies van Proof General, kloon de nieuwe versie van GitHub

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

Voeg vervolgens het volgende toe aan uw .emacs:

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

Zorg ervoor dat de emacs waarop je de werkelijke Emacs uitvoert. Als u problemen ondervindt met niet-overeenkomende versies, moet u mogelijk makefile opnieuw uitvoeren met expliciet het Emacs-pad

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

Installatie met Nix

Waarschuwing: dit is niet de standaard manier om Coq te installeren.

Voor gebruikers van Linux (en MacOS) die toegang willen hebben tot up-to-date versies van Coq of verschillende versies van Coq op dezelfde machine willen kunnen gebruiken, zonder het gebruik van opam, en zonder te hoeven compileren vanaf bron, dit is een alternatieve oplossing.

Nix is een pakketbeheerder voor OS van het Unix-type zoals Linux en MacOS. Het komt met een eigen verzameling pakketten die over het algemeen veel actueler wordt gehouden dan die van Debian of Ubuntu. Het conflicteert niet met de pakketbeheerder van uw distributie omdat het niets installeert in /usr/bin en dergelijke.

Eerst moet u Nix installeren :

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

Om ervoor te zorgen dat de benodigde omgevingsvariabelen worden ingesteld, logt u opnieuw in of typt u:

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

Vervolgens wordt met de volgende opdracht de nieuwste versie van Coq geïnstalleerd:

$ nix-env -iA nixpkgs.coq_8_6
 

U kunt CoqIDE ook uitvoeren zonder iets aan uw PATH toe te voegen:

$ nix-shell -p coq_8_6 --run coqide
 

Op dezelfde manier (stel dat je Emacs en Proof-General al hebt geïnstalleerd):

$ nix-shell -p coq_8_6 --run emacs
 

Dit is erg handig om verschillende versies uit te voeren wanneer u ze nodig hebt. Gebruik bijvoorbeeld de volgende opdracht om Coq 8.5 uit te voeren:

$ nix-shell -p coq_8_5 --run coqide