W poprzednim rozdziale dowiedzieliśmy się już co nieco o typach, a także spotkaliśmy kilka z nich oraz kilka sposobów tworzenia nowych typów ze starych (takich jak np. koniunkcja; pamiętaj, że zdania są typami). W tym rozdziale dowiemy się, jak definiować nowe typy przy pomocy indukcji oraz jak użyć rekursji do definiowania funkcji, które operują na tych typach. W Coqu są trzy główne rodzaje typów: produkt zależny, typy induktywne i typy koinduktywne. Z pierwszym z nich już się zetknęliśmy, drugi poznamy w tym rozdziale, trzeci na razie pominiemy. Typ induktywny definiuje się przy pomocy zbioru konstruktorów, które służą, jak sama nazwa wskazuje, do budowania termów tego typu. Konstruktory te są funkcjami (być może zależnymi), których przeciwdziedziną jest definiowany typ, ale niczego nie obliczają — nadają jedynie termom ich "kształt". W szczególności, nie mają nic wspólnego z konstruktorami w takich językach jak C++ lub Java — nie mogą przetwarzać swoich argumentów, alokować pamięci, dokonywać operacji wejścia/wyjścia etc. Tym, co jest ważne w przypadku konstruktorów, jest ich ilość, nazwy oraz ilość i typy przyjmowanych argumentów. To te cztery rzeczy decydują o tym, jakie "kształty" będą miały termy danego typu, a więc i czym będzie sam typ. W ogolności każdy term jest skończonym, ukorzenionym drzewem, którego kształt zależy od charakterystyki konstruktorów tak:

• każdy konstruktor to inny rodzaj węzła (nazwa konstruktora to nazwa węzła)
• konstruktory nierekurencyjne to liście, a rekurencyjne — węzły wewnętrzne
• argumenty konstruktorów to dane przechowywane w danym węźle

Typ induktywny można wyobrażać sobie jako przestrzeń zawierającą te i tylko te drzewa, które można zrobić przy pomocy jego konstruktorów. Nie przejmuj się, jeżeli opis ten wydaje ci się dziwny — sposób definiowania typów induktywnych i ich wartości w Coqu jest diametralnie różny od sposobu definiowania klas i obiektów w językach imperatywnych i wymaga przyzwyczajenia się do niego. Zobaczmy, jak powyższy opis ma się do konkretnych przykładów.

Wstęp

Typy i typowanie statyczne (TODO)

Tutaj historyjka o tym, że im bardziej statyczne jest typowanie, tym szybciej po popełnieniu błędu jesteśmy w stanie go wykryć.

Typy vs testy

Typy, programy, zdania, dowody i specyfikacje (TODO)

Tu zestawić ze sobą P : Prop, A : Type, p : P, x : A. Wytłumaczyć relację między typami, zdaniami, specyfikacjami programów, przestrzeniami, etc.

Przydatne komendy

Czas, aby opisać kilka przydatnych komend.

Przypomnijmy, że komenda Check wyświetla typ danego jej termu, a Print wypisuje jego definicję.

Search wyświetla wszystkie obiekty, które zawierają podaną nazwę. W naszym przypadku pokazały się wszystkie funkcje, w których sygnaturze występuje typ nat.

SearchPattern jako argument bierze wzorzec i wyświetla wszystkie obiekty, które zawierają podterm pasujący do danego wzorca. W naszym przypadku pokazały się twierdzenia, w których występuje podterm mający po lewej dodawanie, a po prawej cokolwiek. Dokładny opis wszystkich komend znajdziesz tutaj.

Typy wbudowane (TODO)

Tutaj będą opisane typy, która można spotkać w normalnych językach programowania, takie jak int czy float.

Funkcje (TODO)

Enumeracje (TODO)

Najprostszym rodzajem typów induktywnych są enumeracje, czyli typy, których wszystkie konstruktory są stałymi.

Definicja typu induktywnego ma następującą postać: najpierw występuje słowo kluczowe Inductive, następnie nazwa typu, a po dwukropku sort (Set, Prop lub Type). Następnie wymieniamy konstruktory typu — dla czytelności każdy w osobnej linii. Mają one swoje unikalne nazwy i są funkcjami, których przeciwdziedziną jest definiowany typ. W naszym przypadku mamy 2 konstruktory, zwane true oraz false, które są funkcjami zeroargumentowymi. Definicję tę możemy odczytać następująco: "true jest typu bool, false jest typu bool i nie ma żadnych więcej wartości typu bool". Uwaga: należy odróżnić symbole := oraz =. Pierwszy z nich służy do definiowania, a drugi do zapisywania równości. Zapis name := term oznacza "niech od teraz name będzie inną nazwą dla term". Jest to komenda, a nie zdanie logiczne. Od teraz jeżeli natkniemy się na nazwę name, będziemy mogli odwinąć jej definicję i wstawić w jej miejsce term. Przykład: Definition five := 5. Antyprzykład: 2 := 5 (błąd składni). Zapis a = b oznacza "a jest równe b". Jest to zdanie logiczne, a nie komenda. Zdanie to rzecz jasna nie musi być prawdziwe. Przykład: 2 = 5. Antyprzykład: five = 5 (jeżeli five nie jest zdefiniowane, to dostajemy komunikat w stylu "nie znaleziono nazwy five").

