almost ok

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index 233c323a21016844fd766ac00be9f278a149eab6..cfc36f690db2797865a1e3a041a428943742a70b 100644 (file)
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -43,8 +43,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
@@ -59,6 +59,11 @@ inductive Formula : Type ≝
 | FNot: Formula → Formula
 .
 
+(* Ripasso 2
+   =========
+   
+   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
@@ -80,13 +85,14 @@ 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.
 
-(* 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.
 
 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
  match F with
@@ -98,7 +104,12 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
   | 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).
@@ -188,14 +199,30 @@ espandere piano piano le definizioni.
 
 ### I comandi da utilizzare
 
-        the thesis becomes (...).
-        
-        we proceed by cases on (...) to prove (...).
+* `the thesis becomes (...).`
+
+  Afferma quale sia la tesi da dimostrare. Se ripetuto
+  permette di espandere le definizioni.
         
-        case ... .
+* `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`.
+   
+  Esempio: `we proceed by cases on H to prove Q.`
+  
+  Esempio: `we proceed by cases on (eqb x 0) to prove Q.`
         
-        done.
+* `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.`
+  
 DOCEND*)
   the thesis becomes ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v). 
   we proceed by cases on (eqb [[ FAtom x ]]_v 0) 
@@ -291,7 +318,7 @@ Abbiamo quindi quattro casi, in tutti si procede con un comando `conclude`:
 * `conclude (...) = (...) by ... .`
 
   Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
-  con cui sini inizia una catena di uguaglianze. La prima formula che si
+  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
@@ -368,9 +395,32 @@ case FAnd.
 Il caso FAnd
 ------------
 
-Una volta assunte eventuali sottoformule e ipotesi induttive 
+Una volta assunte eventuali sottoformule (che chiameremo f ed f1) e 
+relative ipotesi induttive 
 la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v)`.
 
+Utilizzando il lemma `sem_bool` si ottiene l'ipotesi aggiuntiva
+`([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1)`. Si procede poi per casi
+su di essa. 
+
+1. caso in cui vale `[[ FAtom x ]]_v = 0`.
+
+   Componendo le ipotesi induttive con `[[ FAtom x ]]_v = 0` e
+   espandendo alcune definizioni si ottengono
+   `([[ f[FBot/x ] ]]_v = [[ f ]]_v)` e 
+   `([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v)`.
+   
+   La sotto prova termina con una catena di uguaglianze che
+   lavora sul lato sinistro della tesi.
+   Espandendo alcune definizioni, utilizzando 
+   `[[ FAtom x ]]_v = 0` e le nuove ipotesi appena ottenute
+   si arriva a `(min [[ f ]]_v [[ f1 ]]_v)`.
+   Tale espressione è uguale alla parte destra della conclusione.
+
+1. caso in cui vale `[[ FAtom x ]]_v = 1`.
+
+   Analogo al precedente.
+
 DOCEND*)
   assume f : Formula.
   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
@@ -420,7 +470,7 @@ DOCEND*)
 case FOr.
 (*DOCBEGIN
 
-Il caso For
+Il caso FOr
 -----------
 
 Una volta assunte eventuali sottoformule e ipotesi induttive 
@@ -534,10 +584,13 @@ DOCEND*)
 case FNot.
 (*DOCBEGIN
 
-Il caso 
------------
+Il caso FNot 
+------------
+
+Una volta assunte eventuali sottoformule e ipotesi induttive 
+la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v)`.
 
-FISSARE BUG
+Analogo al caso FAnd.
 
 DOCEND*)
   assume f : Formula.