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: 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: 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)
 
j=1... n
     (G; f1 : A1 ... fn : An |- Dj : Aj)
 
j=1... n
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
 
ii
žŽ
 
i
Di{fj |Ž Fix fj{GF}} a1 ... a
 
ii
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:
Fixpoint GF.
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 ElimInduction 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ą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.