Poprzednie rozważania naprowadziły nas na trop dowodzenia twierdzeń za pomocą sprytnie pomyślanych regułek przekształcających jedne napisy w inne, wychodząc od rzeczy uznanych za oczywiste, aż osiągnie się to co chcemy dowieść, lub sprytniej wychodząc od zaprzeczenia tego co chcemy dowieść, tymi samymi regułkami do sprzeczności we wszystkich możliwych przypadkach. Zapewne wielu ludzi wpadło na pomysł że skoro metody te sa algorytmiczne, to można je używać nie tylko na papierze, ale i za pomocą maszyny. Jak widzieliśmy juz w latach 50-tych posiadano dostateczne narzędzia i motywację by budować theorem proovers i dowodzić nimi realne twierdzenia ( np te z ‚Principia Mathematica” Russella i Whiteheada).

    W dalszej części wpisu chciałbym się skupić na Coq. Nie oznacza to bynajmniej że uważam go za najciekawszy czy najlepszy proover. Słynny i nadal chyba najdoskonalszy Mizar – dzieło Andrzej Trybulca ( posiada największą bibliotekę gotowych sformalizowanych teorii na świecie), prosty i ciekawy Mace4/Prover9 bardzo efektywnie wynajdujący kontrprzykłady dla podanych twierdzeń, Isabele, HOL, i wiele innych są przykładami bardzo ciekawych narzędzi. Coq wyróżnia się jednak „niewielkimi kosztami wejścia” i wydaje mi się, że stromą krzywą uczenia. W odróżnieniu np. od Mizara który potrafi sprawdzić dowód zapisany w syntetycznym, lecz bliskim naturalnemu, języku, czym przypomina prace z gołym kompilatorem, Coq oferuje pewną dozę interaktywności. Kiedy mamy do dowiedzenia twierdzenie, to po stosownej formalizacji – czyli po zdefiniowaniu stosownych pojęć i zapisaniu twierdzenia w odpowiednim języku Coq oferuje wybór taktyk dowodowych, przekształceń i reguł inferencji pozwalających na dowodzenie do pewnego stopnia wręcz na chybił-trafił. Oczywiście taka bezmyślna taktyka nadaje się do dowodzenia tylko bardzo prostych twierdzeń, z drugiej strony skoro czasami nie wiadomo od czego zacząć….

    Coq składa się z środowiska obliczeniowego Coq który jest narzędziem pracującym w linii komend i przypomina interaktywne środowiska programistyczne znane np. z pythona czy języków funkcyjnych, lub z tekstowych sesji matlaba. W tym trybie pracy możliwe jest zaczytanie wcześniej przygotowanego zestawu skryptów, ich „kompilacja” i uzyskanie odpowiedzi czy skrypty sa poprawne.
