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
  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 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
  63  match F with
  64   [ FBot ⇒ 0
  65   | FTop ⇒ 1
  66   | FAtom n ⇒ min (v n) 1
  67   | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
  68   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  69   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  70   | FNot F1 ⇒ 1 - (sem v F1)
  71   ]
  72 .
  73
  74 (* ATTENZIONE
  75    ==========
  76
  77    Non modificare quanto segue.
  78 *)
  79 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  80 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  81 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
  82 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
  83
  84 (* ATTENZIONE
  85    ==========
  86
  87    Non modificare quanto segue.
  88 *)
  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 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
  92  match F with
  93   [ FBot ⇒ FBot
  94   | FTop ⇒ FTop
  95   | FAtom n ⇒ if eqb n x then G else (FAtom n)
  96   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
  97   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
  98   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
  99   | FNot F ⇒ FNot (subst x G F)
 100   ].
 101
 102 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 103 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 104 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 105 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 106 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 107 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 108 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 109
 110 (*DOCBEGIN
 111
 112 La libreria di Matita
 113 =====================
 114
 115 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 116
 117 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
 118 * lemma `eqb_n_n` : `∀x.eqb x x = true`
 119 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
 120
 121 Il teorema di espansione di Shannon
 122 ===================================
 123
 124 Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente
 125 formula ha in un mondo `v` la stessa semantica di `F`:
 126
 127         if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x])
 128
 129 Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso
 130 nel mondo `v`, altrimenti lo sostituisco con `FTop`.
 131
 132 DOCEND*)
 133
 134 theorem shannon :
 135   ∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v.
 136 assume F : Formula.
 137 assume x : ℕ.
 138 assume v : (ℕ → ℕ).
 139 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).
 140 (*DOCBEGIN
 141
 142 La dimostrazione
 143 ================
 144
 145 La dimostrazione procede per induzione sulla formula `F`. Si ricorda che:
 146
 147 1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un
 148    simbolo `→` è opportuno usare il comando `assume` oppure `suppose` (che
 149    vengono nuovamente spiegati in seguito).
 150
 151 2. Ogni caso (o sotto caso) della dimostrazione:
 152
 153    1. Inizia con una sequenza di comandi `assume` o `suppose` oppure
 154       `by induction hypothesis we know`. Tale sequenza di comandi può anche
 155       essere vuota.
 156
 157    2. Continua poi con almeno un comando `the thesis becomes`.
 158
 159    3. Eventualmente seguono vari comandi `by ... we proved` per combinare le
 160       ipotesi tra loro o utilizzare i teoremi già disponibili per generare nuove
 161       ipotesi.
 162
 163    4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`.
 164
 165    5. Se necessario un comando `conclude` seguito da un numero anche
 166       molto lungo di passi `= (...) by ... .` per rendere la parte
 167       sinistra della vostra tesi uguale alla parte destra.
 168
 169    6. Ogni caso termina con `done`.
 170
 171 3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot)
 172    avrà tante ipotesi induttive quante sono le sue sottoformule e tali
 173    ipotesi sono necessarie per portare a termine la dimostrazione.
 174
 175 DOCEND*)
 176 case FBot.
 177 (*DOCBEGIN
 178
 179 Il caso FBot
 180 ------------
 181
 182 La tesi è
 183
 184         [[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v
 185
 186 Si procede per casi su `eqb [[FAtom x]]_v 0`. In entrambi i casi basta
 187 espandere piano piano le definizioni.
 188
 189 ### I comandi da utilizzare
 190
 191         the thesis becomes (...).
 192
 193         we proceed by cases on (...) to prove (...).
 194
 195         case ... .
 196
 197         done.
 198
 199 DOCEND*)
 200   the thesis becomes ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
 201   we proceed by cases on (eqb [[ FAtom x ]]_v 0)
 202     to prove ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
 203   case true.
 204     the thesis becomes ([[ if true then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
 205     the thesis becomes ([[ FBot[FBot/x]]]_v = [[FBot]]_v).
 206     the thesis becomes ([[ FBot ]]_v = [[FBot]]_v).
 207     the thesis becomes (0 = 0).
 208     done.
 209   case false.
 210     done.
 211 case FTop.
 212 (*DOCBEGIN
 213
 214 Il caso FTop
 215 ------------
 216
 217 Analogo al caso FBot
 218
 219 DOCEND*)
 220   we proceed by cases on (eqb [[ FAtom x ]]_v 0)
 221     to prove ([[ if eqb [[FAtom x]]_v 0 then FTop[FBot/x] else (FTop[FTop/x]) ]]_v = [[FTop]]_v).
 222   case true.
 223     done.
 224   case false.
 225     done.
 226 case FAtom.
 227 (*DOCBEGIN
 228
 229 Il caso (FAtom n)
 230 -----------------
 231
 232 Questo è il caso più difficile di tutta la dimostrazione.
 233
 234 La tesi è `([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v)`
 235
 236 Per dimostrarla è necessario utilizzare il lemma `decidable_eq_nat` per
 237 ottenere l'ipotesi agiuntiva `n = x ∨ n ≠ x` che chiameremo `H` e il lemma
 238 `sem_bool` per ottenre l'ipotesi aggiuntiva `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1`
 239 che chiameremo `H1`.
 240
 241 Si procede poi per casi sull'ipotesi `H`, e in ogni suo sotto caso si procede
 242 per casi su `H1`.
 243
 244 Nei casi in cui è presente l'ipotesi aggiuntiva `n ≠ x` è bene
 245 ottenre tramite il lemma `not_eq_to_eqb_false` l'ipotesi aggiuntiva
 246 `eqb n x = false`.
 247
 248 Abbiamo quindi quattro casi, in tutti si procede con un comando `conclude`:
 249
 250 1. Caso in cui `n=x` e `[[ FAtom x ]]_v = 0`.
 251
 252    Utilizzando l'ipotesi `[[ FAtom x ]]_v = 0` e espandendo alcune definizioni
 253    si ottiene che la parte sinistra della conclusione è
 254
 255          ([[ if eqb n x then FBot else (FAtom  n) ]]_v)
 256
 257    Usando l'ipotesi `n = x`, poi il lemma `eqb_n_n` e espandendo alcune
 258    definizioni si ottiene `0`. Tornando ad usare le due ipotesi
 259    `n=x` e `[[ FAtom x ]]_v = 0` si ottiene una formula uguale al
 260    lato destro della conclusione.
 261
 262 2. Caso in cui `n=x` e `[[ FAtom x ]]_v = 1`.
 263
 264    Analogo al caso precedente.
 265
 266 3. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 0`.
 267
 268    Si ottiene l'ipotesi aggiuntiva `eqb n x = false` usando il lemma
 269    `not_eq_to_eqb_false` insieme all'ipotesi `n ≠ x`. Usando il comando
 270    conlude e l'ipotesi `[[ FAtom x ]]_v = 0`, la nuova ipotesi appena
 271    ottenuta e espandendo alcune definizioni si ottiene una formula
 272    uguale a quella di destra.
 273
 274 4. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 1`.
 275
 276    Analogo al caso precedente.
 277
 278 ### I comandi da usare
 279
 280 * `assume ... : (...) .`
 281
 282   Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume
 283   un numero naturale `n`.
 284
 285 * `by ..., ..., ..., we proved (...) (...).`
 286
 287   Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi.
 288   Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi
 289   `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`.
 290
 291 * `conclude (...) = (...) by ... .`
 292
 293   Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
 294   con cui sini inizia una catena di uguaglianze. La prima formula che si
 295   scrive deve essere esattamente uguale alla parte sinistra della conclusione
 296   originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.`
 297   Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
 298   di una definizione, la parte `by ...` deve essere omessa.
 299
 300 * `= (...) by ... .`
 301
 302   Continua un comando `conclude`, lavorando sempre sulla parte sinistra della
 303   tesi.
 304
 305 DOCEND*)
 306   assume n : ℕ.
 307   the thesis becomes ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 308   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H).
 309   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H1).
 310   we proceed by cases on H to prove
 311     ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 312   case Left. (* H2 : n = x *)
 313     we proceed by cases on H1 to prove
 314       ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 315     case Left. (* H3 : [[ FAtom x ]]_v = 0 *)
 316       conclude
 317           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 318         = ([[ if eqb 0 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
 319         = ([[ if true then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v).
 320         = ([[ (FAtom n)[ FBot/x ] ]]_v).
 321         = ([[ if eqb n x then FBot else (FAtom  n) ]]_v).
 322         = ([[ if eqb n n then FBot else (FAtom  n) ]]_v) by H2.
 323         = ([[ if true then FBot else (FAtom  n) ]]_v) by eqb_n_n.
 324         = ([[ FBot ]]_v).
 325         = 0.
 326         = [[ FAtom x ]]_v by H3.
 327         = [[ FAtom n ]]_v by H2.
 328       done.
 329     case Right.
 330       conclude
 331           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 332         = ([[ if eqb 1 0 then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
 333         = ([[ if false then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v).
 334         = ([[ (FAtom n)[ FTop/x ] ]]_v).
 335         = ([[ if eqb n x then FTop else (FAtom  n) ]]_v).
 336         = ([[ if eqb n n then FTop else (FAtom  n) ]]_v) by H2.
 337         = ([[ if true then FTop else (FAtom  n) ]]_v) by eqb_n_n.
 338         = ([[ FTop ]]_v).
 339         = 1.
 340         = [[ FAtom x ]]_v by H3.
 341         = [[ FAtom n ]]_v by H2.
 342       done.
 343   case Right.
 344     by not_eq_to_eqb_false, H2 we proved (eqb n x = false) (H3).
 345     we proceed by cases on H1 to prove
 346       ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
 347     case Left.
 348       conclude
 349           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 350         = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.
 351         = [[ (FAtom n)[ FBot/x ] ]]_v.
 352         = [[ if eqb n x then FBot else (FAtom n) ]]_v.
 353         = [[ if false then FBot else (FAtom n) ]]_v by H3.
 354         = [[ FAtom n ]]_v.
 355       done.
 356     case Right.
 357       conclude
 358           ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
 359         = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.
 360         = [[ FAtom n[ FTop/x ] ]]_v.
 361         = [[ if eqb n x then FTop else (FAtom n) ]]_v.
 362         = [[ if false then FTop else (FAtom n) ]]_v by H3.
 363         = [[ FAtom n ]]_v.
 364       done.
 365 case FAnd.
 366 (*DOCBEGIN
 367
 368 Il caso FAnd
 369 ------------
 370
 371 Una volta assunte eventuali sottoformule e ipotesi induttive
 372 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)`.
 373
 374 DOCEND*)
 375   assume f : Formula.
 376   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 377   assume f1 : Formula.
 378   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1).
 379   the thesis becomes
 380     ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v).
 381   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 382   we proceed by cases on H2 to prove
 383     ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v).
 384   case Left.
 385     by H3, H we proved
 386       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 387     by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 388     by H3, H1 we proved
 389       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 390     by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
 391     conclude
 392         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
 393       = ([[ if eqb 0 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
 394       = ([[ if true then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v).
 395       = ([[ (FAnd f f1)[ FBot/x ] ]]_v).
 396       = ([[ FAnd (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
 397       = (min [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v).
 398       = (min [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5.
 399       = (min [[ f ]]_v [[ f1 ]]_v) by H6.
 400       = ([[ FAnd f f1 ]]_v).
 401     done.
 402   case Right.
 403     by H3, H we proved
 404       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 405     by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 406     by H3, H1 we proved
 407       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 408     by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
 409     conclude
 410         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
 411       = ([[ if eqb 1 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
 412       = ([[ if false then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v).
 413       = ([[ (FAnd f f1)[ FTop/x ] ]]_v).
 414       = ([[ FAnd (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
 415       = (min [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v).
 416       = (min [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5.
 417       = (min [[ f ]]_v [[ f1 ]]_v) by H6.
 418       = ([[ FAnd f f1 ]]_v).
 419     done.
 420 case FOr.
 421 (*DOCBEGIN
 422
 423 Il caso For
 424 -----------
 425
 426 Una volta assunte eventuali sottoformule e ipotesi induttive
 427 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)`.
 428
 429 Analogo al caso FAnd.
 430
 431 DOCEND*)
 432   assume f : Formula.
 433   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 434   assume f1 : Formula.
 435   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1).
 436   the thesis becomes
 437     ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v).
 438   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 439   we proceed by cases on H2 to prove
 440     ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v).
 441   case Left.
 442     by H3, H we proved
 443       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 444     by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 445     by H3, H1 we proved
 446       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 447     by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
 448     conclude
 449         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
 450       = ([[ if eqb 0 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
 451       = ([[ if true then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v).
 452       = ([[ (FOr f f1)[ FBot/x ] ]]_v).
 453       = ([[ FOr (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
 454       = (max [[ f[ FBot/x ] ]]_v [[ f1[ FBot/x ] ]]_v).
 455       = (max [[ f ]]_v [[ f1[ FBot/x ] ]]_v) by H5.
 456       = (max [[ f ]]_v [[ f1 ]]_v) by H6.
 457       = ([[ FOr f f1 ]]_v).
 458     done.
 459   case Right.
 460     by H3, H we proved
 461       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 462     by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 463     by H3, H1 we proved
 464       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 465     by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
 466     conclude
 467         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
 468       = ([[ if eqb 1 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
 469       = ([[ if false then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v).
 470       = ([[ (FOr f f1)[ FTop/x ] ]]_v).
 471       = ([[ FOr (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
 472       = (max [[ f[ FTop/x ] ]]_v [[ f1[ FTop/x ] ]]_v).
 473       = (max [[ f ]]_v [[ f1[ FTop/x ] ]]_v) by H5.
 474       = (max [[ f ]]_v [[ f1 ]]_v) by H6.
 475       = ([[ FOr f f1 ]]_v).
 476     done.
 477 case FImpl.
 478 (*DOCBEGIN
 479
 480 Il caso FImpl
 481 -------------
 482
 483 Una volta assunte eventuali sottoformule e ipotesi induttive
 484 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)`.
 485
 486 Analogo al caso FAnd.
 487
 488 DOCEND*)
 489   assume f : Formula.
 490   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 491   assume f1 : Formula.
 492   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H1).
 493   the thesis becomes
 494     ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v).
 495   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 496   we proceed by cases on H2 to prove
 497     ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v).
 498   case Left.
 499     by H3, H we proved
 500       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 501     by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 502     by H3, H1 we proved
 503       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 504     by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
 505     conclude
 506         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
 507       = ([[ if eqb 0 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
 508       = ([[ if true then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v).
 509       = ([[ (FImpl f f1)[ FBot/x ] ]]_v).
 510       = ([[ FImpl (f[ FBot/x ]) (f1[ FBot/x ]) ]]_v).
 511       = (max (1 - [[ f[ FBot/x ] ]]_v) [[ f1[ FBot/x ] ]]_v).
 512       = (max (1 -  [[ f ]]_v) [[ f1[ FBot/x ] ]]_v) by H5.
 513       = (max (1 -  [[ f ]]_v) [[ f1 ]]_v) by H6.
 514       = ([[ FImpl f f1 ]]_v).
 515     done.
 516   case Right.
 517     by H3, H we proved
 518       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 519     by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 520     by H3, H1 we proved
 521       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
 522     by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
 523     conclude
 524         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
 525       = ([[ if eqb 1 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
 526       = ([[ if false then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v).
 527       = ([[ (FImpl f f1)[ FTop/x ] ]]_v).
 528       = ([[ FImpl (f[ FTop/x ]) (f1[ FTop/x ]) ]]_v).
 529       = (max (1 - [[ f[ FTop/x ] ]]_v) [[ f1[ FTop/x ] ]]_v).
 530       = (max (1 - [[ f ]]_v) [[ f1[ FTop/x ] ]]_v) by H5.
 531       = (max (1 - [[ f ]]_v) [[ f1 ]]_v) by H6.
 532       = ([[ FImpl f f1 ]]_v).
 533     done.
 534 case FNot.
 535 (*DOCBEGIN
 536
 537 Il caso
 538 -----------
 539
 540 FISSARE BUG
 541
 542 DOCEND*)
 543   assume f : Formula.
 544   by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H).
 545   the thesis becomes
 546     ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v).
 547   by sem_bool we proved ([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1) (H2).
 548   we proceed by cases on H2 to prove
 549     ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v = [[ FNot f ]]_v).
 550   case Left.
 551     by H1, H we proved
 552       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 553     by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
 554     conclude
 555         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
 556       = ([[ if eqb 0 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
 557       = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
 558       = ([[ (FNot f)[ FBot/x ] ]]_v).
 559       = ([[ FNot (f[ FBot/x ]) ]]_v).
 560       = (1 - [[ f[ FBot/x ] ]]_v).
 561       = (1 - [[ f ]]_v) by H5.
 562       = ([[ FNot f ]]_v).
 563     done.
 564   case Right.
 565     by H1, H we proved
 566       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
 567     by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
 568     conclude
 569         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
 570       = ([[ if eqb 1 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
 571       = ([[ if false then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
 572       = ([[ (FNot f)[ FTop/x ] ]]_v).
 573       = ([[ FNot (f[ FTop/x ]) ]]_v).
 574       = (1 - [[ f[ FTop/x ] ]]_v).
 575       = (1 - [[ f ]]_v) by H5.
 576       = ([[ FNot f ]]_v).
 577     done.
 578 qed.
 579