Chapter 2 Il proof-assistant Coq

Coq è un proof-assistant progettato per scrivere specifiche formali e programmi e per verificare che i programmi soddisfino le loro specifiche. Viene fornito un linguaggio di specifica, chiamato Gallina, i cui termini possono rappresentare programmi, loro proprietà o prove di queste. Grazie all'isomorfismo di Curry-Howard, programmi, proprietà e prove sono formalizzati nello stesso linguaggio, chiamato Calcolo delle Costruzioni (Co)Induttive (CIC), che è un'estensione del l-calcolo caratterizzata da un ricco sistema di tipi funzionali e dalla presenza di tipi induttivi e coinduttivi primitivi, nello stile di Martin-Löf. L'estrema espressività di CIC permette di utilizzare Coq anche come un logical environment per la codifica di teorie matematiche. Per esempio, la libreria standard di Coq copre la logica del primo ordine, l'aritmetica sui numeri naturali e quelli interi, una primitiva codifica della teoria degli insiemi e la teoria assiomatica dei numeri reali, fino alla definizione e alle prime proprietà delle derivate. In Coq, sono state sviluppate anche teorie di complessità molto maggiore, come la Teoria Costruttiva delle Categorie [SH95] o la Teoria degli Insiemi di Zermelo-Fraenkel [Wer97].

Tutti i judgement logici in Coq sono di tipaggio. Pertanto, il vero cuore del sistema è il type-checker, che verifica la correttezza delle prove, ovvero che i programmi soddisfino le rispettive specifiche. L'architettura di Coq è stata attentamente studiata in modo che la sua ``correttezza'' sia garantita esclusivamente da quella del type-checker. In altre parole, se CIC è consistente e il type-checker non contiene bug, allora ogni prova costruita in Coq sarà effettivamente un termine che dimostra la tesi, ovvero che abita in CIC il termine che la rappresenta. Come conseguenza, ogni possibile estensione del sistema che non interessi il type-checker è sicura. In particolare, questo permette di dare la possibilità all'utente di definire nuove tattiche da aggiungere al proof-engine.

La seconda componente critica di Coq, oltre al type-checker, è il program extractor, che permette di sintetizzare programmi funzionali che obbediscano alle loro specifiche formali, scritte come asserzioni logiche in CIC. La correttezza del program extractor è necessaria sia per garantire che il termine funzionale estratto (un termine di F_w) realizzi, nel senso di Kleene, la prova in CIC, sia per garantire la corrispondenza fra il codice estratto, scritto nella sintassi concreta di un dialetto di ML, e il termine di F_w.

La possibilità teorica di descrivere parzialmente¹ un sottoinsieme di CIC in CIC stesso, e in particolare l'esistenza di un suo type-checker e di un program extractor, permetterebbe il boot-strapping delle componenti critiche di Coq, ottenendo cosí il primo proof-assistant certificato. Il progetto, decisamente ambizioso, è stato portato a termine con successo da Barras e Werner (vedi [BW97]) per una parte significativa di CIC, ovvero quella puramente funzionale (il Calcolo delle Costruzioni)².

Coq e il suo sistema logico hanno rappresentato un difficile, ma stimolante banco di prova per HELM per diversi motivi. Innanzi tutto Coq e Lego, basati su dialetti differenti di CIC, rappresentano i sistemi attualmente più complessi fra quelli basati sull'isomorfismo di Curry-Howard; a causa dell'architettura assolutamente monolitica di Coq, che è un tipico prodotto del modello application-centric che HELM vuole superare, il codice è estremamente complesso; numerose funzionalità sono state integrate nel sistema in momenti successivi, portando ad un degrado della pulizia dei singoli moduli, che ora presentano alti livelli di accoppiamento e bassi livelli di coesione. Per questi motivi, l'aggiunta al sistema di un modulo per l'esportazione verso XML è stato un compito non facile e dispendioso in termini di tempo. Un ulteriore motivo per la scelta di Coq è stato l'elevatissima espressività di CIC, che viene ripagata con un'alta complessità del sistema logico e conseguente difficoltà nell'interpretazione dei l-termini. Una tecnica per rendere comprensibili le prove di Coq, quindi, potrebbe essere probabilmente applicata con successo anche a sistemi meno complessi.

Nella prossima sezione introdurremo in dettaglio la sintassi e le regole di riduzione, convertibilità e tipaggio di CIC. Nelle successive presenteremo alcune caratteristiche di Coq e daremo qualche esempio d'utilizzo del sistema.

2.1 Il Calcolo delle Costruzioni (Co)Induttive

Fra diversi calcoli funzionali tipati, come il l-calcolo, e le logiche basate su natural deduction esiste un isomorfismo, noto con il nome di corrispondenza di Curry-Howard. I due sistemi più semplici messi in relazione sono la logica proposizionale e il l-calcolo tipato semplice [GLT89]: alle proposizioni corrispondono i tipi del l-calcolo; agli alberi di prova, i l-termini; la b-riduzione e l'eliminazione dei tagli completano l'isomorfismo. Si dice che un termine t abita un tipo T se t ha tipo T. In altre parole, T è abitato da t se e solamente se t è una dimostrazione di T. Affinché il sistema sia consistente, è necessario che un particolare tipo ^ non sia abitato o, equivalentemente, che esista un tipo disabitato.

Le logiche e conseguentemente i calcoli possono essere classificati in base alla loro espressività. Questa può essere aumentata in due maniere: introducendo nuovi oggetti (nuovi tipi) oppure potenziando gli algoritmi (le astrazioni). Per esempio, il passaggio dalla logica proposizionale al calcolo dei predicati è ottenuto introducendo nuovi oggetti; quello dalla logica del primo ordine alle logiche di ordine superiore introducendo nuove astrazioni. Sfruttando la prima tecnica, diventa possibile definire direttamente tipi di dati astratti, sia induttivi che coinduttivi, specificandone i costruttori (le osservazioni nel caso coinduttivo) e i distruttori, ovvero i principi di (co)ricorsione [Gim94]. La seconda tecnica, invece, permette la definizione di termini e tipi con gradi sempre maggiori di dipendenza, che si rispecchiano nel livello di polimorfismo del calcolo: se nel l-calcolo tipato semplice l'unica astrazione permessa è quella dei termini sui termini (l-astrazione), nei l-calcoli del cubo di Barendregt ([Bar92]), in corrispondenza con i sistemi di tipi puri (PTS), si rendono possibili astrazioni di termini sui tipi e/o di tipi sui tipi e/o di tipi sui termini (tipi dipendenti).

Un ulteriore elemento che discrimina i sistemi logici è la predicatività. Nei sistemi predicativi esiste un ordinamento parziale fra i tipi, che impedisce le astrazioni su quelli maggiori; in quelli impredicativi non esiste questo vincolo. La predicatività è un concetto strettamente connesso a quello di costruttività, in quanto, nei sistemi impredicativi, è possibile applicare funzioni a tipi non ancora definiti al momento della loro dichiarazione. In altre parole, la predicatività non permette la definizione di un oggetto d che riferisca una collezione D della quale d sia un elemento, evitando circoli viziosi. Nonostante sia possibile costruire sistemi logici impredicativi consistenti, è molto facile ottenere sistemi inconsistenti, come mostra Coquand in [Coq86] applicando il paradosso di Girard a numerosi sistemi impredicativi.

