Typy indukcyjne w Coqu
Definicja
Oto definicja typu indukcyjnego reprezentującego polimorficzne listy z
długością, tj. dla dowolnego A typu Set i dowolnego n
typu nat, (listn A n) oznacza typ
``lista elementów typu A, długości n''
Inductive listn [A:Set] : nat -> Set :=
| niln : (listn A O)
| consn : A -> (n:nat)(listn A n) -> (listn A (S n)).
Po wprowadzeniu tej definicji typy listn i jego konstruktorów są
następujące:
listn : Set->nat->Set
niln : (A:Set)(listn A O)
consn : (A:Set)A->(n:nat)(listn A n)->(listn A (S n))
Na definicję indukcyjną skłądają się następujace elementy:
-
nazwa typu indukcyjnego -- listn,
- lista parametrów -- [A:Set]
Parametry to niezmienne argumenty typu indukcyjnego. Wszystkie
wystąpienia listn w jego definicji muszą być zaaplikowane go
parametru A. Z tego powodu kolejny argument listn typu
nat nie mógłby być parametrem. Oprócz tego typy konstruktorów oraz
samego listn są abstrahowane ze względu na parametry.
- typ (rodzaj) typu indukcyjnego -- nat -> Set
Musi to być produkt (może być zależny) zakończony jednym z sortów
(Set, Prop lub Type). Jeśli sortem tym jest Set mówimy o
typie indukcyjnym, jeśli Prop -- o predykacie
indukcyjnym.
- lista deklaracji konstruktorów oddzielona |
Każda deklaracja konstruktora składa się z jego nazwy, oraz typu.
Typ musi być produktem (może być zależnym), zakończonym definiowanym
typem indukcyjnym, zaaplikowanym do parametrów i innych argumentów,
czyli w tym przypadku (listn A _) gdzie ostatnia pozycja
zależy od konstruktora.
Dodatkowym warunkiem, który muszą spełniać typy konstruktorów jest
warunek pozytywności. Mówi on, że listn może wystąpić w typie
argumentu konstruktora wyłącznie na końcu, tzn. argumenty
konstruktora mogą być postaci coś1 -> ... ->
cośn -> (listn A _), gdzie w cośi nie
występuje listn. Następująca deklaracja konstruktora:
nbzdura : A -> (n:nat)((listn A n) -> A) -> (listn A n)
nie jest poprawna.
Case -- analiza przypadków
Załóżmy, że chcemy udowodnić predykat P dla dowolnej listy, wiedząc,
że jest prawdziwy dla dowolnej listy pustej oraz dla dowolnej listy
niepustej.
Mamy zatem:
A:Set;
P:(n:nat)(listn A n) -> Prop;
d_pusta : (P O (niln A));
d_niepusta : (n':nat)(a':A)(l':(list A n')) -> (P (S n') (consn A a' n' l'));
n:nat; l:nat
============================================================================
<P>Cases l of
niln => d_pusta
| (consn a n l) => (d_niepusta n a l)
end
: (P n l)
Należy zwrócić uwagę na następujące fakty:
-
parametr A jest globalny. Mogłaby to być też jakaś
konkretna stała, np. typ nat lub bool
- najogólniejszy typ P to ``argumenty listn ->
(listn z tymi argumentami ) -> sort''
Predykat P mógłby mieć też prostszy typ ``argumenty listn -> sort'', czyli nat -> sort, jak
[n:nat](listn B n) (dla jakiegoś B:Set) lub
[n:nat](Even n) albo być stałą typu ``sort'', jak nat, czy
bool. W tym ostatnim przypadku nie jest konieczne
umieszczanie <P> przes konstrukcją Cases.
Możliwym skomplikowanym predykatem P, jest np.
[n:nat;l:(list A n)](niepusta A (S n) (consn A a n l))
(gdzie niepusta to
hipotetyczny zdefiniowany wcześniej predykat, typu
(A:Set)(n:nat)(listn A n) -> Prop, a a to jakiś
element typu A).
- typy gałęzi instrukcji Cases muszą odpowiadać typom
konstruktorów, tylko na końcu zamiast (listn
argumenty) stoi P zaaplikowane do odpowiedniego
argumentu i do listy skonstruowanej danym konstruktorem.
- zauważmy, że po lewej stronie => konstruktory występują
bez parametru A. Po prawej muszą już mieć parametr.
Z instrukcją Cases związana jest następująca reguła, zwana
i (jota) redukcją:
Cases (niln A) of niln => d_puste | ... end
žŽi
d_puste
Cases (consn a' n' l') of ... | (consn a n l) => (d_niepusta n a l) end
žŽi
(d_niepuste n' a' l')
Rekurencja strukturalna
Rekurencja strukturalna służy zarówno do definiowania funkcji jak i do
robienia dowodów indukcyjnych. W Coqu istnieje konstrukcja
Fix do definiowania funkcji lokalnych oraz jego uproszczona
wersja, używająca słowa kluczowego Fixpoint, służąca do
definiowania funkcji globalnych.
Najczęściej używana składnia operatora Fix, to:
Fix fi{ |
f1 [x11:t11;...;xi11:ti11] : tk11 := d1 with |
... with |
fn [x1n:t1n; ...; xinn:tinn] : tknn := dn}
|
Funkcje f1... fn definiowane są wzajemnie rekurencyjnie, i
następnie z tej wspólnej definicji wybierana jest funkcja fi. Każda
funkcja fj definiowana jest przez rekurencję strukturalną ze
względu na argument ij. Typ tijj musi zatem być typem
indukcyjnym.
W ciałach funkcji (d1... dn) może występować dowolne fj, ale
musi być zaaplikowane do co najmniej ij, argumentów, z czego
ostatni musi być strukturalnie mniejszy niż argument wywołania
funkji, czyli ``strzeżony'' poprzez co najmniej jedną konstrukcję
Cases.
Powyższa składnia operatora Fix jest równoważna następującej:
Fix fi{ |
f1/i1 : (x11:t11;...;xi11:ti11)tk11 := [x11:t11;...;xi11:ti11]d1 with |
... with |
fn/in : (x1n:t1n; ...; xinn:tinn)tknn := [x1n:t1n; ...; xinn:tinn]dn}
|
którą w skrócie piszemy Fix fi{f1/i1 : A1 := D1...
fn/in : An:=Dn}
Reguła typowania jest zgodna z oczekiwaniem:
|
(G |- Aj : sj) |
|
(G; f1 : A1 ... fn : An |- Dj : Aj) |
|
|
|
G |- Fix fi{f1/i1 : A1 := D1...
fn/in : An:=Dn} : Ai
|
|
jeśli sj Î {Set,Prop,Type} oraz oczywiście Dj są
poprawnie zbudowane (zaczynają się od odpowiedniej liczby abstrakcji i
przestrzegają wspomniane wyżej warunki dobrego ufundowania wywołań
f1... fn)
Reguła redukcji związana z operatorem Fix, zwana jest również
i-redukcją, i wyraża się następująco (dla GF ş f1/i1 :
A1 := D1... fn/in : An:=Dn)
Fix |
fi{GF} a1 ... a |
|
žŽ |
|
Di{fj |Ž Fix |
fj{GF}} a1 ... a |
|
jeżeli aii zaczyna się od konstruktora. Oczywiście bez tego
warunku reguła ta w oczywisty sposób prowadziłaby do nieterminacji.
Żeby wyjaśnić znaczenie najczęściej używanej komendy
Fixpoint, przyjmijmy, że
GF ş |
f1 [x11:t11;...;xi11:ti11] : tk11 := d1 with |
... with |
fn [x1n:t1n; ...; xinn:tinn] : tknn := dn
|
Wprowadzenie komendy:
odpowiada wprowadzeniu następującego ciągu komend:
Definition f1:=Fix f1{GF}. |
... |
Definition fn:=Fix fn{GF}.
|
Kilka przykładów
Zaczniemy od funkcji na liczbach naturalnych (których użyjemy do
definiowania funkcji na listach z długością).
Fixpoint npol_podloga [n:nat] : nat :=
Cases n of
O => O
| (S n') => (npol_sufit n')
end
with npol_sufit [n:nat] : nat :=
Cases n of
O => O
| (S n') => (S (npol_podloga n'))
end.
Pierwsza z powyższych funkcji oblicza ë n/2 ű, a
druga é n/2 ů.
Poniższe funkcje na listach z długością wybierają co drugi element z
listy wejsciowej, pierwsza z nich zaczyna od pierwszego elementu, a
druga -- od drugiego. Ich typy (a konkretnie dlugości list wyjściowych)
opisane są za pomocą npol_podloga i npol_sufit.
Fixpoint codrugi_zpierwszym [A:Set;n:nat; l:(listn A n)]
: (listn A (npol_sufit n)) :=
<[n](listn A (npol_sufit n))>Cases l of
niln => (niln A)
| (consn a n' l') => (consn A a ? (codrugi_bezpierw A n' l'))
end
with codrugi_bezpierw [A:Set;n:nat; l:(listn A n)]
: (listn A (npol_podloga n)) :=
<[n](listn A (npol_podloga n))>Cases l of
niln => (niln A)
| (consn a n' l') => (codrugi_zpierwszym A n' l')
end.
Obiekty indukcyjne i dowodzenie
Dowodzenie formuł indukcyjnych -- wprowadzanie
Aby skonstruować obiekt indukcyjny z konstruktorów, używamy
taktyki Constructor i. np. po wprowadzeniu
Goal (A,B:Prop)B->A\/
B.
Intros.
mamy sytuacje:
1 subgoal
A : Prop
B : Prop
H : B
============================
A\/
B
Polecenie Constructor 2. spowoduje odnalezienie drugiego
konstruktora predykatu indukcyjnego or -- i zaaplikowanie go.
Jest ona zatem równoważna Apply or_intror.
Wywołanie Constructor. bez numeru spowoduje znalezienie
pierwszego konstruktora, który może być zaaplikowany do bieżącego
``celu'' i zaaplikowanie go. W naszym przykładzie, byłby to
konstruktor or_introl, co poprowadziłoby dowód na manowce.
Dla konstrukcji o dwóch konstruktorach (tak jak np. or, ale
również np. nat, czy bool),
można stosować taktyki Left. i Right., które
oznaczają odpowiednio Constructor 1. i Constructor
2.
Dla konstrukcji o jednym konstruktorze (jak and) taktyka
Split równoważna jest taktyce Constructor 1.
Podobna do nich jest również taktyka Exists, stworzona z myślą
o dowodzeniu formuł egzystencjalnych (konstrukcja indukcyjna
sig z jednym konstruktorem exist).
Wszystkie powyższe taktyki mogą przyjmować parametry tak samo jak
taktyka Apply (jeśli ich automatyczna synteza nie jest
możliwa). Niektóre wykonują automatycznie Intros.
Używanie obiektów indukcyjnych -- eliminacja
Pierwszą techniką eliminacji specyficzną dla obiektów indukcyjnych
jest analiza przypadków, czyli używanie konstrukcji Cases.
Sluży do tego taktyka Case. Tworzy ona tyle ``pod-celów'' ile
jest konstruktorów danego typu. Uwaga! Jest ona dosyć głupia -- dla
typów indukcyjnych zależnych bierze również pod uwagę przypadki
``niemożliwe'' (np. lista o długości Řzaczynająca się od consn)
Różne warianty Case (robiące automatycznie Intros
i/lub czyszczenie niepotrzebnych hipotez), to Destruct oraz
NewDestruct.
Dowody indukcyjne robi się w Coq'u przy pomocy taktyki
Elim. Dla danego typu indukcyjnego, np. nat, używa ona
lematu nat_ind, udowodnionego automatycznie (przy pomocy
Fix i Cases) zaraz po wprowadzeniu definicji
indukcyjnej. (Pozostale automatyczne stałe -- nat_rec i
nat_rect używane są przez Elim, gdy ``cel'' jest w
sorcie Set lub Type, a nie Prop, jak zazwyczaj).
W zasadzie Elim n. odpowiada Apply nat_ind. o ile
nat jest typem n oraz ``cel'' jest w sorcie Prop.
Wariantami Elim są Induction i
NewInduction.
Do równoległych dowodów po dwóch zmiennych służy Double
Induction.
Ważnymi taktykami związanymi z równością są
Discriminate i Injection. Pierwsza wykorzystuje
nieprawdziwe założenie o równości dwóch termów danego typu
indukcyjnego zaczynających się od różnych konstruktorów do
udowodnienia fałszu i w konsekwencji czegokolwiek.
Injection aplikuje (udowodniony naprędce) lemat o
różnowartościowości konstruktorów jako funkcji.
Ich sprytnym połączeniem jest taktyka Simplify_eq.
Taktyką, która stara się nadrobić niedostatki taktyki Case
dla typów zależnych (jak np. nie zauważanie, że listy o długości zero
nie da się skonstruować przez consn), jest taktyka
Inversion. Używając skomplikowanego (dowodzonego w locie)
lematu wyprowadza ona jak najwięcej możliwych informacji z konkretnej
instancji zależnego typu indukcyjnego.
Jej warianty to Inversion_clear oraz Dependent
Inversion.
Ponieważ lemat generowany przez Inversion jest spory, w
przypadku, gdy wielokrotnie używamy tej taktyki dla tej samej
konstrukcji indukcyjnej, możemy nadać temu lematowi nazwę, a następnie
używać go poprzez Apply. Do generowania służy polecenie
Derive Inversion.
This document was translated from LATEX by
HEVEA.