UWAGA: ten rozdział właśnie ulega konceptualnemu przeobrażeinu i może być nie na miejscu, tzn. zawierać rzeczy, o których jeszcze nie było mowy.

Logika boolowska

Zadania z funkcji boolowskich, sprawdzające radzenie sobie w pracy z enumeracjami, definiowaniem funkcji przez dopasowanie do wzorca i dowodzeniem przez rozbicie na przypadki. Chciałem, żeby nazwy twierdzeń odpowiadały tym z biblioteki standardowej, ale na razie nie mam siły tego ujednolicić.

Definicje

Zdefiniuj następujące funkcje boolowskie:

• negb (negacja)
• andb (koniunkcja)
• orb (alternatywa)
• implb (implikacja)
• eqb (równoważność)
• xorb (alternatywa wykluczająca)
• nor
• nand

Twierdzenia

Udowodnij, że zdefiniowane przez ciebie funkcje mają spodziewane właściwości.

Właściwości negacji

Eliminacja

Elementy neutralne

Anihilacja

Łączność

Przemienność

Rozdzielność

Wyłączony środek i niesprzeczność

Prawa de Morgana

eqb, xorb, norb, nandb

Różne

Rekordy (TODO)

W wielu językach programowania występują typy rekordów (ang. record types). Charakteryzują się one tym, że mają z góry określoną ilość pól o potencjalnie różnych typach. W językach imperatywnych rekordy wyewoluowały zaś w obiekty, które różnią się od rekordów tym, że mogą zawierać również funkcje, których dziedziną jest obiekt, w którym funkcja się znajduje. W Coqu mamy do dyspozycji rekordy, ale nie obiekty. Trzeba tu po raz kolejny pochwalić siłę systemu typów Coqa — o ile w większości języków rekordy są osobnym konstruktem językowym, o tyle w Coqu mogą być one z łatwością reprezentowane przez typy induktywne z jednym konstruktorem (wraz z odpowiednimi projekcjami, które dekonstruują rekord).

Z typem induktywnym o jednym konstruktorze już się zetknęliśmy, próbując zdefiniować liczby wymierne. Powyższa definicja używająca rekordu ma drobną przewagę nad poprzednią, w której słowo kluczowe Inductive pada explicité:

• wygląda ładniej
• ma projekcje

Dzięki projekcjom mamy dostęp do poszczególnych pól rekordu bez konieczności jego dekonstruowania — nie musimy używać konstruktu match ani taktyki destruct, jeżeli nie chcemy. Często bywa to bardzo wygodne. Projekcję sign możemy interpretować jako funkcję, która bierze liczbę wymierną r i zwraca jej znak, zaś projekcja denominator_not_zero mówi nam, że mianownik żadnej liczb wymiernej nie jest zerem. Pozwa tymi wizualno-praktycznymi drobnostkami, obie definicje są równoważne (w szczególności, powyższa definicja, podobnie jak poprzednia, nie jest dobrą reprezentacją liczb wymiernych).

Ćwiczenie (kalendarz)

Zdefiniuj typ induktywny reprezentujący datę i napisz ręcznie wszystkie projekcje. Następnie zdefiniuj rekord reprezentujący datę i zachwyć się tym, ile czasu i głupiego pisania zaoszczędziłbyś, gdybyś od razu użył rekordu...

Klasy (TODO)

Mechanizmem ułatwiającym życie jeszcze bardziej niż rekordy są klasy. Niech nie zmyli cię ta nazwa — nie mają one nic wspólnego z klasami znanymi z języków imperatywnych. Bliżej im raczej do interfejsów, od których są zresztą dużo silniejsze. W językach imperatywnych interfejs możemy zaimplementować zazwyczaj definiując nowy typ. W Coqu możemy uczynić typ instancją klasy w dowolnym miejscu — nawet jeżeli to nie my go zdefiniowaliśmy. Co więcej, instancjami klas mogą być nie tylko typy, ale dowolne termy. Klasy są w Coqu pełnoprawnym tworem — mogą mieć argumenty, zawierać inne klasy, być przekazywane jako argumenty do funkcji etc. Używa się ich zazwyczaj dwojako:

• zamiast rekordów (zwiększa to nieco czytelność)
• jako interfejsy

