coq 튜토리얼
coq 시작하기

비고

Coq 테스트 및 설치

설치하지 않고 테스트하기

Coq를 컴퓨터에 설치하지 않고 테스트를 시작하려는 신규 사용자의 경우 JsCoq라는 온라인 IDE가 있습니다 ( 여기에서 프레젠테이션). 패키지 하위 창을 통해 잘 알려진 다양한 추가 패키지를 테스트 할 수 있습니다.

설치

다운로드 페이지 에는 Windows 및 MacOS 용 설치 관리자가 포함되어 있습니다.

Linux 사용자는 일반적으로 최신 버전을 얻으려면 opam을 사용하여 소스에서 컴파일하는 것이 좋습니다. 그렇게하는 방법에 대한 기본 지침이 여기 에 나와 있습니다 .

간단한 증거

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

브라우저에서 사용해보십시오 .

MacOS에 Coq 설치

여기 에서 dmg 패키지를 다운로드하여 전체 번들을 설치할 수 있습니다.

번들은 여러분의 증명을 쓰기 위해 사용될 수있는 CoqIDE를 포함하고 있거나 여러분의 터미널에서 인터프리터를 실행하기 위해 coqtop 명령을 사용할 수 있습니다

MacOS에 Coq를 설치하는 것은 homebrew를 사용하는 것 또한 쉽습니다.

brew install coq

또는 MacPorts를 사용하는 경우

sudo port install coq

Coq에는 좋은 vi 지원이 없습니다. 사용성이 좋은 emacs에서 Proof General을 사용할 수 있습니다.

Proof General을 설치하려면 Proof General의 이전 버전을 제거하십시오. 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 경로를 지정하여 makefile을 다시 실행해야 할 수도 있습니다

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

Nix로 설치

경고 : 이것은 Coq를 설치하는 표준 방법이 아닙니다.

Linux 사용자 (또는 MacOS) 사용자가 최신 버전의 Coq에 액세스하거나 opam을 사용하는 번거 로움없이 컴파일 할 필요없이 같은 컴퓨터에서 여러 버전의 Coq을 사용할 수 있기를 원하는 사용자 원본, 이것은 대안 솔루션입니다.

Nix 는 Linux 및 MacOS와 같은 Unix 유형 OS 용 패키지 관리자입니다. 데비안 또는 우분투보다 훨씬 더 최신으로 유지되는 자체 패키지 모음이 함께 제공됩니다. /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

PATH에 아무 것도 추가하지 않고 CoqIDE를 실행할 수도 있습니다.

$ 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.