X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Fshannon.ma;h=f708c19baf8fb963ae27811ed99dccab5c0112ff;hb=f9480e116110345956ef873c88dba78f73fa225b;hp=ccbaf956d95a42c3105edf22adf8c5044bb5b5ca;hpb=dfe4fff39d66e00326f4ff7cfbcbdf96ac178a66;p=helm.git diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma index ccbaf956d..f708c19ba 100644 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ b/helm/software/matita/contribs/didactic/shannon.ma @@ -1,11 +1,19 @@ -(* Esercitazione di logica 29/10/2008. - - Note per gli esercizi: +(* Esercizio -1 + ============ - http://www.cs.unibo.it/~tassi/exercise-duality.ma.html - + 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) + *) + (* Esercizio 0 =========== @@ -21,49 +29,8 @@ Matricola2: ... Account2: ... - Prima di abbandonare la postazione: - - * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella) - /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui - account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma - - * mandatevi via email o stampate il file. Per stampare potete usare - usare l'editor gedit che offre la funzionalità di stampa *) -(*DOCBEGIN - -Il teorema di dualità -===================== - -Il teorema di dualizzazione dice che date due formule `F1` ed `F2`, -se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le -loro dualizzate lo sono (`dualize F1 ≡ dualize F2`). - -L'ingrediente principale è la funzione di dualizzazione di una formula `F`: - - * Scambia FTop con FBot e viceversa - - * Scambia il connettivo FAnd con FOr e viceversa - - * Sostituisce il connettivo FImpl con FAnd e nega la - prima sottoformula. - - Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in - `¬A ∧ (B ∨ ⊤)`. - -Per dimostrare il teorema di dualizzazione in modo agevole è necessario -definire altre nozioni: - -* La funzione `negate` che presa una formula `F` ne nega gli atomi. - Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`. - -* La funzione `invert` permette di invertire un mondo `v`. - Ovvero, per ogni indice di atomo `i`, se `v i` restituisce - `1` allora `(invert v) i` restituisce `0` e viceversa. - -DOCEND*) - (* ATTENZIONE ========== @@ -77,8 +44,8 @@ interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t definition max ≝ λn,m. if eqb (n - m) 0 then m else n. definition min ≝ λn,m. if eqb (n - m) 0 then n else m. -(* Ripasso - ======= +(* Ripasso 1 + ========= Il linguaggio delle formule, dove gli atomi sono rapperesentati da un numero naturale @@ -93,23 +60,16 @@ inductive Formula : Type ≝ | FNot: Formula → Formula . -(* Esercizio 1 - =========== +(* Ripasso 2 + ========= - Modificare la funzione `sem` scritta nella precedente - esercitazione in modo che valga solo 0 oppure 1 nel caso degli - atomi, anche nel caso in cui il mondo `v` restituisca un numero - maggiore di 1. - - Suggerimento: non è necessario usare il costrutto if_then_else - e tantomento il predicato di maggiore o uguale. È invece possibile - usare la funzione `min`. -*) + La semantica di una formula `F` in un mondo `v`: `[[ F ]]_v` +*) let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ match F with [ FBot ⇒ 0 | FTop ⇒ 1 - | FAtom n ⇒ (*BEGIN*)min (v n) 1(*END*) + | FAtom n ⇒ min (v n) 1 | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) @@ -126,63 +86,31 @@ notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative wi notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. interpretation "Semantic of Formula" 'semantics v a = (sem v a). +lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1. intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ]. |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed. -definition v20 ≝ λx. - if eqb x 0 then 2 - else if eqb x 1 then 1 - else 0. - -(* Test 1 - ====== - - La semantica della formula `(A ∨ C)` nel mondo `v20` in cui - `A` vale `2` e `C` vale `0` deve valere `1`. - -*) -eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. - -(*DOCBEGIN - -La libreria di Matita -===================== - -Gli strumenti per la dimostrazione assistita sono corredati da -librerie di teoremi già dimostrati. Per portare a termine l'esercitazione -sono necessari i seguenti lemmi: - -* lemma `sem_le_1` : `∀F,v. [[ F ]]_v ≤ 1` -* lemma `min_1_1` : `∀x. x ≤ 1 → 1 - (1 - x) = x` -* lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1` -* lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v` -* lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v` -* lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3` - -DOCEND*) - -(* ATTENZIONE - ========== +(* Ripasso 3 + ========= - Non modificare quanto segue. + L'operazione di sostituzione di una formula `G` al posto dell'atomo + `x` in una formula `F`: `F[G/x]` *) -lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1. intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ]. |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed. -lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1. intros; cases n; [left;reflexivity] cases n1; right; reflexivity; qed. -lemma min_max : ∀F,G,v. min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v. intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed. -lemma max_min : ∀F,G,v. max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v. intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed. -lemma min_1_1 : ∀x.x ≤ 1 → 1 - (1 - x) = x. intros; inversion H; intros; destruct; [reflexivity;] rewrite < (le_n_O_to_eq ? H1); reflexivity;qed. -lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H; [apply le_O_n|apply le_n]qed. + let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ match F with [ FBot ⇒ FBot - | FTop ⇒ (*BEGIN*)FTop(*END*) - | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*)) - (*BEGIN*) + | FTop ⇒ FTop + | FAtom n ⇒ if eqb n x then G else (FAtom n) | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2) | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2) | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2) - (*END*) | FNot F ⇒ FNot (subst x G F) ]. - + +(* ATTENZIONE + ========== + + Non modificare quanto segue. +*) notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }. notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }. interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). @@ -190,19 +118,402 @@ definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). +lemma min_1_sem: ∀F,v.min 1 [[ F ]]_v = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. +lemma max_0_sem: ∀F,v.max [[ F ]]_v 0 = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. +definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C). + +(*DOCBEGIN + +La libreria di Matita +===================== + +Per portare a termine l'esercitazione sono necessari i seguenti lemmi: + +* lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y` +* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1` +* lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false` +* lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true` +* 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 chiesti 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) + +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, 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 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`. +I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`, +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 `n`, +occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi +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, usando 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 concludono con +una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza +e i lemmi `min_1_sem` oppure `max_0_sem`. + +DOCEND*) + +lemma shannon_false: + ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +suppose ([[ FAtom x ]]_v = 0) (H). +we proceed by induction on F to prove ([[ F[FBot/x] ]]_v = [[ F ]]_v). +case FBot. + the thesis becomes ([[ FBot[FBot/x] ]]_v = [[ FBot ]]_v). + the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v). + done. +case FTop. + the thesis becomes ([[ FTop[FBot/x] ]]_v = [[ FTop ]]_v). + the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v). + done. +case FAtom. + assume n : ℕ. + the thesis becomes ([[ (FAtom n)[FBot/x] ]]_v = [[ FAtom n ]]_v). + the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v). + by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1). + we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v). + case Left. + by H2, eq_to_eqb_true we proved (eqb n x = true) (H3). + conclude + ([[ if eqb n x then FBot else (FAtom n) ]]_v) + = ([[ if true then FBot else (FAtom n) ]]_v) by H3. + = ([[ FBot ]]_v). + = 0. + = ([[ FAtom x ]]_v) by H. + = ([[ FAtom n ]]_v) by H2. + done. + case Right. + by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3). + conclude + ([[ if eqb n x then FBot else (FAtom n) ]]_v) + = ([[ if false then FBot else (FAtom n) ]]_v) by H3. + = ([[ FAtom n ]]_v). + done. +case FAnd. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]_v = [[ FAnd f1 f2 ]]_v). + conclude + ([[ (FAnd f1 f2)[FBot/x] ]]_v) + = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]_v). + = (min [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v). + = (min [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1. + = (min [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FAnd f1 f2 ]]_v). + done. +case FOr. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]_v = [[ FOr f1 f2 ]]_v). + conclude + ([[ (FOr f1 f2)[FBot/x] ]]_v) + = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]_v). + = (max [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v). + = (max [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1. + = (max [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FOr f1 f2 ]]_v). + done. +case FImpl. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]_v = [[ FImpl f1 f2 ]]_v). + conclude + ([[ (FImpl f1 f2)[FBot/x] ]]_v) + = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]_v). + = (max (1 - [[ f1[FBot/x] ]]_v) [[ f2[FBot/x] ]]_v). + = (max (1 - [[ f1 ]]_v) [[ f2[FBot/x] ]]_v) by H1. + = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2. + = ([[ FImpl f1 f2 ]]_v). + done. +case FNot. + assume f : Formula. + by induction hypothesis we know ([[ f[FBot/x] ]]_v = [[ f ]]_v) (H1). + the thesis becomes ([[ (FNot f)[FBot/x] ]]_v = [[ FNot f ]]_v). + conclude + ([[ (FNot f)[FBot/x] ]]_v) + = ([[ FNot (f[FBot/x]) ]]_v). + = (1 - [[ f[FBot/x] ]]_v). + = (1 - [[ f ]]_v) by H1. + = ([[ FNot f ]]_v). + done. +(*END*) +qed. + +lemma shannon_true: + ∀F,x,v. [[ FAtom x ]]_v = 1 → [[ F[FTop/x] ]]_v = [[ F ]]_v. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +suppose ([[ FAtom x ]]_v = 1) (H). +we proceed by induction on F to prove ([[ F[FTop/x] ]]_v = [[ F ]]_v). +case FBot. + the thesis becomes ([[ FBot[FTop/x] ]]_v = [[ FBot ]]_v). + the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v). + done. +case FTop. + the thesis becomes ([[ FTop[FTop/x] ]]_v = [[ FTop ]]_v). + the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v). + done. +case FAtom. + assume n : ℕ. + the thesis becomes ([[ (FAtom n)[FTop/x] ]]_v = [[ FAtom n ]]_v). + the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v). + by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1). + we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v). + case Left. + by H2, eq_to_eqb_true we proved (eqb n x = true) (H3). + conclude + ([[ if eqb n x then FTop else (FAtom n) ]]_v) + = ([[ if true then FTop else (FAtom n) ]]_v) by H3. + = ([[ FTop ]]_v). + = 1. + = ([[ FAtom x ]]_v) by H. + = ([[ FAtom n ]]_v) by H2. + done. + case Right. + by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3). + conclude + ([[ if eqb n x then FTop else (FAtom n) ]]_v) + = ([[ if false then FTop else (FAtom n) ]]_v) by H3. + = ([[ FAtom n ]]_v). + done. +case FAnd. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]_v = [[ FAnd f1 f2 ]]_v). + conclude + ([[ (FAnd f1 f2)[FTop/x] ]]_v) + = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]_v). + = (min [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v). + = (min [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1. + = (min [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FAnd f1 f2 ]]_v). + done. +case FOr. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]_v = [[ FOr f1 f2 ]]_v). + conclude + ([[ (FOr f1 f2)[FTop/x] ]]_v) + = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]_v). + = (max [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v). + = (max [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1. + = (max [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FOr f1 f2 ]]_v). + done. +case FImpl. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]_v = [[ FImpl f1 f2 ]]_v). + conclude + ([[ (FImpl f1 f2)[FTop/x] ]]_v) + = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]_v). + = (max (1 - [[ f1[FTop/x] ]]_v) [[ f2[FTop/x] ]]_v). + = (max (1 - [[ f1 ]]_v) [[ f2[FTop/x] ]]_v) by H1. + = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2. + = ([[ FImpl f1 f2 ]]_v). + done. +case FNot. + assume f : Formula. + by induction hypothesis we know ([[ f[FTop/x] ]]_v = [[ f ]]_v) (H1). + the thesis becomes ([[ (FNot f)[FTop/x] ]]_v = [[ FNot f ]]_v). + conclude + ([[ (FNot f)[FTop/x] ]]_v) + = ([[ FNot (f[FTop/x]) ]]_v). + = (1 - [[ f[FTop/x] ]]_v). + = (1 - [[ f ]]_v) by H1. + = ([[ FNot f ]]_v). + done. +(*END*) +qed. theorem shannon : - ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v. -intros; elim F; -[1,2: cases (eqb [[FAtom x]]_v 0); reflexivity; -|4,5,6: cases (eqb [[FAtom x]]_v 0) in H H1; simplify; intros; rewrite > H; rewrite > H1; reflexivity; -|7: cases (eqb [[FAtom x]]_v 0) in H; simplify; intros; rewrite > H; reflexivity; -| cases (sem_bool (FAtom x) v); rewrite > H; simplify; - cases (decidable_eq_nat n x); destruct H1; - [1,3: rewrite > eqb_n_n; simplify; rewrite >H;reflexivity;. - |*:simplify in H; rewrite > (not_eq_to_eqb_false ?? H1); simplify; reflexivity;]] + ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v). +by sem_bool we proved ([[ FAtom x]]_v = 0 ∨ [[ FAtom x]]_v = 1) (H). +we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v). +case Left. + conclude + ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v) + = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). + = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H. + = (max 0 (min 1 [[ F[FBot/x] ]]_v)). + = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem. + = ([[ F[FBot/x] ]]_v). + = ([[ F ]]_v) by H1, shannon_false. + done. +case Right. + conclude + ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v) + = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). + = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H. + = (max (min 1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)). + = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem. + = (max [[ F[FTop/x] ]]_v 0). + = ([[ F[FTop/x] ]]_v) by max_0_sem. + = ([[ F ]]_v) by H1, shannon_true. + done. +(*END*) qed. +(*DOCBEGIN + +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` + 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: + + 1. Inizia con una sequenza di comandi `assume` o `suppose` oppure + `by induction hypothesis we know`. Tale sequenza di comandi può anche + essere vuota. + + 2. Continua poi con almeno un comando `the thesis becomes`. + + 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 (...)`. + + 5. Se necessario un comando `conclude` seguito da un numero anche + molto lungo di passi `= (...) by ... .` per rendere la parte + sinistra della vostra tesi uguale alla parte destra. + + 6. Ogni caso termina con `done`. + +3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot) + avrà tante ipotesi induttive quante sono le sue sottoformule e tali + ipotesi sono necessarie per portare a termine la dimostrazione. + +I comandi da utilizzare +======================= + +* `the thesis becomes (...).` + + Afferma quale sia la tesi da dimostrare. Se ripetuto + permette di espandere le definizioni. + +* `we proceed by cases on (...) to prove (...).` + + Permette di andare per casi su una ipotesi (quando essa è della forma + `A ∨ B`). + + Esempio: `we proceed by cases on H to prove Q.` + +* `case ... .` + + Nelle dimostrazioni per casi o per induzioni si utulizza tale comando + per inizia la sotto prova relativa a un caso. Esempio: `case Fbot.` +* `done.` + + Ogni caso di una dimostrazione deve essere terminato con il comando + `done.` - \ No newline at end of file +* `assume ... : (...) .` + + Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume + un numero naturale `n`. + +* `by ..., ..., ..., we proved (...) (...).` + + Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi. + Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi + `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`. + +* `conclude (...) = (...) by ... .` + + Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando + con cui si inizia una catena di uguaglianze. La prima formula che si + scrive deve essere esattamente uguale alla parte sinistra della conclusione + originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.` + Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione + di una definizione, la parte `by ...` deve essere omessa. + +* `= (...) by ... .` + + Continua un comando `conclude`, lavorando sempre sulla parte sinistra della + tesi. + +DOCEND*)