Nie będziemy po raz trzeci powtarzać (kulawej) definicji liczb wymiernych — użycie do tego klas zamiast rekordów sprowadza się do zamienienia słowa kluczowego Record na Class w poprzedniej definicji. Przyjrzyjmmy się za to wykorzystaniu klasy w roli interfejsu. Argument A : Type po nazwie klasy mówi nam, że nasz interfejs będą mogły implementować typy. Dalej zapis : Type mówi nam, że nasza klasa jest typem — klasy, jako ulepszone rekordy, są typami induktywnymi z jednym konstruktorem. Nasza klasa ma dwa pola, które będzie musiał podać użytkownik chcący uczynić swój typ jej instancją: funkcję eq_dec oraz jej specyfikację, która mówi nam, że eq_dec zwraca true wtedy i tylko wtedy, gdy jej argumenty są równe. Wobec tego typy będące instancjami EqDec można interpretować jako typy, dla których równość elementów można sprawdzić za pomocą jakiegoś algorytmu. Nie wszystkie typy posiadają tę własność — problematyczne są szczególnie te, których elementy są w jakiś sposób "nieskończone".

Instancje klas definiujemy przy pomocy słowa kluczowego #[refine] Instance. Jeżeli używamy klasy jako interfejsu, który implementować mogą typy, to zazwyczaj będziemy potrzebować tylko jednej instancji, więc jej nazwa będzie niemal identyczna jak jej typ (dzięki temu łatwo będzie ją zapamiętać). Po symbolu := w nawiasach klamrowych definiujemy pola, które nie są dowodami. Całość, jako komenda, musi kończyć się kropką. Gdy klasa nie zawiera żadnych pól będących dowodami, definicja jest zakończona. W przeciwnym przypadku Coq przechodzi w tryb dowodzenia, w którym każdemu polu będącemu dowodem odpowiada jeden podcel. Po rozwiązaniu wszystkich podcelów instancja jest zdefiniowana. W naszym przypadku klasa ma dwa pola — funkcję i dowód na to, że funkcja spełnia specyfikację — więc w nawiasach klamrowych musimy podać jedynie funkcję. Zauważmy, że nie musimy koniecznie definiować jej właśnie w tym miejscu — możemy zrobić to wcześniej, np. za pomocą komendy Definition albo Fixpoint, a tutaj odnieść się do niej używając jej nazwy. W przypadku bardziej skomplikowanych definicji jest to nawet lepsze wyjście, gdyż zyskujemy dzięki niemu kontrolę nad tym, w którym miejscu rozwinąć definicję, dzięki czemu kontekst i cel stają się czytelniejsze. Ponieważ nasza klasa ma pole, które jest dowodem, Coq przechodzi w tryb dowodzenia. Dowód, mimo iż wymaga rozpatrzenia ośmiu przypadków, mieści się w jednej linijce — widać tutaj moc automatyzacji. Prześledźmy, co się w nim dzieje. Najpierw rozbijamy wartości boolowskie x i y. Nie musimy wcześniej wprowadzać ich do kontekstu taktyką intros, gdyż destruct sam potrafi to zrobić. W wyniku tego dostajemy cztere podcele. W każdym z nich taktyką split rozbijamy równoważność na dwie implikacje. Sześć z nich ma postać P -> P, więc radzi sobie z nimi taktyka trivial. Dwie pozostałe mają przesłanki postaci false = true albo true = false, które są sprzeczne na mocy omówionych wcześniej właściwości konstruktorów. Taktyką inversion 1 wskazujemy, że pierwsza przesłanka implikacji zawiera taką właśnie sprzeczną równość termów zrobionych różnymi konstruktorami, a Coq załatwia za nas resztę. Jeżeli masz problem z odczytaniem tego dowodu, koniecznie przeczytaj ponownie fragment rozdziału pierwszego dotyczący kombinatorów taktyk. Jeżeli nie potrafisz wyobrazić sobie podcelów generowanych przez kolejne taktyki, zastąp chwilowo średniki kropkami, a jeżeli to nie pomaga, udowodnij całe twierdzenie bez automatyzacji. Dzięki takim ćwiczeniom prędzej czy później oswoisz się z tym sposobem dowodzenia, choć nie jest to sztuka prosta — czytanie cudzych dowodów jest równie trudne jak czytanie cudzych programów. Prawie nigdy zresztą nowopowstałe dowody nie są od razu zautomatyzowane aż w takim stopniu — najpierw są przeprowadzone w części lub w całości ręcznie. Automatyzacja jest wynikiem dostrzeżenia w dowodzie pewnych powtarzających się wzorców. Proces ten przypomina trochę refaktoryzację kodu — gdy dostrzeżemy powtarzające się fragmenty kodu, przenosimy je do osobnych procedur. Analogicznie, gdy dostrzegamy powtarzające się fragmenty dowodu, łączymy je kombinatorami taktyk lub piszemy własne, zupełnie nowe taktyki (temat pisania własnych taktyk poruszę prędzej czy później). Od teraz będę zakładał, że nie masz problemów ze zrozumieniem takich dowodów i kolejne przykładowe dowody będę pisał w bardziej zwratej formie. Zauważ, że definicję instancji kończymy komendą Defined, a nie Qed, jak to było w przypadku dowodów twierdzeń. Wynika to z faktu, że Coq inaczej traktuje specyfikacje i programy, a inaczej zdania i dowody. W przypadku dowodu liczy się sam fakt jego istnienia, a nie jego treść, więc komenda Qed każe Coqowi zapamiętać jedynie, że twierdzenie udowodniono, a zapomnieć, jak dokładnie wyglądał proofterm. W przypadku programów takie zachowanie jest niedopuszczalne, więc Defined każe Coqowi zapamiętać term ze wszystkimi szczegółami. Jeżeli nie wiesz, której z tych dwóch komend użyć, użyj Defined.