Agli inizi degli anni '70, sono emersi due logical framework, basati sulla teoria dei tipi, che hanno pesantemente influenzato la definizione di CIC. Il primo, la Teoria Intuizionistica dei Tipi di Martin-Löf, cerca una nuova fondazione della matematica basandosi su principi costruttivi. Il sistema, predicativo, è caratterizzato da una grande espressività nella definizione di tipi induttivi. Il secondo, il l-calcolo polimorfico F_w di Girard, è un calcolo funzionale impredicativo molto espressivo, nel quale possono essere rappresentate prove di teoremi scritti in logiche di ordine superiore. I tipi induttivi possono venire codificati ricorrendo al polimorfismo (es. i numeri naturali vengono codificati ricorrendo ai numerali di Church). Nel 1985, combinando le idee di entrambi i sistemi in un'estensione di ordine superiore del linguaggio del sistema Automath, Coquand presenta la prima versione del Calcolo delle Costruzioni (CoC). In questo sistema logico si possono realizzare potenti assiomatizzazioni, ma i tipi induttivi non possono essere definiti direttamente, ma solo codificati uniformemente in modo funzionale, a scapito della semplicità e dell'efficienza implementativa. Nel 199 Luo [Luo90] ottiene un'estensione consistente del sistema, chiamata Calcolo delle Costruzioni Esteso, che ammette impredicatività sulle proposizioni, di tipo Prop, e predicatività per i tipi di dati, di tipo Type_i. Il formalismo viene nuovamente esteso nel 1989 da T. Coquand e C. Pauline-Mohring con l'aggiunta di tipi induttivi primitivi, ottenendo il Calcolo delle Costruzioni Induttive [Coq86].

In seguito all'implementazione di Coq, numerose modifiche sono state proposte al sistema logico, fra cui le definizioni mutuamente induttive, i tipi coinduttivi e gli operatori primitivi di analisi per casi e definizione di funzioni per (co)punto fisso. Poiché le diverse estensioni sono state date separatamente, non esiste oggi nessun articolo noto all'autore in cui siano date la sintassi e le regole di tipaggio per l'intero calcolo: i due lavori più importanti sono la tesi di dottorato di Werner [Wer94], che descrive la versione originaria di CIC, e l'articolo di Gimenez [Gim94] in cui vengono introdotte l'analisi per casi e le definizioni per (co)ricorsione. Nel prossimo paragrafo e nei successivi, quindi, verranno descritte la sintassi e le regole di riduzione, convertibilità e tipaggio di CIC come ricavate dall'autore attingendo a diverse fonti, compreso il codice di Coq. In particolare, ringrazio sentitamente Hugo Herbelin che, tramite comunicazioni private, mi ha enormemente aiutato a ricostruire alcune delle regole più complesse. Gli eventuali errori presenti sono da attribuirsi esclusivamente a mie incomprensioni.

2.1.1 La sintassi

In tutto il capitolo, con un piccolo abuso di notazione, le successioni di qualsiasi genere indiciate da 1 a n potranno essere vuote, salvo indicazioni contrarie.

Siano

V una famiglia numerabile di nomi di variabili, x,y,z,... Î V.
C una famiglia numerabile di nomi di costanti, c,c₁,...,c_n Î C.
I una famiglia numerabile di nomi di tipi (co)induttivi, i,i₁,...,i_n Î I.
K una famiglia numerabile di nomi di costruttori di tipi (co)induttivi,
k,k₁,...,k_n,k₁¹,...,k_n_₁¹,...,k₁^m,..., k_n_{_m}^m Î K.

I termini ben formati, che verranno indicati con t,f,u,T,U,N,M, sono definiti induttivamente in tabella 2.1.1,

t ::= x identificatori

| c costanti

| i tipi (co)induttivi

| k costruttori di tipi (co)induttivi

| Set | Prop | Type(j) sort

| t t applicazione

| l x:t.t l-astrazione

| P x:t.t prodotto dipendente

| <t>CASES_i t OF analisi per casi

k₁

x
Þ t | ... | k_n

x
Þ t

END

| FIX_l {x/n₁ : t := t ; ... ; x/n_m : t := t} definizione per punto fisso

| COFIX_l {x : t := t ; ... ; x : t := t} definizione per co-punto fisso

Table 2.1: Sintassi dei termini di CIC

dove m,n₁,...,n_m,j e l sono interi positivi, l è al più uguale al numero di funzioni definite nel proprio (CO)FIX e x è una sequenza, eventualmente vuota, di identificatori, la cui lunghezza verrà indicata con |x|. Con s,s₁,...,s_n verranno indicate le sort. Si utilizzerà la notazione T₁ ® T₂ per P x:T₁.T₂ quando x non compare libera in T₂. Il tipo induttivo i nel CASES è ridondante, in quanto tipi induttivi distinti hanno costruttori distinti, e viene indicato per maggiore chiarezza.

Si noti che, in CIC, non esistono distinzioni fra tipi e termini.

Le parentesi tonde verranno utilizzate per rendere concreta la sintassi astratta, con l'usuale convenzione per la quale l'applicazione è associativa a sinistra e la l-astrazione a destra.

Nella l-astrazione e nei tipi dipendenti la x è legata nei corpi, ovvero dopo il punto. Analogamente, le x sono legate nelle definizioni per (co)punto fisso nei corpi delle funzioni del proprio blocco, ovvero dopo i simboli di assegnazione, e dopo le doppie frecce nella definizione per casi. Le definizioni di variabili libere, di a-conversione e di sostituzione sono quelle usuali.

Alcune forme di termini hanno usi particolari. Gli arity, definiti induttivamente nel modo seguente e indicati con A,B,A₁,...,A_n, sono i tipi dei tipi induttivi. I tipi di costruttori per i, indicati con C(i),C₁(i),...,C_n(i) o semplicemente con C,C₁,...,C_n quando non c'è possibilità di confusione, sono i possibili tipi dei costruttori del tipo induttivo i.

A ::= s | P x : t.A

C(i)	::=	(i t₁ ... t_h)
	\|	P x : t.C(i)
	\|	T ® C(i)

sotto le condizioni che

tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrano liberi in t,t₁,...,t_h
i ¹ x
Se i dipende da k parametri e il suo arity è P x₁:T₁... P x_l : T_l.s, allora h = k + l
i occorra solo strettamente positivamente in T

dove i occorre solo strettamente positivamente in T se