Definicja funkcji wygląda tak: najpierw mamy słowo kluczowe Definition (jeżeli funkcja nie jest rekurencyjna), następnie argumenty funkcji w postaci (name : type); po dwukropku przeciwdziedzina, a po symbolu := ciało funkcji. Podstawowym narzędziem służącym do definiowania funkcji jest dopasowanie do wzorca (ang. pattern matching). Pozwala ono sprawdzić, którego konstruktora użyto do zrobienia dopasowywanej wartości. Podobnym tworem występującym w językach imperatywnych jest instrukcja switch, ale dopasowanie do wzorca jest od niej dużo potężniejsze. Nasza funkcja działa następująco: sprawdzamy, którym konstruktorem zrobiono argument b — jeżeli było to true, zwracamy false, a gdy było to false, zwracamy true.

Ćwiczenie (andb i orb)

Zdefiniuj funkcje andb (koniunkcja boolowska) i orb (alternatywa boolowska).

Zanim odpalimy naszą funkcję, powinniśmy zadać sobie pytanie: w jaki sposób programy są wykonywane? W celu lepszego zrozumienia tego zagadnienia porównamy ewaluację programów napisanych w językach imperatywnych oraz funkcyjnych. Rozważmy bardzo uproszczony model: interpreter wykonuje program, który nie dokonuje operacji wejścia/wyjścia, napisany w jakimś języku imperatywnym. W tej sytuacji działanie interpretera sprowadza się do tego, że czyta on kod programu instrukcja po instrukcji, a następnie w zależności od przeczytanej instrukcji odpowiednio zmienia swój stan. W języku czysto funkcyjnym taki model ewaluacji jest niemożliwy, gdyż nie dysponujemy globalnym stanem. Zamiast tego, w Coqu wykonanie programu polega na jego redukcji. O co chodzi? Przypomnijmy najpierw, że program to term, którego typem jest specyfikacja, czyli typ sortu Set. Termy mogą być redukowane, czyli zamieniane na równoważne, ale prostsze, przy użyciu reguł redukcji. Prześledźmy wykonanie programu negb true krok po kroku.

Redukcja delta odwija definicje. Żeby użyć jakiejś redukcji, używamy komendy Eval cbv redukcje in term.

Redukcja beta podstawia argument do funkcji.

Redukcja jota dopasowuje term do wzorca i zamienia go na term znajdujący się po prawej stronie => dla dopasowanego przypadku.

Żeby zredukować term za jednym zamachem, możemy pominąć nazwy redukcji występujące po cbv — w taki wypadku zostaną zaaplikowane wszystkie możliwe redukcje, czyli program zostanie wykonany. Do jego wykonania możemy też użyć komend Eval cbn oraz Eval compute (a także Eval simpl, ale taktyka simpl jest przestarzała, więc nie polecam).

Ćwiczenie (redukcja)

Zredukuj "ręcznie" programy andb false false oraz orb false true. Jak widać, wykonanie programu w Coqu jest dość toporne. Wynika to z faktu, że Coq nie został stworzony do wykonywania programów, a jedynie do ich definiowania i dowodzenia ich poprawności. Aby użyć programu napisanego w Coqu w świecie rzeczywistym, stosuje się zazwyczaj mechanizm ekstrakcji, który pozwala z programu napisanego w Coqu automatycznie uzyskać program w Scheme, OCamlu lub Haskellu, które są od Coqa dużo szybsze i dużo powszechniej używane. My jednak nie będziemy się tym przejmować. Zdefiniowawszy naszą funkcję, możemy zadać sobie pytanie: czy definicja jest poprawna? Gdybyśmy pisali w jednym z języków imperatywnych, moglibyśmy napisać dla niej testy jednostkowe, polegające np. na tym, że generujemy losowo wejście funkcji i sprawdzamy, czy wynik posiada żądaną przez nas właściwość. Coq umożliwia nam coś dużo silniejszego: możemy wyrazić przy pomocy twierdzenia, że funkcja posiada interesującą nas własność, a następnie spróbować je udowodnić. Jeżeli nam się powiedzie, mamy całkowitą pewność, że funkcja rzeczywiście posiada żądaną własność.

