coq Handledning
Komma igång med coq

Anmärkningar

Testa och installera Coq

Testa utan att installera

För nya användare som vill börja testa Coq utan att installera det på sin maskin finns det en online-IDE som heter JsCoq (presentation här ). Underfönstret för paket gör det möjligt att testa olika välkända ytterligare paket.

Installation

Nedladdningssidan innehåller installatörer för Windows och MacOS.

Användare av Linux rekommenderas vanligtvis att sammanställa från källan med hjälp av opam för att få den senaste versionen. Grundläggande instruktioner för hur du gör det ges här .

Ett enkelt bevis

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

Prova det i din webbläsare .

Installera Coq på MacOS

Du kan installera hela paketet genom att ladda ner dmg-paketet härifrån .

Paketet innehåller en CoqIDE som kan användas för att skriva dina bevis eller du kan använda kommandot coqtop att köra tolk på din terminal

Installation av Coq på MacOS är också lätt att använda homebrew

brew install coq

eller om du använder MacPorts

sudo port install coq

Det finns inget bra vi-stöd för Coq. Du kan använda Proof General inom emacs som har god användbarhet.

För att installera Proof General tar du bort gamla versioner av Proof General klonar den nya versionen från GitHub

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

Lägg sedan till följande till dina .emacs:

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

Se till att emacerna du kör faktiska Emacs. Om du får problem med matchningsversionen av versionen kanske du måste köra makefile igen och specificera Emacs-sökvägen uttryckligen

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

Installation med Nix

Varning: detta är inte det vanliga sättet att installera Coq.

För användare av Linux (och MacOS) som vill få tillgång till uppdaterade versioner av Coq eller för att kunna använda flera versioner av Coq på samma maskin, utan besväret med att använda opam, och utan att behöva sammanställa från källa, detta är en alternativ lösning.

Nix är en paketansvarig för operativsystem av Unix-typ som Linux och MacOS. Den levereras med sin egen samling paket som i allmänhet hålls mycket mer uppdaterad än Debians eller Ubuntu. Det kommer inte i konflikt med din distributionss pakethanterare eftersom den inte installerar något i /usr/bin och sådant.

Först måste du installera Nix :

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

För att säkerställa att de nödvändiga miljövariablerna ställs in loggar du in igen eller skriver:

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

Därefter installerar följande kommando den senaste versionen av Coq:

$ nix-env -iA nixpkgs.coq_8_6

Du kan också köra CoqIDE utan att lägga till något i din PATH:

$ nix-shell -p coq_8_6 --run coqide

På liknande sätt (antar att du redan har Emacs och Proof-General installerat):

$ nix-shell -p coq_8_6 --run emacs

Detta är mycket användbart för att köra olika versioner när du behöver dem. Till exempel, för att köra Coq 8.5, använd följande kommando:

$ nix-shell -p coq_8_5 --run coqide

Exempel på ett bevis genom induktion

Här är ett enkelt bevis genom induktion.

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.