Ćwiczenie (EqDec)

Zdefiniuj instancje klasy EqDec dla typów unit oraz nat.

Ćwiczenie (równość funkcji)

Czy możliwe jest zdefiniowanie instancji klasy EqDec dla typu:

• bool -> bool
• bool -> nat
• nat -> bool
• nat -> nat
• Prop

Jeżeli tak, udowodnij w Coqu. Jeżeli nie, zaargumentuj słownie.

Instancje klas mogą przyjmować argumenty, w tym również instancje innych klas albo inne instancje tej samej klasy. Dzięki temu możemy wyrazić ideę interfejsów warunkowych. W naszym przypadku typ option A może być instancją klasy EqDec jedynie pod warunkiem, że jego argument również jest instancją tej klasy. Jest to konieczne, gdyż porównywanie termów typu option A sprowadza się do porównywania termów typu A. Zauważ, że kod eq_dec a a' nie odwołuje się do definiowanej właśnie funkcji eq_dec dla typu option A — odnosi się do funkcji eq_dec, której dostarcza nam instancja _ : EqDec A. Jak widać, nie musimy nawet nadawać jej nazwy — Coqa interesuje tylko jej obecność. Na podstawie typów termów a i a', które są Coqowi znane, potrafi on wywnioskować, że eq_dec a a' nie jest wywołaniem rekurencyjnym, lecz odnosi się do instancji innej niż obecnie definiowana. Coq może ją znaleźć i odnosić się do niej, mimo że my nie możemy (gdybyśmy chcieli odnosić się do tej instancji, musielibyśmy zmienić nazwę z _ na coś innego).

Ćwiczenie (równość list)

Zdefiniuj instancję klasy EqDec dla typu list A.

Ćwiczenie (równość funkcji 2)

Niech A i B będą dowolnymi typami. Zastanów się, kiedy możliwe jest zdefiniowanie instancji klasy EqDec dla A -> B.

Rozstrzygalność

Próba udowodnienia tego twierdzenia pokazuje nam zasadniczą różnicę między logiką konstruktywną, która jest domyślną logiką Coqa, oraz logiką klasyczną, najpowszechniej znanym i używanym rodzajem logiki. Każde zdanie jest, w pewnym "filozoficznym" sensie, prawdziwe lub fałszywe i to właśnie powyższe zdanie oznacza w logice klasycznej. Logika konstruktywna jednak, jak już wiemy, nie jest logiką prawdy, lecz logiką udowadnialności i ma swoją interpretację obliczeniową. Powyższe zdanie w logice konstruktywnej oznacza: program komputerowy exluded_middle rozstrzyga, czy dowolne zdanie jest prawdziwe, czy fałszywe. Skonstruowanie programu o takim typie jest w ogólności niemożliwe, gdyż dysponujemy zbyt małą ilością informacji: nie wiemy czym jest zdanie P, a nie posiadamy żadnego ogólnego sposobu dowodzenia lub obalania zdań o nieznanej nam postaci. Nie możemy np. użyć indukcji, gdyż nie wiemy, czy zdanie P zostało zdefiniowane induktywnie, czy też nie. W Coqu jedynym sposobem uzyskania termu o typie forall P : Prop, P \/ ~ P jest przyjęcie go jako aksjomat.

