W poprzednim odcinku:
„Po zatwierdzeniu dostaniemy komunikat: next_weekday (next_weekday saturday) = tuesday … Łał, jak oni to zrobili!? … Qed.<- ;-) ładny koniec dowodu.

    W tym odcinku nastąpi obiecany przykład nieco bardzie skomplikowanego dowodu. Obawiam się żę wpis ten będzie najbardziej bałaganiarski ze wszystkich, i najtrudniejszy w odbiorze, a to z powodu sporej ilości komentarzy/kodu. Na spodzie wpisu znajdziecie kod omawiany w tekście bez zbędnych dodatków – można kopiować i wkleić. W zasadzie chyba samo czytanie nie ma sensu – proszę samemu pobawic się Coq.
    Zanim pokażemy coś większego, pobawimy się w kilka definicji i powiemy coś o definiowaniu własnych modułów. Aby definiować własne obiekty, celowe może być odcięcie się od „biblioteki” Coq by nie powodować konfliktów nazw czy definicji. W tym celu użyjemy komendy:

Module PierwszeKotyZaPloty.

    Od tego momentu wszystkie poniższe komendy aż do sekwencji End PierwszeKotyZaPloty. maja ograniczony zasięg leksykalny i nie powodują konfliktów z podobnymi typami zdefiniowanymi w domyślnej bibliotece Coq. Dalsze działania rozpoczniemy od zdefiniowania liczb naturalnych posługując się pomysłem z teorii Peano:

Inductive nat: Set :=
| O:nat
| S:nat->nat.

    Proszę zauważyć, że nie musieliśmy w żaden szczególny sposób określać funkcji S ( a jest to funkcja ma bowiem typ nat->nat). Funkcja ta pełni oczywiście rolę następnika.

    Kolejną definicją będzie funkcja poprzednika:

Definition pred (n:nat): nat :=
match n with
| O => O
|S m => m
end.

    Działa to tak: funkcja pred wymaga jednego argumentu w postaci liczby naturalnej. Jeśli argument ten to „O” wówczas funkcja zwraca „O” jako swoją wartość. Jeśli jednak argument jest różny od „O” to musi on być postaci „S m”, a wówczas opuszczamy „S” i mamy poprzednik liczby „S m” czyli zwracamy „m”. Co by się stało gdybyśmy popełnili błąd i zamiast „S m” twierdzili że możliwe argumenty mają inną postać?

Definition pred (n:nat): nat :=
match n with
| O => O
| S ( S m) => m
end.

    Proszę sprawdzić!
    Sprawdźmy teraz jak zdefiniowane funkcje działają w praktyce. Sprawdźmy jak Coq zrozumiał definicję funkcji S.