Praca w trybie tekstowym z pewnością jest bardzo użyteczną umiejętnością, zwłaszcza dla osób profesjonalnie użytkujących Coq, pozwala bowiem pracować z naprawdę sporymi teoriami o wielkiej liczbie twierdzeń itp. zapisanych w setkach plików. Dla osoby początkującej z pewnością znacznie ciekawszym sa środowiska interaktywne z interfejsem graficznym, wyposażone w menu z podpowiedziami i tym podobne ułatwienia. Środowiska takie nadają się także do prowadzenia dydaktyki – sądząc po sporej ilości kursów opartych na Coq jest to bynajmniej nie banalna część jego zastosowań.
     Wspomnę tu o trzech takich narzędziach – nadmieniając jedynie, że język programowania Coq nazywa się Gallina:

  • ProofWeb  którego autorem jest Cezary Kaliszyk i zespół programistów – działa świetnie i umożliwia zapoznanie się z systemem Coq bez potrzeby instalacji czegokolwiek – całość działa w przeglądarce – proszę sprawdzić! W szczególności polecam – jeśli ktoś chce sprawdzić przykłady które tu zostaną podane do posłużenia się tym środowiskiem. Warto wspomnieć że strona zawiera także kurs logiki oraz przygotowane skrypty z ćwiczeniami – warto spróbować! Uwaga – ProofWeb posiada własną bibliotekę regułek inferencji i taktyk dowodowych – ja zaś posługiwać się będę czystym Coq bez żadnych dodatków. Pomimo że poniżej używam kilku przykładów zaczerpniętych z materiałów ProofWeb, ich dowody sa poprowadzone inaczej – aby byly kompatybilne z „gołym Coq”. Te same przykłady mają swoje dowody w ProofWeb ( proszę poszukać;-) – jednak ich przeprowadzenie w Coq wymaga zaczytania biblioteki ProofWeb z której ja staram się tu nie korzystać.
  • ProofGeneral – to środowisko przygotowane do pracy z Emacsem. Osobiście używałem raz – nie lubię Emacsa. Jednak dla osób lubiących ten system operacyjny – środowisko to może okazać się bardzo produktywne, zwłaszcza, że nie jest ono ograniczone do wspierania jedynie Coq, i pozwala używać kilka rozmaitych systemów stosowanych w informatyce teoretycznej i matematyce jak Isabele, HOL, ACL2 itp.

    Coq wraz z CoqIde można ściągnąć za darmo ze strony http://coq.inria.fr/download . Coq jest systemem opensource, dystrybuowanym na podstawie licencji GNU Lesser General Public Licence Version 2.1 (LGPL). Coq został napisany głównie w Objective Caml. Prace nad jego stworzeniem rozpoczęto w roku 1984, autorami są Thierry Coquand and Gérard Huet którzy zaczęli prace, oraz Christine Paulin. Oczywiście lista autorów jest znacznie dłuższa. Coq powstał w instytucie INRIA we Francji.
     Instalacja pod Linuxem jest prosta i sprowadza się do użycia standardowych narzędzi dostępnych w dystrybucji, np. w wypadku Ubuntu wystarczy użyć: apt-get install coqide, dla Fedory: yum install coqide, i zgodzić się na pociągnięcie zależności. W wypadku Windows musimy ściągnąć stosowny instalator ze strony podanej powyżej i zainstalować program własnoręcznie. Dostępne są także wersję dla Mac OS oraz źródła programu.

    Pominiemy kwestię użycia interfejsu tekstowego, i przejdziemy do użycia CoqIde. Po uruchomieniu środowiska dostajemy okienko z trzema sekcjami:

1. okno w którym wprowadzamy komendy
2. okienko z komunikatami błędów i ostrzeżeniami
3. okienko w którym oglądamy wyniki naszych prac ( niejako standardowe wyjście programu).

    Jak na poniższym obrazku:

    Aby przejść od słów do czynów, wpiszmy pierwsze komendy w okienko komend (1). Proponuję aby poniższe sekwencje wpisać np. w ProfWeb który swoim wyglądem imituje CoqIde:

Na początek prosty przykład definicji typu wyliczeniowego ( czyli zbioru skończonego):

Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
     Po wpisaniu powyższego w pole (1) należy zatwierdzić to co się wprowadziło naciskając strzałkę w dół ( co spowoduje analizę wpisu i przejście do następnej komendy). Można także użyć wygodnej sekwencji ctrl-alt-down ( klawisz strzałki) – co niestety u mnie pod Ubuntu nie działa…
     Po zatwierdzeniu system zwraca nam komunikat który możemy odczytać w oknie (2) :

day is defined
dayrect is defined
dayind is defined
dayrec is defined

    Następnie definiujemy prostą funkcję pobierająca jako argument zmienną o type „day” i zwracającą wynik o tym samym typie:

Definition nextweekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.

     Po zatwierdzeniu system upewnia nas że „next_weekday is defined”
     Spróbujmy wyliczyć nasza funkcję dla kilku argumentów:

Eval simpl in (nextweekday friday).
Eval simpl in (nextweekday (nextweekday saturday)).

Co wyszło? Możemy teraz zapisać pierwsze twierdzenie dotyczące zdefiniowanej funkcji:

Example testnextweekday:
(nextweekday (nextweekday saturday)) = tuesday.

    Po zatwierdzeniu dostaniemy komunikat:

1 subgoal

============================
nextweekday (nextweekday saturday) = tuesday

    jak widać system nie przyjął równości na wiarę i oczekuje od nas uzupełnienia podanej zależności dowodem. Mamy konkluzję do dowiedzenia, i jest ono napisane pod kreską, nad kreska znajdują się zas dane przesłanki – w tym wypadku ich zbiór jest pusty. Jeśli teraz będziemy chcieli bawić się w dalsze definiowanie bez dostarczenia dowodu, system zaprotestuje pouczając nas że znajdujemy się w proof mode. Działania systemu zostały niejako wstrzymane do momentu w którym dowiedziemy naszej tezy. No to dowodzimy:

Proof. <- rozpoczynamy dowód. Nie trzeba tego robić, ale jak ładnie wygląda!
unfold nextweekday._ <- rozpiszmy definicję naszej funkcji. jak widać jawne wyliczenie prowadzi do oczywistej równości…
reflexivity. <- …którą uważamy za prawdziwą na mocy prawa zwrotności relacji równości
Qed. <- ;-) ładny koniec dowodu.

    Kilka słów komentarza. W powyższym „dowodzie” użyliśmy dwu tak zwanych taktyk dowodowych. Pierwsza nosi nazwę unfold, jej składnia to unfold nazwaobiektu_ i polega na wpisaniu w miejsce nazwy obiektu jego definicji. W naszym przypadku takie postępowanie pozwoliło od razu na wyliczenie wartości funkcji nextweekday z definicji. Wynikiem zastosowania tej taktyki była równość ( proszę sprawdzić!) w postaci tuesday = tuesday Wynik ten jest kolejnym twierdzeniem które musimy dowieść! Kolejnym krokiem było zastosowanie taktyki reflexivity czyli powołanie się na własność relacji równości. Ten sam dowód mógłby byc zapisany w nieco mniej wyrafinowany sposób: Proof. simpl. reflexivity. Qed. ( w jednej linii). Tym razem stosujemy taktykę simpl która sprowadza się do uproszenia wyrażeń przez wyliczanie tego co da się wyliczyć wprost.

    Taktyki o których tu mowa, to przykłady reguł inferencji, o jakich była mowa poprzednio, o mniej lub bardziej wymyślnych formach. Taktyki proste, jak te które sprowadzają się do rozpisania definicji funkcji są dosyć oczywiste, należy jednak wiedzieć, że Coq dostarcza taktyk w liczbie około 200 przy czym są wśród nich tak „proste” jak unfold czy simpl , skomplikowane jak induction realizująca indukcję matematyczną (postaram się o przykład w następnym wpisie), praktyczne jak taauto która umie dowieść skomplikowane tautologie logiczne, czy pochodna do niej intuition , są taktyki operujące po stronie przesłanek jak i taktyki operujące na konkluzjach. Można za ich pomocą eliminować implikacje, kwantyfikatory, dodawać dodatkowe założenia i budować lematy. Użytkownik może także samodzielnie budować własne taktyki, nazwać je i stosować kiedy mu to potrzebne. Spis gotowych taktyk wraz z opisem można znaleźć tu: http://coq.inria.fr/doc/tactic-index.html

    Podam teraz przykłady z klasycznego rachunku zdań:
Variables A B C D : Prop.

Theorem example01 : A /\ B -> B /\ A._
Proof. <- mamy dowieść implikacji A /\ B -> B /\ A.
intros. <- rozbijamy implikację na hipotezę H: A /\ B i konkluzję B /\ A.
destruct H. <- destruct to taktyka która sprawdza możliwe przypadki, w naszym przypadku hipoteza H zostaje rozbita na przesłanki H:A i H0:B. Obie przesłanki muszą być spełnione.
split. <-tym razem rozbijamy konkluzję na możliwe przypadki – w naszym wypadku mamy dowieść konkluzję 1. A i 2. B
assumption. <- konkluzja 1. wynika z założenia H.
assumption. <- konkluzja 2. wynika z założenia H0.
Qed. <- dowiedliśmy tezy.

(* komentarz w kodzie Coq tworzymy tak jak tu)
(Kontynuujmy wprowadzanie dalszych taktyk*)

Theorem example04 : A \/ B -> B \/ A._
Proof.
intros.
destruct H.
right.
assumption.
left.
assumption.
Qed.

    Po standardowym początku w którym pozbyliśmy sie implikacji, dokonaliśmy rozbicia na przypadki zostawiając tylko jeden ( z powodu obecności alternatywy). Tym razem pojawiły sie taktyki dotyczące alternatywy left i right które zostawiają z alternatywy odpowiednio lewy i prawy czynnik konkluzji. W każdym przypadku prawdziwość wynika z spostrzeżenia że konkluzja pojawia się w przesłankach.

    W następnym odcinku będą trochę bardziej złożone konstrukcje, a potem, na koniec postaram się uzupełnić wpisy o uwagi na temat Dependent Type Theory i Izomorfizmu Curryego-Howarda.