1 \chapter{Esempio: il Teorema di Euclide}
10 $n = 4$ dell'ultimo teorema di Fermat. Lo sviluppo della dimostrazione ha lo scopo
11 di servire come un'introduzione all'esecuzione di dimostrazioni interattive di alto livello
12 in \holn\footnote{Le dimostrazioni discusse di sotto si possono trovare in
15 ciononostante, si raccomanda di seguire l'esempio in modo completo
16 al fine di ottenere una vera sensazione dell'uso di \HOL{} per dimostrare teoremi non-banali.
18 Alcuni tutorial sulla descrizione di sistemi di dimostrazione, mostrano il sistema mentre esegue
19 incredibili gesta di dimostrazione automatica di teoremi. In questo esempio, \textit{non}
20 abbiamo seguito questo approccio; piuttosto, cerchiamo di mostrare come si affronta
21 nella realt� il problema di dimostrare teoremi in \holn{}: quando
22 � possibile pi� di un modo per dimostrare qualcosa, considereremo
23 le scelte; quando sorge una difficolt�, tenteremo di spiegare come affrontare
31 gli strumenti di dimostrazione da \ml{bossLib} (o se essi falliscono, dalle
32 librerie di basso livello).
43 Ora iniziamo la formalizzazione. Al fine di definire il concetto di
44 numero primo, abbiamo prima bisogno di definire la relazione di \emph{divisibilit�}:
56 \ml{divides\_def}, ed � anche restituita dall'invocazione di
57 \ml{Define}. Approfittiamo di questo ed effettuiamo un binding del nome
58 \ML{} \ml{divides\_def} alla definizione. Nel modo usuale di
70 Poi definiamo la propriet� di essere un numero \emph{primo}: un numero $p$ �
89 non completamente chiaro e spesso tremendamente difficile di ricerca dei giusti lemmi
91 problema generale quando si affronta qualsiasi tipo di dimostrazione.}. Fortunatamente, stiamo
93 decisamente pi� semplice di spiegare come dimostrare i teoremi richiesti.
95 \paragraph{Strumenti di dimostrazione}
96 Lo sviluppo illustrer� che c'� spesso pi� di un modo di
99 la tattica di riscrittura \ml{RW\_TAC} per espandere le definizioni ed eseguire semplificazioni
100 di base, riducendo spesso un goal alla sua essenza.
108 Il tipo ML di \ml{RW\_TAC} �
112 sempre \ml{arith\_ss}---e a una lista di teoremi, i
113 teoremi saranno aggiunti al simpset come regole di riscrittura aggiuntive.
120 Spesso comunque, ci rimane un goal che richiede un p� di studio prima di
127 la semplificazione e la ricerca automatica di una dimostrazione nello stile della risoluzione, non saranno sufficienti per
133 le regole di riscrittura da usare? Questo � piuttosto problematico, specialmente dal momento che il numero di
134 teorie progenitrici, e di teoremi al loro interno, � grande. Ci sono molte
137 \item Si pu� usare il sistema di help per cercare definizioni e
138 teoremi, cos� come procedure di dimostrazione; per esempio, un'invocazione di
145 che si sta cercando prima che il sistema di help sia utile, cos� i due
146 seguenti strumenti di ricerca sono spesso pi� utili.
147 \item \verb+DB.match+ permette l'uso di pattern per individuare il
154 \paragraph{Composizione di tattiche}
155 Una volta che � stata trovata una dimostrazione di una proposizione, � d'abitudine, bench�
156 non necessario, avviare un processo di \emph{revisione}, in cui la
157 sequenza di tattiche originaria � composta in un'unica tattica. A volte,
159 da un punto di vista estetico. Alcuni utenti spendono un bel p� di tempo per raffinare queste tattiche,
161 sono ricette di dimostrazione \emph{ad hoc}, una per ciascun teorema. Nel
166 Iniziamo dimostrando un numero di teoremi circa la relazione
167 \verb+divides+. Vedremo che ciascuno di questi teoremi iniziali pu� essere
168 dimostrato con una singola invocazione di \ml{METIS\_TAC}. Sia \ml{RW\_TAC}
169 sia \ml{METIS\_TAC} sono ragionatori piuttosto potenti, e la scelta di un
170 ragionatore in una situazione particolare � una questione di esperienza. La
172 � definita per mezzo di un quantificatore esistenziale, e \ml{METIS\_TAC}
174 corso di una dimostrazione. Per un semplice esempio, si consideri la dimostrazione di $\forall x.\
191 Il manager di dimostrazione ci dice che c'� soltanto una dimostrazione da gestire, e
192 ripete il goal dato. Ora espandiamo la definizione di
193 \verb+divides+. Si noti che ha luogo un'$\alpha$-conversione al fine di
194 mantenere distinta la $x$ del goal e la $x$ nella definizione di
218 Poi un passo di semplificazione conclude la dimostrazione.
235 Cosa � appena successo qui? L'applicazione di \ml{RW\_TAC} al goal
236 lo ha decomposto in una lista vuota di subgoal; in altre parole, il goal � stato
241 quel livello pu� essere dimostrato. Questo processo di `svolgimento' continua fino a quando
242 lo stack � vuoto, o fino a quando raggiunge un goal con pi� di un subgoal
266 Abbiamo visto un modo di dimostrare il teorema. Comunque, come menzionato
268 definizione di \ml{divides} e trovi l'istanziazione richiesta per
303 collezione di teoremi circa \ml{divides}. Come menzionato in precedenza, i
304 teoremi forniti a \ml{METIS\_TAC} nelle seguenti dimostrazioni (di solito) non
372 \noindent Assumeremo che le dimostrazioni di sopra siano state eseguite, e
375 singola invocazione di \ml{METIS\_TAC}:
385 Vediamo come questo � dimostrato. Il modo pi� semplice � di iniziare a semplificare
386 con la definizione di \ml{divides}:
400 Considerando il goal, di base abbiamo tre possibilit�: (1) trovare una
401 collezione di lemmi che insieme implicano il goal e usare
404 non calza nella `forma' di un qualsiasi teorema pre-dimostrato di cui l'autore sia a
408 possibilit� di costruzione previste dal costruttore del suo datatype'' [corrisponde al pattern matching di ML (ndt)]. Dal momento che
409 l'occorrenza di $m$ nel goal ha il tipo $num$, i casi considerati saranno
437 \noindent Proviamo \ml{RW\_TAC} di nuovo:
448 fallito di espandere la definizione della moltiplicazione nell'espressione
451 Perch�, visto che si suppone che \verb+arith_ss+ e di conseguenza \ml{RW\_TAC} siano esperte
454 da parte del sistema di riscrittura sembra che, in generale, renda alcune
470 � spesso utile a questo scopo. Essa prende una lista di nomi di teorie, e
473 Se la lista dei nomi di teorie � vuota, allora sono incluse nella ricerca
504 di riscrittura:
539 Ora vediamo che, al fine di fare progressi nella dimostrazione, dovremo fare
540 un case split su $x$ comunque, e che avremmo dovuto fare lo split su di esso
565 a un goal $g$, prima $t_1$ � applicato a $g$, dando una lista di nuovi
567 risultanti da queste applicazioni di $t_2$ sono raccolti insieme e
582 giusta. Il processo di {\it trovare\/} la dimostrazione ora � terminato, e
584 tattica come abbiamo visto di sopra. Al posto di usare \ml{top\_thm} e il goalstack,
601 Archiviare i teoremi nel nostro script di salvataggio della sessione in questo stile
603 rende anche pi� facile trasformare il nostro script in un file di teoria, come facciamo
609 maggiore di $0$ e $\leq n$ divide il fattoriale di
621 Una dimostrazione lucidata di {\small{\it DIVIDES\_FACT\/}} � la
637 Esamineremo questa dimostrazione nel dettaglio, cos� dovremmo prima tentare di
649 ci� di cui abbiamo bisogno. Questa strategia per il caso induttivo � un p� vaga,
665 Al posto di eseguire un'induzione direttamente su $n-m$, faremo un'induzione su una variabile
711 goal banale; se � un successore, allora possiamo usare la definizione di
733 numero $x$ � minore di s� stesso), e quindi passare il teorema
756 Usando i teoremi identificati di sopra, il subgoal rimanente pu�
774 Quest'ultimo passo, cio� l'invocazione di \ml{RW\_TAC},
776 l'unica differenza � l'uso di \ml{DIVIDES\_LMUL} nel semplificatore
777 \emph{al posto di} \ml{DIVIDES\_RMUL} in \ml{METIS\_TAC}. Questo � dovuto al
791 caso di passo. Una cosa ovvia da provare � la semplificazione con le
806 \noindent E ora, per mezzo di \ml{DIVIDES\_RMUL} e l'ipotesi d'induzione, abbiamo
821 Abbiamo concluso la ricerca della dimostrazione, e possiamo spostarci al compito di
824 in un file o nel buffer di un editor di testo. Avremmo dunque qualcosa
825 di simile a ci� che segue:
844 Abbiamo aggiunto uno schema di numerazione per tenere traccia dei rami nella
845 dimostrazione. Possiamo cucire insieme l'espressioni di sopra nella seguente tattica
881 Per molti utenti, questa sarebbe la conclusione di questa dimostrazione: la
882 tattica ora pu� essere impacchettata in un'invocazione di
884 e tenta di dimostrare il termine usando la tattica fornita. Essa
886 il teorema alla teoria sviluppata.} o di \ml{store\_thm} e quella
890 Per iniziare, entrambi i rami dell'induzione iniziano con un'invocazione di
891 \ml{RW\_TAC}, e la semantica di \ml{THEN} ci permette di fondere le
892 occorrenze di \ml{RW\_TAC} prima di \ml{THENL}. La tattica rimaneggiata
906 se continua a dimostrare il goal!) Ora si ricordi che l'uso di \ml{RW\_TAC}
909 invocazione di \ml{METIS\_TAC}:
924 piacerebbe che ci fosse un'unica invocazione di \ml{METIS\_TAC} per concludere
925 la dimostrazione. La semantica di \ml{THEN} e di \ml{ALL\_TAC} vengono
926 in nostro aiuto: divideremo la costruzione di $m$ nel caso base,
928 caso induttivo di passo inalterato attraverso \ml{THENL}. Questo si ottiene
944 \ml{THENL}: i due sotto casi nel caso base e il caso di passo
950 possiamo abbreviare la tattica di nuovo.
963 Ora abbiamo concluso il nostro esercizio di revisione delle tattiche. Certamente,
965 goal; i lemmi richiesti per l'invocazione finale di \ml{METIS\_TAC}
966 sono stati trovati attraverso un processo incrementale di revisione.
968 \subsection{Divisibilit� e fattoriale (di nuovo!)}
970 Nella precedente dimostrazione, abbiamo fatto un passo di semplificazione iniziale al fine
971 di esporre una variabile su cui indurre. Comunque, la dimostrazione in realt�
993 		assunzioni. L'uso di \ml{THEN} assicura che la tatticca venga applicata
1021 {\ml{DECIDE\_TAC} � una procedura di decisione per un'utile classe di formule aritmetiche.}
1057 		$m$ � il successore di qualche numero $k$. Potremmo desiderare di affermare
1058 		questo fatto con un'invocazione di ``\ml{by}'' nel modo seguente:
1063 non gestisce enunciati esistenziali. Anche un'applicazione di
1066 Quando capita una situazione di questo tipo, � spesso meglio iniziare una nuova dimostrazione per il
1068 di nuovo. Un nuovo goalstack sar� creato e aggiunto a quello
1069 corrente\footnote{Questa aggiunta di tentativi di dimostrazione (goalstack) � differente
1070   dall'aggiunta di goal e giustificazioni all'interno di un particolare
1071 	goalstack.} e sar� stampata una panoramica dei tentativi di dimostrazione
1098 		mezzo di una specie di gioco di prestigio con la funzione ``\ml{before}''\footnote{Una
1158 		implica che $0 < n$ e cos�, di nuovo per mezzo di \ml{lem}, possiamo trasformare $n$
1159 		in un successore, abilitando di conseguenza l'espansione di \ml{FACT}, come nella
1178 \noindent La dimostrazione ora si conclude nello stesso modo di quella precedente:
1231 Ora siamo nella posizione di dimostrare un lemma pi� sostanziale: ogni numero
1241 d'induzione e per la transitivit� di \ml{divides} abbiamo finito; altrimenti,
1259 d'induzione che vale per ogni numero $m$ strettamente minore di $n$:
1307 Nel secondo caso, otteniamo un divisore di $n$ che non � $1$ n� $n$
1327 una collezione di teoremi. Tenteremo un'esposizione pi�
1360 la transitivit� della divisibilit� per ottenere il fatto che questo divisore di $x$ �
1361 anche un divisore di $n$, concludendo quindi questo ramo della dimostrazione:
1405 tutto ci� che dobbiamo fare � esibire un primo. E ne abbiamo gi� uno a portata di mano:
1419 tattica, dai passi individuali di dimostrazione, ma non lo descriveremo\footnote{
1421  seguita da un'invocazione di \ml{METIS\_TAC} con lemmi adeguati.}.
1422 Piuttosto andiamo avanti, perch� il nostro obiettivo finale � a portata di mano.
1424 \section{Il teorema di Euclide}
1426 \noindent{\bf Teorema.} Ogni numero ha un primo pi� grande di lui.\\
1429 tale che tutti i $p$ pi� grandi di $n$ non sono primi. Si consideri $\mbox{\tt
1449 contraddizione pu� essere avviata usando la funzione di \ml{bossLib}
1451 goal attuale e quindi la si usa nel tentativo di dimostrare la falsit�
1471 Cos� abbiamo l'ipotesi che tutti i $p$ al di sopra di un certo $n$ non
1472 specificato non sono primi, e il nostro compito � di mostrare che ci� non pu� essere. A questo
1473 punto approfittiamo della grande ispirazione di Euclide e costruiamo un
1474 termine esplicito da $n$. Nella dimostrazione informale ci viene chiesto di `considerare'
1475 il termine $\mbox{\tt FACT}\ n + 1$\footnote{Il parser di HOL pensa che
1492 E' evidente che l'antecedente di \ml{th} pu� essere eliminato. In
1493 \holn{}, si potrebbe fare questo in un cosiddetto stile di dimostrazione {\it in avanti\/} (dimostrando
1509     L'invocazione di \ml{MP\_TAC} ($\vdash M$) applicata a un goal
1528     Si ricordi che zero � minore di qualsiasi fattoriale, un fatto che si trova in
1538 Si noti l'uso `on-the-fly' di \verb+DECIDE+ per fornire una riscrittura
1539 \textit{ad hoc}. Osservando il goal rimanente, si potrebbe pensare che il nostro obiettivo, di
1543 $\vdash A \imp B = \neg A \lor B$ come una regola di riscrittura orientata da destra a sinistra per mezzo
1544 dell'uso di \ml{GSYM}\footnote{In parole povere, \ml{GSYM} scambia i lati sinistro e
1545 destro di qualsiasi equazione che trova.}.
1564 e di conseguenza che $p = 1$, quindi che $p$ non � primo, a quel punto abbiamo finito.
1565 Questo pu� essere impacchettato tutto in una singola invocazione di \ml{METIS\_TAC}:
1589     Il teorema di Euclide ora � dimostrato, e possiamo riposare. Comunque, questa
1595 		dimostrazione informale. Il seguente dimostra il teorema di Euclide nello
1597 		di pi� della dimostrazione standard basata su tattiche appena data\footnote{Si noti
1626 che lo renda disponibile per le sessioni future, ma che non ci richieda di
1627 di passare di nuovo attraverso lo sforzo di dimostrare il teorema. Persino avere
1631 Al fine di fare questo abbiamo bisogno un file con il nome
1633 esportare. Questo file ha quindi bisogno di essere compilato. Di fatto, usiamo realmente
1634 il compilatore di Moscow ML, accuratamente aumentato con il contesto logico
1636 esattamente lo stesso di quello accettato dal sistema interattivo, cos� abbiamo
1637 bisogno di fare un poco di lavoro per smussare lo script originario nella
1640 Daremo un'illustrazione di conversione a una forma che possa essere
1644 \] come nostra linea di base. Questo
1667 \ml{euclidScript.sml}, e copiare in esso il corpo di
1681 sistema interattivo, il compilatore richiede che ogni espressione di primo livello
1690 prima della definizione di \ml{divides}, aggiungiamo:
1727 Ora abbiamo creato quattro nuovi file, varie forme di \ml{euclidTheory}
1754 in \holn{}. La discussione ha illustrato gli strumenti di alto  livello forniti in
1756 la `levigatura delle tattiche', la semplificazione esplorativa, e la `biforcazione' di
1757 nuovi tentativi di dimostrazione. Abbiamo anche tentato di dare un'idea dei processi di
1759 casuale di altre osservazioni.
1762 \item Nonostante la dimostrazione del teorema di Euclide sia breve e semplice da
1764 forse sorprendente di sviluppo a supporto dell'impostazione dell'argomento
1765 classico di Euclide.
1771 tattiche di basso livello.
1773 \item La semplificazione � un cavallo di battaglia delle tattiche; persino quando � stato usato
1776 confidenza con i punti di forza e di debolezza del semplificatore.
1778 \item Un problema comune con i sistemi interattivi di dimostrazione � trattare con
1780 di usare le ipotesi senza ricorrere direttamente alla loro indicizzazione
1784 script di dimostrazione difficili da manutenere. Comunque, pu� confondere lavorare con
1785 un grande insieme di ipotesi, nel qual caso i seguenti approcci possono essere
1794 I numeri associati alle ipotesi dal gestore di dimostrazione verosimilmente potrebbero
1799 In alcuni casi, � utile essere in grado di cancellare un'ipotesi. Questo si pu�
1804 \item Nell'esempio, non abbiamo usato le caratteristiche pi� avanzate di
1806 funzionalit� rispetto alla semplice sequenza di semplificazione, procedure
1807 di decisione, e ragionamento automatico al primo ordine. Il tatticale
1812     informale\/} al fine di avere successo quando di fa una dimostrazione
1817 	caso di cane che si morde la coda, ed � una strategia povera da adottare.
1818 	La comprensione della struttura di alto livello della dimostrazione � uno dei
1819 	fattori pi� importanti negli esercizi di verifica di successo.
1821 L'autore ha notato che molti degli esperti di verifica pi� di successo
1822 lavorano usando un foglio di carta per tenere traccia dei passi principali che
1826 Dall'altra parte, uno dei vantaggi di avere una logica meccanizzata
1827 � che la macchina pu� essere usata come un calcolatore di espressioni formali,
1829 possibilit� di dimostrazione.
1835 teorema di Euclide, gli strumenti hanno funzionato piuttosto bene. Tuttavia, a volte
1837 usare, o persino scrivere, degli strumenti di dimostrazione pi� specializzati, e di conseguenza
1840 \item Avere una buona conoscenza dei lemmi disponibile, e di dove essi
1843 deve sapere cosa � stato gi� dimostrato. Abbiamo visto che i punti di ingresso

Indexes created Tue Sep 03 12:52:19 MDT 2024