Check S (S ( S O)).
    daje w wyniku: S(S(S(O)) : nat

    Jak widać system rozpoznaje że obiekt S (S ( S O)) jest typu nat.

Eval simpl in ( pred ( S (S ( S O)))).

    Widzimy, że funkcja pred rzeczywiście wylicza n-1…

End PierwszeKotyZaPloty.

    W tym miejscu możemy zamknąć nasz moduł, który utworzyliśmy w celach dydaktycznych i zaczytać do środowiska bibliotekę Arith w której, w identyczny jak powyżej sposób, zdefiniowane sa liczby naturalne. Wykonujemy to komendą:

Require Import Arith.

    Sprawdźmy co da nam komenda analogiczna do wykonanej wcześniej:

Check S (S ( S O)).

    wynik to: 3:nat .

    Twórcy Coq wprowadzili „ułatwienie” w operowaniu liczbami w postaci ich standardowej graficznej reprezentacji. Jednak posługując sie biblioteką Arith w istocie operujemy na typach zdefiniowanych za pomocą wcześniejszych definicji. Aby się o tym przekonać poprośmy Coq o wypisanie definicji funkcji S (Coq wypisze co o niej wie):

Print S.
    Wynik to: Inductive nat: Set :=O: nat | S: nat->nat For S: Argument scope is [nat scope].

Print PierwszeKotyZaPloty.S.
    Wynik to: Inductive PierwszeKotyZaPloty.nat: Set :=O: PierwszeKotyZaPloty.nat | S: PierwszeKotyZaPloty.nat->PierwszeKotyZaPloty.nat

    Jak widać elementy zbioru który zdefiniowaliśmy sa innego typu niż elementy ze standardowej biblioteki co pozwala operować na nich jednocześnie bez popadania w konflikt. Jeszcze raz podkreślę, że powyższe definicje, poza „przestrzenią leksykalną” niczym się nie różnią, zaś w plikach definiujących bibliotekę Arith można znaleźć definicję zbioru nat wyglądająca dokładnie jak nasza definicja w module PierwszeKotyZaPloty.

    Skoro mamy zdefiniowane liczby naturalne, możemy budować na ich funkcje. Spróbujmy zatem zdefiniować sumę pierwszych n liczb naturalnych. Definicja będzie rekurencyjna:

Fixpoint sum_n(n:nat):nat :=
match n with
|O=> O
|S m => S m + sum_n m
end.

    Sprawdźmy czy to działa.

Eval simpl in sum_n 5.
    Wynik to: 15:nat. Wygląda dobrze.

    W dalszej kolejności będziemy dowodzić Twierdzenia w postaci: Theorem Gauss_suma: forall n:nat, 2*sum_n n = n* (n+1). czyli wzoru na sumę n początkowych liczb naturalnych, której wyliczenie przypisuje się młodemu Gaussowi podczas zajęć szkolnych. Zanim jednak tego dokonamy zdefiniujemy kilka lematów. Tak naprawdę lematy powstały podczas nieudanych prób dowodu podczas interakcji z systemem. Usiłowałem wymyślać dowód operując różnymi taktykami i definiowałem własności których mi brakło dla zakończenia dowodu. Oczywiście w wersji finalnej wstawimy Lematy tak, że znajdą się elegancko przed samym twierdzeniem i jego dowodem co skutecznie ukryje ich pochodzenie ;-). W komentowanym kodzie zdecydowałem się jednak jeden z nich zostawić w środku dowodu aby pokazać że może on tam się znajdować.
    Dodatkowa uwaga zanim zaczniemy jest taka: aby zrozumieć co się dzieje należy odpalić CoqIde lub ProofWeb. Treść skryptu poniżej nie zawiera bardzo ważnej informacji – wyniku operacji jakie podaje Coq – czyli stanu systemu. Bez tej informacji zrozumienie tego o co chodzi może być bardzo trudne.
    Zacznijmy od prostego lematu dotyczącego własności następnika:

Lemma nastepnik: forall n:nat, S n = n+1.

    Przykład ten jest interesujący bowiem posłużymy się w celu dowodu taktyką induction względem liczby n.

Lemma nastepnik: forall n:nat, S n = n+1.
Proof.
induction n.

    Tutaj komentarz: w wyniku użycia taktyki induction n dostajemy rozbicie tezy na dwa cele do dowiedzenia. Oto wynik jaki wypisuje Coq:

2 subgoals
============================
1 = 0 + 1

subgoal 2 is:
S (S n) = S n + 1

    Wszystko to jest możliwe dzięki indukcyjnej definicji zbioru obiektów nat. Wiadomo jakie są możliwe przypadki ( z definicji typu nat wiemy że albo O albo S n). W istocie w sensie praktycznym taktyka induction dokonuje analizy możliwych przypadków w oparciu o definicję obiektów którymi operujemy ( i przypomina tym samym taktykę destruct, która wcale indukcją nie jest!). Jednak oczywiście sama zasada indukcji nie jest tak prosta. Aby sprawdzić jak wygląda zasada indukcji zapisana w Coq do liczb naturalnych sprawdźmy jak jest zdefiniowany schemat ind_nat. Możemy to zrobić nie przerywając dowodu ( po prostu sprawdzamy definicje przez co nie ingerujemy w treść dowodu twierdzenia):

Check nat_ind.

    Otrzymamy jako wynik:

nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

    Jak widać jest to schemat indukcji zapisany dla liczb naturalnych zdefiniowanych za pomocą elementu „O” i operacji następnika „S” co nie powinno dziwić. Warto nadmienić, że taktyka induction to mniej więcej to samo, w odróżnieniu jednak od nat_ind nie ma ona zapewne tak prostej definicji. Opieram się tu na przypuszczeniach które należałoby sprawdzić czytając kod Coq i na komentarzach z manuala Coq. Wydaje się że można rzecz wyjaśnić tak: taktyka induction jest taktyką ogólna, działająca dla dowolnych typów, zbiorów i definicji predykatów ( na przykład także dla typu bool, gdzie mamy tylko 2 możliwe przypadki). W pewnym sensie w porównaniu z nat_ind jest to raczej metataktyka która bierze pod uwagę definicje obiektów na których działa – i która w wypadku liczb naturalnych jak wyżej redukuje sie do nat_ind. Ważną wiadomością tutaj jest, ze definiując własne typy danych ( powiedzmy drzewa, listy, bagi – czyli zbiory zbiorów itp. struktury rekurencyjne) możemy dla nich zdefiniować własne taktyki indukcji – i w ten sposób rozszerzyć możliwości Coq. Są to jednak rozważania przekraczające moją wiedzę. Aby nie być całkowicie gołosłownym poniżej pokażę jednak przykład własnoręcznie zdefiniowanej prostej taktyki – do własnej indukcji stąd daleko ale …

    Wracając do naszego dowodu zapiszmy jeszcze raz całość bez zbędnych komentarzy:

Lemma nastepnik: forall n:nat, S n = n+1.
Proof.
induction n.
trivial.
(*simpl;reflexivity.*)
simpl.
rewrite IHn.
reflexivity.
Qed.

    Po taktyce induction n nastąpiła taktyka trivial która w tym przypadku oznacza to samo co wykomentowany ciąg simpl;reflexivity. Taktyka trivial dowodzi tych twierdzeń które sprowadzają się do wyliczenia wartości i sprawdzenia równości. W tym kroku dowiedliśmy prawdziwości twierdzenia dla wartości początkowej „O”. Następnie przeszliśmy do kolejnego zadania – wykonania kroku indukcyjnego od n do n+1. Po uproszczeniu simpl otrzymujemy do dowiedzenia równanie postaci S (S n) = S (n + 1) przy założeniu że IHn : S n = n + 1. IHn oznacza tu hipotezę indukcyjną po n. Jeśli w konkluzji skorzystać z tej hipotezy – dostaniemy to co nas interesuje – dokonujemy tego przez użycie taktyki rewrite IHn. – przepisujemy tezę używając przesłanki. I mamy koniec dowodu.

    Zdefiniujmy następny lemat dotyczący rozdzielności mnożenia względem dodawania:

Lemma mult_distributive: forall n m l:nat, n*(m+l)= n*m +n*l.
Proof. intros. ring. Qed.

    Tym razem (leniwie) użyliśmy taktyki ring odwołującej się do własności pierścienia liczb naturalnych – taktyka ta może być użyta z dowolnymi obiektami o strukturze pierścienia.

    Teraz gotowi do dowiedzenia naszego twierdzenia. Poniższy dowód nie jest ani ładny, ani najprostszy, ani szczególnie pomysłowy – jest barokowy. Moim celem było użycie tak wielu elementów języka jak tylko się uda, przy czym zawsze przedkładałem jawne wyliczanie tego i owego nad użycie samograjów w rodzaju ring – które jeśli je tu zastosować w odpowiednim miejscu – proszę spróbować – przyspiesza dowód. Poniżej komentarze do linii oznaczonych numerami:

Theorem Gauss_suma: forall n:nat, 2*sum_n n = n* (n+1).
Proof.
induction n.
simpl;trivial.
Ltac UFx x:= unfold x;fold x. (* 0*)
UFx sum_n. (*1*)
(*unfold sum_n. *)
(*fold sum_n.*)

