From: Enrico Tassi Date: Thu, 6 Nov 2008 20:03:39 +0000 (+0000) Subject: exercise ready X-Git-Tag: make_still_working~4583 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=66155917bd62757397bc324029d0baade2cc281f;p=helm.git exercise ready --- diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma index 13b9b018b..6979cbbf0 100644 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ b/helm/software/matita/contribs/didactic/shannon.ma @@ -119,6 +119,8 @@ 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 @@ -135,20 +137,46 @@ Per portare a termine l'esercitazione sono necessari i seguenti lemmi: 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 ha in un mondo `v` la stessa semantica di `F`: +formula è equivalente a `F`: - if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) + IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso -nel mondo `v`, altrimenti lo sostituisco con `FTop`. +in un mondo mondo `v`, altrimenti lo sostituisco con `FTop`. -DOCEND*) +La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`. -definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C). +Vediamo la dimostrazione del primo, che asserisce + + ∀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 sottofrmule e le ipotesi induttive, si conclude +con una catena di uguaglianze. + +Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo, +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)`. +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 +una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza +e i lemmi `min_1_sem` e `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 : (ℕ → ℕ). @@ -238,10 +266,12 @@ case FNot. = (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 : (ℕ → ℕ). @@ -331,10 +361,12 @@ case FNot. = (1 - [[ f ]]_v) by H1. = ([[ FNot f ]]_v). done. +(*END*) qed. theorem shannon : ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F. +(*BEGIN*) assume F : Formula. assume x : ℕ. assume v : (ℕ → ℕ). @@ -366,6 +398,7 @@ case Right. = ([[ F[FTop/x] ]]_v) by max_0_sem. = ([[ F ]]_v) by H1, shannon_true. done. +(*END*) qed. (*DOCBEGIN @@ -403,60 +436,6 @@ Si ricorda che: avrà tante ipotesi induttive quante sono le sue sottoformule e tali ipotesi sono necessarie per portare a termine la dimostrazione. -La dimostrazione -================ - -... - -Il caso (FAtom n) ------------------ - -Questo è il caso più difficile di tutta la dimostrazione. - -La tesi è `([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v)` - -Per dimostrarla è necessario utilizzare il lemma `decidable_eq_nat` per -ottenere l'ipotesi agiuntiva `n = x ∨ n ≠ x` che chiameremo `H` e il lemma -`sem_bool` per ottenre l'ipotesi aggiuntiva `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` -che chiameremo `H1`. - -Si procede poi per casi sull'ipotesi `H`, e in ogni suo sotto caso si procede -per casi su `H1`. - -Nei casi in cui è presente l'ipotesi aggiuntiva `n ≠ x` è bene -ottenre tramite il lemma `not_eq_to_eqb_false` l'ipotesi aggiuntiva -`eqb n x = false`. - -Abbiamo quindi quattro casi, in tutti si procede con un comando `conclude`: - -1. Caso in cui `n=x` e `[[ FAtom x ]]_v = 0`. - - Utilizzando l'ipotesi `[[ FAtom x ]]_v = 0` e espandendo alcune definizioni - si ottiene che la parte sinistra della conclusione è - - ([[ if eqb n x then FBot else (FAtom n) ]]_v) - - Usando l'ipotesi `n = x`, poi il lemma `eqb_n_n` e espandendo alcune - definizioni si ottiene `0`. Tornando ad usare le due ipotesi - `n=x` e `[[ FAtom x ]]_v = 0` si ottiene una formula uguale al - lato destro della conclusione. - -2. Caso in cui `n=x` e `[[ FAtom x ]]_v = 1`. - - Analogo al caso precedente. - -3. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 0`. - - Si ottiene l'ipotesi aggiuntiva `eqb n x = false` usando il lemma - `not_eq_to_eqb_false` insieme all'ipotesi `n ≠ x`. Usando il comando - conlude e l'ipotesi `[[ FAtom x ]]_v = 0`, la nuova ipotesi appena - ottenuta e espandendo alcune definizioni si ottiene una formula - uguale a quella di destra. - -4. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 1`. - - Analogo al caso precedente. - I comandi da utilizzare ======================= @@ -468,11 +447,9 @@ I comandi da utilizzare * `we proceed by cases on (...) to prove (...).` Permette di andare per casi su una ipotesi (quando essa è della forma - `A ∨ B`) oppure su una espressione come `eqb n m`. + `A ∨ B`). Esempio: `we proceed by cases on H to prove Q.` - - Esempio: `we proceed by cases on (eqb x 0) to prove Q.` * `case ... .`