Induktywne predykaty i relacje

Przypomnijmy, że predykaty to funkcje, których przeciwdziedziną jest sort Prop, czyli funkcje zwracające zdania logiczne. Predykat P : A -> Prop można rozumieć jako właściwość, którą mogą posiadać termy typu A, zaś dla konkretnego x : A zapis P x interpretować można "term x posiada właściwóść P". O ile istnieją tylko dwa rodzaje induktwynych zdań (prawdziwe i fałszywe), o tyle induktywnie zdefiniowane predykaty są dużo bardziej ciekawe i użyteczne, gdyż dla jednych termów mogą być prawdziwe, a dla innych nie.

Predykat even ma oznaczać właściwość "bycia liczbą parzystą". Jego definicję można zinterpretować tak:

• "0 jest liczbą przystą"
• "jeżeli n jest liczbą parzystą, to n + 2 również jest liczbą parzystą"

Jak widać, induktywna definicja parzystości różni się od powszechnie używanej definicji, która głosi, że "liczba jest parzysta, gdy dzieli się bez reszty przez 2". Różnica jest natury filozoficznej: definicja induktywna mówi, jak konstruować liczby parzyste, podczas gdy druga, "klasyczna" definicja mówi, jak sprawdzić, czy liczba jest parzysta. Przez wzgląd na swą konstruktywność, w Coqu induktywne definicje predykatów czy relacji są często dużo bardziej użyteczne od tych nieinduktywnych, choć nie wszystko można zdefiniować induktywnie.

Jak możemy udowodnić, że 0 jest liczbą parzystą? Posłuży nam do tego konstruktor even0, który wprost głosi, że even 0. Nie daj się zwieść: even0, pisane bez spacji, jest nazwą konstruktora, podczas gdy even 0, ze spacją, jest zdaniem (czyli termem typu Prop), które można interpretować jako "0 jest liczbą parzystą".

Jak możemy udowodnić, że 2 jest parzyste? Konstruktor even0 nam nie pomoże, gdyż jego postać (even 0) nie pasuje do postaci naszego twierdzenia (even 2). Pozostaje nam jednak konstruktor evenSS. Jeżeli przypomnimy sobie, że 2 to tak naprawdę S (S 0), natychmiast dostrzeżemy, że jego konkluzja pasuje do postaci naszego twierdzenia. Możemy go więc zaaplikować (pamiętaj, że konstruktory są jak zwykłe funkcje, tylko że niczego nie obliczają — nadają one typom ich kształty). Teraz wystarczy pokazać, że even 0 zachodzi, co już potrafimy.

Jak pokazać, że 4 jest parzyste? Tą samą metodą, która pokazaliśmy, że 2 jest parzyste. 4 to S (S (S (S 0))), więc możemy użyć konstruktora evenSS. Zamiast jednak pisać apply evenSS, możemy użyć taktyki constructor. Taktyka ta działa na celach, w których chcemy skonstruować wartość jakiegoś typu induktywnego (a więc także gdy dowodzimy twierdzeń o induktywnych predykatach). Szuka ona konstruktora, który może zaaplikować na celu, i jeżeli znajdzie, to aplikuje go, a gdy nie — zawodzi. W naszym przypadku pierwsze dwa użycia constructor aplikują konstruktor evenSS, a trzecie — konstruktor even0.

A co, gdy chcemy pokazać, że 42 jest parzyste? Czy musimy 22 razy napisać constructor? Na szczęście nie — wystarczy posłużyć się kombinatorem repeat (jeżeli nie pamiętasz, jak działa, zajrzyj do rozdziału 1).

A jak pokazać, że 1 nie jest parzyste? Mając w kontekście dowód na to, że 1 jest parzyste (H : even 1), możemy zastantowić się, w jaki sposób dowód ten został zrobiony. Nie mógł zostać zrobiony konstruktorem even0, gdyż ten dowodzi, że 0 jest parzyste, a przecież przekonaliśmy się już, że 0 to nie 1. Nie mógł też zostać zrobiony konstruktorem evenSS, gdyż ten ma w konkluzji even (S (S n)), podczas gdy 1 jest postaci S 0 — nie pasuje on do konkluzji evenSS, gdyż "ma za mało Sów". Nasze rozumowanie prowadzi do wniosku, że za pomocą even0 i evenSS, które są jedynymi konstruktorami even, nie można skonstruować even 1, więc 1 nie może być parzyste. Na podstawie wcześniejszych doświadczeń mogłoby się nam wydawać, że destruct załatwi sprawę, jednak tak nie jest — taktyka ta jest w tym przypadku upośledzona i nie potrafi nam pomóc. Zamiast tego możemy się posłużyć taktyką inversion. Działa ona dokładnie w sposób opisany w poprzednim akapicie.

