From: Enrico Tassi Date: Fri, 7 Nov 2008 09:05:48 +0000 (+0000) Subject: exercise ready X-Git-Tag: make_still_working~4582 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c83b0752a7c3b7be6cfe0ad4b10cf6d7915d492c;p=helm.git exercise ready --- diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma index 6979cbbf0..cb42e8198 100644 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ b/helm/software/matita/contribs/didactic/shannon.ma @@ -1,14 +1,15 @@ (* Esercizio -1 ============ - 1. Leggere ATTENTAMENTE, e magari stampare, la documentazione reperibile - all'URL seguente: + 1. Leggere ATTENTAMENTE, e magari stampare, la documentazione + reperibile all'URL seguente: http://mowgli.cs.unibo.it/~tassi/exercise-shannon.ma.html - 2. Questa volta si fa sul serio: - l'esercizio proposto è molto difficile, occorre la vostra massima - concentrazione (leggi: niente cut&paste selvaggio, cercate di capire!) + 2. Questa volta si fa sul serio: + + l'esercizio proposto è MOLTO difficile, occorre la vostra massima + concentrazione (leggi: niente cut&paste selvaggio) *) @@ -134,43 +135,70 @@ Per portare a termine l'esercitazione sono necessari i seguenti lemmi: * lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v` * lemma `max_0_sem` : `∀F,v.max [[ F ]]_v 0 = [[ F ]]_v` +Nota su `x = y` e `eqb x y` +--------------------------- + +Se vi siete mai chiasti la differenza tra `x = y` ed `eqb x y` +quanto segue prova a chiarirla. + +Presi due numeri `x` e `y` in ℕ, dire che `x = y` significa i due numeri +sono lo stesso numero, ovvero che se `x` è il numero `3`, +anche `y` è il numero `3`. + +`eqb` è un funzione, un programma, che confronta due numeri naturali +e restituisce `true` se sono uguali, `false` se sono diversi. L'utilizzo +di tale programma è necessario per usare il costrutto (che è a sua volta +un programma) `if E then A else B`, che lancia il programma `E`, +e se il suo +risultato è `true` si comporta come `A` altrimenti come `B`. Come +ben sapete i programmi possono contenere errori. In particolare anche +`eqb` potrebbe essere sbagliato, e per esempio restituire sempre `true`. +I teoremi `eq_to_eqb_true` e +`not_eq_to_eqb_false` sono la dimostrazione che il programma `eqb` è +corretto, ovvero che che se `x = y` allora `eqb x y` restituisce `true`, +se `x ≠ y` allora `eqb x y` restituisce `false`. + Il teorema di espansione di Shannon =================================== -Si definisce un connettivo logico `IFTE A B C` come `FOr (FAnd A B) (FAnd (FNot A) C)`. +Si definisce un connettivo logico `IFTE A B C` come + + FOr (FAnd A B) (FAnd (FNot A) C) Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente formula è equivalente a `F`: IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) -Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso -in un mondo mondo `v`, altrimenti lo sostituisco con `FTop`. +Ovvero, fissato un mondo `v`, sostituisco l'atomo `x` con `FBot` se tale +atomo è falso, lo sostituisco con `FTop` se è vero. La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`. -Vediamo la dimostrazione del primo, che asserisce +Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo. +Il lemma asserisce quanto segue: ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v -Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver supposto -che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`. +Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver +supposto che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`. I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`, -una volta assunte le sottofrmule e le ipotesi induttive, si conclude -con una catena di uguaglianze. +una volta assunte le sottoformule e le relative ipotesi induttive, +si conclude con una catena di uguaglianze. -Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo, +Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo `n`, occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi -aggiuntiva `n = x ∨ n ≠ x` su cui si procede poi per casi. -In entrambi i casi, usanto i lemmi `eq_to_eqb_true` e `not_eq_to_eqb_false` -si ottengolo le ipotesi aggiuntive `(eqb n x = true)` e `(eqb n x = false)`. +aggiuntiva `n = x ∨ n ≠ x` (dove `x` è l'atomo su cui predica il teorema). +Si procede per casi sull'ipotesi appena ottenuta. +In entrambi i casi, usanto i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false` +si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`. Entrambi i casi si concludono con una catena di uguaglianze. Il teorema principale si dimostra utilizzando il lemma `sem_bool` per ottenre l'ipotesi `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` su cui -si procede poi per casi. Entrambi i casi si cncludono con +si procede poi per casi. Entrambi i casi si concludono con una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza -e i lemmi `min_1_sem` e `max_0_sem`. +e i lemmi `min_1_sem` oppure `max_0_sem`. DOCEND*) @@ -409,8 +437,9 @@ Note generali Si ricorda che: 1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un - simbolo `→` è opportuno usare il comando `assume` oppure `suppose` (che - vengono nuovamente spiegati in seguito). + simbolo `→` è opportuno usare il comando `assume` oppure `suppose` + oppure (se si è in un caso di una dimostrazione per induzione) il comando + `by induction hypothesis we know` (che vengono nuovamente spiegati in seguito). 2. Ogni caso (o sotto caso) della dimostrazione: @@ -420,8 +449,8 @@ Si ricorda che: 2. Continua poi con almeno un comando `the thesis becomes`. - 3. Eventualmente seguono vari comandi `by ... we proved` per combinare le - ipotesi tra loro o utilizzare i teoremi già disponibili per generare nuove + 3. Eventualmente seguono vari comandi `by ... we proved` per + utilizzare i teoremi già disponibili per generare nuove ipotesi. 4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`.