coq Tutorial
Erste Schritte mit coq
Suche…
Bemerkungen
In diesem Abschnitt erhalten Sie einen Überblick darüber, was coq ist und warum ein Entwickler es verwenden möchte.
Es sollte auch alle großen Themen in coq erwähnen und auf die verwandten Themen verweisen. Da die Dokumentation für coq neu ist, müssen Sie möglicherweise erste Versionen dieser verwandten Themen erstellen.
Testen und Installieren von Coq
Testen ohne zu installieren
Für neue Benutzer, die Coq testen möchten, ohne es auf ihrem Computer zu installieren, gibt es eine Online-IDE namens JsCoq (Präsentation hier ). Das Paket-Unterfenster ermöglicht das Testen verschiedener bekannter Zusatzpakete.
Installation
Die Download-Seite enthält Installationsprogramme für Windows und MacOS.
Benutzern von Linux wird im Allgemeinen empfohlen, sie mit opam zu kompilieren, um die neueste Version zu erhalten. Grundlegende Anweisungen dazu finden Sie hier .
Ein einfacher Beweis
Theorem my_first_theorem : 1 + 1 = 2.
Proof.
reflexivity.
Qed.
Versuchen Sie es in Ihrem Browser .
Installieren Sie Coq unter MacOS
Sie können das gesamte Paket installieren, indem Sie das dmg-Paket von hier herunterladen.
Das Bundle enthält ein CoqIDE, mit dem Sie Ihre Proofs schreiben können, oder Sie können den Befehl coqtop , um den Interpreter auf Ihrem Terminal auszuführen
Die Installation von Coq unter MacOS ist auch mit Homebrew problemlos möglich
brew install coq
oder wenn Sie MacPorts verwenden
sudo port install coq
Es gibt keine gute vi-Unterstützung für Coq. Sie können Proof General innerhalb von emacs verwenden, was eine gute Benutzerfreundlichkeit bietet.
Um Proof General zu installieren, müssen Sie die alte Version von Proof General aus GitHub klonen
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make
Fügen Sie dann Ihren .emacs Folgendes hinzu:
;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")
Stellen Sie sicher, dass die Emacs, die Sie ausführen, die tatsächlichen Emacs ausführen. Bei Problemen mit Versionskonflikten müssen Sie möglicherweise das Makefile erneut ausführen, indem Sie den Emacs-Pfad explizit angeben
make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
Installation mit Nix
Warnung: Dies ist nicht die Standardmethode zur Installation von Coq.
Für Benutzer von Linux (und MacOS), die Zugriff auf aktuelle Coq-Versionen erhalten möchten oder mehrere Coq-Versionen auf demselben Computer verwenden können, ohne Opam verwenden zu müssen und keine Kompilierung durchführen muss Quelle ist dies eine alternative Lösung.
Nix ist ein Paketmanager für Betriebssysteme des Typs Unix wie Linux und MacOS. Es verfügt über eine eigene Sammlung von Paketen, die im Allgemeinen viel aktueller ist als die von Debian oder Ubuntu. Es steht nicht in Konflikt mit dem Paketmanager Ihrer Distribution, da in /usr/bin nichts installiert wird.
Zunächst müssen Sie Nix installieren :
$ curl https://nixos.org/nix/install | sh
Um sicherzustellen, dass die erforderlichen Umgebungsvariablen festgelegt sind, melden Sie sich entweder erneut an oder geben Sie Folgendes ein:
. $HOME/.nix-profile/etc/profile.d/nix.sh
Dann installiert der folgende Befehl die neueste Version von Coq:
$ nix-env -iA nixpkgs.coq_8_6
Sie können CoqIDE auch ausführen, ohne etwas zu Ihrem PFAD hinzuzufügen:
$ nix-shell -p coq_8_6 --run coqide
Ähnlich (vorausgesetzt, Sie haben bereits Emacs und Proof-General installiert):
$ nix-shell -p coq_8_6 --run emacs
Dies ist sehr nützlich, um verschiedene Versionen auszuführen, wenn Sie diese benötigen. Um Coq 8.5 auszuführen, verwenden Sie beispielsweise den folgenden Befehl:
$ nix-shell -p coq_8_5 --run coqide
Beispiel eines Beweises durch Induktion
Hier ist ein einfacher Beweis durch 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.