Nasze twierdzenie głosi, że funkcja negb jest inwolucją, tzn. że dwukrotne jej zaaplikowanie do danego argumentu nie zmienia go, lub też, innymi słowy, że negb jest swoją własną odwrotnością. Dowód przebiega w następujący sposób: taktyką intro wprowadzamy zmienną b do kontekstu, a następnie używamy taktyki destruct, aby sprawdzić, którym konstruktorem została zrobiona. Ponieważ typ bool ma dwa konstruktory, taktyka ta generuje nam dwa podcele: musimy udowodnić twierdzenie osobno dla przypadku, gdy b = true oraz dla b = false. Potem przy pomocy taktyki cbn redukujemy (czyli wykonujemy) programy negb (negb true) i negb (negb false). Zauważ, że byłoby to niemożliwe, gdyby argument był postaci b (nie można wtedy zaaplikować żadnej redukcji), ale jest jak najbardziej możliwe, gdy jest on postaci true albo false (wtedy redukcja przebiega jak w przykładzie). Na koniec używamy taktyki reflexivity, która potrafi udowodnić cel postaci a = a. destruct jest taktykowym odpowiednikiem dopasowania do wzorca i bardzo często jest używany, gdy mamy do czynienia z czymś, co zostało za jego pomocą zdefiniowane. Być może poczułeś dyskomfort spowodowany tym, że cel postaci a = a można udowodnić dwoma różnymi taktykami (reflexivity oraz trivial) albo że termy można redukować na cztery różne sposoby (Eval cbn, Eval cbv, Eval compute, Eval simpl). Niestety, będziesz musiał się do tego przyzwyczaić — język taktyka Coqa jest strasznie zabałaganiony i niesie ze sobą spory bagaż swej mrocznej przeszłości. Na szczęście od niedawna trwają prace nad jego ucywilizowaniem, czego pierwsze efekty widać już od wersji 8.5. W chwilach desperacji uratować może cię jedynie dokumentacja:

• Indeks taktyk
• Ltac

Zauważmy, że nie musimy używać taktyki intro, żeby wprowadzić b do kontekstu: taktyka destruct sama jest w stanie wykryć, że nie ma go w kontekście i wprowadzić je tam przed rozbiciem go na konstruktory. Zauważmy też, że oba podcele rozwiązaliśmy w ten sam sposób, więc możemy użyć kombinatora ; (średnika), żeby rozwiązać je oba za jednym zamachem.

Ćwiczenie (logika boolowska)

Udowodnij poniższe twierdzenia.

Ćwiczenie (róża kierunków)

Zdefiniuj typ opisujący kierunki podstawowe (północ, południe, wschód, zachód - dodatkowe punkty za nadanie im sensownych nazw).

Zdefiniuj funkcje turnL i turnR, które reprezentują obrót o 90 stopni przeciwnie/zgodnie z ruchem wskazówek zegara. Sformułuj i udowodnij twierdzenia mówiące, że:

• obrót cztery razy w lewo/prawo niczego nie zmienia
• obrót trzy razy w prawo to tak naprawdę obrót w lewo (jest to tzw. pierwsze twierdzenie korwinizmu)
• obrót trzy razy w lewo to obrót w prawo (jest to tzw. drugie twierdzenie korwinizmu)
• obrót w prawo, a potem w lewo niczego nie zmienia
• obrót w lewo, a potem w prawo niczego nie zmienia
• każdy kierunek to północ, południe, wschód lub zachód (tzn. nie ma innych kierunków)

Zdefiniuj funkcję opposite, które danemu kierunkowi przyporządkowuje kierunek do niego przeciwny (czyli północy przyporządkowuje południe etc.). Wymyśl i udowodnij jakąś ciekawę specyfikację dla tej funkcji (wskazówka: powiąż ją z turnL i turnR).

Zdefiniuj funkcję is_opposite, która bierze dwa kierunki i zwraca true, gdy są one przeciwne oraz false w przeciwnym wypadku. Wymyśl i udowodnij jakąś specyfikację dla tej funkcji. Wskazówka: jakie są jej związku z turnL, turnR i opposite?

Pokaż, że funkcje turnL, turnR oraz opposite są injekcjami i surjekcjami (co to dokładnie znacz, dowiemy się później). Uwaga: to zadanie wymaga użyci taktyki inversion, która jest opisana w podrozdziale o polimorfizmie.

Ćwiczenie (różne enumeracje)

Zdefiniuj typy induktywne reprezentujące:

• dni tygodnia
• miesiące
• kolory podstawowe systemu RGB

Wymyśl do nich jakieś ciekawe funkcje i twierdzenia.

Ważne enumeracje

Typ pusty

Empty_set jest, jak sama nazwa wskazuje, typem pustym. Żaden term nie jest tego typu. Innymi słowy: jeżeli jakiś term jest typu Empty_set, to mamy sprzeczność.