Lemma mult_distributive’: forall n m l:nat, (m+l)*n= m*n +l*n. (* 2 *)
Proof. (*początek dowodu lematu*)
intros.
ring.
Qed. (*koniec dowodu lematu*)

rewrite mult_distributive.
rewrite IHn.
rewrite <-nastepnik. (*3*)
rewrite <-mult_distributive’.
(*rewrite nastepnik.*)
SearchRewrite( _ * _ ). (* 4*)
rewrite plus_comm.(*5*)
rewrite mult_comm.(*6*)
rewrite nastepnik.
(*ring*) (*7*)
rewrite mult_plus_distr_r.(*8*)
rewrite mult_plus_distr_l.(*9*)
simpl.
ring.
Qed.

    Teraz komentarze dotyczące dowodu.
(*0*) (*1*) – chyba najciekawsza część dywagacji – definicja własnej taktyki poleceniem Ltac. Taktyka UFx pobiera argument x i wykonuje kolejno unfold x po czym fold x. Jak widać Coq dysponuje „podjęzykiem” definicji taktyk, podany przykład jest w pewnym sensie banalny bo sprowadza się do bezpośredniego wykonania dwu innych taktyk jedna po drugiej, przykłady które można znaleźć w rozmaitych materiałach o Coq służą do automatyzacji dowodów i w istocie są dosyć skomplikowanymi „podprogramami” analizującymi możliwe przypadki i wyniki zastosowanych taktyk, dopasowujące wzorce itp. Polecam materiały pana Adama Chlipala wymienione poniżej jeśli kogoś to interesuje.
(*2*) – w trakcie dowodu wprowadzamy lemat. Coq nie zakłada a priori przemienności działań więc dowodzimy sobie potrzebnej tożsamości.
(*3*) – dokonujemy przepisania tezy za pomocą lematu następnik dowiedzionego wcześniej., Tym razem jednak przepisujemy równość tam występująca od prawej do lewej co sygnalizuje znak <- ( można także użyć -> i przepisać od lewej do prawej co jest zresztą domyślnym trybem stosowania równości).
(*4*) (5*) (*6*) – tak naprawdę to dowodzenie lematu dla zamienionej kolejności wyrażeń w możeniu nie było konieczne. W bibliotece Coq znajdują się stosowne twierdzenia dotyczące przemienności dodawania i mnożenia. SearchRewrite( wzorzec ) pozwala na znalezienie wszystkich zdefiniowanych twierdzeń które odpowiadają wzorcowi _ * _ gdzie podkreślenie oznacza dowolne wyrażenie. Znalezione w ten sposób lematy/twierdzenia wykorzystujemy w dowodzie.
(*7*) (*8*) (*9*) – poprzedni krok przekształcił całe rozumowanie w działanie z zakresu algebry które można rozwiązać po prostu wyliczając wartości po obydwu stronach równości za pomocą taktyki ring. Ja jednak proponuję użyć – głównie po to by podać ich nazwy – lematów dotyczących rozdzielności mnożenia względem dodawania lewostronnie i prawostronnie.

    Na zakończenie podam kilka poleceń które wypisują definicje obiektów z których korzystaliśmy:

Print nat.
Print mult_distributive.
Print Gauss_suma.

    Pierwsza definicja pokazuje sposób a jaki skonstruowaliśmy zbiór nat. Druga pokazuje konstrukcję lematu mult_dystributive, trzecia twierdzenia Gauss_suma. Dwa ostatnie obiekty to nazwy twierdzeń/lematów. W wypadku twierdzenia Gauss_suma zwracany przez Coq wynik, to dosyć koszmarna i bardzo nieczytelna funkcja która jako argument pobiera liczbę naturalną ( Gauss_suma = fun n:nat=> … ) a zwraca dowód twierdzenia które wypisaliśmy powyżej. Nie posiadam szczególnie głębokiej wiedzy na ten temat, jednak z jednej strony podana funkcja realizuje jawnie zależność opisaną tutaj, jako interpretację BHK dla dowodu twierdzenia z kwantyfikatorem ogólnym, a zarazem jest praktyczną realizacją izomorfizmu Curryego-Howarda jak opisano tu. Jeśli znajdę czas na pisanie kolejnego 4-tego odcinka tego cyklu – bedzie on poświęcony właśnie tym zagadnieniom.

    Dla zainteresowanych którzy zdadzą pytanie: czy to wszystko ma jakieś znaczenie praktyczne, dodaję na koniec przykład którego nie rozumiem, i nie umiem skomentować bo moja motywacja jest raczej matematyczna i teoretyczna. Tu jednak coś dla praktyków. Coq potrafi generować kod źródłowy programów w Ocamlu, Haskell lub Scheme. Oto przykład który znalazłem gdzieś na grupach dyskusyjnych ( nie jest kompletny, nie udało mi się go wykonać w całości z powodu niezgodności bibliotek, wyraźnie jednak widać że „coś” zwraca ;-)

