Najkrótsza sesja Coqa.

Coq w wersji command-line:

[zawodnik@maszyna]$ coqtop
Welcome to Coq 8.0pl2 (Jan 2005)

Coq < Quit.

[zawodnik@maszyna]$

zeby miec historie i edycje linii:
[zawodnik@maszyna]$ ledit coqtop
(w labie nie dziala :( )

albo w buforze shellowym w emacsie.

Albo lepiej uruchomić środowisko coqide (w labie: coqide.opt)

Termy

Prop oznacza typ "proposition", czyli typ formuł logicznych
identycznosc na typie A ("\lambda x:A.x") to "fun x:A => x"
rzutowanie ("\lambda x:A.\lambda y:B.x") to "fun (x:A) (y:B) => x"
inne rzutowanie ("\lambda x:A.\lambda y:A.x") to "fun x y : A => x"
dla kazdego A i B, A implikuje B ("\forall A \forall B. A->B"), to "forall A B:Prop, A->B"

Komendy trybu normalnego

Każde polecenie zaczynamy z wielkiej litery i kończymy kropką.

Definition nazwa := term.
Definition nazwa : typ := term.
- wprowadza definicje do srodowiska

Parameter nazwa : typ.
- wprowadza "zmienna" do srodowiska

Lemma nazwa : formula.
Theorem nazwa : formula.
- przechodzi do trybu wpisywania dowodow, po szczesliwym zakonczeniu wprowadza lemat/twierdzenie do srodowiska

Goal formula.
- j.w. tylko wprowadza nazwe Unnamed_thm, chyba ze zakonczymy dowod przez Save nazwa.

Komendy informacyjne:

Check term.
- wyswietla typ termu
(w coqide: Queries/Check lub F3

Print nazwa.
- wyswietla definicje stalej
(w coqide: Queries/Print lub F4)

Tryb dowodowy.

Taktyki

Taktyki piszemy z małej litery, komendy z dużej. Kończymy kropką.

intro.
intros.
intro A.
intros A B H.

apply term.

assumption.

auto.

unfold nazwa.
unfold 1 2 3 nazwa.
unfold nazwa in H.

apply H; intros. <- robi intros dla kazdego subgoala generowanego przez apply H.

Komendy

Koniec dowodu

Save.
Qed.
Save nazwa. (po Goal'u)

Chodzenie po sub-goalach

Show 2.
Focus.
Focus 2.
Unfocus.

Wyświetlanie

Show Proof.
Show Script.
Show Tree.
(w coqide najlepiej poprzez okienko Queries)

Rezygnacja

Restart.
Abort.
(w coqide najlepiej się cofnąć do początku dowodu)