From 79a184f4d6a78a737909d7358e926716e9bab257 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 5 Nov 2008 22:46:24 +0000
Subject: [PATCH] still some glitches, but reaching a decent state

---
 .../matita/contribs/didactic/shannon.ma       | 291 ++++++++++++++----
 1 file changed, 231 insertions(+), 60 deletions(-)

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index d88f46ad7..5e1db41e8 100644
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -1,3 +1,18 @@
+(* Esercizio -1
+   ============
+   
+   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!)
+       
+*)
+
+
 (* Esercizio 0
    ===========
 
@@ -66,36 +81,13 @@ notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 f
 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).
 
-(*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 `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
-
-
-DOCEND*)
-
 (* ATTENZIONE
    ==========
    
    Non modificare quanto segue.
 *)
 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
@@ -115,13 +107,96 @@ notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associat
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 
+(*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 `eqb_n_n` : `∀x.eqb x x = true`
+* lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
+
+Il teorema di espansione di Shannon
+===================================
+
+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`:
+
+        if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x])
+        
+Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso
+nel mondo `v`, altrimenti lo sostituisco con `FTop`.
+
+DOCEND*)
+
 theorem shannon : 
   ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v.
 assume F : Formula.
 assume x : ℕ.
 assume v : (ℕ → ℕ).
 we proceed by induction on F to prove ([[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v).
+(*DOCBEGIN
+
+La dimostrazione 
+================
+
+La dimostrazione procede per induzione sulla formula `F`. 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).
+   
+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 combinare le 
+      ipotesi tra loro o 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.
+
+DOCEND*)
 case FBot.
+(*DOCBEGIN
+
+Il caso FBot
+------------
+
+La tesi è 
+
+        [[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v
+
+Si procede per casi su `eqb [[FAtom x]]_v 0`. In entrambi i casi basta 
+espandere piano piano le definizioni.
+
+### I comandi da utilizzare
+
+        the thesis becomes (...).
+        
+        we proceed by cases on (...) to prove (...).
+        
+        case ... .
+        
+        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) 
     to prove ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
@@ -134,6 +209,14 @@ case FBot.
   case false.
     done.
 case FTop.
+(*DOCBEGIN
+
+Il caso FTop
+------------
+
+Analogo al caso FBot
+
+DOCEND*)
   we proceed by cases on (eqb [[ FAtom x ]]_v 0)
     to prove ([[ if eqb [[FAtom x]]_v 0 then FTop[FBot/x] else (FTop[FTop/x]) ]]_v = [[FTop]]_v).
   case true.
@@ -141,6 +224,85 @@ case FTop.
   case false.
     done.     
 case FAtom.
+(*DOCBEGIN
+
+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 usare
+
+* `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 sini 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*)
   assume n : ℕ.
   the thesis becomes ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H).
@@ -179,27 +341,37 @@ case FAtom.
         = [[ FAtom n ]]_v by H2.
       done.
   case Right.
+    by not_eq_to_eqb_false, H2 we proved (eqb n x = false) (H3).
     we proceed by cases on H1 to prove 
       ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
     case Left.
       conclude 
           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
-        = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.  
+        = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.  
         = [[ (FAtom n)[ FBot/x ] ]]_v.
         = [[ if eqb n x then FBot else (FAtom n) ]]_v.
-        = [[ if false then FBot else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2).
+        = [[ if false then FBot else (FAtom n) ]]_v by H3.
         = [[ FAtom n ]]_v. 
       done.
     case Right.
       conclude 
           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
-        = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.  
+        = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.  
         = [[ FAtom n[ FTop/x ] ]]_v.
         = [[ if eqb n x then FTop else (FAtom n) ]]_v.
-        = [[ if false then FTop else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2).
+        = [[ if false then FTop else (FAtom n) ]]_v by H3.
         = [[ FAtom n ]]_v. 
       done.
 case FAnd.
+(*DOCBEGIN
+
+Il caso FAnd
+------------
+
+Una volta assunte eventuali sottoformule e 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)`.
+
+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).
   assume f1 : Formula.
@@ -246,6 +418,17 @@ case FAnd.
       = ([[ FAnd f f1 ]]_v).
     done.
 case FOr.
+(*DOCBEGIN
+
+Il caso For
+-----------
+
+Una volta assunte eventuali sottoformule e ipotesi induttive 
+la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v)`.
+
+Analogo al caso FAnd.
+
+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).
   assume f1 : Formula.
@@ -292,6 +475,17 @@ case FOr.
       = ([[ FOr f f1 ]]_v).
     done.
 case FImpl.
+(*DOCBEGIN
+
+Il caso FImpl
+-------------
+ 
+Una volta assunte eventuali sottoformule e ipotesi induttive 
+la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v)`.
+
+Analogo al caso FAnd.
+
+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).
   assume f1 : Formula.
@@ -338,6 +532,14 @@ case FImpl.
       = ([[ FImpl f f1 ]]_v).
     done.
 case FNot.
+(*DOCBEGIN
+
+Il caso 
+-----------
+
+FISSARE BUG
+
+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).
   the thesis becomes 
@@ -355,6 +557,7 @@ case FNot.
       = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
       = ([[ (FNot f)[ FBot/x ] ]]_v).
       = ([[ FNot (f[ FBot/x ]) ]]_v).
+      (* FIXME, ASSERT IN PARAMOD = (1 - [[ f[ FBot/x ] ]]_v). = [[ FNot f ]]_v). *)
       change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v).
       = (1 - [[ f ]]_v) by H5.
       change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
@@ -375,35 +578,3 @@ case FNot.
     done.
 qed.
 
-let rec maxatom (F : Formula) on F : ℕ ≝
-  match F with
-  [ FTop ⇒ 0
-  | FBot ⇒ 0
-  | FAtom n ⇒ n
-  | FAnd F1 F2 ⇒ max (maxatom F1) (maxatom F2)
-  | FOr F1 F2 ⇒ max (maxatom F1) (maxatom F2)
-  | FImpl F1 F2 ⇒ max (maxatom F1) (maxatom F2)
-  | FNot F1 ⇒ maxatom F1
-  ]
-.
-
-let rec expandall (F : Formula) (v : ℕ → ℕ) (n : nat) on n: Formula ≝
-  match n with
-  [ O ⇒ F
-  | S m ⇒ 
-      if eqb [[ FAtom n ]]_v 0 
-      then (expandall F v m)[FBot/n] 
-      else ((expandall F v m)[FTop/n])
-  ]
-.
-
-lemma BDD : ∀F,n,v. [[ expandall F v n ]]_v = [[ F ]]_v.
-intros; elim n; simplify; [reflexivity]
-cases (sem_bool (FAtom (S n1)) v); simplify in H1; rewrite > H1; simplify;
-[ lapply (shannon (expandall F v n1) (S n1) v);
-  simplify in Hletin; rewrite > H1 in Hletin; simplify in Hletin;
-  rewrite > Hletin; assumption;
-| lapply (shannon (expandall F v n1) (S n1) v);
-  simplify in Hletin; rewrite > H1 in Hletin; simplify in Hletin;
-  rewrite > Hletin; assumption;]
-qed.
-- 
2.39.2