Fixpoint fact_body (a n : nat) : nat :=
match n with
| 0 => a
| S m => fact_body (a*n) m
end.

Definition fact : nat -> nat := fact_body 1.
Extraction Language Scheme. (*lub Ocaml, lub Haskell*)
Extract Inlined Constant plus => „(+)”.
Extract Inlined Constant mult => „(*)”.
Extraction fact_body.
Extraction fact.

    Zgodnie z opisami jakie znalazłem tu i tam, taka generacja kodu ma służyć wytwarzaniu certyfikowanych programów komputerowych w realnych językach programowania.
——————————-

    Podczas przygotowywania tych wpisów korzystałem z wielu źródeł które wymienię tu w przypadkowej kolejności. Wszystkie kody uruchamiałem za pomocą CoqIde, niektóre sprawdzałem w ProofWeb.

  • Podstawowym źródłem informacji jest oczywiście strona domowa projektu Coq: http://coq.inria.fr na która powoływałem się na początku. W sekcjach zawierających dokumentację można znaleźć zarówno formalną specyfikację języka Gallina jak i manual do samego narzędzia. W szczególności znajduje tam indeks taktyk.
  • Podstawowe źródło wiedzy o Coq jakie użyłem podczas tej prezentacji to: „Software Foundations” Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, Brent Yorgey, with Andrew W. Appel, Arthur Chargueraud, Anthony Cowley, Jeffrey Foster, Michael Hicks, Ranjit Jhala, Greg Morrisett, Chung-chieh Shan, Leonid Spesivtsev, and Andrew Tolmach. http://www.cis.upenn.edu/~bcpierce/sf/ Polecam wszystkim zainteresowanym zwłaszcza zagadnieniami dowodzenia poprawności programów. Jest to kompletne źródło z którego można się nauczyć używać Coq, podobno także w praktyce programistycznej.
  • Kilka przykładów zaczerpnąłem ze strony kursu „Interactive Computer Theorem Proving „ Adam Chlipala http://adam.chlipala.net/itp/ Kolejne samodzielne źródło informacji na temat systemu Coq. Bardzo dobre.

    Różne pomysły i koncepcje, słowem trivia lub przypadki szczególne ( ale kształcące):