tutti i tipi mutuamente induttivi con i non occorrono in T oppure
T = P x : T₁.T₂ e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono liberi in T₁ e i occorre solo strettamente positivamente in T₂ oppure
T = (i' t₁... t_n) e i' è un tipo mutuamente induttivo con i e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono liberi in t₁ ... t_n oppure
T = (i' t₁ ... t_n) e i', diverso da i, è l'unico tipo mutuamente induttivo del suo blocco, dipendente da m < n parametri, e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono liberi in t_m+1,...,t_n e occorrono solo positivamente in modo debole in tutti i tipi dei costruttori di i'

dove i occorre solo positivamente in modo debole in C, tipo di costruttore di i', se

C = (i t₁ ... t_n) oppure
C = T ® C' e i appare solo positivamente in modo debole in C' e i appare solo strettamente positivamente in T dove i' venga sostituito con una variabile x fresca oppure
C = P x:T.C' e i occorre solo positivamente in modo debole in C' e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono in T dove i' venga sostituito con una variabile x fresca

2.1.2 Le riduzioni e la convertibilità

Prima di dare le regole di riduzione di CIC, è necessario definire i contesti e gli ambienti.

Contesti e ambienti

Un contesto G è una lista ordinata di dichiarazioni di variabili (e loro tipi) e prende la forma [(x₁ : T₁),...,(x_n : T_n)] dove le x_i sono tutte distinte. Per indicare che (x:T) è un elemento di G scriveremo (x:T)ÎG. x Î G significa $ T.(x:T) Î G. [] denota il contesto vuoto.

Un ambiente E è una lista ordinata di dichiarazioni di (tipi e corpi di) costanti e di tipi mutuamente (co)induttivi e prende la forma [w₁,...,w_n] dove w_j ha la forma c : T := t (dichiarazione di costante c) oppure la forma

P x₁:U₁... P x_h:U_h.

{i₁ : A₁ := {k₁¹ : C₁¹ ; ... ; k

n₁

: C

n₁

} ;

... ;

i_m : A_m := {k₁^m : C₁^m ; ... ; k

n_m

: C

n_m

}

}_(CO)IND

(dichiarazione del blocco di tipi mutuamente (co)induttivi i₁,...,i_m, dipendenti dai parametri x₁,...,x_h, i cui costruttori sono k₁¹,...,k_n_{_m}^m) dove x₁,...,x_h sono legati in A₁,...,A_m,C₁¹,...,C_n_{_m}^m e i₁,...,i_m possono apparire in C₁¹,...,C_n_{_m}^m e (CO)IND deve essere IND per i tipi induttivi e COIND per quelli coinduttivi.

Tutti i nomi delle costanti definite in un ambiente debbono essere distinti, cosí come quelli dei tipi mutuamente (co)induttivi e dei loro costruttori. Le notazioni per l'appartenenza e l'ambiente vuoto sono le stesse usate per i contesti. Infine, i Î E e k Î E sono definiti in maniera ovvia.

Le regole per l'introduzione di definizioni nell'ambiente e nei contesti verranno date nel paragrafo 2.1.3 essendo mutuamente definite con le regole di tipaggio di CIC. Per la sintassi utilizzata in Coq il lettore è rimandato al manuale utente [BBC⁺97].

b-riduzione, d-riduzione, i-riduzione e unfolding (o espansione)

In CIC è necessario definire quattro tipi di riduzioni, chiamate b-riduzione, i-riduzione, d-riduzione e unfolding (o espansione). Le prime due corrispondono all'eliminazione dei tagli per l'implicazione ed i tipi induttivi. La terza è standard nello studio della semantica dei linguaggi di programmazione. La quarta si incontra, in forme talvolta meno ristrette, nei linguaggi di programmazione lazy. [b-riduzione] È quella standard: (l x:T.M) N _bM{N/x} con la side condition, usualmente lasciata implicita, che le variabili libere di N non siano catturate in M{N/x}. [i-riduzione] Equivale alla b-riduzione per i tipi (co)induttivi. Nell'ambiente E contenente la dichiarazione

P x₁:U₁... P x_h:U_h.

{i₁ : A₁ := {k₁¹ : C₁¹ ; ... ; k

n₁

: C

n₁

} ;

... ;

i_m : A_m := {k₁^m : C₁^m ; ... ; k

n_m

: C

n_m

}

}_(CO)IND

si ha

<T>CASES

i_l

(k_j^l t₁ ... t_h t'₁ ... t'

n_j

) OF

k₁^l

x¹

Þ f₁ | ... | k_n^l

xⁿ

Þ f_n

END

f_j{t'₁/x₁ ; ... ; t'

n_j

}

dove l Î {1,...,m}, " l Î {1,...,n_j}.|x_l| = n_l e x^j = (x₁,...,x_n_{_j}) [d-riduzione] È quella standard: nell'ambiente E contenente la dichiarazione c:T:=t si ha c _dt. [unfolding o espansione] Esiste in due varianti, per la ricorsione e per la co-ricorsione. Siano FIX^j un'abbreviazione sintattica per

FIX_j {x₁/n₁ : T₁ := f₁ ; ... ; x_m/n_m : T_m := f_m}

e COFIX^j un'abbreviazione sintattica per

COFIX_j {x₁ : T₁ := f₁ ; ... ; x_m : T_m := f_m}

Si ha

(FIX^j t₁ ... t

n_j - 1

k) _FIX (f_j{FIX¹/x₁ ; ... ; FIX^m/x_m} t₁... t

n_j - 1

<T>CASES_i (COFIX^j t₁ ... t_h) OF

k₁

x¹

Þ f₁ | ... | k_n

xⁿ

Þ f_n

END

_COFIX

<T>CASES_i (f_j{COFIX¹/x₁ ; ... ; COFIX^m/x_m} t₁ ... t_h) OF

k₁

x¹

Þ f₁ | ... | k_n

xⁿ

Þ f_n

END

Si noti che le due regole sono casi ristretti della regola di unfolding standard. Le restrizioni, che sono differenti e giocano ruoli duali nei due casi, combinate con le condizioni GD (Guarded by Destructors) e la duale GC (Guarded by Constructors) definite rispettivamente a pagina 39 e 37, assicurano la terminazione del processo di riduzione, ovvero la normalizzazione forte di CIC. Questa, a sua volta, permette di dimostrare che, dopo la riduzione, ogni termine ha una forma normale. Poiché la forma normale³ di un abitante di un tipo di dato induttivo ha come testa un costruttore del tipo di dato e poiché il tipo induttivo False è privo di costruttori, se ne conclude che, se il sistema è fortemente normalizzabile, allora è anche logicamente consistente, ovvero False è privo di abitanti.

La convertibilità

La convertibilità =_bdi fra termini di CIC è semplicemente definita come la chiusura riflessiva, simmetrica, transitiva e per contesti⁴ delle regole di riduzione _b,_d,_i,_FIX e _COFIX.

La proprietà di normalizzazione forte⁵ assicura la decidibilità della convertibilità. Questa, a sua volta, garantisce la decidibilità del type-checking, definito nella prossima sezione.

2.1.3 Le regole di tipaggio

Diamo ora le regole di tipaggio per i termini di CIC definendo mutuamente due judgement. Il primo, E[G] |- t : T, asserisce che t, in un ambiente E e in un contesto G dipendente da E, ha tipo T. Il secondo, WF(E)[G], asserisce che E è un ambiente valido, ovvero contenente solo definizioni di costanti e di tipi mutuamente (co)induttivi ben tipati, e che G è un contesto valido in E, ovvero contenente solo dichiarazioni di variabili il cui tipo è ben tipato.

Regole del Calcolo delle Costruzioni

WF-Empty

WF([])[[]]

WF-Var

E[G] |- T:s s Î {Prop,Set,Type(i)} x G

WF(E)[G,(x:T)]

WF-Const

E[[]] |- T:s E[[]] |- t:T c E

WF(E;c : T := t)[[]]

Ax-Prop

WF(E)[G]

E[G] |- Prop:Type(n)

Ax-Set

WF(E)[G]

E[G] |- Set:Type(n)

Ax-Acc

WF(E)[G] n < m

E[G] |- Type(n):Type(m)

Var

WF(E)[G] (x:T)Î G

E[G] |- x:T

Const

WF(E)[G] (c:T:=t)Î E

E[G] |- c:T

Prod-SP

E[G] |- T : s₁ E[G,(x:T)] |- U : s₂ s₁ Î {Prop,Set} s₂ Î {Prop,Set}

E[G] |- P x:T.U : s₂

Prod-T

E[G] |- T : Type(n₁) E[G,(x:T)] |- U : Type(n₂) n₁ £ n n₂ £ n

E[G] |- P x:T.U : Type(n)

Lam

E[G] |- P x:T.U : s E[G,(x:T)] |- t : U

E[G] |- l x:T.t : P x : T.U

App

E[G] |- t:P x:U.T E[G] |- u : U

E[G] |- (t u) : T{u/x}

Conv

E[G] |- T₁ : s E[G] |- t:T₂ E[G] |- T₁ =

bdi

T₂

E[G] |- t : T₁

Regole per i tipi (co)induttivi

Per brevità, in tutte le regole che seguono, con * viene indicata la seguente dichiarazione di tipi mutuamente (co)induttivi:

P x₁:U₁... P x_h:U_h.

{i₁ : A₁ := {k₁¹ : C₁¹ ; ... ; k

n₁

: C

n₁

} ;

... ;

i_m : A_m := {k₁^m : C₁^m ; ... ; k

n_m

: C

n_m

}

}_(CO)IND

WF-Ind

(E[[]] |- (P x₁:U₁ ... P x_h:U_h.A_j : s_j)

j=1,...,m

(E[[y₁:A₁^* ; ... ; y_m:A_m^*]] |- C_l^j{y₁/i₁ ; ... ;y_m/i_m} : s_l^j)

j=1,...,m ; l=1,...,n_j

i₁,...,i_m,k₁¹,...,k

n_m

i₁,...,i_m,k₁¹,...,k

n_m

distinti

WF(E,*)[[]]

dove A_j^* = P x₁:U₁...P x_h : U_h.A_j per j Î {1,...,m}

e con il vincolo sintattico che in C₁¹,...,C_n_{_m}^m i primi h argomenti

delle applicazioni la cui testa è uno dei tipi induttivi i₁,...,i_m siano x₁,...,x_h

Ind

WF(E)[G] * Î E

E[G] |- i_j:P x₁:U₁... P x_h:U_h.A_j

se j £ m

Constr

WF(E)[G] * Î E

E[G] |- k_l^j:P x₁:U₁... P x_h:U_h.C_l^j

se	j £ m
e	l £ n_j

Case

* Î E E[G] |- t:(i_l t₁... t_h t'₁... t'_s)

E[G] |- T : A [(i_l t₁... t_h):A_l{t₁/x₁ ; ... ; t_h/x_h}|A]

(E[G] |- f_j : D{C_j^l{t₁/x₁ ; ... ; t_h/x_h},T,(k_j^l t₁ ... t_h)})

j=1,...,n_l

E[G] |-

æ
ç
ç
ç
ç
ç
ç
è

<T>CASES

i_l

t OF

k₁^l

x¹

Þ f₁ | ... | k

n_l

xⁿ

Þ f

n_l

END

ö
÷
÷
÷
÷
÷
÷
ø

: (T t'₁... t'_s t)

Fix

(E[G] |- T_l:s_l)

l = 1,...,m

(E[G,(x₁:T₁),...,(x_m:T_m)] |- f_l : T_l)

l = 1,...,m

(GD

{x₁,...,x_m,n₁,...,n_m,x,[],T})

l = 1,...,m

E[G] |- FIX_j {x₁/n₁ : T₁ := f₁ ; ... ; x_m/n_m : T_m := f_m} : T_j

dove f_j = l y₁:T'₁ ... l y_n_{_j}_-1:T'_n_{_j}_-1. l x:(i t₁ ... t_n)T

CoFix

(E[G] |- T_l:s_l)

l = 1,...,m

(E[G,(x₁:T₁),...,(x_m:T_m)] |- f_l : T_l)

l = 1,...,m

(GC

₀{x₁,...,x_m,f_l})

l = 1,...,m

E[G] |- COFIX_j {x₁ : T₁ := f₁ ; ... ; x_m : T_m := f_m} : T_j

Restano da definire le condizioni GD,GC e [T:A|B] e l'operatore D{.,.,.}:

[D{.,.,.}] Sia T l'insieme dei termini di CIC. Si definisce D : {C/C è un tipo di costruttore per i} × T × T ® T per induzione strutturale sul primo argomento:

D{(i t₁ ... t_n),T,t}	=	(T t₁ ... t_n t)
D{(x:T)C,T,t}	=	P x:t.D{C,T,(c x)}

In CIC non viene permesso di eliminare un tipo (co)induttivo di un arity qualsiasi per ottenere un altro tipo. La prima motivazione è la distinzione fra ciò che è computazionalmente rilevante in fase di estrazione (ovvero ciò che ha arity Set) e ciò che non lo è (che ha arity Prop): poiché l'informazione computazionalmente non rilevante viene eliminata in fase di esportazione, diventa impossibile eliminare un tipo non informativo per ottenerne uno informativo, a meno che questo non sia un tipo singoletto (singleton), ovvero un tipo (co)induttivo con un solo costruttore i cui parametri siano tutti non informativi. La seconda motivazione è legata all'impredicatività: come viene mostrato da Coquand in [Coq86], permettendo l'eliminazione di un tipo impredicativo a favore di uno predicativo, diventa possibile codificare il paradosso di Burali-Forti nella teoria dei tipi. In [Wer94] viene spiegato come evitare il paradosso di Coquand in presenza di tipi induttivi primitivi, limitando l'eliminazione di tipi all'eliminazione forte, che è l'eliminazione verso Type di tipi induttivi ``piccoli'' in Set. Diamo, quindi, la definizione di tipo (co)induttivo piccolo seguita dalla condizione di ammissibilità dell'eliminazione di un tipo (co)induttivo in favore di un altro: [Tipo (co)induttivo piccolo] Un costruttore di un tipo (co)induttivo si dice piccolo se ha un tipo della forma P x₁:T₁ ... P x_h:T_h.(i t₁ ... t_n) dove T₁,...,T_h hanno tutti tipo Set o Prop. Un tipo (co)induttivo si dice piccolo quando tutti i suoi costruttori sono piccoli. [Condizione di eliminazione di un tipo (co)induttivo]La condizione [T:A|B] è definita come la più piccola relazione che soddisfa le seguenti regole:
Prod

[(i x):A'|B'

[i:P x : A.A' | P x : A.B']

Prop-Prop

[i:Prop|i ® Prop]

Prop-Singleton

i è un tipo singoletto

[i:Prop | i ® Set]

Set-PS

s Î {Prop,Set}

[i: Set | i ® s]

Set-Small (eliminazione forte)

i è un tipo (co)induttivo piccolo s = Type(i)

[i: Set | i ® s]

Type

s Î {Prop,Set,Type(j)}

[i: Type(l) | i ® s]

[Condizione GD(Guarded by Destructors)] Scopo diquesta condizione è assicurare la normalizzazione forte in presenza di definizioni di funzioni per punto fisso, le quali debbono specificare l'argomento che decresce ad ogni iterazione. In pratica, la condizione richiede che ogni chiamata ricorsiva sia effettuata su un termine ``più corto'' come argomento che deve decrescere, ovvero su un argomento ottenuto dall'applicazione di uno o più distruttori al parametro decrescente dato in input. La normalizzazione forte è ottenuta combinando la GD e i vincoli dati sull'unfolding con l'invariante che la forma normale degli abitanti di un tipo induttivo abbiano al più un numero finito di costruttori. La condizione GD{x₁,...,x_m,n₁,...,n_m,x,l,T} dove x₁,...,x_m sono le funzioni ricorsivamente definite per punto fisso, n₁,...,n_m gli indici dei loro parametri decrescenti, l l'insieme, inizialmente vuoto, di variabili che possono essere usate come parametri decrescenti e T il termine nel quale le chiamate devono essere guardate, è definita per induzione sulla struttura di T secondo le regole seguenti, in cui, nelle chiamate ricorsive, vengono omessi tutti i parametri, tranne gli ultimi due, che sono gli unici non costanti. La condizione vale:

se T = P z : M.N e GD{l,M} e GD{l,N} valgono
se T = l z : M.N e GD{l,M} e GD{l,N} valgono
se T = (x_j t₁... t_n_{_j}_{- 1} t_n_{_j} t_n_{_j}_{+ 1}... t_n) se (GD{l,t_h})_h=1,...,n vale eRS{x₁,...,x_m,n₁,...,n_m,x,l,t_j} vale dove j Î {1,...,m}
se T = (t t₁ ... t_n) dove t {x₁,...,x_m} e (GD{l,t_h})_h=1,...,n vale
se T è una variabile o una costante o un tipo induttivo o un costruttore di un tipo induttivo o una sort
se T = FIX_j {y₁/n'₁ : T₁ := f₁ ; ... ; y_d/n'_d : T_d := f_d} e (GD{l,T_h})_h=1,...,d e (GD{l,f_h})_h=1,...,d valgono
se T = COFIX_j {y₁ : T₁ := f₁ ; ... ; y_d : T_d := f_d} e (GD{l,T_h})_h=1,...,d e (GD{l,f_h})_h=1,...,d valgono
se T= (

<U>CASES_i t OF

k₁

x¹
Þ f₁ | ... | k_d

x^d
Þ f_d

END
) e vale una delle seguenti tre condizioni mutuamente esclusive:
- i è un tipo induttivo e t = (z t₁ ... t_r) dove z Î l È {x} e valgono GD{l,U}, GD{l,t} e (GD{l È PR{k_h,x^h},G'_h})_h=1,...,d dove PR{k_h,(x₁,...,x_r)} = {x_j / il j-esimo parametro del costruttore k_h è ricorsivo in uno dei tipi induttivi mutuamente ricorsivi con il suo tipo} e G_h = l y₁:t₁ ... l y_n_{_h}:t_n_{_h}.G'_h dove n_h è il numero dei parametri del costruttore k_h.
- i è un tipo coinduttivo e valgono GD{l,U}, GD{l,t} e (GD{l,f_h})_h=1,...,d
- i è un tipo induttivo, non vale t = (z t₁ ... t_r) dove z Î l È {x} e valgono GD{l,U}, GD{l,t} e (GD{l,f_h})_h=1,...,d

dove RS è la condizione definita come segue: [Condizione RS(Really Smaller)]La condizione RS controlla che il termine passato come parametro attuale nella posizione occupata dal parametro formale decrescente riduca, per ogni possibile istanziazione delle sue variabili libere, esclusivamente a termini più piccoli. La condizione RS{x₁,...,x_m,n₁,...,n_m,x,l,T} è definita per induzione sulla struttura di T secondo le regole seguenti, in cui, nelle chiamate ricorsive, vengono omessi tutti i parametri, tranne gli ultimi due, che sono gli unici non costanti. La condizione vale⁶

se T = (z t₁ ... t_n) dove z Î l
se T = l z : M.N e RS{l,M} e RS{l,N} valgono
se T = FIX_j {y₁/n'₁ : T₁ := f₁ ; ... ; y_d/n'_d : T_d := f_d} e (RS{l,f_h})_h=1,...,d vale
se T = COFIX_j {y₁ : T₁ := f₁ ; ... ; y_d : T_d := f_d} e (RS{l,f_h})_h=1,...,d vale
se T= (

<U>CASES_i t OF

k₁

x¹
Þ f₁ | ... | k_d

x^d
Þ f_d

END
) e vale una delle seguenti tre condizioni mutuamente esclusive:
- i è un tipo induttivo e t = (z t₁ ... t_r) dove z Î l È {x} e valga (RS{l È PR{k_h,x^h},G'_h})_h=1,...,d dove PR{k_h,(x₁,...,x_r)} = {x_j / il j-esimo parametro del costruttore k_h è ricorsivo in uno dei tipi induttivi mutuamente ricorsivi con il suo tipo} e G_h = l y₁:t₁ ... l y_n_{_h}:t_n_{_h}.G'_h dove n_h è il numero dei parametri del costruttore k_h.
- i è un tipo coinduttivo e vale (RS{l,f_h})_h=1,...,d
- i è un tipo induttivo, non vale t = (z t₁ ... t_r) dove z Î l È {x} e vale (RS{l,f_h})_h=1,...,d

[Condizione GC(Guarded by Constructors)] Scopo di questa condizione è assicurare la normalizzazione forte in presenza di definizioni di funzione per co-punto fisso (o massimo punto fisso). In pratica, la condizione richiede che il risultato di ogni chiamata ricorsiva venga utilizzato come argomento di un costruttore. In questo modo, il termine di tipo coinduttivo generato dalla chiamata di funzione ``si allunga'' ad ogni iterazione e si possono generare, con politica lazy, termini aventi un numero infinito di costruttori (osservazioni). Questo non è in contrasto con la normalizzazione forte, che viene ottenuta combinando la GC e i vincoli dati sull'unfolding (che è lazy) con l'invariante che il numero di distruttori (CASES) su tipi coinduttivi in un termine di CIC è sempre finito. Si noti la dualità con la GD. La condizione GC_h{x₁,...,x_m,T}, dove h Î {0,1}, x₁,...,x_m sono le funzioni definite per co-punto fisso e T è il termine nel quale le chiamate devono essere guardate, è definita per induzione sulla struttura di T secondo le regole seguenti, in cui i parametri x₁,...,x_m vengono omessi nelle chiamate ricorsive in quanto costanti. La condizione vale

se T = (z t₁ ... t_n) dove z Î {x₁,...,x_m} e h = 1 e x₁,...,x_m non occorrono libere in t₁,...,t_n
se T = (k t₁ ... t_n) dove k è il costruttore di un tipo coinduttivo che aspetta n parametri e per ogni j Î {1,...,n} se k è ricorsivo nel j-esimo parametro allora vale GC₁{t_j}, altrimenti x₁,...,x_m non occorrono libere in t_j
se T = (t t₁ ... t_n) dove t {x₁,...,x_m} e t non è un costruttore di un tipo coinduttivo e x₁,...,x_m non appaiono libere in t,t₁,...,t_n
se T è una sort o un tipo (co)induttivo o un costruttore di un tipo (co)induttivo
se T = l z:M.N e x₁,...,x_m non occorrono libere in M e vale GC_h{N}
se T = FIX_j {y₁/n'₁ : T₁ := f₁ ; ... ; y_d/n'_d : T_d := f_d} e x₁,...,x_m non occorrono libere in f₁,...,f_d,T₁,...,T_d
se T = COFIX_j {y₁ : T₁ := f₁ ; ... ; y_d : T_d := f_d} e x₁,...,x_m non occorrono libere in f₁,...,f_d,T₁,...,T_d
se T= (

<U>CASES_i t OF

k₁

x¹
Þ f₁ | ... | k_d

x^d
Þ f_d

END
) e x₁,...,x_m non occorrono libere in U e t e vale una delle due seguenti condizioni mutuamente esclusive:
- U = l z:M.(i t₁ ... t_r) dove i è un tipo coinduttivo e vale (GC_h{f_l})_{l Î {1,...,d}}
- U ¹ l z:M.(i t₁ ... t_r) dove i è un tipo coinduttivo e x₁,...,x_m non occorrono libere in f₁,...,f_d

2.2 Il Calcolo delle Costruzioni (Co)Induttive in Coq

Nella sezione precedente è stato introdotto formalmente CIC in modo che fosse al tempo stesso facilmente comprensibile e il più vicino possibile al sistema logico implementato in Coq. In questa sezione verranno descritte informalmente alcune importanti caratteristiche dell'implementazione di Coq a cui verrà fatto riferimento nei prossimi capitoli.

2.2.1 Alcune estensioni a CIC

Coq estende la versione di CIC descritta nella sezione precedente in diverse maniere e con diversi scopi. Vediamo solo le estensioni rilevanti nell'ambito di questa tesi:

Livelli degli universi impliciti

Chiamiamo livello dell'universo l'indice i in Type(i). Nonostante nella presentazione data di CIC gli universi (ovvero le sort Type) siano totalmente ordinati (dall'indice i), è in verità sufficiente un ordinamento parziale, generato essenzialmente dalle due side-condition della regola di tipaggio Prod-T. Per l'utente è estremamente oneroso indicare esplicitamente i livelli degli universi. Inoltre, dando nuove definizioni e teoremi, diventa necessario avere un meccanismo di interpolazione dei livelli. In altre parole, dati due tipi di sort Type(i) e Type(i+1), è possibile dare una definizione contenente un tipo di sort Type(j) che, durante il type-checking, deve soddisfare i due vincoli i < j e j < (i + 1). Se si vuole permetterne la definizione, è necessario ammettere livelli razionali oppure incrementare tutti i livelli degli universi maggiori di i + 1. Per questi motivi, in Coq si è scelto di inferire automaticamente il grafo dell'ordinamento parziale fra i livelli degli universi. L'utente, quindi, scriverà solamente Type e il sistema manterrà internamente il grafo dell'ordinamento parziale, verificando che non si formino cicli, che vengono generati da oggetti non ben tipati.

La soluzione, benché sembri la migliore adottabile, non è esente da problemi. Il principale è che, fissato un particolare ambiente E, può succedere che due termini t₁ e t₂ siano ben tipati se presi separatamente, ma non lo sia la loro congiunzione a causa di formazione di cicli nel grafo degli universi. Questo è un esempio minimale dovuto al Prof. Andrea Asperti e all'autore di questa tesi:

E	=	[	(P: *Type:= Type* ® *Type*),
			(Q: *Type:= Type* ® *Type*),
			(p:P := l x:*Type*.x),
			(q:Q := l x:*Type*.x)
		]

t₁ : Type := (p Q)

t₂ : Type := (q P)

La ciclicità è immediata per la totale simmetria fra i ruoli giocati da p,P e q,Q.

In casi non minimali, il vero problema per l'utente diventa capire quali siano le dichiarazioni che creano ciclicità. Per alleviarlo, una soluzione possibile è la creazione di un'opportuna interfaccia che permetta di visualizzare la parte problematica del grafo degli universi, esplicitando le dipendenze inferite dal sistema. In pratica, comunque, lo strano fenomeno si presenta raramente⁷.

Cast

I cast vengono introdotti in CIC per associare esplicitamente un tipo al termine corrispondente. Per la proprietà dell'esistenza di un tipo principale per ogni termine di CIC, l'operatore non aggiunge alcuna informazione ai termini⁸. Ciò nonostante, i cast possono essere utili durante la dimostrazione di un teorema: per esempio, è possibile scrivere tattiche per inferire alcuni termini; poterne specificare il tipo tramite un cast aumenta il numero dei casi in cui il termine può essere effettivamente inferito.

In Coq, il cast viene malamente utilizzato anche per aumentare le prestazioni del type-checker, inserendo cast nel l-termine per alcuni termini. In questo modo, quando il tipo del termine verrà successivamente richiesto, potrà essere recuperato dal cast. L'errore, riconosciuto dal team di sviluppo di Coq, è l'inserimento di questa informazione all'interno dei termini utilizzando un operatore che ha già un altro significato: il risultato è l'indistinguibilità dei due utilizzi del cast. Come conseguenza, è impossibile risalire al termine originale da quello ``decorato'', il quale è notevolmente più grande a causa dell'informazione ridondante. Quest'uso del cast verrà abbandonato nella versione 7 del sistema.

La sintassi concreta utilizzata in Coq per il cast di un termine t al tipo T è t::T. La regola di tipaggio è quella ovvia:

Cast

E[G] |- t : T₂ T₁ =

bdi

T₂

E[G] |- (t::T₁):T₁

Metavariabili

L'isomorfismo di Curry-Howard, che fa corrispondere alle prove completate i l-termini, può essere esteso per trattare prove non ancora terminate. L'estensione prevede l'aggiunta ai l-termini delle metavariabili, che corrispondono alle congetture non ancora provate. Le metavariabili, che appartengono ad una classe sintattica distinta da quella delle variabili, sono particolari termini che hanno un tipo, ma non hanno ancora un corpo. Completare la prova significa abitare il tipo di ogni metavariabile con un termine ben tipato nell'ambiente e nel contesto della metavariabile. La sintassi concreta per le metavariabili usata in Coq è ?i, dove i è un intero e viene data una mappa che ad ogni metavariabile associa il suo tipo. Utilizzando come sintassi astratta (? : T) per indicare una metavariabile il cui tipo è T, la regola di tipaggio diventa:

Meta

E[G] |- T : s

E[G] |- (?:T):T

Per esempio, se ?1 è una metavariabile che ha come tipo

P A:Prop.P B:Prop.A ® (A ® B) ® B

allora

l A:Prop. l B:Prop. l H:A. l H0:(A ® B). (?1 A B H H0)

abita

P A:Prop.P B:Prop.A ® (A ® B) ® B

In Coq, in ogni momento può esistere una sola prova non terminata. È, però, possibile e auspicabile ammettere l'esistenza contemporanea di più prove non terminate. Questo corrisponde alla possibilità, negata in Coq, di introdurre nell'ambiente termini contenenti metavariabili. Con questa estensione, una prova si dice non terminata se contiene almeno una metavariabile, oppure se dipende transitivamente da una costante che ne contiene.

Termini impliciti

I l-termini contengono molta informazione ridondante. Come conseguenza, diventa possibile scrivere una procedura di type-inference che permette di omettere alcuni dei tipi contenuti in un termine. Questa è implementata in Coq, dove i termini lasciati impliciti vengono indicati con un punto interrogativo o, talvolta, addirittura omessi. Esistono, quindi, due differenti scelte: aggiungere i termini impliciti a CIC, come è necessario fare con le metavariabili, oppure evitare di farlo. In quest'ultimo caso, adottato da Coq, i termini impliciti vengono, almeno concettualmente, inferiti prima di effettuare il type-checking e il type-checker non viene modificato. La separazione del motore di type-inference da quello di type-checking permette di non basare la correttezza dell'intero sistema sul primo, che diventa un'estensione non critica. Al tempo stesso, però, non viene aumentata l'efficienza del type-checker, nè diminuita l'occupazione in spazio dei l-termini inferiti. L'altro approccio è stato adottato per un diverso sistema logico in [NL98], dove i termini impliciti vengono aggiunti al sistema logico e il type-checker viene integrato con la type-inference, ottenendo notevolissimi risultati: sia la dimensione delle prove che il tempo richiesto per il type-checking sono in O(n^0.62) dove n è il valore ottenuto senza l'introduzione dei tipi impliciti e le costanti nascoste sono basse.

2.2.2 Particolarità implementative

Come consuetudine in tutti i sistemi basati sull'isomorfismo di Curry-Howard a partire da Automath, le variabili vengono internamente rappresentate ricorrendo agli indici di de Brujin. In Coq, inoltre, questi vengono utilizzati anche per denotare le entità definite in maniera mutuamente induttiva all'interno del loro blocco. Per esempio, la rappresentazione interna della definizione

P A : Prop. {

tree : Set := {

emptyT : (tree A) ;

node:A ® (forest A)

} ;

forest : Set := {

emptyF : (forest A) ;

cons:(tree A)® (forest A) ® (forest A)

}

è la seguente

P Prop. {

tree : Set := {

emptyT : (1 3) ;

node:3 ® (2 3)

} ;

forest : Set := {

emptyF : (2 3) ;

cons:(1 3)® (2 3) ® (2 3)

}

Un'altra particolarità dell'implementazione di Coq è la rappresentazione interna dell'operatore CASES, che si presenta, senza alcun ragionevole motivo, in due forme distinte, una generale e una esclusivamente per l'eliminazione non dipendente. Nel secondo caso, il tipo dei rami del CASES, indicato fra parentesi angolose, è privo della l-astrazione sul termine su cui si effettua l'analisi per casi; per distinguere le due rappresentazioni, l'unico modo è analizzare la struttura del tipo del tipo dei rami. In entrambi i casi, la ridondanza fra il tipo induttivo e i suoi costruttori viene eliminata a favore del primo, l-astraendo i rami del CASES sui parametri dei costruttori. Pertanto, il seguente termine

l n : nat.

<l z:nat.nat>CASES_nat n OF

O Þ O | (S m) Þ m

END

può venire rappresentato internamente come l'eliminazione dipendente

l nat.

<l nat.nat>CASES_nat 1 OF

O | l nat.1

END

o come quella non dipendente

l nat.

<nat>CASES_nat 1 OF

O | l nat.1

END

2.2.3 Il livello degli oggetti, ovvero la manipolazione degli ambienti

Definiamo oggetti tutte le entità che possono essere presenti in un ambiente. In CIC, esse sono le definizioni di costanti, introdotte con la regola WF-Const, e le definizioni di tipi mutuamente (co)induttivi, introdotte con la regola WF-Ind. Coq non solo introduce una sintassi concreta per queste regole, ma raffina la classe delle costanti in definizioni e teoremi e introduce due nuovi tipi di oggetti, gli assiomi e le variabili. Questi ultimi hanno un tipo, ma sono privi di corpo. Pertanto, non sono soggetti a d-riduzione e hanno, come regola di introduzione, la seguente:

WF-AxVar

E[[]] |- T:s c E

WF(E;c : T)[[]]

La differenza fra assiomi e variabili verrà spiegata nel paragrafo 2.2.4. La differenza fra teoremi e definizioni è invece nel loro grado di opacità: i teoremi sono, di norma, opachi, ovvero su di essi non viene effettuata d-espansione, secondo il principio della proof-irrilevance. Le definizioni, invece, sono, di norma, trasparenti, ovvero soggette a d-espansione. È possibile, e talvolta utile, modificare l'opacità di un termine, per esempio per formulare un teorema su una prova o per costruire tipi di dati astratti, le cui definizioni non sono accessibili se non nel corpo di determinate funzioni.

2.2.4 Le sezioni e il meccanismo di cottura

Dowek ha introdotto in Coq le sezioni e le variabili, ovvero un meccanismo per strutturare le teorie matematiche in blocchi al cui interno vengono utilizzati assiomi che vengono ``scaricati'' all'uscita dal blocco. Il meccanismo è ben noto ai matematici: per esempio, quando si formulano teoremi nella teoria dei gruppi, le proprietà che li caratterizzano vengono date come assiomi; i teoremi vengono poi applicati a qualsiasi struttura matematica che è provata essere un gruppo, come l'insieme dei numeri naturali. L'operazione di scaricamento consiste nell'astrarre, tramite P, tutti i tipi dipendenti da una variabile c rispetto a c stessa; conseguentemente, tutti i termini dipendenti dalla variabile scaricata vengono l-astratti sulla prova della variabile e tutti i termini che da lei dipendevano devono essere applicati alla prova. Le variabili vengono invece eliminate, in quanto il loro scope è la sezione che le contiene. Al livello degli oggetti, l'operazione viene chiamata cottura.

Un semplice esempio, utilizzando la sintassi di Coq, sarà chiarificatore. Si consideri la seguente teoria:

Section S.
 Variable A : Prop.
 Variable B : Prop.

 Theorem AB_A_B : (A -> B) -> A -> B.
 Proof.
  Exact [ab:(A ->B)][a:A](ab a).
 Qed.

 Theorem A_AB_B : A -> (A -> B) -> B.
 Proof.
  Exact [a:A][ab:(A->B)](AB_A_B ab a).
 Qed.
End S.

La sintassi utilizzata da Coq dovrebbe essere autoesplicativa, premesso che ``[x:T]t'' viene usato per ``l x:T.t'', ``(x:T)t'' per ``P x:T.t'' e ``->'' per ``®''. Dopo la chiusura della sezione (con ``End S''), il suo contenuto viene cucinato. Il risultato è lo stesso che si sarebbe ottenuto dando le seguenti definizioni:

Theorem AB_A_B : (A:Prop)(B:Prop)(A -> B) -> A -> B.
Proof.
 Exact [A:Prop][B:Prop][ab:(A ->B)][a:A](ab a).
Qed.

Theorem A_AB_B : (A:Prop)(B:Prop)A -> (A -> B) -> B.
Proof.
 Exact [A:Prop][B:Prop][a:A][ab:(A->B)](AB_A_B A B ab a).
Qed.

2.2.5 Nomi e section path

Le sezioni contengono una lista ordinata formata da definizioni di oggetti o da altre sezioni. In questo modo, ad una sezione corrisponde in maniera naturale un albero, i cui nodi interni sono sezioni e le cui foglie sono (definizioni di) oggetti. Una teoria di Coq (un file ``.v'') altro non è che una sezione avente come nome quello del file. Caricare diverse teorie nell'ambiente significa, quindi, costruire una foresta. Come conseguenza, risulta immediato associare ad ogni oggetto un section path, ovvero un identificatore univoco ottenuto concatenando, con opportuni delimitatori, tutti i nomi delle sezioni nel cammino radice-foglia e giustapponendoci il nome dell'oggetto.

In verità, però, la chiusura di una sezione e la conseguente cottura di tutti i suoi oggetti la distruggono, spostando tutte le sue foglie al livello superiore ed accorciandone il section path. In questo modo, i section-path non vengono più utilizzati per identificare gli oggetti, che restano completamente individuati dal loro nome, e il modello ad albero, che è estremamente naturale, diventa non più valido. Per esempio, in quello che segue, la definizione di A data nella sezione S2 non è valida perché entra in conflitto con quella data nella sezione S1:

Section S1.
 Axiom A : Prop.
End S1.

Section S2.
 Axiom A : Prop.
End S2.

Ovviamente, il problema si presenta anche fra definizioni date in teorie differenti. Poiché è impensabile non creare conflitti fra i nomi definiti in teorie scritte da autori diversi, gli sviluppatori di Coq hanno scelto di applicare un meccanismo di shading fra le teorie: la definizione data nell'ultima teoria caricata è l'unica accessibile.

Anticipiamo subito che, durante la procedura di esportazione da Coq, abbiamo scelto di identificare tutti gli oggetti per mezzo del loro section path invece che del loro nome, aderendo al naturale modello ad albero.

2.3 Il sistema Coq

Non intendiamo qui dare la sintassi di Coq o spiegare le tattiche che mette a disposizione, in quanto non saranno rilevanti nell'ambito di questa tesi. Rimandiamo, quindi, il lettore al manuale utente [BBC⁺97] e ai due tutorial [HKP98] e [Gim98]. Nel prossimo paragrafo, invece, vedremo brevemente due caratteristiche interessanti del sistema. In quello successivo daremo un breve esempio d'utilizzo, il cui scopo è esclusivamente quello di fornire al lettore una prima impressione sulle potenzialità ed i limiti di Coq.

2.3.1 Parsing e pretty-printing

In Coq vien fornita all'utente la possibilità di estendere sia le regole di parsing che quelle di pretty-printing⁹. Infatti, Coq utilizza una struttura dati uniforme, chiamata albero di sintassi astratta (AST), per la rappresentazione interna sia dei termini di CIC, sia dei comandi dati al sistema. Un tool, chiamato Camlp4 (per Caml Pre-Processor-Pretty-Printer), permette di definire e modificare a run time i due insiemi di regole utilizzate per trasformare le sequenze di token della sintassi concreta da e verso gli AST. Ogni regola è, a grandi linee, costituita da due parti: un pattern, che viene confrontato con l'input, e una azione, che genera l'output corrispondente. La definizione di queste regole permette di associare notazioni testuali agli oggetti definiti in Coq, eventualmente rendendo impliciti i parametri che possono essere inferiti dal sistema; in questo modo, per esempio, è possibile in Coq utilizzare la notazione A /\ B per (and A B) o quella x = y per (eq ? x y).

Nonostante questo sistema permetta spesso di rendere i termini più leggibili, è soggetto a diverse limitazioni:

Le regole grammaticali sono fattorizzate sintatticamente: Camlp4 non tenta di espandere i non terminali per individuare ulteriori fattorizzazioni. Pertanto, l'utente deve fattorizzare a mano tutte le regole.
Quando si aggiunge una nuova regola di parsing, non viene controllato che la grammatica resti LL(1), con conseguenti problemi durante il parsing.
Le regole vengono rimosse all'uscita delle sezioni, permettendo esclusivamente la definizione di notazioni locali e costringendo, quindi, a definire le varie regole al top-level.
A parte pochi esempi, la notazione testuale è del tutto insufficiente per la rappresentazione delle espressioni matematiche, normalmente scritte usando consolidate notazioni bidimensionali a cui è bene non rinunciare, pena un considerevole aumento della difficoltà di interpretazione dei termini.

2.3.2 Un esempio d'utilizzo di Coq

In questa sezione, mostriamo un piccolo esempio d'uso di Coq, ovvero la prova di un semplice teorema, chiamato easy, che afferma che ogni numero naturale o è 0, oppure è uguale alla somma di 1 e di un altro naturale. Ad ogni passo descriveremo brevemente lo scopo della tattica utilizzata e le regole di tipaggio utilizzate da questa per costruire il l-termine. Enunciamo il teorema:

Coq < Theorem easy: (n:nat)(n = O \/ (EX m : nat | (plus (S O) m) = n)).
1 subgoal
  
  ============================
   (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n)

Assumiamo n (ovvero utilizzamo Lam):

easy < Intro.
1 subgoal
  
  n : nat
  ============================
   n=O\/(EX m:nat | (plus (S O) m)=n)

Lavoriamo per induzione su n (ovvero utilizziamo Case). La tattica genera due nuovi goal, uno per il caso base e uno per il passo induttivo, che andremo a provare separatamente:

easy < Elim n.
2 subgoals
  
  n : nat
  ============================
   O=O\/(EX m:nat | (plus (S O) m)=O)

subgoal 2 is:
 (n0:nat)
  n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ->(S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

Dimostriamo la disgiunzione provando la parte sinistra (utilizziamo Constr):

easy < Left.
2 subgoals
  
  n : nat
  ============================
   O=O

subgoal 2 is:
 (n0:nat)
  n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ->(S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

Applichiamo la proprietà riflessiva (utilizziamo Constr in quanto l'uguaglianza di Leibniz è il tipo induttivo con un unico costruttore che afferma la riflessività della relazione). Questo termina la prova del caso base.

easy < Reflexivity.
1 subgoal
  
  n : nat
  ============================
   (n0:nat)
    n0=O\/(EX m:nat | (plus (S O) m)=n0)
    ->(S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

Passiamo al passo induttivo. Introduciamo n0 e l'ipotesi induttiva H (utilizzando Lam due volte):

easy < Intros.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

Dimostriamo la disgunzione provando la parte destra (utilizziamo Constr):

easy < Right.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (EX m:nat | (plus (S O) m)=(S n0))

Chiediamo, per nostra comodità, di effettuare bdi-riduzione sul goal (utilizziamo Conv):

easy < Simpl.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (EX m:nat | (S m)=(S n0))

Il quantificatore esistenziale è definito in Coq nel modo usuale come un S-tipo, ovvero come un tipo induttivo con un unico costruttore che prende un valore e la prova che la proprietà vale per quel valore. Per completare la prova, pertanto, applichiamo il costruttore al valore n0 (utilizziamo App e Constr)...

easy < Exists n0.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (S n0)=(S n0)

...e alla prova che (S n0)=(S n0) (utilizziamo nuovamente App e Constr):

easy < Reflexivity.
Subtree proved!

La prova è terminata, pertanto possiamo salvarla ...

easy < Qed.

...e chiedere di vedere il l-termine che abbiamo costruito:

Coq < Print easy.
easy = 
[n:nat]
 (nat_ind [n0:nat]n0=O\/(EX m:nat | (plus (S O) m)=n0)
   (or_introl O=O (EX m:nat | (plus (S O) m)=O) (refl_equal nat O))
   [n0:nat; _:(n0=O\/(EX m:nat | (plus (S O) m)=n0))]
    (or_intror (S n0)=O (EX m:nat | (plus (S O) m)=(S n0))
      (ex_intro nat [m:nat](S m)=(S n0) n0 (refl_equal nat (S n0)))) n)
     : (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n)

Essendo la dimostrazione molto semplice, è stato necessario utilizzare solamente tattiche alquanto primitive, di cui è facile comprendere l'operato. Per casi più complessi, però, le operazioni compiute dalle tattiche sul l-termine risultano decisamente oscure. Inoltre, si noti che, nonostante le regole di pretty-printing, il l-termine appare, almeno a prima vista, poco leggibile e di grandi dimensioni rispetto alla semplicità della dimostrazione. Fermandosi un attimo ad analizzarlo, però, magari aiutandosi con le indicazioni date, sarà semplice individuare tutti i passi logici compiuti: la parte rilevante della storia dell'intera dimostrazione è memorizzata al suo interno.

I termini associati alle prove non banali, comunque, possono rapidamente crescere di dimensioni, con conseguente impossibilità di essere interpretati in questa forma. Per ovviare al problema, almeno parzialmente, Coq mette a disposizione un tool, chiamato Natural, per generare automaticamente a partire dal l-termine una sua descrizione in linguaggio naturale. Nel nostro caso, il risultato è buono, anche se si nota una notevole artificiosità, specie nel passo induttivo, e resta il problema dell'insufficienza della notazione testuale:

Coq < Natural easy.
Theorem : easy.
Statement : (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n).
Proof : 
Consider an element n of nat.
We will prove n=O\/(EX m:nat | (plus (S O) m)=n) by induction on n.
Case 1. (base):
  We have directly O=O.
  With this result we have O=O\/(EX m:nat | (plus (S O) m)=O).
Case 2. (inductive):
  We know an element n0 of nat such that
  n0=O\/(EX m:nat | (plus (S O) m)=n0) (H).
  We will prove (S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0)).
  We have directly (S n0)=(S n0).
  With this result we have
  (EX m:nat | (S m)=(S n0)) which is equivalent to
  (EX m:nat | (plus (S O) m)=(S n0)).
Q.E.D.

Il risultato ideale, a nostro parere irraggiungibile senza l'intervento umano, sarebbe:

Theorem : easy.
Statement : (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n).
Proof : 
Consider an element n of nat.
We will prove n=O\/(EX m:nat | (plus (S O) m)=n) by induction on n.
Case 1. (base):
  We have directly O=O.
Case 2. (inductive, n=(S n0)):
  We will prove (EX m:nat | (plus (S O) m)=(S n0)).
  Since (plus (S O) m)=(S m) we can choose n0 for m,
  yelding the thesis.
Q.E.D.

Per termini più complessi, Natural genera descrizioni eccessivamente artificiose e talvolta troppo dettagliate, che possono però essere utilizzate proficuamente come scheletro per una riscrittura in linguaggio naturale della prova da parte dell'utente, come per l'esempio precedente.
I comandi dati interattivamente al sistema vengono normalmente inseriti all'interno dei file ``.v'' (per Vernacular, il linguaggio utilizzato per interagire con Coq). Per motivi di efficienza, è possibile compilare i file ``.v'' in file ``.vo'', che contengono esclusivamente le definizioni degli oggetti sotto forma di l-termini e le regole di parsing e pretty-printing. I file ``.vo'', che sono il vero prodotto del processo di scrittura delle teorie in Coq, sono in un formato proprietario binario, soggetto a modifiche ad ogni nuova versione del sistema. Pertanto, per conseguire gli obiettivi del progetto HELM, è stato necessario sviluppare un modulo per Coq, descritto nel prossimo capitolo, che permetta di esportare la rappresentazione interna dei termini e degli oggetti in un formato standard qual'è XML.

1: Il teorema di incompletezza di Gödel impedisce la dimostrazione in CIC della sua stessa strong normalization, in quanto dimostrarlo implicherebbe, come semplice corollario, la consistenza di CIC. Infatti, in un sistema strong normalizable, la forma canonica di ogni termine che abita un tipo induttivo ha come testa un costruttore, di cui il tipo induttivo False che rappresenta ^ è privo; ne consegue che False non è abitato, ovvero che il sistema è logicamente consistente.
2: In questo caso non valgono le ipotesi del teorema di incompletezza di Gödel; di conseguenza, è stato possibile dimostrare anche la strong normalization
3: Per il ragionamento è sufficiente la forma normale di testa debole.
4: La chiusura per contesti è quella standard, che asserisce le proprietà di congruenza di =_bdi, e non ha relazioni con i contesti definiti in precedenza.
5: B.Werner in [Wer94] dimostra la normalizzazione forte di una versione più primitiva di CIC anche nel caso in cui si consideri la h-conversione. Il risultato è fortemente basato sugli studi di Geuvers [Geu93]
6: La condizione viene introdotta in [Gim94] dove è semplicemente il controllo che T sia un identificatore appartenente a l. La forma presentata qui, che è inedita a conoscenza dell'autore, è stata ricavata ex-novo (e successivamente implementata) assieme al Dott. Luca Padovani partendo dall'osservazione del comportamento di Coq. Non è stata, però, data alcuna prova di correttezza (ovvero non è stata provata la normalizzazione forte del sistema quando si utilizzi questa definizione). Pertanto, la definizione può essere considerata ``sospetta''.
7: Questa affermazione è falsa nello studio delle teorie che dipendono pesantemente dalla stratificazione degli universi, come la Teoria delle Categorie, in cui si devono distinguere le categorie grandi da quelle piccole, e quella degli insiemi, in cui non vanno confusi gli insiemi grandi e piccoli. In queste teorie, è usuale procedere duplicando sintatticamente le stesse definizioni contenenti Type al solo fine di fare inferire al sistema diversi livelli per gli universi: le definizioni con il livello minore diverranno quelle piccole, le altre le grandi.
8: L'affermazione è falsa se il livello degli universi viene inferito, come avviene in Coq.
9: Le regole di parsing sono quelle che permettono di associare alla notazione testuale utilizzata dall'utente la rappresentazione interna dei l-termini. Le regole di pretty-printing compiono l'operazione inversa.