coq Samouczek
Rozpoczęcie pracy z Coq

Uwagi

Testowanie i instalowanie Coq

Testowanie bez instalacji

Dla nowych użytkowników, którzy chcą rozpocząć testowanie Coq bez instalowania go na swoim komputerze, dostępne jest internetowe IDE o nazwie JsCoq ( tutaj prezentacja). Podokno pakietu umożliwia testowanie różnych dobrze znanych dodatkowych pakietów.

Instalacja

Strona pobierania zawiera instalatory dla Windows i MacOS.

Użytkownikom Linuksa zaleca się kompilowanie ze źródła przy użyciu opam, aby uzyskać najnowszą wersję. Podstawowe instrukcje, jak to zrobić, podano tutaj .

Prosty dowód

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

Wypróbuj w swojej przeglądarce .

Zainstaluj Coq na MacOS

Możesz zainstalować cały pakiet, pobierając pakiet dmg stąd .

Pakiet zawiera CoqIDE, którego można używać do pisania dowodów lub można użyć polecenia coqtop do uruchomienia interpretera na terminalu

Instalacja Coq na MacOS jest również łatwa w użyciu homebrew

brew install coq

lub jeśli korzystasz z MacPorts

sudo port install coq

Nie ma dobrego wsparcia vi dla Coq. Możesz używać Proof General w emacs, który ma dobrą użyteczność.

Aby zainstalować Proof General, usuń stare wersje Proof General, sklonuj nową wersję z GitHub

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

Następnie dodaj do .emac:

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

Upewnij się, że emacs, z którego korzystasz, to rzeczywisty Emacs. Jeśli napotkasz problemy z niedopasowaniem wersji, być może będziesz musiał ponownie uruchomić makefile, podając jawnie ścieżkę Emacsa

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

Instalacja za pomocą Nix

Ostrzeżenie: nie jest to standardowy sposób instalowania Coq.

Dla użytkowników Linuksa (i MacOS), którzy chcą uzyskać dostęp do aktualnych wersji Coq lub móc korzystać z kilku wersji Coq na tym samym komputerze, bez kłopotów z użyciem opama i bez konieczności kompilacji z źródło, jest to alternatywne rozwiązanie.

Nix to menedżer pakietów dla systemów operacyjnych typu Unix, takich jak Linux i MacOS. Zawiera własną kolekcję pakietów, która jest na ogół znacznie bardziej aktualna niż Debiana lub Ubuntu. Nie powoduje konfliktu z menedżerem pakietów twojej dystrybucji, ponieważ nie instaluje niczego w /usr/bin i tym podobnych.

Najpierw musisz zainstalować Nix :

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

Aby upewnić się, że niezbędne zmienne środowiskowe są ustawione, zaloguj się ponownie lub wpisz:

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

Następnie następujące polecenie zainstaluje najnowszą wersję Coq:

$ nix-env -iA nixpkgs.coq_8_6

Możesz także uruchomić CoqIDE bez dodawania czegokolwiek do ŚCIEŻKI:

$ nix-shell -p coq_8_6 --run coqide

Podobnie (zakładając, że masz już zainstalowane Emacsa i Proof-General):

$ nix-shell -p coq_8_6 --run emacs

Jest to bardzo przydatne do uruchamiania różnych wersji, gdy są potrzebne. Na przykład, aby uruchomić Coq 8.5, użyj następującego polecenia:

$ nix-shell -p coq_8_5 --run coqide

Przykład dowodu indukcyjnego

Oto prosty dowód indukcyjny.

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.