——————————-

    I to już wszystko moi drodzy. W zasadzie wyczerpałem swoją wiedzę ;-) w omawianym temacie. W planach miał być jeszcze jakiś bardziej skomplikowany dowód ale pisanie kodu w Buzz jest niezbyt przyjemne. Najbardziej skomplikowaną rzeczą z jaką w Coq spotkałem próbując ją zrozumieć choć trochę były prace Vladimira Voyevodskyego na temat Univalent Fundations of Mathematics ( tu mozna oglądnąć video z wykładu Vladimira – bardzo ładne ale trudne ). Musze przyznać że zgadzam się z jego opinią – używanie proof czeckerów w matematyce jest nieuniknione. Zaufanie jakie możemy pokładać w systemach takich jak Coq jest wcale nie mniejsze niż to kŧóre pokładamy w grupie recenzentów z czasopism. Voyevodsky w którymś ze swoich wykładów wspomniał że ma prace która leży nieopublikowana od 2 lat – recenzenci sprawdzają… Z drugiej strony on sam jako recenzent – tez niektóre artykuły sprawdza już całkiem długo. Kolejnym zagadnieniem jest zabawa amatora. Każda osoba która zada sobie trud zrozumienia podstaw Coq i zechce sformalizować swoje pomysły uzyskuje dostęp do „niezmordowanego krytyka” który potrafi sprawdzić poprawność twierdzeń dowodów a nawet pomóc w znalezieniu dowodu. Oczywiście tym co zniechęca jest ilość pracy jakiej to wymaga. Z jednej strony język Coq jest bardzo ekspresywny i można w nim wyrazić bardzo wiele stosunkowo niewielkim nakładem pracy. Z drugiej strony będąc świadomym jak wygląda nawet prosty ale nietrywialny dowód typowego twierdzenia ( np. usiłując sobie wyobrazić jak mogłaby przebiegać formalizacja dowodu który przedstawił tutaj +Artur Popławski) widać, że to jest praca na wiele wiele wieczorów… Na zakończenie odrobina statystyki: w pracy http://r6.ca/Goedel/goedel1.html o tytule „Essential Incompleteness of Arithmetic Verified by Coq” dokonano formalizacji dowodu znanego tw. Goedla. Na końcu autor zawarł sekcję o podtytule „statistics” która pozwolę sobie tu zacytować:

    „My proof, excluding standard libraries and the library for Pocklington’s criterion, consists of 46 source files, 7 036 lines of specifications, 37 906 lines of proof, and 1 267 747 total characters. The size of the gzipped tarball (gzip -9) of all the source files is 146 008 bytes, which is an estimate of the information content of my proof. „

    Życzę powodzenia – a jeśli komuś się spodobało – i będzie używał – proszę o dzielenie się wynikami.

———–Cały Kod————–
Require Import Arith.
Check S (S ( S O)).
Print S.

Check pred ( S (S ( S O))).
Eval simpl in S(S(S(S O))).

Fixpoint sum_n(n:nat):nat :=
match n with
|O=> O
|S m => S m + sum_n m
end.

Eval simpl in sum_n 5.

Lemma nastepnik: forall n:nat, S n = n+1.
Proof.
induction n.
(*simpl;reflexivity.*)
trivial.
simpl.
rewrite IHn.
reflexivity.
Qed.

Lemma mult_distributive: forall n m l:nat, n*(m+l)= n*m +n*l.
Proof.
intros.
ring.
Qed.
Lemma mult_distributive’: forall n m l:nat, (m+l)*n= m*n +l*n.
Proof.
intros.
ring.
Qed.

Lemma nastepnik’: forall n:nat, S n = 1+n.
intros.
induction n. trivial. simpl. rewrite IHn. trivial. Qed.

Ltac UFx x:= unfold x;fold x.

Theorem Gauss_suma: forall n:nat, 2*sum_n n = n* (n+1).
Proof.
induction n.
simpl;trivial.
(*Ltac UFx x:= unfold x;fold x.*)
UFx sum_n.
(*unfold sum_n.*)
(*fold sum_n.*)
rewrite mult_distributive.
rewrite IHn.
rewrite <-nastepnik.
rewrite <-mult_distributive’.
(*rewrite nastepnik.*)
SearchRewrite(_*_).
rewrite plus_comm.
rewrite mult_comm.
rewrite nastepnik.
(*ring.*)
(*SearchRewrite(_*_).*)
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
simpl.
symmetry.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
simpl.
ring.
Qed.
Check nat_ind.

Print nat.
Print mult_distributive.
Print Gauss_suma.

Fixpoint fact_body (a n : nat) : nat :=
match n with
| 0 => a
| S m => fact_body (a*n) m
end.
Definition fact : nat -> nat := fact_body 1.
Extraction Language Haskell.
Extract Inlined Constant plus => „(+)”.
Extract Inlined Constant mult => „(*)”.
Extraction fact_body.
Extraction fact.
———–Koniec Cały Kod————–