Jak pokazać, że 3 nie jest parzyste? Pomoże nam w tym, jak poprzednio, inwersja. Tym razem jednak nie załatwia ona sprawy od razu. Jeżeli zastanowimy się, jak można pokazać even 3, to dojdziemy do wniosku, że można to zrobić konstruktorem evenSS, gdyż 3 to tak naprawdę S (S 1). To właśnie robi pierwsza inwersja: mówi nam, że H : even 3 można uzyskać z zaaplikowania evenSS do 1, jeżeli tylko mamy dowód H1 : even 1 na to, że 1 jest parzyste. Jak pokazać, że 1 nie jest parzyste, już wiemy.

Ćwiczenie (odd)

Zdefiniuj induktywny predykat odd, który ma oznaczać "bycie liczbą nieparzystą" i udowodnij, że zachowuje się on jak należy.

Indukcja po dowodzie

Biblioteka Arith zawiera różne definicje i twierdzenia dotyczące arytmetyki. Będzie nam ona potrzebna w tym podrozdziale. Jak udowodnić, że suma liczb parzystych jest parzysta? Być może właśnie pomyślałeś o indukcji. Spróbujmy zatem:

Próbując jednak indukcji po n, a potem po m, docieramy do martwego punktu. Musimy udowodnić even n', podczas gdy zachodzi even (S n') (czyli even n' jest fałszywe). Wynika to z faktu, że przy indukcji n zwiększa się o 1 (P n -> P (S n)), podczas gdy w definicji even mamy konstruktor głoszący, że (even n -> even (S (S n))). Być może w drugiej kolejności pomyślałeś o taktyce destruct: jeżeli sprawdzimy, w jaki sposób udowodniono even n, to przy okazji dowiemy się też, że n może być jedynie postaci 0 lub S (S n'). Dzięki temu powinniśmy uniknąć problemu z poprzedniej próby.

Niestety, taktyka destruct okazała się za słaba. Predykat even jest induktywny, a zatem bez indukcji się nie obędzie. Rozwiązaniem naszych problemów nie będzie jednak indukcja po n lub m, lecz po dowodzie na to, że n jest parzyste.

Indukcja po dowodzie działa dokładnie tak samo, jak indukcja, z którą zetknęliśmy się dotychczas. Różni się od niej jedynie tym, że aż do teraz robiliśmy indukcję jedynie po termach, których typy były sortu Set lub Type. Indukcja po dowodzie to indukcja po termie, którego typ jest sortu Prop. W naszym przypadku użycie induction Hn ma następujący skutek:

• W pierwszym przypadku Hn to po prostu konstruktor even0, a zatem n jest zerem.
• W drugim przypadku Hn to evenSS n' Hn', gdzie n jest postaci S (S n'), zaś Hn' jest dowodem na to, że n' jest parzyste.

Taktyki replace i assert

Przy następnych ćwiczeniach mogą przydać ci się taktyki replace oraz assert.

Taktyka replace t with t' pozwala nam zastąpić w celu każde wystąpienie termu t termem t'. Jeżeli t nie ma w celu, to taktyka zawodzi, a w przeciwnym wypadku dodaje nam jeden podcel, w którym musimy udowodnić, że t = t'. Można też zastosować ją w hipotezie, pisząc replace t with t' in H.

Taktyka assert (x : A) dodaje do kontekstu term x typu A oraz generuje jeden dodatkowy podcel, w którym musimy skonstruować x. Zawodzi ona, jeżeli nazwa x jest już zajęta.

Ćwiczenie (właściwości even)

Udowodnij poniższe twierdzenia. Zanim zaczniesz, zastanów się, po czym należy przeprowadzić indukcję: po wartości, czy po dowodzie?