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

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