Powyższe dywagacje nie przeszkadzają nam jednak w udowadnianiu, że reguła wyłączonego środka zachodzi dla pewnych konkretnych zdań. Zdanie takie będziemy nazywać zdaniami rozstrzygalnymi (ang. decidable). O pozostałych zdaniach będziemy mówić, że są nierozstrzygalne (ang. undecidable). Ponieważ w Coqu wszystkie funkcje są rekurencyjne, a dowody to programy, to możemy powyższą definicję rozumieć tak: zdanie jest rozstrzygalne, jeżeli istnieje funkcja rekurencyjna o przeciwdzidzinie bool, która sprawdza, czy jest ono prawdziwe, czy fałszywe. Przykładami zdań, predykatów czy problemów rozstrzygalnych są:

• sprawdzanie, czy lista jest niepusta
• sprawdzanie, czy liczba naturalna jest parzysta
• sprawdzanie, czy dwie liczby naturalne są równe

Przykładem problemów nierozstrzygalnych są:

• dla funkcji f g : nat -> nat sprawdzenie, czy forall n : nat, f n = g n — jest to w ogólności niemożliwe, gdyż wymaga wykonania nieskończonej ilości porównań (co nie znaczy, że nie da się rozwiązać tego problemu dla niektórych funkcji)
• sprawdzenie, czy słowo o nieskończonej długości jest palindromem

Ćwiczenie

Techniczne apekty rozstrzygalności

Podsumowując powyższe rozważania, moglibyśmy stwierdzić: zdanie P jest rozstrzygalne, jeżeli istnieje term typu P \/ ~ P. Stwierdzenie takie nie zamyka jednak sprawy, gdyż bywa czasem mocno bezużyteczne. Żeby to zobrazować, spróbujmy użyć twierdzenia eq_nat_dec do napisania funkcji, która sprawdza, czy liczna naturalna n występuje na liście liczb naturalnych l:

Coq nie akceptuje powyższego kodu, racząc nas informacją o błędzie:

Nasza porażka wynika z faktu, że do zdefiniowania funkcji, która jest programem (jej dziedzina i przeciwdziedzina są sortu Type) próbowaliśmy użyć termu eq_nat_dec n h, który jest dowodem (konkluzją eq_nat_dec jest równość, która jest sortu Prop). Mimo korespondencji Curry'ego-Howarda, która odpowiada za olbrzymie podobieństwo specyfikacji i zdań, programów i dowodów, sortu Type i sortu Prop, są one rozróżniane i niesie to za sobą konsekwencje: podczas gdy programów możemy używać wszędzie, dowodów możemy używać jedynie do konstruowania innych dowodów. Praktycznie oznacza to, że mimo iż równość liczb naturalnych jest rozstrzygalna, pisząc program nie mamy możliwości jej rozstrzygania za pomocą eq_nat_dec. To właśnie miałem na myśli pisząc, że termy typu P \/ ~ P są mocno bezużyteczne. Uszy do góry: nie wszystko stracone! Jest to tylko drobna przeszkoda, którą bardzo łatwo ominąć:

Typ sumbool jest niemal dokładną kopią or, jednak nie żyje on w Prop, lecz w Type. Ta drobna sztuczka, że termy typu sumbool A B formalnie są programami, mimo że ich naturalna interpretacja jest taka sama jak or, a więc jako dowodu dysjunkcji.

Ćwiczenie

Udowodnij twierdzenie eq_nat_dec' o rozstrzygalności = na liczbach naturalnych. Użyj typu sumbool. Następnie napisz funkcję inb_nat, która sprawdza, czy liczba naturalna n jest obecna na liście l.

Kiedy nie warto rozstrzygać? (TODO)

Tutaj coś w stylu n < m \/ n = m \/ n > m

Rozstrzygalność jako pułapka na negacjonistów (TODO)

Techniczne aspekty rozstrzygalności 2 (TODO)

Ślepota boolowska (TODO)

Reflekcja w małej skali (TODO)