helm/software/matita/contribs/didactic/shannon.ma

   1 (* Esercizio -1
   2    ============
   3
   4    1. Leggere ATTENTAMENTE, e magari stampare, la documentazione
   5       reperibile all'URL seguente:
   6
   7         http://mowgli.cs.unibo.it/~tassi/exercise-shannon.ma.html
   8
   9    2. Questa volta si fa sul serio:
  10
  11       l'esercizio proposto è MOLTO difficile, occorre la vostra massima
  12       concentrazione (leggi: niente cut&paste selvaggio)
  13
  14 *)
  15
  16
  17 (* Esercizio 0
  18    ===========
  19
  20    Compilare i seguenti campi:
  21
  22    Nome1: ...
  23    Cognome1: ...
  24    Matricola1: ...
  25    Account1: ...
  26
  27    Nome2: ...
  28    Cognome2: ...
  29    Matricola2: ...
  30    Account2: ...
  31
  32 *)
  33
  34 (* ATTENZIONE
  35    ==========
  36
  37    Non modificare quanto segue
  38 *)
  39 include "nat/minus.ma".
  40 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  41 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
  42 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
  43 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
  44 definition max ≝ λn,m. if eqb (n - m) 0 then m else n.
  45 definition min ≝ λn,m. if eqb (n - m) 0 then n else m.
  46
  47 (* Ripasso 1
  48    =========
  49
  50    Il linguaggio delle formule, dove gli atomi sono
  51    rapperesentati da un numero naturale
  52 *)
  53 inductive Formula : Type ≝
  54 | FBot: Formula
  55 | FTop: Formula
  56 | FAtom: nat → Formula
  57 | FAnd: Formula → Formula → Formula
  58 | FOr: Formula → Formula → Formula
  59 | FImpl: Formula → Formula → Formula
  60 | FNot: Formula → Formula
  61 .
  62
  63 (* Ripasso 2
  64    =========
  65
  66    La semantica di una formula `F` in un mondo `v`: `[[ F ]]_v`
  67 *)
  68 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
  69  match F with
  70   [ FBot ⇒ 0
  71   | FTop ⇒ 1
  72   | FAtom n ⇒ min (v n) 1
  73   | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
  74   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  75   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  76   | FNot F1 ⇒ 1 - (sem v F1)
  77   ]
  78 .
  79
  80 (* ATTENZIONE
  81    ==========
  82
  83    Non modificare quanto segue.
  84 *)
  85 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  86 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  87 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
  88 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
  89 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.
  90
  91 (* Ripasso 3
  92    =========
  93
  94    L'operazione di sostituzione di una formula `G` al posto dell'atomo
  95    `x` in una formula `F`: `F[G/x]`
  96 *)
  97
  98 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
  99  match F with
 100   [ FBot ⇒ FBot
 101   | FTop ⇒ FTop
 102   | FAtom n ⇒ if eqb n x then G else (FAtom n)
 103   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 104   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 105   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 106   | FNot F ⇒ FNot (subst x G F)
 107   ].
 108
 109 (* ATTENZIONE
 110    ==========
 111
 112    Non modificare quanto segue.
 113 *)
 114 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 115 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 116 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 117 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 118 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 119 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 120 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 121 lemma min_1_sem: ∀F,v.min 1 [[ F ]]_v = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
 122 lemma max_0_sem: ∀F,v.max [[ F ]]_v 0 = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
 123 definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C).
 124
 125 (*DOCBEGIN
 126
 127 La libreria di Matita
 128 =====================
 129
 130 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 131
 132 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
 133 * lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1`
 134 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
 135 * lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true`
 136 * lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v`
 137 * lemma `max_0_sem` : `∀F,v.max [[ F ]]_v 0 = [[ F ]]_v`
 138
 139 Nota su `x = y` e `eqb x y`
 140 ---------------------------
 141
 142 Se vi siete mai chiesti la differenza tra `x = y` ed `eqb x y`
 143 quanto segue prova a chiarirla.
 144
 145 Presi due numeri `x` e `y` in ℕ, dire che `x = y` significa i due numeri
 146 sono lo stesso numero, ovvero che se `x` è il numero `3`,
 147 anche `y` è il numero `3`.
 148
 149 `eqb` è un funzione, un programma, che confronta due numeri naturali
 150 e restituisce `true` se sono uguali, `false` se sono diversi. L'utilizzo
 151 di tale programma è necessario per usare il costrutto (che è a sua volta
 152 un programma) `if E then A else B`, che lancia il programma `E`,
 153 e se il suo
 154 risultato è `true` si comporta come `A` altrimenti come `B`. Come
 155 ben sapete i programmi possono contenere errori. In particolare anche
 156 `eqb` potrebbe essere sbagliato, e per esempio restituire sempre `true`.
 157 I teoremi `eq_to_eqb_true` e
 158 `not_eq_to_eqb_false` sono la dimostrazione che il programma `eqb` è
 159 corretto, ovvero che che se `x = y` allora `eqb x y` restituisce `true`,
 160 se `x ≠ y` allora `eqb x y` restituisce `false`.
 161
 162 Il teorema di espansione di Shannon
 163 ===================================
 164
 165 Si definisce un connettivo logico `IFTE A B C` come
 166
 167         FOr (FAnd A B) (FAnd (FNot A) C)
 168
 169 Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente
 170 formula è equivalente a `F`:
 171
 172         IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])
 173
 174 Ovvero, fissato un mondo `v`, sostituisco l'atomo `x` con `FBot` se tale
 175 atomo è falso, lo sostituisco con `FTop` se è vero.
 176
 177 La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`.
 178
 179 Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo.
 180 Il lemma asserisce quanto segue:
 181
 182         ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v
 183
 184 Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver
 185 supposto che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`.
 186 I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`,
 187 una volta assunte le sottoformule e le relative ipotesi induttive,
 188 si conclude con una catena di uguaglianze.
 189
 190 Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo `n`,
 191 occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi
 192 aggiuntiva `n = x ∨ n ≠ x` (dove `x` è l'atomo su cui predica il teorema).
 193 Si procede per casi sull'ipotesi appena ottenuta.
 194 In entrambi i casi, usando i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false`
 195 si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`.
 196 Entrambi i casi si concludono con una catena di uguaglianze.
 197
 198 Il teorema principale si dimostra utilizzando il lemma `sem_bool` per
 199 ottenre l'ipotesi `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` su cui
 200 si procede poi per casi. Entrambi i casi si concludono con
 201 una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza
 202 e i lemmi `min_1_sem` oppure `max_0_sem`.
 203
 204 DOCEND*)
 205
 206 lemma shannon_false:
 207   ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v.
 208 (*BEGIN*)
 209 assume F : Formula.
 210 assume x : ℕ.
 211 assume v : (ℕ → ℕ).
 212 suppose ([[ FAtom x ]]_v = 0) (H).
 213 we proceed by induction on F to prove ([[ F[FBot/x] ]]_v = [[ F ]]_v).
 214 case FBot.
 215   the thesis becomes ([[ FBot[FBot/x] ]]_v = [[ FBot ]]_v).
 216   the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v).
 217   done.
 218 case FTop.
 219   the thesis becomes ([[ FTop[FBot/x] ]]_v = [[ FTop ]]_v).
 220   the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v).
 221   done.
 222 case FAtom.
 223   assume n : ℕ.
 224   the thesis becomes ([[ (FAtom n)[FBot/x] ]]_v = [[ FAtom n ]]_v).
 225   the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 226   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).
 227   we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 228     case Left.
 229       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
 230       conclude
 231           ([[ if eqb n x then FBot else (FAtom n) ]]_v)
 232         = ([[ if true then FBot else (FAtom n) ]]_v) by H3.
 233         = ([[ FBot ]]_v).
 234         = 0.
 235         = ([[ FAtom x ]]_v) by H.
 236         = ([[ FAtom n ]]_v) by H2.
 237     done.
 238     case Right.
 239       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
 240       conclude
 241           ([[ if eqb n x then FBot else (FAtom n) ]]_v)
 242         = ([[ if false then FBot else (FAtom n) ]]_v) by H3.
 243         = ([[ FAtom n ]]_v).
 244     done.
 245 case FAnd.
 246   assume f1 : Formula.
 247   by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
 248   assume f2 : Formula.
 249   by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
 250   the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]_v = [[ FAnd f1 f2 ]]_v).
 251   conclude
 252       ([[ (FAnd f1 f2)[FBot/x] ]]_v)
 253     = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]_v).
 254     = (min [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v).
 255     = (min [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1.
 256     = (min [[ f1 ]]_v [[ f2 ]]_v) by H2.
 257     = ([[ FAnd f1 f2 ]]_v).
 258   done.
 259 case FOr.
 260   assume f1 : Formula.
 261   by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
 262   assume f2 : Formula.
 263   by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
 264   the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]_v = [[ FOr f1 f2 ]]_v).
 265   conclude
 266       ([[ (FOr f1 f2)[FBot/x] ]]_v)
 267     = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]_v).
 268     = (max [[ f1[FBot/x] ]]_v  [[ f2[FBot/x] ]]_v).
 269     = (max [[ f1 ]]_v  [[ f2[FBot/x] ]]_v) by H1.
 270     = (max [[ f1 ]]_v  [[ f2 ]]_v) by H2.
 271     = ([[ FOr f1 f2 ]]_v).
 272   done.
 273 case FImpl.
 274   assume f1 : Formula.
 275   by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
 276   assume f2 : Formula.
 277   by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
 278   the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]_v = [[ FImpl f1 f2 ]]_v).
 279   conclude
 280       ([[ (FImpl f1 f2)[FBot/x] ]]_v)
 281     = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]_v).
 282     = (max (1 - [[ f1[FBot/x] ]]_v) [[ f2[FBot/x] ]]_v).
 283     = (max (1 - [[ f1 ]]_v) [[ f2[FBot/x] ]]_v) by H1.
 284     = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2.
 285     = ([[ FImpl f1 f2 ]]_v).
 286   done.
 287 case FNot.
 288   assume f : Formula.
 289   by induction hypothesis we know ([[ f[FBot/x] ]]_v = [[ f ]]_v) (H1).
 290   the thesis becomes ([[ (FNot f)[FBot/x] ]]_v = [[ FNot f ]]_v).
 291   conclude
 292       ([[ (FNot f)[FBot/x] ]]_v)
 293     = ([[ FNot (f[FBot/x]) ]]_v).
 294     = (1 - [[ f[FBot/x] ]]_v).
 295     = (1 - [[ f ]]_v) by H1.
 296     = ([[ FNot f ]]_v).
 297   done.
 298 (*END*)
 299 qed.
 300
 301 lemma shannon_true:
 302   ∀F,x,v. [[ FAtom x ]]_v = 1 → [[ F[FTop/x] ]]_v = [[ F ]]_v.
 303 (*BEGIN*)
 304 assume F : Formula.
 305 assume x : ℕ.
 306 assume v : (ℕ → ℕ).
 307 suppose ([[ FAtom x ]]_v = 1) (H).
 308 we proceed by induction on F to prove ([[ F[FTop/x] ]]_v = [[ F ]]_v).
 309 case FBot.
 310   the thesis becomes ([[ FBot[FTop/x] ]]_v = [[ FBot ]]_v).
 311   the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v).
 312   done.
 313 case FTop.
 314   the thesis becomes ([[ FTop[FTop/x] ]]_v = [[ FTop ]]_v).
 315   the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v).
 316   done.
 317 case FAtom.
 318   assume n : ℕ.
 319   the thesis becomes ([[ (FAtom n)[FTop/x] ]]_v = [[ FAtom n ]]_v).
 320   the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 321   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).
 322   we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 323     case Left.
 324       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
 325       conclude
 326           ([[ if eqb n x then FTop else (FAtom n) ]]_v)
 327         = ([[ if true then FTop else (FAtom n) ]]_v) by H3.
 328         = ([[ FTop ]]_v).
 329         = 1.
 330         = ([[ FAtom x ]]_v) by H.
 331         = ([[ FAtom n ]]_v) by H2.
 332     done.
 333     case Right.
 334       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
 335       conclude
 336           ([[ if eqb n x then FTop else (FAtom n) ]]_v)
 337         = ([[ if false then FTop else (FAtom n) ]]_v) by H3.
 338         = ([[ FAtom n ]]_v).
 339     done.
 340 case FAnd.
 341   assume f1 : Formula.
 342   by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
 343   assume f2 : Formula.
 344   by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
 345   the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]_v = [[ FAnd f1 f2 ]]_v).
 346   conclude
 347       ([[ (FAnd f1 f2)[FTop/x] ]]_v)
 348     = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]_v).
 349     = (min [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v).
 350     = (min [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1.
 351     = (min [[ f1 ]]_v [[ f2 ]]_v) by H2.
 352     = ([[ FAnd f1 f2 ]]_v).
 353   done.
 354 case FOr.
 355   assume f1 : Formula.
 356   by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
 357   assume f2 : Formula.
 358   by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
 359   the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]_v = [[ FOr f1 f2 ]]_v).
 360   conclude
 361       ([[ (FOr f1 f2)[FTop/x] ]]_v)
 362     = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]_v).
 363     = (max [[ f1[FTop/x] ]]_v  [[ f2[FTop/x] ]]_v).
 364     = (max [[ f1 ]]_v  [[ f2[FTop/x] ]]_v) by H1.
 365     = (max [[ f1 ]]_v  [[ f2 ]]_v) by H2.
 366     = ([[ FOr f1 f2 ]]_v).
 367   done.
 368 case FImpl.
 369   assume f1 : Formula.
 370   by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
 371   assume f2 : Formula.
 372   by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
 373   the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]_v = [[ FImpl f1 f2 ]]_v).
 374   conclude
 375       ([[ (FImpl f1 f2)[FTop/x] ]]_v)
 376     = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]_v).
 377     = (max (1 - [[ f1[FTop/x] ]]_v) [[ f2[FTop/x] ]]_v).
 378     = (max (1 - [[ f1 ]]_v) [[ f2[FTop/x] ]]_v) by H1.
 379     = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2.
 380     = ([[ FImpl f1 f2 ]]_v).
 381   done.
 382 case FNot.
 383   assume f : Formula.
 384   by induction hypothesis we know ([[ f[FTop/x] ]]_v = [[ f ]]_v) (H1).
 385   the thesis becomes ([[ (FNot f)[FTop/x] ]]_v = [[ FNot f ]]_v).
 386   conclude
 387       ([[ (FNot f)[FTop/x] ]]_v)
 388     = ([[ FNot (f[FTop/x]) ]]_v).
 389     = (1 - [[ f[FTop/x] ]]_v).
 390     = (1 - [[ f ]]_v) by H1.
 391     = ([[ FNot f ]]_v).
 392   done.
 393 (*END*)
 394 qed.
 395
 396 theorem shannon :
 397   ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F.
 398 (*BEGIN*)
 399 assume F : Formula.
 400 assume x : ℕ.
 401 assume v : (ℕ → ℕ).
 402 the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v).
 403 by sem_bool we proved ([[ FAtom x]]_v = 0 ∨ [[ FAtom x]]_v = 1) (H).
 404 we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v).
 405 case Left.
 406   conclude
 407       ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v)
 408     = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 409     = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 410     = (max (min  [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
 411     = (max (min  0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H.
 412     = (max 0 (min 1 [[ F[FBot/x] ]]_v)).
 413     = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem.
 414     = ([[ F[FBot/x] ]]_v).
 415     = ([[ F ]]_v) by H1, shannon_false.
 416   done.
 417 case Right.
 418   conclude
 419       ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v)
 420     = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 421     = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 422     = (max (min  [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
 423     = (max (min  1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H.
 424     = (max (min  1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)).
 425     = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem.
 426     = (max [[ F[FTop/x] ]]_v 0).
 427     = ([[ F[FTop/x] ]]_v) by max_0_sem.
 428     = ([[ F ]]_v) by H1, shannon_true.
 429   done.
 430 (*END*)
 431 qed.
 432
 433 (*DOCBEGIN
 434
 435 Note generali
 436 =============
 437
 438 Si ricorda che:
 439
 440 1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un
 441    simbolo `→` è opportuno usare il comando `assume` oppure `suppose`
 442    oppure (se si è in un caso di una dimostrazione per induzione) il comando
 443    `by induction hypothesis we know` (che vengono nuovamente spiegati in seguito).
 444
 445 2. Ogni caso (o sotto caso) della dimostrazione:
 446
 447    1. Inizia con una sequenza di comandi `assume` o `suppose` oppure
 448       `by induction hypothesis we know`. Tale sequenza di comandi può anche
 449       essere vuota.
 450
 451    2. Continua poi con almeno un comando `the thesis becomes`.
 452
 453    3. Eventualmente seguono vari comandi `by ... we proved` per
 454       utilizzare i teoremi già disponibili per generare nuove
 455       ipotesi.
 456
 457    4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`.
 458
 459    5. Se necessario un comando `conclude` seguito da un numero anche
 460       molto lungo di passi `= (...) by ... .` per rendere la parte
 461       sinistra della vostra tesi uguale alla parte destra.
 462
 463    6. Ogni caso termina con `done`.
 464
 465 3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot)
 466    avrà tante ipotesi induttive quante sono le sue sottoformule e tali
 467    ipotesi sono necessarie per portare a termine la dimostrazione.
 468
 469 I comandi da utilizzare
 470 =======================
 471
 472 * `the thesis becomes (...).`
 473
 474   Afferma quale sia la tesi da dimostrare. Se ripetuto
 475   permette di espandere le definizioni.
 476
 477 * `we proceed by cases on (...) to prove (...).`
 478
 479   Permette di andare per casi su una ipotesi (quando essa è della forma
 480   `A ∨ B`).
 481
 482   Esempio: `we proceed by cases on H to prove Q.`
 483
 484 * `case ... .`
 485
 486   Nelle dimostrazioni per casi o per induzioni si utulizza tale comando
 487   per inizia la sotto prova relativa a un caso. Esempio: `case Fbot.`
 488
 489 * `done.`
 490
 491   Ogni caso di una dimostrazione deve essere terminato con il comando
 492   `done.`
 493
 494 * `assume ... : (...) .`
 495
 496   Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume
 497   un numero naturale `n`.
 498
 499 * `by ..., ..., ..., we proved (...) (...).`
 500
 501   Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi.
 502   Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi
 503   `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`.
 504
 505 * `conclude (...) = (...) by ... .`
 506
 507   Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
 508   con cui si inizia una catena di uguaglianze. La prima formula che si
 509   scrive deve essere esattamente uguale alla parte sinistra della conclusione
 510   originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.`
 511   Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
 512   di una definizione, la parte `by ...` deve essere omessa.
 513
 514 * `= (...) by ... .`
 515
 516   Continua un comando `conclude`, lavorando sempre sulla parte sinistra della
 517   tesi.
 518
 519 DOCEND*)