coq учебник
Начало работы с coq

замечания

Тестирование и установка Coq

Тестирование без установки

Для новых пользователей, которые хотят начать тестирование Coq без его установки на своем компьютере, существует онлайн-среда IDE под названием JsCoq (презентация здесь ). Под-окно пакета позволяет тестировать различные известные дополнительные пакеты.

Монтаж

На странице загрузки содержатся инсталляторы для Windows и MacOS.

Пользователям Linux обычно рекомендуется скомпилировать исходный код с помощью opam, чтобы получить последнюю версию. Основные инструкции о том, как сделать так , приведены здесь .

Простое доказательство

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

Попробуйте в своем браузере .

Установите Coq на MacOS

Вы можете установить весь комплект, загрузив пакет dmg отсюда .

Пакет содержит CoqIDE, который можно использовать для написания ваших доказательств, или вы можете использовать команду coqtop для запуска интерпретатора на вашем терминале

Установка Coq на MacOS легко, используя homebrew, также

brew install coq

или если вы используете MacPorts

sudo port install coq

Для Coq нет хорошей поддержки vi. Вы можете использовать Proof General в emacs, который имеет хорошее удобство использования.

Чтобы установить Proof General, удалите старые версии Proof General clone новой версии от GitHub

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

Затем добавьте следующее в ваш .emacs:

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

Убедитесь, что emacs вы используете фактический Emacs. Если вы столкнулись с проблемами несоответствия версии, возможно, вам придется запустить makefile снова, явно указывая путь Emacs

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

Установка с Nix

Внимание: это не стандартный способ установки Coq.

Для пользователей Linux (и MacOS), которые хотят получить доступ к обновленным версиям Coq или иметь возможность использовать несколько версий Coq на одном и том же компьютере, без хлопот использования opam и без компиляции из источник, это альтернативное решение.

Nix - это менеджер пакетов для Unix-типа, таких как Linux и MacOS. Он поставляется со своей собственной коллекцией пакетов, которая, как правило, хранится гораздо более актуально, чем Debian или Ubuntu. Это не противоречит менеджеру пакетов вашего дистрибутива, потому что он не устанавливает ничего в /usr/bin и тому подобное.

Во-первых, вам нужно установить Nix :

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

Чтобы установить необходимые переменные среды, выполните вход снова или введите:

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

Затем следующая команда установит последнюю версию Coq:

$ nix-env -iA nixpkgs.coq_8_6

Вы также можете запустить CoqIDE, не добавляя ничего в свой PATH:

$ nix-shell -p coq_8_6 --run coqide

Аналогично (предположим, что у вас уже установлены Emacs и Proof-General):

$ nix-shell -p coq_8_6 --run emacs

Это очень полезно для запуска различных версий, когда они вам понадобятся. Например, для запуска Coq 8.5 используйте следующую команду:

$ nix-shell -p coq_8_5 --run coqide

Пример доказательства по индукции

Вот простое доказательство индукции.

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.