Jeżeli mamy term typu Empty_set, to możemy w sposób niemal magiczny wyczarować term dowolnego typu A, używając dopasowania do wzorca z pustym wzorcem.

Ćwiczenie (create_unique)

Udowodnij, że powyższa funkcja jest unikalna.

Ćwiczenie (no_fun_from_nonempty_to_empty)

Pokaż, że nie istnieją funkcje z typu niepustego w pusty.

Singleton

unit jest typem, który ma tylko jeden term, zwany tt (nazwa ta jest wzięta z sufitu).

Funkcja delete jest w pewien sposób "dualna" do napotkanej przez nas wcześniej funkcji create. Mając term typu Empty_set mogliśmy stworzyć term dowolnego innego typu, zaś mając term dowolnego typu A, możemy "zapomnieć o nim" albo "skasować go", wysyłając go funkcją delete w jedyny term typu unit, czyli tt. Uwaga: określenie "skasować" nie ma nic wspólnego z fizycznym niszczeniem albo dealokacją pamięci. Jest to tylko metafora.

Ćwiczenie (delete_unique)

Pokaż, że funkcja delete jest unikalna.

Reguły eliminacji dla enumeracji

Najprymitywniejszymi z typów induktywnych są enumeracje. Definiując je, wymieniamy po prostu wszystkie ich elementy.

Reguła definiowania przez przypadki jest banalnie prosta: jeżeli w jakimś inny typie P uda nam się znaleźć po jednym elemencie dla każdego z elementów naszego typu I, to możemy zrobić funkcję I -> P.

Regułę zdefiniować możemy za pomocą dopasowania do wzorca.

Zależną regułę definiowania przez przypadki możemy uzyskać z poprzedniej uzależniając przeciwdziedzinę P od dziedziny.

Definicja, jak widać, jest taka sama jak poprzednio, więc obliczeniowo obie reguły zachowują się tak samo. Różnica leży jedynie w typach - druga reguła jest ogólniejsza.

Sumy (TODO)

Suma A i B to typ, którego termy są albo termami typu A, zawiniętymi w konstruktor inl, albo termami typu B, zawiniętymi w konstruktor inr. Suma, w przeciwieństwie do produktu, zdecydowanie nie ma projekcji.

Ćwiczenie (sumy bez projekcji)

Pokaż, że suma nie ma projekcji.

Enumeracje z argumentami (TODO)

Produkty (TODO)

Produkt typów A i B to typ, którego termami są pary. Pierwszy element pary to term typu A, a drugi to term typu B. Tym, co charakteryzuje produkt, są projekcje:

• fst : forall A B : Type, prod A B -> A wyciąga z pary jej pierwszy element
• snd : forall A B : Type, prod A B -> B wyciąga z pary jej drugi element

Ćwiczenie (projekcje)

Zdefiniuj projekcje i udowodnij poprawność swoich definicji.

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

Prymitywne rekordy (TODO)

Tutaj wprowadzić prymitywne projekcje i porównać ze zwykłymi rekordami.

Programowanie a dowodzenie - eliminacja zdań (TODO)

Tutaj opisać ograniczenia na eliminację dowodów zdań.

Typy hybrydowe

Ostatnim z typów istotnych z punktu widzenia silnych specyfikacji jest typ o wdzięcznej nazwie sumor.

Jak sama nazwa wskazuje, sumor jest hybrydą sumy rozłącznej sum oraz dysjunkcji or. Możemy go interpretować jako typ, którego elementami są elementy A albo wymówki w stylu "nie mam elementu A, ponieważ zachodzi zdanie B". B nie zależy od A, a więc jest to zwykła suma (a nie suma zależna, czyli uogólnienie produktu). sumor żyje w Type, a więc jest to specyfikacja i liczy się konkretna postać jego termów, a nie jedynie fakt ich istnienia.

Ćwiczenie (pred')

Zdefiniuj funkcję pred', która przypisuje liczbie naturalnej jej poprzednik. Poprzednikiem 0 nie powinno być 0. Mogą przydać ci się typ sumor oraz sposób definiowania za pomocą taktyk, omówiony w podrozdziale dotyczącym sum zależnych.

Typy pozytywne i negatywne (TODO)

Tutaj tłumaczenie co to znaczy, że typ jest pozytywny/negatywny.

Moduły (TODO)

Nie lubię Coqowego systemu modułów, więc w tym rozdziale jeszcze długo nic nie zagości.

Styl, czyli formatowanie, wcięcia i komentarze (TODO)

Tu będzie rozdział o stylu, czyli rzeczach takich jak czytelne formatowanie kodu czy pisanie zrozumiałych komentarzy.

Formatowanie kodu i wcięcia

Komentarze

Ars nazywandi, czyli trudna sztuka wymyślania nazw